# 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

```