[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