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