Werner Kluge's SEMCD machine is an abstract machine for the evaluation of the nameless λcalculus. The Λterms can be evaluated with either a normal order or a applicative order reduction strategy until weak head normal form, i.e. the machine is weakly normalising.
A machine configuration consists of four components:
S
,E
,M
,C
,D
.
The C
stack holds the Λterm that is being evaluated.
Applications are deconstructed on this stack and depending on the reduction strategy either the arguments are
pushed back onto the C
stack for evaluation (applicative order)
or moved directly to the E
stack (normal order).
The environment stack, E
, works in a similar fashion to the nested environments used in programming languages.
Each argument is stored on E
, either as part of a suspension which is an environment and term pair (in the normal order case),
or as a single value (in the applicative order case).
This mechanism implements a delayed substitution  when the argument variable is found in C
, the environment is searched for the correct
value or suspension.
When executing the term in the C
stack, the machine needs to keep track of its progress.
Application constructor symbols are pushed onto the M
stack to acheive this.
These constructors give the machine enough information to determine how to process the argument and operator in the C
stack.
Finally, the dump, D
, is used to store a continuation which tells the machine what to do when it has
completed execution of the C
stack.
The SEMCD machine is an example of a transition system.
The transition relation between configurations is →
.
It is defined by the rules given below.
The following conventions are used:
db(i)
where i≥0
is a de Bruijn number.
This is used to reference arguments in the E
stack.
var(v)
, where v
can be any symbol, is an unbound variable.

) is used to build stacks.
If S
is a stack, then [sS]
is the same stack but with s
pushed onto it,
and [t,sS]
is the same stack but with s
and t
pushed onto it.
The empty stack is []
.
e_{1}
and e_{2}
is written as
@(e_{1},e_{2})
for normal order applications,
and @'(e_{1},e_{2})
for applicative order applications.
@(i)
where i≥0
is a normal order numbered applicator.
The term @'(i)
where i≥0
is an applicative order numbered applicator.
The term ap(i)
where i≥0
is used when either a normal order numbered applicator or
an applicative order numbered applicator can be used.
irreducible_@(i)
where i≥0
is a normal order numbered irreducible application.
The term irreducible_@'(i)
where i≥0
is an applicative order irreducible application.
The term irreducible_ap(i)
where i≥0
is used when either a normal order irreducible application or
an applicative order numbered irreducible application can be used.
susp(E,v)
represents a suspension with environment E
and value v
that is to be
evaluated in the environment.
Λ(e)
represents an abstraction with body e
.
T
is ⟨[],[],[], T, []⟩
.
The rules are given in the order in which they are to be tried. As soon as one rule is found to be applicable it is used and all other rules discarded. This gives rules a certain priority which is needed as the transition system without them is not monogenic.
1a 
⟨S, E, [], [db(i)C], D⟩ → ⟨[eS], E, [], C, D⟩ where e=lookup(i,E)

1b 
⟨S, E, [ap(i)M], [db(j)C], D⟩ → ⟨[eS], E, [ap(i1)M], C, D⟩ where i>0 , e=lookup(j,E)

1c 
⟨S, E, [], [var(v)C], D⟩ → ⟨[var(v)S], E, [], C, D⟩

1d 
⟨S, E, [ap(i)M], [var(v)C], D⟩ → ⟨[var(v)S], E, [ap(i1)M], C, D⟩ where i>0

3 
⟨S, E, [@(2)M], [cC], D⟩ → ⟨[susp(E,c)S], E, [@(1)M], C, D⟩

2a 
⟨S, E, M, [@'(e1,e2)C], D⟩ → ⟨S, E, [@'(2)M], [e2,e1C], D⟩

2b 
⟨S, E, M, [@(e1,e2)C], D⟩ → ⟨S, E, [@(2)M], [e2,e1C], D⟩

4a 
⟨S, E, [], [Λ(e)C], D⟩ → ⟨[susp(E,Λ(e))S], E, [], C, D⟩

4b 
⟨S, E, [ap(i)M], [Λ(e)C], D⟩ → ⟨[susp(E,Λ(e))S], E, [ap(i1)M], C, D⟩ where i>0

5a 
⟨[susp(E',Λ(e1)),e2S], E, [ap(0)], C, D⟩ → ⟨S, [e2E'], [], [e1], (E, [], C, D)⟩

5b 
⟨[susp(E',Λ(e1)),e2S], E, [ap(0),ap(i)M], C, D⟩ → ⟨S, [e2E'], [], [e1], (E, [ap(i1)M], C, D)⟩ where i>0

6 
⟨[susp(E', e)S], E, M, C, D⟩ → ⟨S, E', [], [e], (E, M, C, D)⟩ where e=irredicible_ap(e1,e2)

7a 
⟨[e1,e2S], E, [@'(0)], C, D⟩ → ⟨[irreducible_@'(e2,e1)S], E, [], C, D⟩

7b 
⟨[e1,e2S], E, [@'(0),ap(i)M], C, D⟩ → ⟨[irreducible_@'(e2,e1)S], E, [ap(i1)M], C, D⟩

8a 
⟨[e1,e2S], E, [@(0)], C, D⟩ → ⟨[irreducible_@(e1,e2)S], E, [], C, D⟩

8b 
⟨[e1,e2S], E, [@'(0),ap(i)M], C, D⟩ → ⟨[irreducible_@(e1,e2)S], E, [ap(i1)M], C, D⟩

9 
⟨S, E, [], [], (E', M', C', D')⟩ → ⟨S, E', M', C', D'⟩

A closer look at the rules follows:
1a 
⟨S, E, [], [db(i)C], D⟩ → ⟨[eS], E, [], C, D⟩ where e=lookup(i,E)

If we have a de Bruijn number on C
and M
is empty,
then look up the variable in E
and push the found value onto S
.
1b 
⟨S, E, [ap(i)M], [db(j)C], D⟩ → ⟨[eS], E, [ap(i1)M], C, D⟩ where i>0 , e=lookup(j,E)

If we have a de Bruijn number on C
and M
is not empty (it contains a numbered applicator),
then look up the variable in E
and push the found value onto S
then decrement the applicator.
1c 
⟨S, E, [], [var(v)C], D⟩ → ⟨[var(v)S], E, [], C, D⟩

If we have an unbound variable on C
and M
is empty,
then push the variable onto S
.
1d 
⟨S, E, [ap(i)M], [var(v)C], D⟩ → ⟨[var(v)S], E, [ap(i1)M], C, D⟩ where i>0

If we have an unbound variable on C
and a numbered applicator on M
,
then push the variable onto S
and decrement the applicator.
3 
⟨S, E, [@(2)M], [cC], D⟩ → ⟨[susp(E,c)S], E, [@(1)M], C, D⟩

Build the argument suspension, push it onto S
then decrement the index of the normal order applicator on M
, i.e., set it to 1
.
Why has this been placed above 2a and 2b? Try this to see why:
(normalapply (lambda x z) ((lambda w (w w)) (lambda w (w w))))
2a 
⟨S, E, M, [@'(e1,e2)C], D⟩ → ⟨S, E, [@'(2)M], [e2,e1C], D⟩

If we have an applicative applicator on top of C
,
then pop it off C
and push a numbered applicative order applicator onto M
with index 2
.
2b 
⟨S, E, M, [@(e1,e2)C], D⟩ → ⟨S, E, [@(2)M], [e2,e1C], D⟩

If we have a normal applicator on top of C
,
then pop it off C
and push a numbered normal order applicator onto M
with index 2
.
4a 
⟨S, E, [], [Λ(e)C], D⟩ → ⟨[susp(E,Λ(e))S], E, [], C, D⟩

If M
is empty and we have an abstraction on top of C
,
then create a suspension and push it onto S
.
4b 
⟨S, E, [ap(i)M], [Λ(e)C], D⟩ → ⟨[susp(E,Λ(e))S], E, [ap(i1)M], C, D⟩ where i>0

If the top of M
is an applicator and the top of C
is an abstraction,
then create a suspension, push this suspension onto S
, and decrement the applicator index.
5a 
⟨[susp(E',Λ(e1)),e2S], E, [ap(0)], C, D⟩ → ⟨S, [e2E'], [], [e1], (E, [], C, D)⟩

If there is a suspension then an argument on top of S
and a single applicator with index 0
on M
,
then do the reduction, push the continuation onto D
,
pop M
,
set E
and C
to the contents of the suspension and
add the argument to E
.
5b 
⟨[susp(E',Λ(e1)),e2S], E, [ap(0),ap(i)M], C, D⟩ → ⟨S, [e2E'], [], [e1], (E, [ap(i1)M], C, D)⟩ where i>0

If there is a suspension then an argument on top of S
, and two applicators on M
(the top one having index 0
),
then do the reduction, push the continuation onto D
,
pop M
and decrement the applicator which is now on top on M
,
set E
and C
to the contents of the suspension and
add the argument to E
.
6 
⟨[susp(E', e)S], E, M, C, D⟩ → ⟨S, E', [], [e], (E, M, C, D)⟩ where e=irredicible_ap(e1,e2)

Take the suspension on top of S
and evaluate it.
7a 
⟨[e1,e2S], E, [@'(0)], C, D⟩ → ⟨[irreducible_@'(e2,e1)S], E, [], C, D⟩

If the top of M
is a single applicative applicator of index 0
,
then the top of the S
cannot be reduced so it must be an irreducible application.
Build such a irreducible application and remove the top applicator on M
.
7b 
⟨[e1,e2S], E, [@'(0),ap(i)M], C, D⟩ → ⟨[irreducible_@'(e2,e1)S], E, [ap(i1)M], C, D⟩

If the top of M
is a single applicative applicator of index 0
with an applicator under it,
then the top of the S
cannot be reduced so it must be an irreducible application.
Build such a irreducible application and remove the top applicator on M
and decrement the new top applicator.
8a 
⟨[e1,e2S], E, [@(0)], C, D⟩ → ⟨[irreducible_@(e1,e2)S], E, [], C, D⟩

If the top of M
is a single normal applicator of index 0
,
then the top of the S
cannot be reduced so it must be an irreducible application.
Build such a irreducible application and remove the top applicator on M
.
8b 
⟨[e1,e2S], E, [@(0),ap(i)M], C, D⟩ → ⟨[irreducible_@(e1,e2)S], E, [ap(i1)M], C, D⟩

If the top of M
is a single anormal applicator of index 0
with an applicator under it,
then the top of the S
cannot be reduced so it must be an irreducible application.
Build such a irreducible application and remove the top applicator on M
and decrement the new top applicator.
9. 
⟨S, E, [], [], (E', M', C', D')⟩ → ⟨S, E', M', C', D'⟩

The code stack, C
, is empty so we retrieve the continuation from D
and continue from there.
The following is an implementation of the SEMCD machine and a compiler which generates machine instructions. The code is written in my own dialect of Lisp but it should be easy to port this to Lisp or Scheme.
There is only one global switch which is used to turn debug trace messages on or off.
;;;
;;; This is a switch which will turn on debug printouts showing the state of the machine.
;;;
(set! *semcddebug* nil)
These are simple but useful functions not specific to the SEMCD machine.
;;;
;;; Return the parameters as a list.
;;;
(set! list
(lambda lst lst))
;;;
;;; Predicate to test for the empty list.
;;;
(set! null
(lambda (lst)
(eq nil lst)))
;;;
;;; The empty list will also be considered to be the
;;; value "false". So, we can have (not B) = (null B).
;;;
(set! not null)
The runtime environment is a list of values.
This list is searched with SEMCDlookup
and it is
extended with SEMCDextendenv
.
(set! SEMCDlookup
(lambda (i env)
(if (= 0 i)
(car env)
(SEMCDlookup ( i 1) (cdr env)))))
(set! SEMCDextendenv cons)
The rest of the code will use the following functions to manipulate the machine stacks.
;;; Predicate to test for an empty stack.
(set! SEMCDemptystackp null)
;;; Push an element onto a stack.
(set! SEMCDstackpush cons)
;;; Remove the element at the top of the stack
(set! SEMCDstackremovetop cdr)
;;; Retrieve the element at the top of the stack.
(set! SEMCDstacktop car)
The code is just a list of instructions: (Instr1 Instr2 Instr3 .... InstrN)
Each instruction is an expression tree which is described by the following constructor grammar where
v
is a variable, and i
is an integer.
t ::= (SEMCDvariable v)  (SEMCDdebruijn i)  (SEMCDlambda t)  (SEMCDnormalapplicator t t)  (SEMCDapplicativeapplicator t t)  (SEMCDsuspension t)  (SEMCDirreducibleapplication t t)
The numbered applicators are used internally and they control the preorder transversal of the terms of the form
(SEMCDnormalapplicator t t)
and
(SEMCDapplicativeapplicator t t)
.
These are only found on the M
stack.
;;; Retrieve the next instruction from the code stream.
(set! SEMCDnextinstruction car)
;;; Remove the next instruction from the code stream.
;;; You could see this as "incrementing" an instruction
;;; pointer.
(set! SEMCDremoveinstruction cdr)
A machine configuration, or state, looks like this: (S E M C D)
S
 value stackE
 environmentM
 memory used for a preorder translatorC
 code streamD
 dump where continuations are pushedGetter and setter functions are provided to construct and deconstruct a machine state.
;;;
;;; We need this constant to build an initial state.
;;;
(set! SEMCDemptystate (list nil nil nil nil nil))
;;;
;;; Getter and setter for S (stack) which is the
;;; first element of the machine state.
;;;
(set! SEMCDgetS car)
(set! SEMCDsetS
(lambda (state newS)
(rplaca state newS)
state))
;;;
;;; Getter and setter for E (environment) which is the
;;; second element of the machine state.
;;;
(set! SEMCDgetE
(lambda (state)
(car (cdr state))))
(set! SEMCDsetE
(lambda (state newE)
(rplaca (cdr state) newE)
state))
;;;
;;; Getter and setter for M (applicator store) which is the
;;; third element of the machine state.
;;;
(set! SEMCDgetM
(lambda (state)
(car (cdr (cdr state)))))
(set! SEMCDsetM
(lambda (state newM)
(rplaca (cdr (cdr state)) newM)
state))
;;;
;;; Getter and setter for C (code) which is the
;;; fourth element of the machine state.
;;;
(set! SEMCDgetC
(lambda (state)
(car (cdr (cdr (cdr state))))))
(set! SEMCDsetC
(lambda (state newC)
(rplaca (cdr (cdr (cdr state))) newC)
state))
;;;
;;; Getter and setter for D (dump) which is the
;;; fifth element of the machine state.
;;;
(set! SEMCDgetD
(lambda (state)
(car (cdr (cdr (cdr (cdr state)))))))
(set! SEMCDsetD
(lambda (state newD)
(rplaca (cdr (cdr (cdr (cdr state)))) newD)
state))
The various data types and their constructors, recognisers, and destructors are given here:
;;;
;;; The variable data type.
;;; SEMCDmakevariable : the constructor
;;; SEMCDvariablep : recogniser predicate
;;; SEMCDgetvariable : the deconstructor
;;;
(set! SEMCDmakevariable
(lambda (v)
(cons 'SEMCDvariable v)))
(set! SEMCDvariablep
(lambda (v)
(and (consp v)
(eq (car v)
'SEMCDvariable))))
(set! SEMCDgetvariable cdr)
;;;
;;; The deBruijn number data type.
;;; SEMCDmakedebruijn : the constructor
;;; SEMCDdebruijnp : recogniser predicate
;;; SEMCDgetdebruijn : the deconstructor
;;;
;;; A de Bruijn number is a bound variable reference.
;;; The number is the address of the variable which is
;;; an index into the run time environment.
;;;
(set! SEMCDmakedebruijn
(lambda (v)
(cons 'SEMCDdebruijn v)))
(set! SEMCDdebruijnp
(lambda (v)
(and (consp v)
(eq (car v)
'SEMCDdebruijn))))
(set! SEMCDgetdebruijn cdr)
;;;
;;; Some constants that can be compared with
;;; eq
;;;
(set! SEMCDapplicativeapplicator
(cons "applicative" "applicator"))
(set! SEMCDnormalapplicator
(cons "normal" "applicator"))
;;;
;;; The normalapplicator data type.
;;; SEMCDmakenormalapplicator : the constructor
;;; SEMCDnormalapplicatorp : recogniser predicate
;;; SEMCDgetnormalapplicatoroperand : a deconstructor
;;; SEMCDgetnormalapplicatoroperator : a deconstructor
;;;
(set! SEMCDmakenormalapplicator
(lambda (operator operand)
(list SEMCDnormalapplicator
operator
operand)))
(set! SEMCDnormalapplicatorp
(lambda (v)
(and (consp v)
(eq (car v)
SEMCDnormalapplicator))))
(set! SEMCDgetnormalapplicatoroperator
(lambda (v)
(car (cdr v))))
(set! SEMCDgetnormalapplicatoroperand
(lambda (v)
(car (cdr (cdr v)))))
;;;
;;; The applicativeapplicator data type.
;;; SEMCDmakeapplicativeapplicator : the constructor
;;; SEMCDapplicativeapplicator : recogniser predicate
;;; SEMCDgetapplicativeapplicatoroperator : a deconstructor
;;; SEMCDgetapplicativeapplicatoroperand : a deconstructor
;;;
(set! SEMCDmakeapplicativeapplicator
(lambda (operator operand)
(list SEMCDapplicativeapplicator
operator
operand)))
(set! SEMCDapplicativeapplicatorp
(lambda (v)
(and (consp v)
(eq (car v)
SEMCDapplicativeapplicator))))
(set! SEMCDgetapplicativeapplicatoroperator
(lambda (v)
(car (cdr v))))
(set! SEMCDgetapplicativeapplicatoroperand
(lambda (v)
(car (cdr (cdr v)))))
;;;
;;; A helper function.
;;;
(set! SEMCDapplicatorp
(lambda (v)
(or (SEMCDnormalapplicatorp v)
(SEMCDapplicativeapplicatorp v))))
;;;
;;; The numbered applicator data type. This is a pair
;;; (applicator * number).
;;; SEMCDmakenumberedapplicator : the constructor
;;; SEMCDnumberedapplicatorp : recogniser predicate
;;; SEMCDgetnumberedapplicatorapplicator : a deconstructor
;;; SEMCDgetnumberedapplicatornumber : a deconstructor
;;;
(set! SEMCDmakenumberedapplicator cons)
(set! SEMCDnumberedapplicatorp
(lambda (v)
(and (consp v)
(let ((type
(SEMCDgetnumberedapplicatorapplicator v)))
(or
(eq type SEMCDapplicativeapplicator)
(eq type SEMCDnormalapplicator))))))
(set! SEMCDgetnumberedapplicatorapplicator car)
(set! SEMCDgetnumberedapplicatornumber cdr)
;;;
;;; The anonymous lambda data type.
;;; SEMCDmakelambda : the constructor
;;; SEMCDlambdap : recogniser predicate
;;; SEMCDgetlambda : the deconstructor
;;;
(set! SEMCDmakelambda
(lambda (exp)
(cons 'SEMCDlambda exp)))
(set! SEMCDlambdap
(lambda (v)
(and (consp v)
(eq (car v)
'SEMCDlambda))))
(set! SEMCDgetlambdaexp cdr)
;;;
;;; The suspension data type. This is a pair
;;; (env * exp).
;;; SEMCDmakesuspension : the constructor
;;; SEMCDsuspensionp : recogniser predicate
;;; SEMCDgetsuspensionenv : a deconstructor
;;; SEMCDgetsuspensionexp : a deconstructor
;;;
(set! SEMCDmakesuspension
(lambda (env exp)
(list 'SEMCDsuspension
env
exp)))
(set! SEMCDsuspensionp
(lambda (v)
(and (consp v)
(eq (car v)
'SEMCDsuspension))))
(set! SEMCDgetsuspensionenv
(lambda (v)
(car (cdr v))))
(set! SEMCDgetsuspensionexp
(lambda (v)
(car (cdr (cdr v)))))
;;;
;;; The irreducible applicator data type.
;;; SEMCDmakeirreducibleapplicator : the constructor
;;; SEMCDirreducibleapplicatonp : recogniser predicate
;;;
(set! SEMCDmakeirreducibleapplication
(lambda (app operator operand)
(list 'SEMCDirreducibleapplication
app
operator
operand)))
(set! SEMCDirreducibleapplicationp
(lambda (v)
(and (consp v)
(eq (car v)
'SEMCDirreducibleapplication))))
Here we have the transition function which drives the SEMCD machine.
The transitions are defined in the errata to the book "Abstract Computing Machines" by Werner Kluge (Springer).
This is a pretty faithful implementation using a tail recursive function which just recurses/loops until it cannot transition any more.
This will happen when the machine stacks
E
, M
, C
, and D
are empty, or,
if no transition can be made and E
, M
, C
, or D
are not empty which is an error.
Some rules (1c & 1d) have been added by myself. Rule 3 has its priority raised above rules 2a & 2b so that we can handle normal order applications which have applications as their operands. Should rules 2a or 2b be tried before rule 3 then you'll see that the operand gets evaluated which is NOT what you want!
;;;
;;; See the transition function for the reasons the
;;; "handle" functions are called.
;;;
(set! SEMCDhandle1a
(lambda (state)
(if *semcddebug* (print "state 1a"))
(SEMCDsetS state
(SEMCDstackpush
(SEMCDlookup
(SEMCDgetdebruijn
(SEMCDnextinstruction
(SEMCDgetC state)))
(SEMCDgetE state))
(SEMCDgetS state)))
;;; remove the instruction
(SEMCDsetC state
(SEMCDremoveinstruction
(SEMCDgetC state)))
;;; continue execution
(SEMCDtransition state)))
(set! SEMCDhandle1b
(lambda (state)
(if *semcddebug* (print "state 1b"))
;;; push the lookup result onto S
(SEMCDsetS state
(SEMCDstackpush
(SEMCDlookup
(SEMCDgetdebruijn
(SEMCDnextinstruction
(SEMCDgetC state)))
(SEMCDgetE state))
(SEMCDgetS state)))
;;; decrement the applicator
(let ((app (SEMCDstacktop
(SEMCDgetM state))))
(SEMCDsetM state
(SEMCDstackremovetop
(SEMCDgetM state)))
(SEMCDsetM state
(SEMCDstackpush
(SEMCDmakenumberedapplicator
(SEMCDgetnumberedapplicatorapplicator app)
(
(SEMCDgetnumberedapplicatornumber app)
1))
(SEMCDgetM state))))
;;; remove the instruction
(SEMCDsetC state
(SEMCDremoveinstruction
(SEMCDgetC state)))
;;; continue execution
(SEMCDtransition state)))
(set! SEMCDhandle1c
(lambda (state)
(if *semcddebug* (print "state 1c"))
;;; push
(SEMCDsetS state
(SEMCDstackpush
(SEMCDnextinstruction
(SEMCDgetC state))
(SEMCDgetS state)))
;;; remove the instruction
(SEMCDsetC state
(SEMCDremoveinstruction
(SEMCDgetC state)))
;;; continue execution
(SEMCDtransition state)))
(set! SEMCDhandle1d
(lambda (state)
(if *semcddebug* (print "state 1d"))
;;; push
(SEMCDsetS state
(SEMCDstackpush
(SEMCDnextinstruction
(SEMCDgetC state))
(SEMCDgetS state)))
;;; decrement the applicator
(let ((app (SEMCDstacktop
(SEMCDgetM state))))
(SEMCDsetM state
(SEMCDstackremovetop
(SEMCDgetM state)))
(SEMCDsetM state
(SEMCDstackpush
(SEMCDmakenumberedapplicator
(SEMCDgetnumberedapplicatorapplicator app)
(
(SEMCDgetnumberedapplicatornumber app)
1))
(SEMCDgetM state))))
;;; remove the instruction
(SEMCDsetC state
(SEMCDremoveinstruction
(SEMCDgetC state)))
;;; continue execution
(SEMCDtransition state)))
(set! SEMCDhandle2a
(lambda (state)
(if *semcddebug* (print "state 2a"))
(let ((instr (SEMCDnextinstruction
(SEMCDgetC state))))
(SEMCDsetC state
(SEMCDremoveinstruction
(SEMCDgetC state)))
(SEMCDsetC state
(SEMCDstackpush
(SEMCDgetapplicativeapplicatoroperator instr)
(SEMCDgetC state)))
(SEMCDsetC state
(SEMCDstackpush
(SEMCDgetapplicativeapplicatoroperand instr)
(SEMCDgetC state))))
(SEMCDsetM state
(SEMCDstackpush
(SEMCDmakenumberedapplicator
SEMCDapplicativeapplicator
2)
(SEMCDgetM state)))
;;; continue execution
(SEMCDtransition state)))
(set! SEMCDhandle2b
(lambda (state)
(if *semcddebug* (print "state 2b"))
(let ((instr (SEMCDnextinstruction
(SEMCDgetC state))))
(SEMCDsetC state
(SEMCDremoveinstruction
(SEMCDgetC state)))
(SEMCDsetC state
(SEMCDstackpush
(SEMCDgetnormalapplicatoroperator instr)
(SEMCDgetC state)))
(SEMCDsetC state
(SEMCDstackpush
(SEMCDgetnormalapplicatoroperand instr)
(SEMCDgetC state))))
(SEMCDsetM state
(SEMCDstackpush
(SEMCDmakenumberedapplicator
SEMCDnormalapplicator
2)
(SEMCDgetM state)))
;;; continue execution
(SEMCDtransition state)))
(set! SEMCDhandle3
(lambda (state)
(if *semcddebug* (print "state 3"))
;;; remove the numbered applicator
(SEMCDsetM state
(SEMCDstackremovetop
(SEMCDgetM state)))
;;; add the numbered applicator to M
(SEMCDsetM state
(SEMCDstackpush
(SEMCDmakenumberedapplicator
SEMCDnormalapplicator
1)
(SEMCDgetM state)))
;;; push the suspension made from the top of C
(SEMCDsetS state
(SEMCDstackpush
(SEMCDmakesuspension
(SEMCDgetE state)
(SEMCDnextinstruction
(SEMCDgetC state)))
(SEMCDgetS state)))
;;; setup the next instruction
(SEMCDsetC state
(SEMCDremoveinstruction
(SEMCDgetC state)))
;;; continue execution
(SEMCDtransition state)))
(set! SEMCDhandle4a
(lambda (state)
(if *semcddebug* (print "state 4a"))
(SEMCDsetS state
(SEMCDstackpush
(SEMCDmakesuspension
(SEMCDgetE state)
(SEMCDnextinstruction
(SEMCDgetC state)))
(SEMCDgetS state)))
;;; setup the next instruction
(SEMCDsetC state
(SEMCDremoveinstruction
(SEMCDgetC state)))
;;; continue execution
(SEMCDtransition state)))
(set! SEMCDhandle4b
(lambda (state)
(if *semcddebug* (print "state 4b"))
(SEMCDsetS state
(SEMCDstackpush
(SEMCDmakesuspension
(SEMCDgetE state)
(SEMCDnextinstruction
(SEMCDgetC state)))
(SEMCDgetS state)))
;;; decrement the applicator
(let ((app (SEMCDstacktop
(SEMCDgetM state))))
(SEMCDsetM state
(SEMCDstackremovetop
(SEMCDgetM state)))
(SEMCDsetM state
(SEMCDstackpush
(SEMCDmakenumberedapplicator
(SEMCDgetnumberedapplicatorapplicator app)
(
(SEMCDgetnumberedapplicatornumber app)
1))
(SEMCDgetM state))))
;;; setup the next instruction
(SEMCDsetC state
(SEMCDremoveinstruction
(SEMCDgetC state)))
;;; continue execution
(SEMCDtransition state)))
(set! SEMCDhandle5ab
(lambda (state)
(if *semcddebug* (print "state 5a/b"))
(let ((ebody nil)
(env nil)
(earg nil))
;;; the closure is on the top of S
(set! ebody (SEMCDgetlambdaexp
(SEMCDgetsuspensionexp
(SEMCDstacktop
(SEMCDgetS state)))))
(set! env (SEMCDgetsuspensionenv
(SEMCDstacktop
(SEMCDgetS state))))
(SEMCDsetS state
(SEMCDstackremovetop
(SEMCDgetS state)))
;;; the argument was under the closure
(set! earg (SEMCDstacktop
(SEMCDgetS state)))
(SEMCDsetS state
(SEMCDstackremovetop
(SEMCDgetS state)))
;;; pop the applicator with index 0
(SEMCDsetM state
(SEMCDstackremovetop
(SEMCDgetM state)))
;;; decrement any applicator which is on top of M
(if (and (SEMCDnumberedapplicatorp
(SEMCDstacktop
(SEMCDgetM state)))
(> (SEMCDgetnumberedapplicatornumber
(SEMCDstacktop
(SEMCDgetM state)))
0))
(let ((app (SEMCDstacktop (SEMCDgetM state))))
(SEMCDsetM state
(SEMCDstackremovetop
(SEMCDgetM state)))
(SEMCDsetM state
(SEMCDstackpush
(SEMCDmakenumberedapplicator
(SEMCDgetnumberedapplicatorapplicator app)
(
(SEMCDgetnumberedapplicatornumber app)
1))
(SEMCDgetM state)))))
;;; push the continuation on to D
(SEMCDsetD state
(SEMCDstackpush
(list
(SEMCDgetE state)
(SEMCDgetM state)
(SEMCDgetC state)
(SEMCDgetD state))
(SEMCDgetD state)))
;;; set E to the continuation environment.
(SEMCDsetE state
env)
;;; add the argument on to the front of E
(SEMCDsetE state
(SEMCDstackpush earg
(SEMCDgetE state)))
;;; clear M
(SEMCDsetM state nil)
;;; set C to the closure code
(SEMCDsetC state (SEMCDstackpush ebody nil)))
;;; continue execution with the closure code
(SEMCDtransition state)))
(set! SEMCDhandle6
(lambda (state)
(if *semcddebug* (print "state 6"))
(let ((exp nil)
(env nil))
(set! exp (SEMCDgetsuspensionexp
(SEMCDstacktop
(SEMCDgetS state))))
(set! env (SEMCDgetsuspensionenv
(SEMCDstacktop
(SEMCDgetS state))))
(SEMCDsetS state
(SEMCDstackremovetop
(SEMCDgetS state)))
(SEMCDsetD state
(SEMCDstackpush
(list
(SEMCDgetE state)
(SEMCDgetM state)
(SEMCDgetC state)
(SEMCDgetD state))
(SEMCDgetD state)))
(SEMCDsetE state env)
(SEMCDsetM state nil)
(SEMCDsetC state exp))
;;; continue execution
(SEMCDtransition state)))
(set! SEMCDhandle7ab
(lambda (state)
(if *semcddebug* (print "state 7a/b"))
;;; On S we see operator then operand.
(let ((operator nil)
(operand nil))
(set! operator (SEMCDstacktop
(SEMCDgetS state)))
(SEMCDsetS state
(SEMCDstackremovetop
(SEMCDgetS state)))
(set! operand (SEMCDstacktop
(SEMCDgetS state)))
(SEMCDsetS state
(SEMCDstackremovetop
(SEMCDgetS state)))
;;; make then push the
;;; irreducible application onto S
(SEMCDsetS state
(SEMCDstackpush
(SEMCDmakeirreducibleapplication
(SEMCDstacktop
(SEMCDgetM state))
operator
operand)
(SEMCDgetS state))) )
;;; pop the applicator off M
(SEMCDsetM state
(SEMCDstackremovetop
(SEMCDgetM state)))
;;; decrement the index of any applicate under the one
;;; we just popped off M
(if (and (SEMCDnumberedapplicatorp
(SEMCDstacktop
(SEMCDgetM state)))
(> (SEMCDgetnumberedapplicatornumber
(SEMCDstacktop
(SEMCDgetM state)))
0))
(let ((app (SEMCDstacktop (SEMCDgetM state))))
(SEMCDsetM state
(SEMCDstackremovetop
(SEMCDgetM state)))
(SEMCDsetM state
(SEMCDstackpush
(SEMCDmakenumberedapplicator
(SEMCDgetnumberedapplicatorapplicator app)
(
(SEMCDgetnumberedapplicatornumber app)
1))
(SEMCDgetM state)))))
;;; continue execution
(SEMCDtransition state)))
(set! SEMCDhandle8ab
(lambda (state)
(if *semcddebug* (print "state 8a/b"))
;;; operator on top of operand
(let ((operator nil)
(operand nil))
(set! operator (SEMCDstacktop
(SEMCDgetS state)))
(SEMCDsetS state
(SEMCDstackremovetop
(SEMCDgetS state)))
(set! operand (SEMCDstacktop
(SEMCDgetS state)))
(SEMCDsetS state
(SEMCDstackremovetop
(SEMCDgetS state)))
(SEMCDsetS state
(SEMCDstackpush
(SEMCDmakeirreducibleapplication
(SEMCDstacktop
(SEMCDgetM state))
operator
operand)
(SEMCDgetS state))) )
;;; pop the top applicator off M
(SEMCDsetM state
(SEMCDstackremovetop
(SEMCDgetM state)))
;;; decrement the index of any applicator underneath the
;;; one we just popped off M
(if (and (SEMCDnumberedapplicatorp
(SEMCDstacktop
(SEMCDgetM state)))
(eq SEMCDnormalapplicator
(SEMCDgetnumberedapplicatorapplicator
(SEMCDstacktop
(SEMCDgetM state))))
(> (SEMCDgetnumberedapplicatornumber
(SEMCDstacktop
(SEMCDgetM state)))
0))
(let ((app (SEMCDstacktop
(SEMCDgetM state))))
(SEMCDsetM state
(SEMCDstackremovetop
(SEMCDgetM state)))
(SEMCDsetM state
(SEMCDstackpush
(SEMCDmakenumberedapplicator
(SEMCDgetnumberedapplicatorapplicator app)
(
(SEMCDgetnumberedapplicatornumber app)
1))
(SEMCDgetM state)))))
;;; continue execution
(SEMCDtransition state)))
(set! SEMCDhandle9
(lambda (state)
(if *semcddebug* (print "state 9"))
(SEMCDsetE state
(SEMCDgetE
(SEMCDgetD state)))
(SEMCDsetM state
(SEMCDgetM
(SEMCDgetD state)))
(SEMCDsetC state
(SEMCDgetC
(SEMCDgetD state)))
(SEMCDsetD state
(SEMCDgetD
(SEMCDgetD state)))
;;; continue execution
(SEMCDtransition state)))
;;;
;;; The heart of the machine.
;;;
(set! SEMCDtransition
(lambda (state)
(if *semcddebug*
(begin
(print '============)
(print (SEMCDgetS state))
(print (SEMCDgetE state))
(print (SEMCDgetM state))
(print (SEMCDgetC state))
(print (SEMCDgetD state))))
(cond
;;;
;;; 1a. Move environment entries to the stack.
;;;
;;; We've got a de Bruijn number on C and M is
;;; empty. Let's lookup the variable in E and
;;; push the bound value onto S.
;;;
((and (SEMCDemptystackp
(SEMCDgetM state))
(SEMCDdebruijnp
(SEMCDnextinstruction
(SEMCDgetC state))))
(SEMCDhandle1a state))
;;;
;;; 1b. Move environment entries to the stack.
;;;
;;; We've got a de Bruijn number on the code
;;; stack and M is not empty  it contains a
;;; numbered applicator so let's lookup the
;;; variable address and push the bound value
;;; onto S then decrement the applicator.
;;;
((and (SEMCDnumberedapplicatorp
(SEMCDstacktop
(SEMCDgetM state)))
(> (SEMCDgetnumberedapplicatornumber
(SEMCDstacktop
(SEMCDgetM state)))
0)
(SEMCDdebruijnp
(SEMCDnextinstruction
(SEMCDgetC state))))
(SEMCDhandle1b state))
;;;
;;; 1c. Move vars to the stack
;;;
;;; We've got an unbound variable on C and
;;; M is empty. Just push the variable
;;; onto S.
;;;
((and (SEMCDemptystackp
(SEMCDgetM state))
(SEMCDvariablep
(SEMCDnextinstruction
(SEMCDgetC state))))
(SEMCDhandle1c state))
;;;
;;; 1d. Move vars to the stack
;;;
;;; We've got an unbound variable on C and
;;; a numbered applicator (i > 0) on M. We'll
;;; push the variable onto S and decrement the
;;; applicator.
;;;
((and (SEMCDnumberedapplicatorp
(SEMCDstacktop
(SEMCDgetM state)))
(> (SEMCDgetnumberedapplicatornumber
(SEMCDstacktop
(SEMCDgetM state)))
0)
(SEMCDvariablep
(SEMCDnextinstruction
(SEMCDgetC state))))
(SEMCDhandle1d state))
;;;
;;; 3. make a suspension for the operand to a normal order application
;;;
;;; Build the argument suspension, push it onto S then decrement the
;;; index of the normal order applicator on M, i.e., set it to 1.
;;;
;;; Why has this been placed above 2a and 2b? Try this to see why:
;;; (normalapply (lambda x z) ((lambda w (w w)) (lambda w (w w))))
((and (SEMCDnumberedapplicatorp (SEMCDstacktop
(SEMCDgetM state)))
(eq SEMCDnormalapplicator
(SEMCDgetnumberedapplicatorapplicator
(SEMCDstacktop
(SEMCDgetM state))))
(= 2 (SEMCDgetnumberedapplicatornumber
(SEMCDstacktop
(SEMCDgetM state)))))
(SEMCDhandle3 state))
;;;
;;; 2a. split applications into their components
;;;
;;; We've got an applicative applicator on top of C.
;;; Pop it off C and push a numbered applicative order
;;; applicator onto M with index 2.
;;;
((SEMCDapplicativeapplicatorp (SEMCDnextinstruction
(SEMCDgetC state)))
(SEMCDhandle2a state))
;;;
;;; 2b. split applications into their components
;;;
;;; We've got a normal applicator on top of C.
;;; Pop it off C and push a numbered normal order
;;; applicator onto M with index 2.
;;;
((SEMCDnormalapplicatorp (SEMCDnextinstruction
(SEMCDgetC state)))
(SEMCDhandle2b state))
;;;
;;; 4a. create a suspension for an abstraction
;;;
;;; M is empty and we've got a lamabda on top of C.
;;; Create a closure and push it onto S.
;;;
((and (SEMCDemptystackp (SEMCDgetM state))
(SEMCDlambdap (SEMCDnextinstruction
(SEMCDgetC state))))
(SEMCDhandle4a state))
;;;
;;; 4b. create a suspension for an abstraction
;;;
;;; The top of M is an applicator with index.
;;; The top of C is a lambda. Create a closure.
;;; Push the closure onto S and decrement the
;;; applicator index.
((and (SEMCDnumberedapplicatorp (SEMCDstacktop
(SEMCDgetM state)))
(> (SEMCDgetnumberedapplicatornumber
(SEMCDstacktop
(SEMCDgetM state)))
0)
(SEMCDlambdap (SEMCDnextinstruction
(SEMCDgetC state))))
(SEMCDhandle4b state))
;;;
;;; 5a/b. implement naive beta reduction
;;;
;;; There is a closure then an argument on top of S.
;;; If there is a single applicator with index 0 on M,
;;; Do the reduction. Push the continuation onto D.
;;; Set E and C to the contents of the closure and
;;; add the argument to E. If there are two applicators
;;; on M (the top one having index 0) then do the same as
;;; in the case with one applicator on M but remember to
;;; decrement the applicator under it.
;;;
((and (SEMCDsuspensionp (SEMCDstacktop
(SEMCDgetS state)))
(SEMCDlambdap (SEMCDgetsuspensionexp
(SEMCDstacktop
(SEMCDgetS state))))
(SEMCDnumberedapplicatorp (SEMCDnextinstruction
(SEMCDgetM state)))
(= 0
(SEMCDgetnumberedapplicatornumber
(SEMCDnextinstruction
(SEMCDgetM state)))))
(SEMCDhandle5ab state))
;;;
;;; 6. Operand closures
;;;
;;; Take the closure on top of S and evaluate it. This was put on
;;; S by step 3.
;;;
((and (SEMCDsuspensionp (SEMCDstacktop
(SEMCDgetS state)))
(SEMCDirreducibleapplicationp (SEMCDgetsuspensionexp
(SEMCDstacktop
(SEMCDgetS state)))))
(SEMCDhandle6 state))
;;;
;;; 7a/b. irreducible applicative applications
;;;
;;; The top of M is either a single applicative applicator of index 0, or
;;; an applicator of index 0 with an applicative applicator under it.
;;; The top of the stack cannot be reduced so it must be an irreducible
;;; application. So build it and remove the top applicator on M and
;;; if there was an applicator under it, decrement its index.
;;;
((and (SEMCDnumberedapplicatorp
(SEMCDstacktop
(SEMCDgetM state)))
(eq SEMCDapplicativeapplicator
(SEMCDgetnumberedapplicatorapplicator
(SEMCDstacktop
(SEMCDgetM state))))
(= 0
(SEMCDgetnumberedapplicatornumber
(SEMCDstacktop
(SEMCDgetM state)))))
(SEMCDhandle7ab state))
;;;
;;; 8a/b. irreducible normal applications
;;;
;;; The top of M is either a single normal applicator of index 0, or
;;; an applicator of index 0 with an normal applicator under it.
;;; The top of the stack cannot be reduced so it must be an irreducible
;;; application. So build it and remove the top applicator on M and
;;; if there was an applicator under it, decrement its index.
;;;
((and (SEMCDnumberedapplicatorp (SEMCDstacktop
(SEMCDgetM state)))
(eq SEMCDnormalapplicator
(SEMCDgetnumberedapplicatorapplicator
(SEMCDstacktop (SEMCDgetM state))))
(= 0
(SEMCDgetnumberedapplicatornumber
(SEMCDstacktop
(SEMCDgetM state)))))
(SEMCDhandle8ab state))
;;;
;;; 9. The code (C) is empty so we retrieve the
;;; continuation from D and continue from there.
;;;
((and (SEMCDemptystackp (SEMCDgetM state))
(SEMCDemptystackp (SEMCDgetC state))
(not (SEMCDemptystackp (SEMCDgetD state))))
(SEMCDhandle9 state))
;;;
;;; Finish. E, M, C, and D are empty and the result
;;; of the computation is on the top of S.
;;;
((and (SEMCDemptystackp (SEMCDgetE state))
(SEMCDemptystackp (SEMCDgetM state))
(SEMCDemptystackp (SEMCDgetC state))
(SEMCDemptystackp (SEMCDgetD state)))
(if *semcddebug* (print "state FINISH"))
;;; return the result of the computation
(SEMCDstacktop (SEMCDgetS state)))
;;;
;;; Otherwise, we've got an error!
;;;
(t (signalexception t
(list
"No transition possible"
state))))))
The following functions will translate a λexpression described by the following grammar where v
is a variable and
c
is a constant (number, string, etc.)
e ::= v  c  (e e)  (normalapply e e)  (lambda v e)
into the input the SEMCD machine expects.
The normalapply
symbol is used to tell the compiler to generate code to force a normal order application of the arguments,
so ((lambda x x) (lambda y y))
is an applicative order application, and
(normalapply (lambda x x) (lambda y y))
is the normal order application of the same operator and argument.
The compiler is an example of a simple recursive descent compiler.
(set! SEMCDcompileexp
(lambda (e rho)
(if (atom e)
(if (symbolp e)
(SEMCDcompilevariable e rho)
(SEMCDcompilequote e rho))
(cond ((eq (car e) 'lambda)
(SEMCDcompilelambda (cadr e) (caddr e) rho))
((eq (car e) 'normalapply)
(SEMCDcompilenormalapplication (cadr e) (caddr e) rho))
(t (SEMCDcompileapplicativeapplication (car e) (cadr e) rho))))))
;;;
;;; A variable will be either a de Bruijn number(/index/address)
;;; if it is bound, or an unbound variable in the form
;;; (SEMCDvariable v).
;;;
(set! SEMCDcompilevariable
(lambda (v r)
(let ((dbn (SEMCDrholookup v r 0)))
(if dbn
(SEMCDmakedebruijn dbn)
(SEMCDmakevariable v)))))
;;;
;;; In this sense "quote" is really those things that are
;;; "autoquote", i.e., numbers, strings, etc.
;;;
(set! SEMCDcompilequote
(lambda (e r)
e))
;;;
;;; To compile an abstraction we need to collect the
;;; argument variable and then use it to extend the
;;; static environment which will be used to compile
;;; the abstraction body.
;;;
(set! SEMCDcompilelambda
(lambda (name body rho)
(if (not (symbolp name))
(signalexception t
(list "Oooops lambda param is not a symbol  "
name))
(SEMCDmakelambda
(SEMCDcompileexp body
(SEMCDextendrho name rho))))))
;;;
;;; Build an application. Simple stuff, just
;;; build the node from the operator and
;;; operand experessions.
;;;
(set! SEMCDcompileapplicativeapplication
(lambda (operator operand rho)
(SEMCDmakeapplicativeapplicator
(SEMCDcompileexp operator rho)
(SEMCDcompileexp operand rho))))
;;;
;;; Pretty much the same as above only the
;;; constructor has been changed.
;;;
(set! SEMCDcompilenormalapplication
(lambda (operator operand rho)
(SEMCDmakenormalapplicator
(SEMCDcompileexp operator rho)
(SEMCDcompileexp operand rho))))
These functions are used by the expression compiler to help it generate de Bruijn numbers.
The static environment is extended with SEMCDextendrho
and SEMCDrholookup
is used to get the number/index/address.
;;;
;;; Search the environment for the given name.
;;; Return the name's index in the environment if
;;; it is to be found there, otherwise return nil.
;;; The function is written in accumulator passing
;;; tail recursive style in order to make it run
;;; in constant stack space. That's why the "number"
;;; is there.
;;;
(set! SEMCDrholookup
(lambda (name rho number)
(cond ((null rho) nil)
((eq name (car rho)) number)
(t (SEMCDrholookup name
(cdr rho)
(+ 1 number))))))
;;;
;;; Extend the static environment by adding a new name.
;;;
(set! SEMCDextendrho cons)
Here we have a simple user interface for the compiler and SEMCD machine. We ask for input, collect it, compile it, then evaluate it with an initialised machine.
(let ((state SEMCDemptystate))
(set! SEMCDtest
(lambda ()
(print 'ready>)
(SEMCDsetS state nil)
(SEMCDsetE state nil)
(SEMCDsetM state nil)
(SEMCDsetD state nil)
(SEMCDsetC state
(cons (SEMCDcompileexp (read)
nil)
nil))
(print (SEMCDtransition state))
(SEMCDtest))))
;;; GO!!!!
(semcdtest)
A test run is shown below
READY>
(lambda x x)
(SEMCDSUSPENSION NIL (SEMCDLAMBDA SEMCDDEBRUIJN . 0))
READY>
((lambda x x) (lambda y y))
(SEMCDSUSPENSION NIL (SEMCDLAMBDA SEMCDDEBRUIJN . 0))
READY>
(lambda x (lambda y x))
(SEMCDSUSPENSION NIL (SEMCDLAMBDA SEMCDLAMBDA SEMCDDEBRUIJN . 1))
W. Kluge. Abstract Computing Machines. A Lambda Calculus Perspective. Springer, 2005.
Copyright © 2015 Barry Watson. All rights reserved.