[Prev][Next][Index][Thread]
rewrite semantics for extended mu-calculus from continuation semantics
In this note I will show how to give a continuation semantics to an extension
of Parigot's mu-calculus from which there follows a simple equational present-
ation and rewrite semantics. Though I have had the semantics since quite a time
the idea to use it for extending mu-calculus and deriving a nice rewrite
semantics for it from this semantics came to me during a talk of Philippe
Audebaud during his talk at the Scott conference in Darmstadt this spring/
summer. I don't precisely remember his presentation, so I cannot compare
what's below with his work; but it looks simpler to me than what I remember
to have seen in the talk.
Maybe Philippe has some further equations to guarantee confluence or things
like that. I personally haven't checked confluence myself. But it is clear that
the machine computations of an extended Krivine's machine are reflected
one-to-one by rewrite derivations in the calculus below.
Anyway the semantic justification of the rewrite rules may be of interest and
facilitate understanding of the calculus.
THE CALCULUS
M ::= x | \x.M | MN | mu alpha. o
C ::= alpha | M::C
o ::= [C]M
Notice that the only extension w.r.t. Parigot's original calulus simply is that
continuation expressions are not only variables but may be stacks of
terms on top of a continuation variable.
SEMANTICS C = D x C D = C -> R
environments e bind variables to elements of D
and continuation variables to elements of C
[|x|] e = e(x)
[|\x.M|]e <d,k> = [|M|] e[x:=d] k
[|MN|] e k = [|M|] e <[|N|]e,k>
[|mu alpha. o|] e k = [|o|] e[alpha:=k]
[|alpha|] e = e(alpha) [|box|] e fix, arbitrary
[|M::C|] e = <[|M|]e,[|C|]e>
[|[C]M|] e = [|M|] e ([|C|]e)
This semantics validates the following equations or rewrite rules :
(\x.M)N -> M[x:=N]
[C] mu alpha. o -> o[alpha:=C]
[C] MN -> [N::C] M
[N::C] (\x.M) -> [C] M[x:=M]
The first rule (traditional beta-rule) may be omitted when one wants to evaluate
simply terms o !!
The remaining three rewrite rules give rise to a Krivine machine for extended
mu-calculus.
Thomas Streicher