Krivine's Machine

Krivine's machine is an abstract machine for the evaluation of the nameless λ-calculus. The Λ-terms are evaluated with a normal order reduction strategy until weak head normal form, i.e. the machine is weakly normalising. Probably the simplest possible lambda calculus machine, its definition using a terminal transition system has only four transition rules.

Krivine's Machine Configuration

The state of the machine consists of three components:

• an environment stack E,
• a term register T, and
• a temporary stack S.

The term register holds the Λ-term that is being evaluated. The temporary stack has term and environment pairs pushed onto, and popped from, it. These pairs are called suspensions. The environment stack contains all of the arguments of the applications which are currently being evaluated. It works in a similar fashion to the nested environments used in programming languages. Each argument is stored as part of a suspension. This is a delayed substitution as the argument is evaluated, using the environment stored with it in the substitution, only when, and if, the arugment is needed.

Krivine's Machine Transition Rules

The transition relation between configurations is ⇒. It is defined by the rules below. In these rules the concatenation operator (|) is used to build stacks. If S is a stack, then [s|S] is the same stack but with s pushed onto it. The empty stack is []. An application of e1 and e2 is written as @(e1,e2). The initial state for term T is ⟨[],T,[]⟩. A final state has the same form.

Rules for expressions

Implementation

The following is an implementation of Krivine's machine written in Barry's Prolog. It should run on any ISO compliant Prolog system.

%%%
%%% Set up the operators.
%%%
:- op(0, xfx, (=>)).
:- op(200, xfx, (=>)).
:- op(0, fx, ('Λ')).
:- op(160, fx, ('Λ')).
:- op(0, fx, (#)).
:- op(150, fx, (#)).


%%%
%%% The transition rules.
%%%
([{Env, Exp}|_], #0, Stack) => (Env, Exp, Stack).
([_|Rest], #N, Stack) => (Rest, #M, Stack) :- M is N-1.
(Env, @(Operator, Operand), Stack) => (Env, Operator, [{Env, Operand}|Stack]).
(Env, 'Λ' Exp, [Top|Tail]) => ([Top|Env], Exp, Tail).

%%%
%%% initial_state(+C, ?S)
%%%
%%% Succeeds if S is the state that corresponds to the configuration
%%% which will execute C with an empty environment.
%%%
initial_state(Code, ([], Code, [])).

%%%
%%% final_state(+S, ?R)
%%%
%%% Succeeds if the state S is a final state with result R.
%%%
final_state(([], T, []), T).


%%%
%%% krivine(+S, ?R)
%%%
%%% Succeeds if Krivine's machine transitions from S to a final
%%% state with result R. This is the transitive closure of the
%%% transition relation.
%%%
krivine(State0, Result) :-
	State0 => State1,
	!,
	krivine(State1, Result).
krivine(State, Result) :-
	final_state(State, Result).
	

Finally a small test.

%%%
%%% test.
%%%
%%% Should give Λ#0 as the result.
%%%
test :-
	initial_state(@('Λ' @(#0, #0),'Λ' #0), Start),
	krivine(Start, Finish),
	print(Finish), nl.
	

References

W. Kluge. Abstract Computing Machines. A Lambda Calculus Perspective. Springer, 2005.