key: cord-0049765-scx2ygig
authors: Almeida, Bernardo; Mordido, Andreia; Vasconcelos, Vasco T.
title: Deciding the Bisimilarity of Context-Free Session Types
date: 2020-03-13
journal: Tools and Algorithms for the Construction and Analysis of Systems
DOI: 10.1007/978-3-030-45237-7_3
sha: 87f9c10385a263b7203c7a26519c0a427d325fa0
doc_id: 49765
cord_uid: scx2ygig

We present an algorithm to decide the equivalence of context-free session types, practical to the point of being incorporated in a compiler. We prove its soundness and completeness. We further evaluate its behaviour in practice. In the process, we introduce an algorithm to decide the bisimilarity of simple grammars.

Session types enhance the expressivity of traditional types for programming languages by allowing the description of structured communication on heterogeneously typed channels [14, 15, 24] . Traditional session types are regular in the sense that the sequences of communication actions admitted by a type are in the union of a regular language (for finite executions) and an ω-regular language (for infinite executions). Introduced by Thiemann and Vasconcelos, context-free session types liberate traditional session types from the shackles of tail recursion, allowing, for example, the safe serialization of arbitrary recursive datatypes [26] .

Session types are often used to discipline interactions in concurrent programs. When associated to (bidirectional, heterogeneous) channels, session types describe the permitted patterns of interaction. For example, a type of the form r e c x . +{ L e a f : Skip , Node : ! I n t ; x ; x } may describe one end of a communication channel. A process holding such a channel end must first select between choices Leaf and Node. If Leaf is chosen, then type Skip forwards the interaction to the continuation, if any. If no continuation is present, then interaction is over. Otherwise, the process must send an integer (! Int) followed by two trees, as witnessed by the recursive calls occurring after the choice of Node. A concurrent process holding the other end of the channel interacts via a dual type: r e c y . &{ L e a f : Skip , Node : ? I n t ; y ; y } In this case the process must be ready to offer both choices, Leaf and Node. For the latter option, the process must further receive an integer (?Int), followed by two trees.

Regular languages cannot capture such behaviour. The best one can do with regular session types (and without resorting to channel passing) is to use a regular type that allows transmitting trees, as well as many other non tree-like structures. The correct behaviour of processes interacting on such a channel would need to be checked at runtime [2, 26] .

If the algorithmic aspects of type equivalence for regular session types are well known (Gay and Hole propose an algorithm to decide subtyting [9] , from which type equivalence can be derived), the same does not apply to context-free session types. Thiemann and Vasconcelos [26] show that the equivalence of context-free session types is decidable, by reducing the problem to the verification of bisimulation for Basic Process Algebra (BPA) which, in turn, was proved decidable by Christensen, Hüttel, and Stirling [6] . Even if the equivalence problem for context-free session types is known to be decidable, no algorithm has been proposed. Padovani [20] introduces a language with context-free session types that avoids the problem of checking the equivalence of types by requiring annotations in the source code. Annotations result in the structural alignment between code and types. This alignment-enforced by an explicit resumption process operator that breaks sequential composition in types-sidesteps the problem central to this paper: that of checking type equivalence. Furthermore, there are some basic equivalences on types that the compiler is not able to identify [20] .

After the breakthrough by Christensen, Hüttel, and Stirling-a result that provides no immediate practical algorithm-the problem of deciding the equivalence of BPA terms has been addressed by several researchers [4, 6, 8, 18] . Most of these works provide no practical algorithm that can be readily used, except the one by Czerwinski and Lasota where a polynomial time algorithm is presented that decides the bisimilarity of normed context-free processes in O(n 5 ) [8] . However, context-free session types are not necessarily normed, which precludes resorting to this algorithm, or using the original result by Baeten, Bergstra, and Klop [3] , as well as improvements by Hirshfeld, Jerrum, and Moller [12, 13] . Moreover, the complexity estimates for deciding bisimilarity in BPA process are not promising. Kiefer provided an EXPTIME lower bound for BPA bisimilarity by proving this problem is EXPTIME-hard [19] , whereas Jančar has provided a double exponential upper bound for this problem and proved that its complexity is O(2 2 pol(n) ) [17] .

The decidability of deterministic pushdown automata (DPDA) has also been subject of much study [16, 22, 23] . Several techniques have been proposed to solve the problem, but no immediate practical algorithm was available until Henry and Sénizergues provide an algorithm for this problem [10] . Its poor performance however precludes its incorporation in a compiler. Furthermore, the algorithm Henry and Sénizergues propose handles the problem of language equivalence rather than the problem of deciding bisimilarity of DPDAs.

Our algorithm to decide the equivalence of context-free session types also allows deciding the bisimilarity of simple grammars (i.e., deterministic grammars in Greibach Normal Formal). It proceeds in three stages. The first stage builds a context-free grammar in Greibach Normal Formal (GNF)-in fact a simple grammar-from two context-free session types in a way that bisimulation is preserved. A basic result from Baeten, Bergstra, and Klop states that any guarded BPA system can be transformed into Greibach Normal Formal (GNF) while preserving bisimulation equivalence, but unfortunately no procedure is presented [3] . The second stage prunes the grammar by removing unreachable symbols in unnormed sequences of non-terminal symbols. This stage builds on the result of Christensen, Hüttel, and Stirling [6] . The third stage constructs an expansion tree, by alternating between expansion and simplification steps. This last stage uses expansion operations proposed by Jančar, Moller, and Hirshfeld [11, 18] , and simplification rules proposed by Caucal, Christensen, Hüttel, Stirling, Jančar, and Moller [5, 6, 18] . The finite representation of bisimulations of BPA transition graphs [5, 6] is paramount for our results of soundness and completeness.

The branching nature of the expansion tree confers an (at least) exponential complexity to the algorithm. However, our experiments with a concrete implementation-both as a stand-alone tool and incorporated in a compiler [2] are promising. We propose heuristics that decrease the execution time in 89% and reduce the number of timeouts by 95% (see Section 5) .

We present an algorithm to decide the equivalence of context-free session types, practical to the point of being readily included in any compiler, an exercise that we conducted in parallel [2] . The main contributions of this work are:

-The proposal and implementation of an algorithm to decide type equivalence of context-free session types; -A proof of its soundness and completeness against the declarative definition; -The proposal and implementation of an algorithm to decide the bisimilarity of simple grammars; and -The empirical study of the runtime behaviour of the implementation.

The rest of the paper is organized as follows: an introduction to context-free session types can be found in Section 2, the algorithm in Section 3, the main results in Section 4, evaluation in Section 5, and conclusions in Section 6.

This section briefly introduces context-free session types, based on the work of Thiemann and Vasconcelos [26] . The types we consider build upon a denumerable set of variables and a set of choice labels. Metavariables X, Y, Z range over variables and over labels. We assume given a set of base types denoted by B. The syntax of types is given by the grammar below. In type µX.T , variable X is bound in the subterm T . The sets of bound and free variables in a given type are defined accordingly. Notation [T /X]S denotes the resulting of substituting T for the (free) occurrences of X in S.

Judgement S characterizes terminated types: context-free session types that exhibit no further action [1] . Notice that all types of the form µX.µX 1 . . . µX n .X, for n ≥ 0, are terminated.

We are not interested in all types generated by the above grammar. If ∆ is a list of pairwise distinct variables, then judgement ∆ T characterises the types of interest: the well-formed types. Type formation system:

Terminated processes have a simple characterisation-types comprising skip, µ and semicolon-which justifies the inclusion of ¬T in the rules for type formation (Thiemann and Vasconcelos [26] introduce a contractive judgement for the effect). Type formation serves two main purposes: ensuring that all variables introduced by µ-types are pairwise distinct and that types underneath a µ are not terminated. This can be clearly seen by formation rule for µ-types, where notation ∆, X is understood as requiring X / ∈ ∆. In the sequel we assume that all types are such that T and denote by T the set such types. The set of actions is generated by the following grammar.

a ::= B | The labelled transition system (LTS) for context-free session types is given by T as the set of states, the set of actions, and the transition relation S a −→ T T defined by the rules below.

Type bisimulation is defined in the usual way from the labelled transition system [21] . We say that a type relation R is a bisimulation if, whenever SRT , for all a we have:

We say that two types are bisimilar, written S ∼ T T , if there is a bisimulation R with SRT .

This section presents an algorithm to decide whether two types are in a type bisimulation. In the process we also provide an algorithm to decide the bisimilarity of simple context-free languages. The algorithm comprises three stages:

1. Translate the two types to a simple grammar, 2. Prune unreachable symbols, and 3. Explore an expansion tree, alternating between simplification and expansion operations, until finding an empty node-case in which it decides positivelyor failing to expand all nodes-case in which it decides negatively.

Translating types to grammars. Type variables X are the non-terminal symbols and LTS labels a are the terminal symbols. Sequences of type variables X are called words; ε denotes the empty word. A context-free grammar in Greibach Normal Form is a pair ( X, P) where X is the start word and P a set of productions of the form Y → a Z (context-free session types do not require productions of the form Y → ε). Due to the deterministic nature of context-free session types, the grammars we are interested in are simple: for each non-terminal symbol Y and terminal symbol a, there is at most one production of the form Y → a Z. Grammars in Greibach normal form naturally induce a labelled transition system by taking words X for states, terminal symbols a for actions, and a −→ P , defined as X Y a −→ P Z Y when X → a Z ∈ P, for the transition relation. The associated bisimilarity is denoted by ∼ P .

The unravelling function on well-formed context-free session types, taken from Thiemann and Vasconcelos [26] , is defined as follows. The function terminates under the assumption that types are well formed. Another function, word, builds a word from a type. In the process it updates a global set P of grammar productions. Word concatenation is denoted by X · Y .

The following lemma relates terminated types to the result of a call to word.

T . Then, T if and only if word(T ) = ε.

Proof. The direct implication follows by rule induction on predicate : Conversely, if word(T ) = ε, using the rules of the definition of word that produce the empty word: To define the translation of context-free session types to simple grammars, assume that {µX 1 .T 1 , . . . , µX n .T n } is the set of all µ-subterms in a given type T . Further assume that i < j whenever X j ∈ free(µX i .T i ). That is, the µ-subterms are topologically sorted with respect to their lexical nesting, innermost subterms first. Now we identify unrolled versions of the µ-subterms.

Clearly each type T i is closed (has no free variables). Notice that if T is a µ-type, then µX n .T n is T itself. Finally, given an initial set of productions P 0 , function grm translates a type T into a grammar composed of a start word and set of productions:

where each P i is computed from P i−1 by the following recurrence,

Notice that word(unr(T i )) is a non-empty word because of Lemma 1 and the fact that each T i is non-terminated by hypothesis. The function grm terminates on all inputs (because recursion is always on subterms) and adds a finite number of productions to the original set. Furthermore, because choices in session types do not contain duplicated labels, the function returns a simple grammar.

To run grm on two well-formed types proceed as follows: rename the second type so that bound variables do not overlap with those of the first; start with an empty set of productions; run the algorithm consecutively on the two types to obtain two initial words and a single set of productions. Example 1. Consider the following pair of context-free session types.

S (µX 1 .&{n : X 1 ; X 1 ; ?int, :?int}); (µX 2 .!int; X 2 ; X 2 )

Starting from the empty set of productions, running grm consecutively on S and on T produces the following set of productions

and two start words

Pruning unnormed productions. For a a non-empty sequence of non-terminal symbols a 1 , . . . , a n , write Y

In this case, the norm of Y , denoted by | Y |, is the length of a. As observed by Christensen, Hüttel, and Stirling [6] , any unnormed word Y is bisimilar to its concatenation with any other word, that is, if Y is unnormed, then Y ∼ P Y X. We use this fact to prune unreachable symbols in unnormed words. And we do this in all productions.

Example 2. Recall Example 1 and notice that X 2 and Y 2 are both unnormed. Then, the last occurrence of X 2 in production X 2 → !int X 2 X 2 is unreachable, hence we simplify the production to obtain X 2 → !int X 2 .

Building an expansion tree. We base the third stage of the algorithm on the notion of expansion tree as proposed by Jančar and Moller [18] , adapting an idea by Hirshfeld [11] . The nodes in trees are labelled by sets of pairs of words. We say that a node N is an expansion of N if N is a minimal set such that:

An expansion tree is built from a root node: the singleton set containing the pair of start words obtained by translating the two types into a grammar. A children node is obtained from its parent node by expansion. However, as Jančar and Moller observed, expansions alone often lead to infinite trees. We then alternate between expansion and simplification operations, until either finding an empty node-case in which we decide equivalence positively-or failing to expand all nodes-case in which we decide equivalence negatively. We say that a branch is successful if it is infinite or finishes in an empty node, otherwise it is said to be unsuccessful.

In the expansion step, each node N derives a single child node, obtained as an expansion of N . As we are dealing with simple grammars, no branching is expected in the expansion tree at this step.

The simplification step consists on the application of the following rules:

Reflexive rule: Omit from a node any pair of the form ( X, X); Congruence rule: Omit from a node N any pair that belongs to the least congruence containing the ancestors of N ;

belongs to the ancestors of N , then create a sibling node for N replacing

is in N and X 0 and Y 0 are normed, then:

Case |X 0 | ≤ |Y 0 |: Let a be a minimal path for X 0 and Z the word such that Y 0 a −→ P Z. Add a sibling node for N including the pairs (X 0 Z, Y 0 ) and ( X, Z Y ) in place of (X 0 X, Y 0 Y ); Otherwise: Let a be a minimal path for Y 0 and Z the word such that X 0 a −→ P Z. Add a sibling node for N including the pairs (X 0 , Y 0 Z) and ( Z X, Y ) in place of (X 0 X, Y 0 Y ).

Contrarily to expansion and to the reflexive and congruence simplifications, BPA rules promote branching in the expansion tree. We iteratively apply the simplification rules to ensure the algorithm computes the simplest possible children nodes derived from N . We can easily show that the simplification function that results from applying the reflexive, congruence, and BPA rules, has a fixed point in the complete partial ordered set of pairs node-ancestors, where the set of ancestors is fixed. The proof builds a partial order on the sets of pairs nodeancestors and uses Tarski's fixed point theorem [25] . The number of children nodes generated by the application of these rules is finite [6, 18] . Notice that the sibling nodes do not exclude the (often) infinite branch resulting from successive expansions.

Checking the bisimilarity of simple grammars. Given a set of productions and two start words X and Y (all pruned), function bisimG alternates between simplification and expansion stages, starting with expansion. To avoid getting stuck in an infinite branch of the expansion tree, we use a breadth-first search on the expansion tree: node-ancestor pairs to be processed are stored in a queue. The initial pair inserted in the queue contains the initial node {( X, Y )} and an empty set of ancestors.

bisimG( X, Y , P) = expand(singletonQueue(({( X, Y )}, ∅), P)

Predicate expand terminates as soon as all nodes fail to expand (signalled by an empty queue), case in which the algorithm returns False, or an empty node is reached, case in which the algorithm returns True. Otherwise, it extracts node n at the front of the queue, simplifies its child node, and recurs. (n, P) , a ∪ n)}, dequeue(q), P)) else expand(dequeue(q), P)

The simplification stage distinguishes the case where all type variables are normed, in which case BPA1 is not required to decide equivalence [5, 6] , from the case where some type variables might be unnormed.

Function simplify applies the various rules iteratively, until reaching a fixed point. The application of the rules (via function apply) produces a set of nodes that are then enqueued. The simplification stage does not introduce new levels in the tree, hence the set of ancestors na is passed to function apply as is.

simplify(na, q, P) = fold(enqueue, q, apply(na, rules, P)) Example 3. The expansion tree for our running example is in Figure 1 . Once a successful branch is reached (marked with ), bisimG( X, Y , P) returns True.

Checking the bisimilarity of context-free session types. Function bisimT decides the equivalence of two well-formed and renamed types, S and T . It starts by computing the start words for S and T by first translating S to a grammar and enriching this with the productions for type T . After pruning the productions in the grammar (function prune), the equivalence of S and T is decided using function bisimG.

bisimT(T, U ) = bisimG( X, Y , prune(P))

where ( X, P ) = grm(S, ∅) ( Y , P) = grm(T, P )

In this section we prove that function bisimT is sound and complete with respect to the meta-theory of context-free session types. We start by showing a full abstraction result between context-free session types and grammars in Greibach Normal Form. Then, based on results from Caucal [5] , Christensen, Hüttel, and Stirling [6] , Jančar and Moller [18] , we conclude that the algorithm we propose is sound and complete.

Type translation is fully abstract. Sections 2 and 3 introduce bisimulation relations on the set T of types ∼ T and on a given set P of productions ∼ P . Our ultimate goal is to prove that we can faithfully analyze the bisimilarity of types by analyzing the bisimilarity of the corresponding grammars. For this purpose, we prove that the translation proposed in Section 3 is a fully abstract encoding, i.e., preserves the bisimilarity relation.

We start showing that the transformation of types to grammars preserves the labelled transitions. The following result states that grammars produced by grm mimic the transitions of the corresponding types and vice-versa. Proof. For the direct implication we proceed by rule induction on the hypothesis, using the definition of word. For the reverse implication, we prove that any transition in the grammar leads to a transition in the corresponding types. The main result of this subsection follows from Lemmas 2 and 3. Now we sketch the proof that pruning grammars also preserves bisimulation. We distinguish the grammars in the context through the subscript of ∼.

Proof. For the direct implication, the bisimulation for X and Y over P is also a bisimulation for X and Y over prune(P). For the reverse implication, if B is a bisimulation for X and Y over prune(P), then B = B ∪ {( V W, V W Z) | (W → V W Z) ∈ P, W unnormed} is a bisimulation for X and Y over P.

Correctness of the algorithm. We now focus on the correctness of the function bisimG. Before proceeding to soundness, we recall the safeness property introduced by Jančar and Moller [18] .

Lemma 4 (Safeness Property). Given a set of productions P, X ∼ P Y if and only if the expansion tree rooted at {( X, Y )} has a successful branch.

Notice that function bisimG builds an expansion tree by alternating between simplification-reflexive, congruence, and BPA-and expansion operations, as proposed by Jančar and Moller. These simplification rules are safe [18] , in the sense that the application of any rule preserves the bisimulation from a parent node to at least one child node and, reciprocally, that bisimulation on a child node implies the bisimulation of its parent node.

While the safeness property is instrumental in proving soundness, the finite witness property is of utmost importance to prove completeness. This result follows immediately from the analysis by Jančar and Moller [18] , which capitalizes on results by Caucal [5] , and Christensen, Hüttel, and Stirling [6] :

Lemma 5 (Finite Witness Property). Given a set of productions P, if X ∼ P Y then the expansion tree rooted at {( X, Y )} has a finite successful branch.

We refer to Caucal, Christensen, Hüttel, and Stirling for details on the proof of existence of a finite witness, as stated in Lemma 5. This proof is particularly interesting in that it highlights the importance of the BPA rules and of pruning productions on reaching such (finite) witness. The results in these two papers also elucidate the reason for the distinction, in the simplification phase, between the cases where all the symbols in the grammar are and are not normed (cf. program variable rules in function expand). The safeness and finite witness properties ensure the termination of the algorithm, its soundness and completeness.

Lemma 6 (Termination). Let ( X, P ) = grm(S, ∅) and ( Y , P) = grm(T, P ). Then, the computation of bisimG( X, Y , prune(P)) always terminates.

Proof. Start by noticing that prune(P) always terminates. For bisimG itself, if S ∼ T T then, by Theorems 1 and 2, we have word(S) ∼ prune(P) word(T ) and thus the existence of a finite successful branch is ensured by the finite witness property (Lemma 5). Hence, breadth-first search eventually terminates.

When S ∼ T T , we easily conclude that all branches in the expansion tree are finite and thus bisimG( X, Y ) terminates. To conclude that all branches are finite, observe that any infinite branch is successful by definition and thus the safeness property would imply word(S) ∼ prune(P) word(T ) and we would have S ∼ T T , by Theorems 1 and 2.

Lemma 7. Let ( X, P ) = grm(S, ∅) and ( Y , P) = grm(T, P ). If bisimG( X, Y , prune(P)) returns True, then X ∼ prune(P) Y .

Proof. Function bisimG returns True whenever it reaches a (finite) successful branch in the expansion tree rooted at {( X, Y )}, i.e., a branch terminating in an empty node. Conclude with the safeness property, Lemma 4.

From the previous results, the soundness of our algorithm is now immediate: the algorithm to check the bisimulation of context-free session types is sound with respect to the meta-theory of context-free session types.

Theorem 3 (Soundness). Let ( X, P ) = grm(S, ∅) and ( Y , P) = grm(T, P ). If bisimG( X, Y , prune(P)) returns True then S ∼ T T .

Proof. From Theorem 1, Theorem 2, and Lemma 7.

Given that the algorithm terminates (Lemma 6), we know that if S ∼ T T , then bisimG( X, Y , prune(P)) returns False, where ( X, P ) = grm(S, ∅) and ( Y , P) = grm(T, P ). We now show that the algorithm to check the bisimulation of context-free session types is complete with respect to the meta-theory of context-free session types. The finite witness property is paramount to achieve this result.

Theorem 4 (Completeness). Let ( X, P ) = grm(S, ∅) and ( Y , P) = grm(T, P ). If S ∼ T T then bisimG( X, Y , prune(P)) returns True.

Proof. Assume S ∼ T T . By Theorems 1 and 2, we have X ∼ prune(P) Y . Hence, Lemma 5 ensures the existence of a finite successful branch on the expansion tree rooted at {( X, Y )}, i.e., a branch terminating in an empty node. Since our algorithm traverses the expansion tree using breadth-first search it will, eventually, reach the empty node and conclude the bisimulation positively.

Theorem 4 ensures that if bisimG( X, Y , P) returns False then S ∼ T T .

This section discusses the behaviour of our algorithm in the real world. Both for testing and for performance evaluation, we require test suites. We started with a carefully crafted, manually produced, suite of valid and invalid tests. This test suite was assembled by gathering pairs of types that emerged from examples we have studied and from programs we have written in FreeST, a programming language with context-free session types [2] . The tests produced by this method are, on the one hand, small, and, on the other hand, lacking diversity.

We then turned our attention to the automatic generation of test cases. Producing pairs of arbitrary (well-formed) types that share no variables is simple. However, the probability that a randomly generated pair of types turns out to be bisimilar is extremely low. For this reason, we generate arbitrary pairs of types that are bisimilar by construction. Theorem 5 naturally induces an algorithm: given a natural number n (the size of the pair), arbitrarily select for the base case (n = 0) one of the pairs in item 1 of the theorem and for the recursive case (n ≥ 1) one of the pairs in 2-12 items.

Theorem 5 (Properties of type bisimilarity).

Proof. 1-3: Bisimulation is a congruence. 4-12: Thiemann and Vasconcelos [26] exhibit the appropriate bisimulations.

For evaluating the algorithm on non-bisimilar pairs we add the following five anti-axioms to the list in Theorem 5:

We generate two types using the same methodology as for the positive case and, then, discard the data collected when the pair turns out to be bisimilar. This produces pairs of types that are much closer than those obtained by random generation, thus hopefully approaching the reality that the compilers face when in production.

We used QuickCheck [7] to generate two test suites. That for bisimilar pairs is constructed based on Theorem 5, whereas the construction of non-bisimilar tests relies on Theorem 5 plus the anti-axioms above. Both test suites comprise 2000 entries, featuring types with a number of nodes (in the syntax tree) ranging from 1 to 200.

The base algorithm described in the previous section turns out to behave quite poorly. We then implemented the following variants.

1. Eliminating redundant productions in the grammar. Since the size of the expansion tree depends, among other things, on the number of productions in the grammar, generating smaller grammars seems a promising optimisation. Rather than blindly adding a new production Y → Z to the grammar (in function word, Section 3), we look, in the set of productions, for a production W → X syntactically equal to the former, up to renaming of non-terminal symbols. In this case, we add no new production and return non-terminal W instead. To find W , we look for the least fixed-point of the transitions in the languages generated by Z and X and compare them. This optimisation does not compromise the results of soundness, completeness, nor termination. 2. Using a filter rule that removes nodes with hopeless pairs. A filter rule ensures that nodes composed by pairs of types with different norms (if normed) are removed from the expansion tree, since these types are not bisimilar. The filter rule preserves the results of soundness, completeness, and termination. 3. Using a double-ended queue to prepend promising children. A double-ended queue allows prioritizing nodes with potential to reach an empty node faster. The algorithm prepends (rather than appends) empty nodes or nodes whose pairs ( X, Y ) are such that | X| ≤ 1 and | Y | ≤ 1. This procedure does not compromise soundness, completeness, nor termination because the number of terminal symbols is finite and the algorithm takes advantage of the reflexive and congruence rules to remove previously visited nodes from the queue.

To better understand how the algorithm performs in practice, we tested all the optimisations and their combinations. We evaluate each variant 1-3 individually (denoted by B1-B3) and all their combinations. For instance, B12 denotes the variant obtained from combining optimisations 1 and 2 above. B stands for the base algorithm, bisimT. We implemented the base algorithm and its variants in Haskell, using the Glasgow Haskell Compiler (version 8.6.5). The evaluation was conducted on a machine with an Intel Core i7-6700K at 4.2GHz and 8 GB of RAM running Arch Linux; tests were run under a timeout of 2 minutes. Figure 2a depicts the distribution of the execution times (in ms) for both test suites and all variants. We observe that the behavior of negatives tests is roughly the same in all variants. However, the execution time for the positive tests differ from variant to variant. These differences mainly depend on the trade-off between the computational effort required for each optimisation and the efficiency they bring to deciding the equivalence of grammars. We observe that including optimisation 1 improves the execution time, while the rest, in general, does not. The combination of optimizations has a positive impact on execution time, with the exception of the B23 variant, whose distribution is worse than the base case. Figure 2b shows the number of timeouts for each variant. The base case, B, has 146 positive tests whose execution time exceeds 2 minutes. The distribution of timeouts per variant exhibits a behavior that is consistent with that of runtime shown in Figure 2a . All combinations lead to a reduction in the number of timeouts, when compared to the base case.

Variant B1, resulting from considering optimisation 1, performs better than all others, presenting a median of 1.4 milliseconds and 7 timeouts, both for the positive tests. By taking advantage of optimisation 1, the number of timeouts reduced by 95%. The remaining positive tests take, on average, 1863.38 ms to complete with the base algorithm and 195.68 ms with variant B1, resulting in an 89% reduction in the execution time. This is the variant in production for the FreeST compiler [2] .

The distribution of the execution time of B1 against the size of the input types is depicted in Figure 2c . As expected, the execution time increases considerably with the number of nodes. Although we have carried out tests with a fairly large number of nodes in the abstract syntax trees, we remark that, when used in a compiler, the algorithm will mostly come across types with a reduced number of nodes.

Context-free session types are a promising tool to describe protocols in concurrent programs. In order to be incorporated in programming languages and effectively used in compilers, a practical algorithm to decide bisimulation is called for. Taking advantage of a process algebra graph representation of types to decide bisimulation [12, 13] , we developed one such algorithm and proved it correct. The algorithm is incorporated in a compiler for a concurrent functional language equipped with context-free session types [2] .

Possible extensions to this work include addressing higher-order session types. We also plan to extend the implementation of the algorithm to cope with contextfree grammars in Greibach Normal Form that are not necessarily deterministic.

Termination, deadlock, and divergence

Freest: Context-free session types in a functional language

Decidability of bisimulation equivalence for process generating context-free languages

An elementary bisimulation decision procedure for arbitrary context-free processes

Décidabilité de l'égalité des langages algébriques infinitaires simples

Bisimulation equivalence is decidable for all context-free processes

Quickcheck: a lightweight tool for random testing of haskell programs

Fast equivalence-checking for normed context-free processes

Subtyping for session types in the pi calculus

Lalblc a program testing the equivalence of dpda's

Bisimulation trees and the decidability of weak bisimulations

A polynomial algorithm for deciding bisimilarity of normed context-free processes

A fast algorithm for deciding bisimilarity of normed context-free processes

Types for dyadic interaction

Language primitives and type discipline for structured communication-based programming

Selected ideas used for decidability and undecidability of bisimilarity

Bisimilarity on basic process algebra is in 2-exptime (an explicit proof)

Techniques for decidability and undecidability of bisimilarity

Bpa bisimilarity is exptime-hard

Context-free session type inference

An Introduction to Bisimulation and Coinduction

The equivalence problem for deterministic pushdown automata is decidable

Decidability of DPDA equivalence

An interaction-based language and its typing system

A lattice-theoretical fixpoint theorem and its applications

Context-free session types

), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use

Acknowledgements. We thank Alcides Fonseca for helping with the testing process, and Filipe Casal, Alexandra Silva, and Peter Thiemman for comments and discussions. This work was supported by FCT through the LASIGE Research Unit, ref. UIDB/00408/2020 and by Cost Action CA15123 EUTypes.