SECD Machine

Hi,

SECD is an abstract machine intended as a target for functional programming language compilers.

It’s a stack-based runtime with a core of 10 opcodes defined with a set of transitions between its four components. Functions take their arguments from the stack. The arguments to built-in instructions are encoded immediately after them in the instruction stream. If C and D are both empty, overall evaluation has completed with the result on S.

  • Stack S register points to a list of intermediate results.
  • Environment E register points to the current environment.
  • Control C register points a location in the program.
  • Dump D register points to a list of triples. Each triple contains snapshots of the stack, environment, and control registers.

The .secd representation of a program encodes the various parts of a functional programming language into the abstract machine code, where each opcode is represented as a number. For example, if we compile the Pure Lisp program below:

Pure Lisp: (LAMBDA (X) (ADD (QUOTE 1) X)) 
SECD(opcodes): ( 3 ( 2 1 1 ( 0 . 0 ) 15 5 ) 4 21 ) 
SECD(mnemonics): ( LDF ( LDC 1 LD ( 0 . X ) ADD RTN ) AP BRK )

It’s something that I’ve messed with in the past, but I wanted to put it here as it might be of interest to Malleable software, the virtual machine implementation is about 150 lines of C. It’s quite easy to reflect about if you’re familiar with stack machines, it’s a pretty straight-forward target, here’s a self-hosted compiler:

(LETREC COMPILE
	(COMPILE LAMBDA (E)
		(COMP E (QUOTE NIL) (QUOTE (4 21))))
	(COMP LAMBDA (E N C)
		(IF (ATOM E)
				(CONS (QUOTE 1) (CONS (LOCATION E N) C)) 
		(IF (EQ (CAR E) (QUOTE QUOTE)) 
				(CONS (QUOTE 2) (CONS (CAR (CDR E)) C)) 
		(IF (EQ (CAR E) (QUOTE ADD)) 
				(COMP (CAR (CDR E)) N (COMP (CAR (CDR (CDR E))) N (CONS (QUOTE 15) C))) 
		(IF (EQ (CAR E) (QUOTE SUB))
				(COMP (CAR (CDR E)) N (COMP (CAR (CDR (CDR E))) N (CONS (QUOTE 16) C))) 
		(IF (EQ (CAR E) (QUOTE MUL))
				(COMP (CAR (CDR E)) N (COMP (CAR (CDR (CDR E))) N (CONS (QUOTE 17) C))) 
		(IF (EQ (CAR E) (QUOTE DIV))
				(COMP (CAR (CDR E)) N (COMP (CAR (CDR (CDR E))) N (CONS (QUOTE 18) C))) 
		(IF (EQ (CAR E) (QUOTE REM)) 
				(COMP (CAR (CDR E)) N (COMP (CAR (CDR (CDR E))) N (CONS (QUOTE 19) C))) 
		(IF (EQ (CAR E) (QUOTE LEQ))
				(COMP (CAR (CDR E)) N (COMP (CAR (CDR (CDR E))) N (CONS (QUOTE 20) C))) 
		(IF (EQ (CAR E) (QUOTE EQ))
				(COMP (CAR (CDR E)) N (COMP (CAR (CDR (CDR E))) N (CONS (QUOTE 14) C))) 
		(IF (EQ (CAR E) (QUOTE CAR))
				(COMP (CAR (CDR E)) N (CONS (QUOTE 10) C))
		(IF (EQ (CAR E) (QUOTE CDR))
				(COMP (CAR (CDR E)) N (CONS (QUOTE 11) C))
		(IF (EQ (CAR E) (QUOTE ATOM))
				(COMP (CAR (CDR E)) N (CONS (QUOTE 12) C))
		(IF (EQ (CAR E) (QUOTE CONS))
				(COMP (CAR (CDR (CDR E))) N (COMP (CAR (CDR E)) N (CONS (QUOTE 13) C)))
		(IF (EQ (CAR E) (QUOTE IF))
				(LET (COMP (CAR (CDR E)) N (CONS (QUOTE 8)
																		(CONS THENPT (CONS ELSEPT C))))
					(THENPT COMP (CAR (CDR (CDR E))) N (QUOTE (9)))
					(ELSEPT COMP (CAR (CDR (CDR (CDR E)))) N (QUOTE	(9)))	)
		(IF (EQ (CAR E) (QUOTE LAMBDA)) 
				(LET (CONS (QUOTE 3) (CONS BODY C)) 
					(BODY COMP (CAR (CDR (CDR E))) (CONS (CAR (CDR E)) N)
																		(QUOTE (5))) )
		(IF (EQ (CAR E) (QUOTE LET)) 
				 (LET	(LET	(COMPLIS ARGS N (CONS (QUOTE 3)
														(CONS BODY (CONS (QUOTE 4)	C))))
									(BODY COMP (CAR (CDR E)) M (QUOTE (5))))
						(M CONS (VARS (CDR (CDR E)))	N)
						(ARGS EXPRS (CDR (CDR E))))
		(IF (EQ (CAR E) (QUOTE LETREC))
				 (LET	(LET	(CONS (QUOTE 6) (COMPLIS ARGS M
														(CONS (QUOTE 3) (CONS BODY (CONS (QUOTE 7) C))))) 
									(BODY COMP (CAR (CDR E)) M (QUOTE (5))))
						(M CONS (VARS (CDR (CDR E))) N) 
						(ARGS EXPRS (CDR (CDR E))))
		(COMPLIS (CDR E) N (COMP (CAR E) N (CONS (QUOTE 4) C)))))))))))))))))))))
	(COMPLIS LAMBDA (E N C)
		(IF (EQ E (QUOTE NIL)) (CONS (QUOTE 2) (CONS (QUOTE NIL) C))
				(COMPLIS (CDR E) N (COMP (CAR E) N (CONS (QUOTE 13) C)))))
	(LOCATION LAMBDA (E N)
		(LETREC
			(IF (MEMBER E (CAR N)) (CONS (QUOTE 0) (POSN E (CAR N)))
					(INCAR (LOCATION E (CDR N))))
		(MEMBER LAMBDA (E N)
					(IF (EQ N (QUOTE NIL)) (QUOTE F)
					(IF (EQ E (CAR N)) (QUOTE T) (MEMBER E (CDR N)))))
		(POSN LAMBDA (E N) 
			(IF (EQ E (CAR N)) (QUOTE 0) (ADD (QUOTE 1) (POSN E (CDR N))))) 
		(INCAR LAMBDA (L) (CONS (ADD (QUOTE 1) (CAR L)) (CDR L)))))
	(VARS LAMBDA (D)
		(IF (EQ D (QUOTE NIL)) (QUOTE NIL)
				(CONS (CAR (CAR D))	(VARS (CDR D)))))
	(EXPRS LAMBDA (D)
		(IF (EQ D (QUOTE NIL)) (QUOTE NIL)
				(CONS (CDR (CAR D)) (EXPRS (CDR D))))) 
)

It compiles to this machine representation:

(6 2 NIL 3 (1 (0.0) 2 NIL 14 8 (2 NIL 9) (2 NIL 1 (0.0) 11 13 1 (1.5) 4 1 (0.0) 10 11 13 9) 5) 13 3 (1 (0.0) 2 NIL 14 8 (2 NIL 9) (2 NIL 1 (0.0) 11 13 1 (1.4) 4 1 (0.0) 10 10 13 9) 5) 13 3 (6 2 NIL 3 (1 (0.0) 11 2 1 1 (0.0) 10 15 13 5) 13 3 (1 (0.0) 1 (0.1) 10 14 8 (2 0 9) (2 1 2 NIL 1 (0.1) 11 13 1 (0.0) 13 1 (1.1) 4 15 9) 5) 13 3 (1 (0.1) 2 NIL 14 8 (2 F 9) (1 (0.0) 1 (0.1) 10 14 8 (2 T 9) (2 NIL 1 (0.1) 11 13 1 (0.0) 13 1 (1.0) 4 9) 9) 5) 13 3 (2 NIL 1 (1.1) 10 13 1 (1.0) 13 1 (0.0) 4 8 (2 NIL 1 (1.1) 10 13 1 (1.0) 13 1 (0.1) 4 2 0 13 9) (2 NIL 2 NIL 1 (1.1) 11 13 1 (1.0) 13 1 (2.3) 4 13 1 (0.2) 4 9) 5) 7 5) 13 3 (1 (0.0) 2 NIL 14 8 (1 (0.2) 2 NIL 13 2 2 13 9) (2 NIL 2 NIL 1 (0.2) 2 13 13 13 1 (0.1) 13 1 (0.0) 10 13 1 (1.1) 4 13 1 (0.1) 13 1 (0.0) 11 13 1 (1.2) 4 9) 5) 13 3 (1 (0.0) 12 8 (1 (0.2) 2 NIL 1 (0.1) 13 1 (0.0) 13 1 (1.3) 4 13 2 1 13 9) (1 (0.0) 10 2 QUOTE 14 8 (1 (0.2) 1 (0.0) 11 10 13 2 2 13 9) (1 (0.0) 10 2 ADD 14 8 (2 NIL 2 NIL 1 (0.2) 2 15 13 13 1 (0.1) 13 1 (0.0) 11 11 10 13 1 (1.1) 4 13 1 (0.1) 13 1 (0.0) 11 10 13 1 (1.1) 4 9) (1 (0.0) 10 2 SUB 14 8 (2 NIL 2 NIL 1 (0.2) 2 16 13 13 1 (0.1) 13 1 (0.0) 11 11 10 13 1 (1.1) 4 13 1 (0.1) 13 1 (0.0) 11 10 13 1 (1.1) 4 9) (1 (0.0) 10 2 MUL 14 8 (2 NIL 2 NIL 1 (0.2) 2 17 13 13 1 (0.1) 13 1 (0.0) 11 11 10 13 1 (1.1) 4 13 1 (0.1) 13 1 (0.0) 11 10 13 1 (1.1) 4 9) (1 (0.0) 10 2 DIV 14 8 (2 NIL 2 NIL 1 (0.2) 2 18 13 13 1 (0.1) 13 1 (0.0) 11 11 10 13 1 (1.1) 4 13 1 (0.1) 13 1 (0.0) 11 10 13 1 (1.1) 4 9) (1 (0.0) 10 2 REM 14 8 (2 NIL 2 NIL 1 (0.2) 2 19 13 13 1 (0.1) 13 1 (0.0) 11 11 10 13 1 (1.1) 4 13 1 (0.1) 13 1 (0.0) 11 10 13 1 (1.1) 4 9) (1 (0.0) 10 2 LEQ 14 8 (2 NIL 2 NIL 1 (0.2) 2 20 13 13 1 (0.1) 13 1 (0.0) 11 11 10 13 1 (1.1) 4 13 1 (0.1) 13 1 (0.0) 11 10 13 1 (1.1) 4 9) (1 (0.0) 10 2 EQ 14 8 (2 NIL 2 NIL 1 (0.2) 2 14 13 13 1 (0.1) 13 1 (0.0) 11 11 10 13 1 (1.1) 4 13 1 (0.1) 13 1 (0.0) 11 10 13 1 (1.1) 4 9) (1 (0.0) 10 2 CAR 14 8 (2 NIL 1 (0.2) 2 10 13 13 1 (0.1) 13 1 (0.0) 11 10 13 1 (1.1) 4 9) (1 (0.0) 10 2 CDR 14 8 (2 NIL 1 (0.2) 2 11 13 13 1 (0.1) 13 1 (0.0) 11 10 13 1 (1.1) 4 9) (1 (0.0) 10 2 ATOM 14 8 (2 NIL 1 (0.2) 2 12 13 13 1 (0.1) 13 1 (0.0) 11 10 13 1 (1.1) 4 9) (1 (0.0) 10 2 CONS 14 8 (2 NIL 2 NIL 1 (0.2) 2 13 13 13 1 (0.1) 13 1 (0.0) 11 10 13 1 (1.1) 4 13 1 (0.1) 13 1 (0.0) 11 11 10 13 1 (1.1) 4 9) (1 (0.0) 10 2 IF 14 8 (2 NIL 2 NIL 2 (9) 13 1 (0.1) 13 1 (0.0) 11 11 11 10 13 1 (1.1) 4 13 2 NIL 2 (9) 13 1 (0.1) 13 1 (0.0) 11 11 10 13 1 (1.1) 4 13 3 (2 NIL 1 (1.2) 1 (0.1) 13 1 (0.0) 13 2 8 13 13 1 (1.1) 13 1 (1.0) 11 10 13 1 (2.1) 4 5) 4 9) (1 (0.0) 10 2 LAMBDA 14 8 (2 NIL 2 NIL 2 (5) 13 1 (0.1) 1 (0.0) 11 10 13 13 1 (0.0) 11 11 10 13 1 (1.1) 4 13 3 (1 (1.2) 1 (0.0) 13 2 3 13 5) 4 9) (1 (0.0) 10 2 LET 14 8 (2 NIL 2 NIL 1 (0.0) 11 11 13 1 (1.5) 4 13 1 (0.1) 2 NIL 1 (0.0) 11 11 13 1 (1.4) 4 13 13 3 (2 NIL 2 NIL 2 (5) 13 1 (0.0) 13 1 (1.0) 11 10 13 1 (2.1) 4 13 3 (2 NIL 1 (2.2) 2 4 13 1 (0.0) 13 2 3 13 13 1 (2.1) 13 1 (1.1) 13 1 (3.2) 4 5) 4 5) 4 9) (1 (0.0) 10 2 LETREC 14 8 (2 NIL 2 NIL 1 (0.0) 11 11 13 1 (1.5) 4 13 1 (0.1) 2 NIL 1 (0.0) 11 11 13 1 (1.4) 4 13 13 3 (2 NIL 2 NIL 2 (5) 13 1 (0.0) 13 1 (1.0) 11 10 13 1 (2.1) 4 13 3 (2 NIL 1 (2.2) 2 7 13 1 (0.0) 13 2 3 13 13 1 (1.0) 13 1 (1.1) 13 1 (3.2) 4 2 6 13 5) 4 5) 4 9) (2 NIL 2 NIL 1 (0.2) 2 4 13 13 1 (0.1) 13 1 (0.0) 10 13 1 (1.1) 4 13 1 (0.1) 13 1 (0.0) 11 13 1 (1.2) 4 9) 9) 9) 9) 9) 9) 9) 9) 9) 9) 9) 9) 9) 9) 9) 9) 9) 5) 13 3 (2 NIL 2 (4 21) 13 2 NIL 13 1 (0.0) 13 1 (1.1) 4 5) 13 3 (1 (0.0) 5) 7 4 21)

I can imagine it might be a viable target for some sort of archival system, the system definition is roughly napkit sized, the system I use on top of the SECD implementation is called Lispkit(purelisp) and it has an additional 10 opcodes, it looks like:

(LETREC main
	(main LAMBDA (INPUT)
		(loop (QUOTE 0) INPUT)
	)
	(loop LAMBDA (X Y)
		(IF (LEQ X Y)
			(loop (incr X) Y)
			(CONS X (CONS Y (QUOTE NIL))))
		)
	(incr LAMBDA (X)
		(ADD (QUOTE 1) X)
	)
)

It’s about 20 times as slow as Uxn, but it’s an interesting playground for anyone who’d like a well documented host system for portable functional programming. Its textual representation is interesting, even tho it’s ascii bytes, it does make for a small artifact size by not requiring padding for intergers and addresses for example. Anyways, I hope you find this interesting :slight_smile:

2 Likes

Hi @neauoire, I spent some time looking at SECD after your posts, but the tree nature of programs was a bit of a bummer to me. The biggest benefit of compiling a language like Lisp is so you end up with a compact array of bytecode. A tree of pointers doesn’t seem different enough from interpretation to be worth doing. Am I missing something?

So I’ve tried both, it’s quite easy to turn the output from a text string, to cells, I compiled the output to a 32-bit binary to try it out(where everything is padded to a 32-bit unsigned integer), and I realized two things:

  • The binary was larger.
  • The format specified an integer length and memory length which wasn’t a restriction before.
  • In terms of parsing, the parser was already present in the system, so it’s not removing any complexity to not use it, and runs only once during loading of a program, or textual input which is really quite fast and doesn’t occur during runtime.

I get the appeal of bytecode, my ideal system uses that and I’m quite satisfied, but were my needs different, this textual intermediate representation is quite useful. Also, this allows for multiple languages hosted on different systems with different limits to target it, so someone could write something in Haskell, and generate a “binary” that is compatible with that same system.

But, this system would fail almost all of Kragen’s requirements for a UVC, or personal archival system.

3 Likes

Thanks for posting this. I’m interested in minimalist Lisp implementations, and I’ve heard about SECD, but like Akkartik I’m not entirely sure of the benefit of adding bytecode and compilation over the top of CONS cells, which are already a pretty minimalist and general storage model. My favourite model so far is PicoLisp which yes, is an interpreter, but it seems pretty small and fast.

It seems possible that a Lisp wouldn’t need to be defined over lambdas but could be directly stack-based.

I’ve been wondering also. If we had a minimal Lisp which is strictly immutable, then we could both make the garbage collector very simple (as in SectorLisp’s ABC collector), and also all lists could be CDR-coded, halving storage and making it more competitive with Forth. (In space, if not in time.) Finally, if all lists were immutable, they’d be loop-free, and while that’s a restriction, it might be a very useful one because there’d be a one-to-one mapping between storage and serialization.

1 Like

SECD is a stack machine in which each data cell is immutable, sorry if that wasn’t clear from the original post.

1 Like

Right, so what I’m thinking about in terms of garbage collection is maybe orthogonal to the SECD design. SECD though seems to still be a stack machine heavily based on the Lisp lambda model, with functions that have parameters that have to be laboriously looked up in environments, which is probably why it’s 20x slower than UXN. One could imagine a much simpler stack machine more like UXN itself (or Joy, or Factor) where functions just directly manipulate the stack and only invoke environment-like structures when they absolutely need to. (Probably at “compile” time, ie at the time of creating a new closure). I probably need to build a working testbed to see if what I’m talking about would be useful at all. (It might lose a lot of security properties by allowing function calls to share a stack, for example).

The paper A Rational Deconstruction of Landin’s SECD Machine suggests a faster way of doing variable lookup, I’ve tried to implement it but it kicks my ass, I don’t think I fully understand how to handle clojures using the indexes alone.

2 Likes

Forty years ago, Peter Landin wrote a profoundly influencial article, “The Mechanical Evaluation of Expressions” [38], where, in retrospect, he outlined a
substantial part of the functional-programming research programme for the following decades. This visionary article stands out for advocating the use of the
λ-calculus as a meta-language and for introducing the first abstract machine
for the λ-calculus (i.e., in Landin’s terms, applicative expressions), the SECD
machine. However, and in addition, it also introduces the notions of ‘syntactic
sugar’ over a core programming language; of ‘closure’ to represent functional
values; of circularity to implement recursion; of thunks to delay computations;
of delayed evaluation; of partial evaluation; of disentangling nested applications
into where-expressions at preprocessing time; of what has since been called de
Bruijn indices; of sharing; of what has since been called graph reduction; of call
by need; of what has since been called strictness analysis; and of domain-specific
languages—all concepts that are ubiquitous in programming languages today.

Wow, I had no idea that one person came up with all those concepts in one paper! Especially that de Bruijn indices were not invented by de Bruijn!

So what I’m thinking is the SECD Stack is the Forth stack, C is (almost) the Forth PC, D is a slightly more general (and perhaps more restricted) Forth Return Stack, and Environment… is very specific to the Lispy lambda way of calling, and isn’t needed for combinators or Forthlike calls. Could we get by with a three-register “SCR” machine backed by immutable cons storage? This might in fact be a terrible idea on many levels; I’m not sure.

(An SCR machine would hold the top of heap on the stack, so as well as lots of quality-of-life problems because the stack is hard to use and in Forth everyone uses RAM to escape from it, if you erased your stack you’d probably lose your whole OS. Oops. Maybe not so great.)

1 Like