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
.
A few equations (and rules) govern what we mean for two trees to be equivalent.
We have:
end = end
and
!s1.s2 = !t1.t2
if both s1=t1
and s2=t2
, and
dualof s = dualof t
if s=t
.
That is,
dualof !s. t = ?s.dualof t
Notice that we dualise the continuation t
but not the message
contents s
.
That is,
dualof ?s.t = !s. dualof t
end
is end
That is,
dualof end = end
dualof
is an involutionThe dualof
operator is its own inverse, that is
dualof dualof !s.t = !s.t
end
That is, dualof s = s
implies s = end
. Try,
dualof s = s
dualof
is a complementA solution to equation
dualof s = t
is t=dualof s
and s=s
.
Equations are written one after another. Try:
x = !end.y
y = ?z.end
!end.z = !end.end
Unification of finite trees may end up in infinite trees. Try:
x = !end.y
y = ?x.end
Can you figure out what is a solution to the following system of equations?
x = !x.end
y = dualof x
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
Reading the solution we see that x1
is the type !end.end
and
y1
is the type ?end.end
, as expected.