Categorical Abstract Machine (CAM)

The Categorical Abstract Machine (CAM), designed by Cousineau, Curien and Mauny, is an abstract machine for the evaluation of the nameless λ-calculus (Λ-calculus). The Λ-terms are evaluated with an applicative order reduction strategy until weak head normal form, i.e. the machine is weakly normalising. Presented here, its definition using a terminal transition system has only seven transition rules. This definition is almost identical to that given in Werner Kluge's book.

Compilation

The CAM doesn't evaluate Λ-terms directly, it executes instructions which represent terms. There are seven such instructions: app, car, cdr, cons, cur, swap, push. The compilation scheme which takes us from Λ-terms to instructions is shown below. In these rules the concatenation operator (|) is used to build sequences of instructions. The sequence of a solitary instruction i is written [i]. The sequence of n instructions i₀,i₁,...,i_n-1 is written [i₀,i₁,...,i_n-1]. If I is an instruction sequence, then [i|I] is the same sequence but with i pushed onto the front. The empty sequence is []. The binary operator @ is used to append sequences together, so [i,j,k] @ [l,m,n] = [i,j,k,l,m,n].

compile(#0) = [cdr]
compile(#(i+1)) = [car| compile(#(i))]
compile(Λe) = [cur(compile(e))]
compile((e₀e₁) = [push] @ compile(e₀) @ [swap] @ compile(e₁) @ [cons, app]

As an example, the Λ-term (Λ#0 Λ#0) is compiled into

	  [push, cur([cdr]), swap, car, cur([cdr]), cons, app]

CAM Configuration

The configuration of the machine consists of three components:

a term register T, and
a code stack C,
a working stack S.

CAM Transition Rules

The transition relation between configurations is →. It is defined by the rules below. We'll use empty for the contents of an empty T register. The initial configuration for program p is ⟨empty,p,[]⟩. A terminal configuration has the form ⟨t,[],[]⟩ for some term t. The datum env(E,v) is an environment sequence where v is the value at address 0 of the sequence and E contains the values for addresses 1,2,... . This works just like the environment stacks found in programming languages. The datum susp(E,c) is a suspension, or closure, of the instruction sequence c and environment E.

Rules

⟨(env(p,q), [car|C], S⟩ → ⟨p, C, S⟩
⟨(env(p,q), [cdr|C], S⟩ → ⟨q, C, S⟩
⟨(p, [cur(c)|C], S⟩ → ⟨susp(p,c), C, S⟩
⟨(p, [push|C], S⟩ → ⟨p, C, [p|S]⟩
⟨(p, [swap|C], [q|S]⟩ → ⟨q, C, [p|S]⟩
⟨(p, [cons|C], [q|S]⟩ → ⟨env(q,p), C, S⟩
⟨(env(susp(p,c),q), [app|C], S⟩ → ⟨env(p,q), [c|C], S⟩

Example Switches

Here we have the switches which control the machine's behaviour. We have only one switch used to trace the transitions as an aid in debugging.


	;;; This is a switch which will turn on debug printouts
;;; showing the state of the machine.
(set! *CAM-debug* nil)

Basic Library Functions

This section contains helpful functions that are not CAM specific.


	;;;
;;; 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)

Term Grammar

This is the input to the second pass of the compiler. Here i is an integer, and e is an environment.

t ::= (CAM-de-bruijn i)
|   (CAM-lambda t)
|   (CAM-application t t)

The following are constructors, destructors and recognisers for the grammar's non-terminals.


	;;;
;;; The deBruijn number data type.
;;;  CAM-make-de-bruijn : the constructor
;;;  CAM-de-bruijn-p    : recogniser predicate
;;;  CAM-get-de-bruijn  : 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! CAM-make-de-bruijn 
      (lambda (v)
	(cons 'CAM-de-bruijn v)))

(set! CAM-de-bruijn-p 
      (lambda (v)
	(and (consp v)
	     (eq (car v) 
		 'CAM-de-bruijn))))

(set! CAM-get-de-bruijn cdr)

;;;
;;; The application data type.
;;;  CAM-make-application         : the constructor
;;;  CAM-application-p            : recogniser predicate
;;;  CAM-get-application-operand  : a deconstructor
;;;  CAM-get-application-operator : a deconstructor
;;;
(set! CAM-make-application 
      (lambda (operator operand)
	(list 'CAM-application 
	      operator 
	      operand)))

(set! CAM-application-p 
      (lambda (v)
	(and (consp v)
	     (eq (car v) 
		 'CAM-application))))

(set! CAM-get-application-operator
      (lambda (v)
	(car (cdr v))))

(set! CAM-get-application-operand
      (lambda (v)
	(car (cdr (cdr v)))))

;;;
;;; The anonymous lambda data type.
;;;  CAM-make-lambda : the constructor
;;;  CAM-lambda-p    : recogniser predicate
;;;  CAM-get-lambda  : the deconstructor
;;;
(set! CAM-make-lambda 
      (lambda (exp)
	(cons 'CAM-lambda exp)))

(set! CAM-lambda-p 
      (lambda (v)
	(and (consp v)
	     (eq (car v) 
		 'CAM-lambda))))

(set! CAM-get-lambda-exp cdr)

Machine Stack Manipulation Functions

The CAM has three stacks/registers:

T : Terms. Instructions construct and deconstruct terms, suspensions, and environments here.
C : Code.
S : Stack. Temporary storage.

The following are functions used to manipulate the registers.


	;;; Predicate to test for an empty stack.
(set! CAM-empty-stack-p null)

;;; Push an element onto a stack.
(set! CAM-stack-push cons)

;;; Remove the element at the top of the stack
(set! CAM-stack-remove-top cdr)

;;; Retrieve the element at the top of the stack.
(set! CAM-stack-top car)

;;; What an empty stack looks like.
(set! CAM-empty-stack nil)

;;;
;;; We need this to build an initial state -
;;; a fresh one every time it is called. 
;;;
;;; The symbol CAM-null-list is a wee bit special.
;;; I added it so that I could more easily read
;;; traces of the machine state. 
;;;
(set! CAM-empty-state 
      (lambda ()
	(list 'CAM-null-list
	      CAM-empty-stack
	      CAM-empty-stack)))
      
;;;
;;; Getter and setter for T which is the
;;; first element of the machine state.
;;;
(set! CAM-get-T car)

(set! CAM-set-T 
      (lambda (state new-T)
	(rplaca state new-T)
	state))

;;;
;;; Getter and setter for C  which is the
;;; second element of the machine state.
;;;
(set! CAM-get-C
      (lambda (state)
	(car (cdr state))))

(set! CAM-set-C 
      (lambda (state new-C)
	(rplaca (cdr state) new-C)
	state))

;;;
;;; Getter and setter for S  which is the
;;; third element of the machine state.
;;;
(set! CAM-get-S
      (lambda (state)
	(car (cdr (cdr state)))))

(set! CAM-set-S 
      (lambda (state new-S)
	(rplaca (cdr (cdr state)) new-S)
	state))

Instructions and Machine Data Types

Here we see the functions used to recognise and execute instructions.


	;;;
;;; The cons data type. This is a pair
;;; (head * tail).
;;;  CAM-cons   : the constructor
;;;  CAM-cons-p : recogniser predicate
;;;  CAM-car    : a deconstructor
;;;  CAM-cdr    : a deconstructor
;;;
(set! CAM-car
      (lambda (lst)
	(car (cdr lst))))

(set! CAM-cdr
      (lambda (lst)
	(car (cdr (cdr lst)))))

(set! CAM-cons
      (lambda (head tail)
	(list 'CAM-cons 
	      head
	      tail)))

(set! CAM-cons-p 
      (lambda (lst)
	(and (consp lst)
	     (eq (car lst)
		 'CAM-cons))))

;;;
;;; The suspension data type. This is a pair
;;; (env * exp).
;;;  CAM-make-suspension    : the constructor
;;;  CAM-suspension-p       : recogniser predicate
;;;  CAM-get-suspension-env : a deconstructor
;;;  CAM-get-suspension-exp : a deconstructor
;;;
(set! CAM-make-suspension 
      (lambda (env exp)
	(cons 'CAM-suspension 
	      (cons env 
		    exp))))

(set! CAM-suspension-p 
      (lambda (v)
	(and (consp v)
	     (eq (car v) 
		 'CAM-suspension))))

(set! CAM-get-suspension-env 
      (lambda (v)
	(car (cdr v))))

(set! CAM-get-suspension-exp 
      (lambda (v)
	(cdr (cdr v))))

;;;
;;; The curried closure data type.
;;;  CAM-make-curry     : the constructor
;;;  CAM-curry-p        : recogniser predicate
;;;  CAM-get-curry-body : a deconstructor
;;;
(set! CAM-make-curry
      (lambda (body)
	(cons 'CAM-curry body)))

(set! CAM-curry-p 
      (lambda (v)
	(and (consp v)
	     (eq (car v) 
		 'CAM-curry))))

(set! CAM-get-curry-body 
      (lambda (v)
	(cdr v)))

The Transition Function

This is the heart of the machine. The transition rules are implemented here.


	
(set! CAM-transition 
      (lambda (state)
	(if *CAM-debug*
	    (begin
	     (print '===============)
	     (print (CAM-get-T state))
	     (print (CAM-get-C state))
	     (print (CAM-get-S state))))

	(let ((instr (CAM-stack-top (CAM-get-C state))))
	  (cond ((and (eq instr 'car)
		      (CAM-cons-p (CAM-get-T state)))
		 (if *CAM-debug* (print 'car))
		 (CAM-set-T state 
			    (CAM-car (CAM-get-T state)))
		 ;;; set up the next instruction and
		 ;;; execute it.
		 (CAM-set-C state 
			    (CAM-stack-remove-top 
			     (CAM-get-C state)))		 
		 (CAM-transition state))
		
		((and (eq instr 'cdr)
		      (CAM-cons-p (CAM-get-T state)))
		 (if *CAM-debug* (print 'cdr))
		 (CAM-set-T state 
			    (CAM-cdr (CAM-get-T state)))
		 ;;; set up the next instruction and
		 ;;; execute it.
		 (CAM-set-C state 
			    (CAM-stack-remove-top 
			     (CAM-get-C state)))		 
		 (CAM-transition state))
		
		((CAM-curry-p instr)
		 (if *CAM-debug* (print 'cur))
		 (CAM-set-T state 
			    (CAM-make-suspension 
			     (CAM-get-T state)
			     (CAM-get-curry-body instr)))
		 ;;; set up the next instruction and
		 ;;; execute it.
		 (CAM-set-C state 
			    (CAM-stack-remove-top 
			     (CAM-get-C state)))		 
		 (CAM-transition state))
		
		((eq instr 'push)
		 (if *CAM-debug* (print 'push))
		 (CAM-set-S state 
			    (CAM-stack-push 
			     (CAM-get-T state)
			     (CAM-get-S state)))
		 ;;; set up the next instruction and
		 ;;; execute it.
		 (CAM-set-C state 
			    (CAM-stack-remove-top 
			     (CAM-get-C state)))		 
		 (CAM-transition state))
		
		((eq instr 'swap)
		 (if *CAM-debug* (print 'swap))
		 (let ((q (CAM-stack-top 
			       (CAM-get-S state)))
		       (p (CAM-get-T state)))
		   
		   (CAM-set-S state
			      (CAM-stack-remove-top
			       (CAM-get-S state)))

		   (CAM-set-S state 
			      (CAM-stack-push 
			       p
			       (CAM-get-S state)))

		   (CAM-set-T state q)

         	   ;;; set up the next instruction and
		   ;;; execute it.
		   (CAM-set-C state 
			      (CAM-stack-remove-top 
			       (CAM-get-C state)))		 
		   (CAM-transition state)))

		((eq instr 'cons)
		 (if *CAM-debug* (print 'cons))
		 (let ((s-top (CAM-stack-top 
			       (CAM-get-S state)))
		       (term (CAM-get-T state)))
		   
		   (CAM-set-S state
			      (CAM-stack-remove-top
			       (CAM-get-S state)))

; write mail about this to the author. This code is 
; shown in the specification in the book but it looks
; incorrect.		   
;		   (CAM-set-S state 
;			      (CAM-stack-push 
;			       term
;			       (CAM-get-S state)))
		   (CAM-set-T state 
			      (CAM-cons
			       s-top
			       term))

         	   ;;; set up the next instruction and
		   ;;; execute it.
		   (CAM-set-C state 
			      (CAM-stack-remove-top 
			       (CAM-get-C state)))		 
		   (CAM-transition state)))

		((and (eq instr 'app)
		      (CAM-cons-p (CAM-get-T state))
		      (CAM-suspension-p (CAM-car 
					 (CAM-get-T state))))
		 (if *CAM-debug* (print 'app))
		 (let* ((term (CAM-get-T state))
			(susp (CAM-car term))
			(p (CAM-get-suspension-env susp))
			(c (CAM-get-suspension-exp susp))
			(q (CAM-cdr term)))
		   
		   (CAM-set-T state 
			      (CAM-cons p q))
		   
         	   ;;; set up the next instruction and
		   ;;; execute it.		 
		   (CAM-set-C state c)
		   (CAM-transition state)))
		
		((and (CAM-empty-stack-p (CAM-get-C state))
		      (CAM-empty-stack-p (CAM-get-S state)))
		 (if *CAM-debug* (print 'finished))
		 ;;; T contains the result in weak normal form.
		 (CAM-get-T state))
	  ;;;
	  ;;; Otherwise, we've got an error!
	  ;;;
		(t (signal-exception t 
				     (list 
				      "No transition possible" 
				      state)))))))

Expression Compiler

The compiler takes an S-expression input and turn it into something the CAM machine can execute. An example input expression is

	((lambda x (x x))(lambda u u))

This is a simple recursive descent compiler which comprises two passes.


	(set! CAM-compile-exp
      (lambda (e)
	(CAM-compile-pass2
	 (CAM-compile-pass1-exp e nil))))

(set! CAM-compile-pass1-exp 
      (lambda (e rho)
	(if (atom e) 
	    (if (symbolp e) 
		(CAM-compile-pass1-variable e rho)
		(signal-exception t (list "invalid input" e)))
	    (cond ((eq (car e) 'lambda) 
		   (CAM-compile-pass1-lambda (cadr e) (caddr e) rho))
		  (t (CAM-compile-pass1-application (car e) (cadr e) rho))))))

;;;
;;; A variable will be either a de Bruijn number(/index/address) 
;;; if it is bound, or an error.
;;;
(set! CAM-compile-pass1-variable 
      (lambda (v r)
	(let ((dbn (CAM-rho-lookup v r 0)))
	  (if dbn 
	      (CAM-make-de-bruijn dbn)
	      (signal-exception t (list "not a bound variable" v))))))

;;;
;;; 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! CAM-compile-pass1-lambda 
      (lambda (name body rho)
	(if (not (symbolp name))
	    (signal-exception t 
			      (list "Oooops lambda param is not a symbol - " 
				    name))
	    (CAM-make-lambda 
	     (CAM-compile-pass1-exp body 
				    (CAM-extend-rho name rho))))))

;;;
;;; Build an application. Simple stuff, just 
;;; build the node from the operator and 
;;; operand experessions.
;;;
(set! CAM-compile-pass1-application 
      (lambda (operator operand rho)
	(CAM-make-application
	 (CAM-compile-pass1-exp operator rho)
	 (CAM-compile-pass1-exp operand rho))))

;;; 
;;; 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! CAM-rho-lookup 
      (lambda (name rho number)
	(cond ((null rho) nil)
	      ((eq name (car rho)) number)
	      (t (CAM-rho-lookup name 
				 (cdr rho) 
				 (+ 1 number))))))
;;;
;;; Extend the static environment by adding a new name.
;;;
(set! CAM-extend-rho cons)



;;; Make sure the curried code instructions
;;; are in list form. 
(set! CAM-compile-pass2-fixup 
      (lambda (exp)
	(cond ((not (consp exp))
	       (cons exp nil))
	      (t exp))))
;;;
;;; Compiler pass 2. The helper function does all the heavy lifting.
;;;
;;; Generate instructions from the nameless lambda calculus.
;;; Just walk the tree.
;;;
(set! CAM-compile-pass2-helper 
      (lambda (exp)
	(cond ((CAM-de-bruijn-p exp)
	       (let ((index (CAM-get-de-bruijn exp)))
		 (if (= 0 index)
		     'cdr
		     (cons 'car (CAM-compile-pass2-helper 
				 (CAM-make-de-bruijn 
				  (- index 1)))))))
	      ((CAM-lambda-p exp)
	       (CAM-make-curry 
		;;; make sure curried abstractions have
		;;; the code body in the form of a list.
		(CAM-compile-pass2-fixup 
		 (CAM-compile-pass2-helper 
		  (CAM-get-lambda-exp exp)))))
	      ((CAM-application-p exp)
	       (list
		'push
		 (CAM-compile-pass2-helper
		  (CAM-get-application-operator exp))
		'swap
		 (CAM-compile-pass2-helper
		  (CAM-get-application-operand exp))
		'cons
		'app))
	      (t (signal-exception t
				   (list "bad input to pass2" 
					 exp))))))

;;;
;;; The wrapper. We want "(lambda x x)" to be translated into 
;;; a list with just the one instruction "((cur cdr))". 
;;; Check for this special case.
;;;
(set! CAM-compile-pass2 
      (lambda (exp)
	(let ((result (CAM-compile-pass2-helper exp)))
	  (if (CAM-curry-p result)
	      (cons result nil)
	      result))))

Test Functions

Here we have a simple test function that reads some input expression, compiles it, then executes it with the CAM machine. The weak normal form of the input is returned if it exists, otherwise an error is signalled.


	(let* ((state nil))
  (set! CAM-test 
	(lambda ()
	  (print 'ready>)
	  (set! state (CAM-empty-state))
	  (CAM-set-C state
		     (CAM-compile-exp (read)))		
	  (CAM-transition state))))

Test Run

A quick test is shown below:


	(CAM-test)
READY>
((lambda x x)(lambda y y))
(CAM-SUSPENSION CAM-NULL-LIST CDR)
OK

References

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