Unification of session trees

The trees

Regular infinite trees are input in the rec notation. Terms are converted to trees and unified. The unifier, if any, is rendered again in rec notation.

Terms are of the form end, dualof s, !t.s, ?t.s, x, rec x.s, and (s), if s and t are terms and x is a variable. Variables are given by the regular expression [a-zA-Z] [a-zA-Z0-9_]*. Comments are those of Java.

Terms are required to be contractive so that they may be converted into meaningful trees. A term s is contractive in variable x if s is

  • end or !s1.t2 or ?s1.s2 of y, for y different from x;

  • dualof s1 or rec y.s1 and s1 is contractive in x.

A term is well formed if each of its subterms of the form rec x.s, term s is contractive in x.

Equational reasoning

A few equations (and rules) govern what we mean for two trees to be equivalent.

Decomposition

We have:

end = end
Load in editor

and

!s1.s2 = !t1.t2
Load in editor

if both s1=t1 and s2=t2, and

dualof s = dualof t
Load in editor

if s=t.

The dual of output is input

That is,

dualof !s. t = ?s.dualof t
Load in editor

Notice that we dualise the continuation t but not the message contents s.

The dual of input is output

That is,

dualof ?s.t = !s. dualof t
Load in editor

The dual of end is end

That is,

dualof end = end
Load in editor

dualof is an involution

The dualof operator is its own inverse, that is

dualof dualof !s.t = !s.t
Load in editor

The only tree that is dual to itself is end

That is, dualof s = s implies s = end. Try,

dualof s = s
Load in editor

dualof is a complement

A solution to equation

dualof s = t
Load in editor

is t=dualof s and s=s.

Unification

Equations are written one after another. Try:

x = !end.y
y = ?z.end
!end.z = !end.end
Load in editor

Unification of finite trees may end up in infinite trees. Try:

x = !end.y
y = ?x.end
Load in editor

Can you figure out what is a solution to the following system of equations?

x = !x.end
y = dualof x
Load in editor

Consider the following program, composed of the parallel composition of two threads. The first sends end on communication channel c. The second receives a value from channel c that gets assigned to variable z.

send end on c | receive z from c

If c is of type x1 on the left thread and c is of type y1 on the right thread, then the two types for c can be obtained by solving the following system of equations.

x1 = !x2.x3
x2 = end
x3 = end
y1 = ?y2.y3
y3 = end
x1 = dualof y1
Load in editor

Reading the solution we see that x1 is the type !end.end and y1 is the type ?end.end, as expected.

Run
$