Checking the Bisimilarity of Simple Grammars

Decides the bisimilarity of two words, according to the labelled transition system defined by the grammar's productions.

Usage

A grammar is composed of a pair of start words and a set of productions. For example:

(S,T)
S -> a S
S -> b S
S -> $
T -> a U
T -> b T
T -> $
U -> a T
U -> b U
U -> $
Load in editor

The Syntax of Simple Grammars

Terminal symbols are identifiers starting with a lower case letter or one of the symbols ~, `, @, #, $, %, ^, &, *, _, +, =, {, }, [, ], :, ;, ", ', ?, /, >, ., <. Nonterminal symbols are identifiers starting with an upper case letter. A word is a blank-separated sequence of zero or more nonterminal symbols. Notice that XY is a word of one only symbol and not the sequence of symbols X and Y. If a sequence of X and Y is sought, use X Y. A production is nonterminal symbol, followed by an arrow ->, followed by a terminal symbol, followed by a word. Productions with an empty right-hand-side are not allowed. The shortest right-hand-side of a production is a terminal symbol. A simple grammar is composed of a pair of words (between parenthesis and separated by a comma) and a list of deterministic productions. We are interested in deterministic grammars : for each non-terminal symbol X and each terminal symbol a, there is at most one production of the form X -> a Y1 ... Yn. We work with start words rather than start symbols, for productions require a non-empty right-hand-side.

The following is an example of a simple grammar and a pair of start words S and T.

(S, T)
S -> a S
T -> b T
Load in editor

The two start words are not bisimilar yet they generate the same language (the empty language). To see that S and T are not bisimilar notice that S has a transition by a which T cannot match.

Grammars Obtained From Context-free Session Types

Consider the two context-free session types below.

forall a => +{Leaf : Skip, Node : !Int;TreeChannel;TreeChannel};a
forall a => +{Leaf : a, Node : !Int;TreeChannel;TreeChannel;a}
where
TreeChannel = +{Leaf : Skip, Node : !Int;TreeChannel;TreeChannel}

A simple grammar that characterises the pair is as follows. The types turn out to be bisimilar.

(S T, U)
S -> +Leaf
S -> +Node V X X
T -> a
V -> !Int
U -> +Leaf T
U -> +Node V X X T
X -> +Leaf
X -> +Node V X X
Load in editor

A more elaborate example with higher-order channels is as follows.

InputTree = +{Node: InputTree; !(?int); InputTree, Leaf: skip}

T = +{Node: U,   Leaf: skip}
U = +{Node: T; !(?int); U,   Leaf: !(?int); T}

This gives rise to the following simple grammar (once again, the two types are bisimilar). In below Bot stands for a nonterminal symbol without productions.

(S, T)
S -> +Node S V S
S -> +Leaf
T -> +Node U
T -> +Leaf
U -> +Node U V T
U -> +Leaf V T
V -> !d W Bot
V -> !c
W -> ?d X Bot
W -> ?c
X -> int
Load in editor

For details on context-free session types, see P. Thiemann, V. T. Vasconcelos. Context-free session types. ACM SIGPLAN Notices. Vol. 51. No. 9. ACM, 2016

Run
$