SECDR

The SECDR machine is an extension to the SECD machine. The SECD machine is an abstract machine that reduces a program in SECD code to its value. The programs that are to be compiled to SECD code are written in are source language that is commonly (but not necessarily) a functional one. The target language is the SECD language.

The letters S, E, C, D stand for stack, environment, code and dump and denote the registers of the machine. The initial machine state has the the code register set to the compiled code (or rather is pointing to the code), the other registers are initially empty. The program execution is the consecutive application of state transition rules until the code is completely consumed. At this final state the program value is to be found on the top of the stack.

A description of the program compilation, the SECD instruction set and the the rules of the program execution can be found here: http://webdocs.cs.ualberta.ca/~you/courses/325/Additional_LN/Lisp/SECD-slides.html. [1] has a more detailed description of the machine and its mode of operation.

[1] also describes some extensions to the source language like delayed evaluation and non-determinism (and its compilation and interpretation). The implementation of non-determinism is realized via the addition of a new register that keeps track of alternate program execution path. The new register is the R-register, hence the name of the SECDR machine. R stands for resumption since with its content the machine can resume the execution at the point where the last non-deterministic choice has been made.

An implementation in the Scheme programming language can be found here (a source code file secdr.scm).

After launching Scheme with the directory containing the file secdr.scm as the working directory, e.g. by issuing

• guile

• racket -I r5rs

• scheme # i.e. MIT-Scheme

• GAUCHE_LOAD_PATH=. gosh

• csi # chicken scheme interpreter

the source code is loaded by executing

(load "secdr.scm")

The Scheme code provides two functions compile and execute to 1.) compile source language programs (a rudimentary LISP variant, SEDR-Lisp henceforth) to SECDR code and 2.) to run the compiled code on the SECDR machine.

In addition there is a function test for self- and regression testing that is invoked by

(test)

The displayed messages should all indicate success.

For example let P the source language program ((LAMBDA (x) (PLUS x x)) 2). We can define it in the host language:

(define P '((LAMBDA (x) (PLUS x x)) 2))

Compiling P (via (compile P)) yields

(() LDC 2 CONS 2 LDF ((x) LD (0 . 0) LD (0 . 0) PLUS 2 RTN) AP ((LAMBDA (x) (PLUS x x)) 2))

The composition of compiling and executing the program, i.e. (execute (compile P)) gives the result

4

SECDR-Lisp provides the forms DELAY and FORCE for delayed evaluation, CHOICE and NONE for non-determinism (N.B. [1] uses OR instead of CHOICE). In addition it sports a BEGIN construct for sequencing and SETQ for (re)defining global variables and modifying local variables.

Non-deterministic programming

An example for non-deterministic function that inserts an item into a list without specifying the insertion position, e.g.

[insert (QUOTE D) (QUOTE (A B C))] (*)

Brackets [...] shall denote input to the SECDR machine. As a shorthand the following notation is introduced

(LAMBDA (x) ...) = λx. ..., (LAMBDA (x y) ...) =λx y. .., etc..

The non-deterministic insert function may be defined like

insert ≡ λx a .(IF (NULL a)

(CONS x NIL)

(CHOICE (CONS x a) (CONS (CAR a) (insert x (CDR a)))))

that yields for a list a with n elements a disjunction of n+1 CHOICEs. CHOICE is a function of two arguments, (CHOICE A B) picks either A or B.

SECDR-evaluation of (*) gives (D A B C). The functions all, take and choose are yielding resp. extracting further results of a multi-valued expression like (*):

(execute (compile '[all (insert (QUOTE D) (QUOTE (A B C)))])) ⟶ ((D A B C) (A D B C) (A B D C) (A B C D))

(execute (compile '[take 2 (insert (QUOTE D) (QUOTE (A B C)))])) ⟶ ((D A B C) (A D B C))

(execute (compile '[choose 2 (insert (QUOTE D) (QUOTE (A B C)))])) ⟶ (A B D C)

In the same manner as insert we might define a function σ (sigma stands for select) that picks a number between 1 and N

(execute (compile '[σ N])) yields a number in the range 1..N, e.g.

(execute (compile '[all (σ 10)])) ⟶ (1 2 3 4 5 6 7 8 9 10)

σ might be implemented like

σ ≡ λn . (IF (EQ n 1) 1 (CHOICE (σ(SUB n 1)) n))

A two-parameter variant of sigma denoted with σ₂ yields the integers within a specified range [σ₂ m n] ∈{m,...,n}.

A useful function that prepends a new element x to a list a if the element and the list are satifying some condition p is build:

build ≡ λx a p.(IF (p x a) (CONS x a) (NONE))

If the condition (p x a) is not met build will backtrack, i.e. returning to the last CHOICE and start over with another execution path. Such a condition is ∉ (not element of), e.g.

(∉ 1 (QUOTE (1 2 3))) = false, or (∉ 4 (QUOTE (1 2 3))) = true.

The argument p to build is a boolean function of two arguments p ≡ λx a . (...) like ∈ or ∉ where x is the candidate that must fulfill together with some list a a requirement in order to be added to the list a that is used to build up the result.

Permutation example: One obtains a permutation of the sequence of numbers 1..N by picking a number in the range (1...N) and add it to a sequence of numbers - provided it is not already included in this sequence - until the resulting sequence contains N elements.

permute ≡ λn a .(IF (EQ (length a) n)

a

(permute n (build (σ n) a ∉))

[permute n NIL] returns a permutation of length n from the the set {1,..,n}, e.g. we obtain all permutations from 1,2,3 with

(compile (execute '[all (permute 3 NIL)] )) ⟶ ((3 2 1) (2 3 1) (3 1 2) (1 3 2) (2 1 3) (1 2 3))

Taking the permute function as a template we may generate the solutions to problems that have other constraints than the ∉-predicate. The N-queens puzzle has as its solution the configuration of N queen chess pieces on a N×N chess board.

We reuse the above permute implementation and just replace "x is not a member of a" with "x does not attack any queen in a":

queens ≡ λn a .(IF (EQ (length a) n)

a

(queens n (build (σ n) a (λx q. NOT(attack-queen x q))))

where

attack-queen ≡ λx a .

(LETREC

((diagonal-attack λx a n.

(IF (NULL a)

F

(IF (OR (EQ (PLUS x n) (CAR a)) (EQ (SUB x n) (CAR a)))

T

(diagonal-attack x (CDR a) (PLUS n 1))))))

(IF (∈ x a) ; x contained in a = straight line attack

T

(diagonal-attack x a 1))); check both diagonals

All 92 solutions for the 8×8 board are obtained with the SECDR program [all (queens 8 NIL)]

The functions take and choose (resp. all) take an optional third (resp. second) argument, a boolean functions that in the same manner as the second argument of build (see above) controls wether a given element is added to the result list.

Ex.: construct the list L with all pairs (x . y) where x, y ∈ {1,2,..,N}and x·y < N and x, y being odd and (x.y) ∈ L implies (y.x) ∉ L. Code:

(all (CONS (σ N) (σ N)) λz a.(∧ (< (× (CAR z) (CDR z)) N) (ODD (CAR z)) (ODD (CDR z)) (∉ (flip z) a))

where ∧ denotes the logical conjunction and flip (x . y) ≡ (y . x).

Powerset example. The starting point is a function rem that non-deterministically removes one element from a list, e.g. the expression (rem '(1 2 3)) has as its values (2 3), (1 3) and (1 2). rem can be implemented as

rem ≡ λa .(IF (NULL (CDR a))

NIL

(CHOICE (CDR a) (CONS (CAR a) (rem (CDR a))))

The iteration operator iter for n-fold iterations on functions f:A→A, e.g. ((iter 2 λx.(CDR x)) '(a b c)) ⇒ (c), is defined as

iter ≡ λn f .(IF (= n 0) id λx.(f ((iter (SUB n 1) f) x)))

with id = λx.x as the identity function. Using exponentiation notation as a short-hand for n-fold iteration we might equate fⁿ ≡ (iter n f). So remⁱ is the function that removes i elements from a list, and the powerset of a set X with n elements can be computed as

powerset(X) = (all rem⁰X) ∪ (all rem¹X) ∪ ... ∪ (all remⁿX).

We code this equation into a powerset function using the two non-deterministic functions σ₂ and rem as

powerset ≡ λx .(all ((iter (σ₂ 0 |x|) rem) x) ∉)

where |x| denotes the absolute value for a number (or more generally the distance from the origin for vectors or complex numbers), |x| also denotes the cardinality of sets and the length of lists. The function ∉ as the second argument to all avoids double entries in the result — since for simplicity lists have been confounded for sets in the above section.

References

• [1] Henderson, Peter. 1980 Functional Programming: Application and Implementation. Prentice Hall.