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

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 -> $
```

**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
```

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.

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
```

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
```

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