abstract machines:

Compilation

C ~ compile

    rule name
C (ef ea) C ea; push; C ef; apply ct_apply
C (λ e) closure (C e; return) c_abs
C v var_c v c_var
C (cons t e0 e1) C e1; push; C e0; push; cons_result t ct_cons
C (match ec e0 e1) C ec; match_call (C e0; pop_env_match) (C e1; pop_env_match) c_match
C (ef va) C ef; apply_var va cv_apply
C (eager_let e0 e1) C e0; eager_let_c; C e1; pop_env_let cv_let
C (cons t v0 v1) cons_result_var t v0 v1 cv_cons
Krivine with eager evaluation
C (ef va) push_var va; C ef  
C (λ e) pop; C e  
C v enter v  
C (eager_let e0 e1) delay (eager_let_c; C e1); C e0 s_eager_let
C (cons t) cons_return t  
C (match ec e0 e1) delay (match (C e0) (C e1)); C ec  
C (lazy_let e0 e1) lazy_let_c (C e0); C e1  

Krivine: “Krivine with eager evaluation” without s_eager_let

categorical, terms in argument:

categorical:

categorical without closures: categorical

Running

re e v = an element of the environment e at the index v

$t = substitute the value of t into the name

old state new state
condition rule name
code environment stack result code environment stack result    
push; c e s Some x c e V x :: s None    
apply; c e V a :: s Some (Cl c' e') c' a :: e' R c e :: s None    
closure c'; c e s None c e s Some (Cl c' e)   e_closure
return _ R c e :: s Some x c e s Some x    
var_c v; c e s None c e s Some (re e v)    
cons_result t; c e V a0 :: V a1 :: s None c e s Some (Cons t a0 a1)    
cons_result_var t v0 v1; c e s None c e s Some (Cons t
(re e v0) (re e v1))
   
match_call c0 c1; c e s Some (Cons t a0 a1) c$t; c a0 :: a1 :: e s None    
pop_env_match; c _ :: _ :: e s Some x c e s Some x    
pop_env_let; c _ :: e s Some x c e s Some x    
apply_var v; c e s Some (Cl c' e') c' re e v :: e' R c e :: s None   e_apply_var
eager_let_c; c e s Some x c x :: e s None    
closure c'; c e s None c e s Some (Cl c')   a_closure
apply_var v; c e s Some (Cl c') c' re e v :: nil R c e :: s None   a_apply_var
Krivine with eager evaluation
push_var v; c e s None c e V (re e v) :: s None    
pop; c e V a :: s None c a :: e s None   pop_value
c e R c' e' :: s None c' e' s Some (Cl c e) c=(pop; _) pop_return
enter v e s None c' e' s None re e v = Cl c' e' enter_closure
enter v e R c' e' :: s None c' e' s Some x re e v = x
∧ x = Cons t _ _
enter_cons
delay c'; c e s None c e R c' e :: s None    
cons_return t _ V a0 :: V a1
:: R c' e' :: s
None c' e' s Some (Cons t a0 a1)    
match c0 c1 e s Some (Cons t a0 a1) c$t a0 :: a1 :: e s None    
lazy_let_c c'; c e s None c Cl c' e :: e s None    

categorical, terms in argument:

categorical:

categorical without closures:

Krivine with eager evaluation:

Krivine: (never has Cons in its environment or stack)