[Prev][Next][Index][Thread]
Krivine's Machine with Control from a Continuation Semantics
Does anybody know whether the following derivation of Krivine's
Machine with Control from a Continuation Semantics is known to the
community?
The new(?) continuation semantics given subsequently arises from
Girard's improved translation of classical logic to intuitionistic
logic when one restricts one's attention to the implicative fragment
and to formulae of negative polarity. It essentially uses the
isomorphism
~ A -> ~ B = ~ ( ~ A /\ B)
In a syntactic guise these ideas have originally been introduced by
Y. Lafont.
Krivine's Machine with Control
The components of Krivine's machine are given by the following
inductive definition
t : Terms := x | lambda x. t | t t | C t
e : Environments ::= Variables --> Closures
(finite functions)
c : Closures : = < t , e > | ret(k)
k : Continuations ::= stop | < c, k >
Transition Rules
< <x, e >, k > --> < e(c), k > if x is in dom(e)
< < lambda x. t, e >, < c, k > > --> < < t, e[x:=c]>, k >
< < t s, e >, k > --> < < t, e >, < < s, e >, k > >
< < C t, e >, k > --> < < t, e >, < ret(k), stop > >
< ret(k), < c, k' > > --> < c, k >
These transition rules derive immediately from the following
Continuation Semantics for the Call-by-Name Lambda-Calculus with
Control
C = ( C -> R ) -> C D = C -> R Env = Var -> D
[|.|] : Term -> Env -> D
[|x|] e = e(x)
[| lambda x. t |] e <d,k> = [| t |] e[d/x] k
[| t s |] e k = [|t|] e < [|t|] e, k >
[| C t |] e k = [|t|] e < ret(k), stop >
where stop is a distinguished continuation and
ret(k) <d,k'> = d(k).
Thomas Streicher