Commit 518a5185 authored by Ioanna M. Dimitriou H.'s avatar Ioanna M. Dimitriou H. 💬

Completed Tromp's SKI-calculus and its binary format:

implementation and tests added.
Added the two new representations to the UI viewer.
All tests pass.
parent c1a6a3d2
......@@ -4,11 +4,12 @@
A toy compiler of the untyped lambda calculus into common lisp (so far), written in common lisp, with an interpreter and a user interface (UI).
The UI includes two REPLs and a viewer of all available transformations of a user-input λ term.
The UI includes a viewer of all available transformations of a user-input λ term, as well as two simple REPLs.
The viewer can also evaluate terms before listing their different representations, and therefore is the recommended part of the UI (Church arithmetic support TBA).
##### Goal
The goal of this project is to compile the untyped λ calculus and extensions thereof into several targets, such as a stack machine, and some assembly languages.
The goal of this project is to compile the untyped λ calculus and extensions thereof into several targets, such as a stack machine (WebAssembly in mind), and some assembly languages.
For learning and understanding compilers, therefore I write most of it by hand. Written in common lisp because I am most comfortable with this language.
......@@ -63,19 +64,21 @@ With primitives:
In the UI's "base REPL", the above evaluate to `:true` and `b`, respectively.
## Implementation features
- A User Interface (UI) in the package `:lambda.ui` (call `(main)`) using self-encoded primitives, which include:
+ Two Read Eval Print Loops (REPLs) for this λ calculus:
* `λ.base` allows you to use the following symbols as primitives: `:ID :TRUE :FALSE :S :AND :OR :IF :Y :OMEGA`
- A User Interface (UI) in the package `:lambda.ui` (call `(main)`) using self-encoded primitives (encoded as λ terms).
The UI includes:
+ A transformation viewer: Input a λ TERM and see its available representations (see next list item). Evaluate the TERM before returning the different representations with =:eval TERM=. In the TERM you can use the same primitives as the `λ.base` REPL below.
+ Two simple Read Eval Print Loops (REPLs) for this λ calculus:
* `λ.base` allows you to use the following symbols as self-encoded primitives: `:ID :TRUE :FALSE :S :AND :OR :IF :Y :OMEGA`
* `λ.church` allows you to use base, as well as numbers in your statements, and the following symbols as primitives for numeric functions:
`:A+ :A* :Aexp :Azero? :A+1 :A-1 :A-factorial`, for plus, times, exponent, zero test, successor, predecessor, and factorial.
+ A transformation viewer: Input a λ term and see its available representations (see next list item).
- Showcases representations of lambda terms in my quest to understand compilers.
So far, showcased representations of lambda terms are the following.
+ The standard, single variable binding, parenthesised lambda terms as quoted common-lisp lists, for example, `'(^ x (x y))`.
+ De Bruijn representation (locally nameless for open terms), the example becomes `'(^ (0 y))`.
+ A common lisp representation, the example becomes `'(lambda (x) (funcall x y))`.
+ TBA: Implementation of Tromp's
* combinatorial logic representation in the form of SKI-calculus (towards a stack machine),
+ An implementation of Tromp's
* combinatorial logic representation in the form of SKI-calculus (towards a stack machine - WebAssembly),
* and his binary representation.
+ TBA: Implementation of Mogensen's continuation passing style self encoding of lambda calculus (Mogensen-Scott encoding).
+ I provide transformations between defined representations.
......@@ -90,9 +93,9 @@ In the UI's "base REPL", the above evaluate to `:true` and `b`, respectively.
By adding a catch-loop stepper-based reducer of the standard representation, I have been able to use cl-quickcheck on arbitrary generated terms, and
quickcheck also examples, theorems, and lemmas from [BarBar84].
Run the quickcheck tests by evaluating `(lambda.quickcheck:run-quickcheck)`.
Extensive manually written tests are performed as well.
Extensive manually written tests are performed as well by evaluating: `(lambda.test:test-all)`
Run all tests for CCL and SBCL by loading `run-all-tests.lisp`, or for a particular common lisp implementation from the command line for example as `ccl -b -l run-all-tests.lisp`.
#### Documented
......@@ -102,14 +105,14 @@ I used the principle of literal programming, with comments in plain text format.
# TODO
Immediate TODO goals, in my priority order, starting from highest priority.
- Implement Tromp's Combinatorial Logic representation in the form of SKI-calculus (towards a stack machine), from his 2018 paper [Tro18].
- Implement Tromp's cross interpreter for SKI-terms.
- Add transformation of SKI-calculus terms to WebAssembly.
- Implement more encodings or/and replace them with primitives of a target language (e.g. WebAssembly).
- Find a nicer way around printing keywords with their dots (print related functions in ui.lisp are messy!)
- Implement UI for steppers.
- Find a faster encoding for natural numbers or integers, or/and get common lisp (or other target languages, such as the above mentioned stack machine)
- Implement Tromp's binary format for closed terms, again from [Tro18].
- Compile to my computer's assembly (with the help of disassembly).
- Implement more encodings or/and replace them with primitives of a target language.
- Unify the 3 UI "modes" into one big REPL. Low priority because it's probably not helping in the main goals of this project.
- Unify the 3 UI "modes" into one big REPL. Low priority because it's probably not that relevant to the main goals of this project.
# References
......
......@@ -12,10 +12,19 @@
(:file "syntax-de-bruijn"
:depends-on ("packages"
"syntax-standard"))
(:file "syntax-ski"
:depends-on ("packages"
"syntax-standard"))
(:file "transformations-ski"
:depends-on ("packages"
"syntax-standard"
"syntax-ski"))
(:file "transformations"
:depends-on ("packages"
"syntax-standard"
"syntax-de-bruijn"))
"syntax-de-bruijn"
"syntax-ski"
"transformations-ski"))
(:file "renames"
:depends-on ("packages"
"syntax-standard"))
......@@ -82,11 +91,17 @@
"test/helpers"
"syntax-standard"
"syntax-de-bruijn"))
(:file "test/syntax-ski"
:depends-on ("packages"
"syntax-ski"
"test/helpers"))
(:file "test/transformations"
:depends-on ("packages"
"test/helpers"
"syntax-standard"
"syntax-de-bruijn"
"syntax-ski"
"transformations-ski"
"transformations"))
(:file "test/renames"
:depends-on ("packages"
......@@ -135,6 +150,7 @@
:depends-on ("packages"
"test/syntax-standard"
"test/syntax-de-bruijn"
"test/syntax-ski"
"test/transformations"
"test/renames"
"test/equality"
......@@ -161,7 +177,9 @@
"test/quickcheck/generators"))
(:file "test/quickcheck/transformations"
:depends-on ("packages"
"syntax-standard"
"syntax-de-bruijn"
"transformations-ski"
"transformations"
"test/quickcheck/helpers"))
(:file "test/quickcheck/renames-equality"
......
......@@ -25,12 +25,24 @@
#:db-term-p
#:db-free-variables))
(defpackage :lambda.syntax-ski
(:use #:cl
#:lambda.syntax-standard)
(:export #:ski-term-p
#:ski-free-variables
#:ski-combinator-p))
(defpackage :lambda.transformations
(:use #:cl
#:lambda.syntax-standard
#:lambda.syntax-de-bruijn)
#:lambda.syntax-de-bruijn
#:lambda.syntax-ski)
(:export #:standard->de-bruijn
#:standard->common-lisp))
#:standard->common-lisp
#:standard->ski
#:ski->standard
#:ski->binary-ski
#:binary-ski->ski))
(defpackage :lambda.renames
(:use #:cl
......@@ -131,12 +143,32 @@
#:lambda.interpreter)
(:export #:^compile))
;; A package with everything as a playground
(defpackage :lambda
(:use #:cl
#:lambda.syntax-standard
#:lambda.syntax-de-bruijn
#:lambda.syntax-ski
#:lambda.transformations
#:lambda.renames
#:lambda.equality
#:lambda.substitution
#:lambda.reducers
#:lambda.encodings
#:lambda.decodings
#:lambda.interpreter
#:lambda.ui
#:lambda.compiler))
;;; Test packages
(defpackage :lambda.test
(:use #:cl
#:lambda.syntax-standard
#:lambda.syntax-de-bruijn
#:lambda.syntax-ski
#:lambda.transformations
#:lambda.renames
#:lambda.equality
......
;;;;syntax-ski.lisp
(in-package :lambda.syntax-ski)
;;; Combinatorial Logic a.k.a. SKI-calculus
;;; and binary combinatorial logic
;; Here I define some basic functions for transforming ski-calculus terms to
;; and from λ calculus, and ski-calculus terms to and from binary ski-calculus.
;; I use the SKI-calculus presentation of [Section 3; Tro18]:
;; "
;; Combinatory Logic (CL) is the equational theory of combinators—terms built
;; up, using application only, from the two constants K and S,
;; [...]
;; I is considered a shorthand for S K K.
;; "
;;
;; I shall denote the combinators by :S, :K, and :I.
;;
;; SKI-calculus can be seen as a subset of λ calculus, which contains the
;; λ terms which do not contain any ^abstractions. Therefore the syntax-standard
;; predicates ^variable, ^application-p can also be used with SKI-calculus
;; terms.
;; Note that ^variable has a different meaning in SKI-calculus as it does in
;; λ calculus, because :SKI-calculus has two (three) primitives: :S,:K, and
;; in some cases :I. I will not need a more specialised SKI-calculus predicate.
;;; other SKI-calculus predicates
(defun ski-term-p (term)
(or (^variable-p term)
(and (^application-p term)
(ski-term-p (first term))
(ski-term-p (second term)))))
;; It seems more efficient to define a new function 'ski-free-variables than to
;; reuse ^free-variables from :lambda.syntax-standard.
(defun ski-free-variables (ski-term)
"Free variables in SKI-calculus are ^variables which are not :S, :K, or :I."
(assert (ski-term-p ski-term))
(labels ((collector (ski-term)
(if (^variable-p ski-term)
(list ski-term)
(append (collector (first ski-term))
(collector (second ski-term))))))
(remove-duplicates
(remove-if (lambda (var) (member var '(:S :K :I)))
(collector ski-term)))))
(defun ski-combinator-p (ski-term)
"Includes a (SKI-TERM-P SKI-TERM) check in SKI-FREE-VARIABLES."
(null (ski-free-variables ski-term)))
......@@ -17,6 +17,7 @@
(test-syntax-standard terms :verbosep verbosep)
(test-syntax-de-bruijn :verbosep verbosep)
(test-syntax-ski :verbosep verbosep)
(test-transformations terms :verbosep verbosep)
(test-renames :verbosep verbosep)
(test-equality :verbosep verbosep)
......
......@@ -15,5 +15,41 @@
;; standard->common-lisp is checked in test/quickcheck/compiler.lisp
;;; Tests involving ski-calculus transformations
;; What can cause a difference between a reduced closed term, and its translated
;; to and from a ski term, is λ²'s rule 4, which replaces '(λ a (b a)) with 'b.
;; This holds because the first form is just a so called lambda-wrapper around
;; 'b, which is eventually going to be a closed term.
(defun lambda-unwrap (term)
(do-abstractions term
(lambda (var body)
(if (and (^application-p body)
(eq var (second body))
(not (member var (^free-variables (first body)))))
(lambda-unwrap (first body))
`(λ ,var ,(lambda-unwrap body))))
'lambda-unwrap))
(defun check-standard->ski->standard (term)
(let ((closed (^closure term)))
(is ^eq
(lambda-unwrap (^reduce-normal closed))
(lambda-unwrap (^reduce-normal (ski->standard
(standard->ski closed)))))))
(defun check-ski->binary-ski->ski (term)
(let* ((closed (^closure term))
(ski (standard->ski closed)))
(is equal
ski
(binary-ski->ski
(ski->binary-ski ski)))))
(defun check-transformations (term free)
(check-standard->de-bruijn term free))
(check-standard->de-bruijn term free)
(check-standard->ski->standard term)
(check-ski->binary-ski->ski term))
;;;;test/syntax-ski.lisp
(in-package :lambda.test)
(defun test-ski-term-p ()
(assert (ski-term-p '((:S x) ((:K :K) :I))))
(assert (ski-term-p ':S))
(assert (not (ski-term-p '())))
(assert (not (ski-term-p '(a b c)))))
(defun test-ski-free-variables ()
(flet ((assert-has-free (ski-term free)
(assert (set-equal (ski-free-variables ski-term)
free))))
(assert-has-free '(((:S x) :K) (:I (y x))) '(x y))
(assert-has-free '((((((:S :I) :K) :S) :K) :I) x) '(x))
(assert-has-free :S nil)
(assert-has-free 'x '(x)))
(handler-case (ski-free-variables '())
(error (error)
(declare (ignore error)))
(:no-error ()
(error "SKI-FREE-VARIABLES not throwing error for empty list argument."))))
(defun test-ski-combinator-p ()
(assert (ski-combinator-p
'(((:S :S) :I) (:K (:I :S)))))
(assert (ski-combinator-p
:I)))
(defun test-syntax-ski (&key verbosep)
(test-ski-term-p)
(test-ski-free-variables)
(test-ski-combinator-p)
(when verbosep
(format *standard-output* "~&SYNTAX-SKI tests passed.~%")))
......@@ -26,11 +26,70 @@
(mapcar 'test-standard->de-bruijn
(mapcar 'car terms-bruijns))))
;;;; SKI-calculus
;;; Functions in transformations-ski.lisp
;; λ² is tested by its results in standard->ski
(defun test-standard->ski->standard (term)
(assert (lambda.transformations::ski-term-p
(standard->ski term)))
(assert (^term-p (ski->standard (standard->ski term))))
(assert (^eq (^reduce-normal term)
(^reduce-normal
(ski->standard
(standard->ski term))))))
(defun test-Tromp-Y-dash-dash-claim ()
(let ((Y-- '((λ x (λ y ((x y) x))) (λ y (λ x (y ((x y) x))))))
(ski-Y-- '(((:S :S) :K) ((:S (:K ((:S :S) (:S ((:S :S) :K))))) :K))))
(assert (equal (standard->ski Y--)
ski-Y--))))
;; tests for the binary representation
(defun test-ski->binary-ski->ski (term)
(let* ((closed (^closure term))
(ski (standard->ski closed)))
(assert (equal ski
(binary-ski->ski
(ski->binary-ski ski))))))
(defun test-ski-Tromp-binary-claim ()
"From [page 8; Tro18], with :S and :K switched."
(assert (equal (ski->binary-ski '(:K ((:S :K) :K)))
'(1 0 1 1 1 0 0 0 1 0 1))))
(defun test-ski-Tromp-binary-size-claims ()
"Taken from [Section 3.2; Tro18]."
(let ((y '(λ f ((λ x (x x)) (λ x (f (x x))))))
(y- '((λ z (z z)) (λ z (λ f (f ((z z) f))))))
(y-- '((λ x (λ y ((x y) x))) (λ y (λ x (y ((x y) x))))))
(omega '((λ x (x x)) (λ x (x x)))))
(assert (= 65 (lambda.transformations::binary-ski-size
(standard->ski y))))
(assert (= 59 (lambda.transformations::binary-ski-size
(standard->ski y-))))
(assert (= 35 (lambda.transformations::binary-ski-size
(standard->ski y--))))
(assert (= 41 (lambda.transformations::binary-ski-size
(standard->ski omega))))))
(defun test-all-transformations-ski (terms)
"All tests related to ski transformations"
(mapcar 'test-standard->ski->standard terms)
(test-Tromp-Y-dash-dash-claim)
(mapcar 'test-ski->binary-ski->ski terms)
(test-ski-Tromp-binary-claim)
(test-ski-Tromp-binary-size-claims))
;;; All transformations.lisp tests
(defun test-transformations (terms &key verbosep)
(mapcar 'test-standard->de-bruijn terms)
(test-de-bruijn-transformations)
(test-all-transformations-ski terms)
(when verbosep
(format *standard-output* "~&TRANSFORMATIONS tests passed.~%")))
......
;;;;transformations-ski.lisp
(in-package :lambda.transformations)
;;; Tromp's compact bracket abstraction "λ²" from [Section 3.2; Tro18]
;; I define each rule separately and add documentation from Tromp's paper.
;; Note that Tromp is using left associativity of application. I do not use
;; this syntactic sugar, to keep my functions simpler. In the documentation
;; strings, I added the "missing" parens.
;; I use the variable SKI where a ski-term should go.
(defun λ²-rule-1 (var ski)
"λ² x. ((S K) M) ≡ (S K), (for all M)
Exploits the fact that S K M behaves as identity."
(when (and (listp ski)
(equal '(:S :K)
(first ski)))
'(:S :K)))
(defun λ²-rule-2 (var ski)
"λ² x. M ≡ K M, (x not in M)
Standard bracket abstraction rule."
(when (not (member var (ski-free-variables ski)))
`(:K ,ski)))
(defun λ²-rule-3 (var ski)
"λ² x. x ≡ I
Standard bracket abstraction rule."
(when (eq var ski)
:I))
(defun λ²-rule-4 (var ski)
"λ² x. (M x) ≡ M, (x not in M)
This holds because the first form is just a so called lambda-wrapper around 'b,
which is eventually going to be itself a λ-abstraction."
(when (and (listp ski)
(eq var (second ski))
(not (member var (ski-free-variables (first ski)))))
(first ski)))
(defun λ²-rule-5 (var ski)
"λ² x. ((x M) x) ≡ λ² x. ((((S S) K) x) M)
Avoids introduction of two Is."
(when (and (listp ski)
(listp (first ski))
(eq var (first (first ski)))
(eq var (second ski)))
(let ((M (second (first ski))))
(λ² var `((((:S :S) :K) ,var) ,M)))))
(defun λ²-rule-6 (var ski)
"λ² x. (M (N L)) ≡ λ² x. (((S (λ² x. M)) N) L), (M, N combinators)
Prevents occurrences of x in L from becoming too deeply nested."
(when (and (listp ski)
(listp (second ski))
(ski-combinator-p (first ski))
(ski-combinator-p (first (second ski))))
(destructuring-bind (M (N L)) ski
(λ² var `(((:S ,(λ² var M)) ,N) ,L)))))
(defun λ²-rule-7 (var ski)
"λ² x. ((M N) L) ≡ λ² x. (((S M) (λ 2 x. L)) N), (M, L combinators)
Prevents occurrences of x in N from becoming too deeply nested."
(when (and (listp ski)
(listp (first ski))
(ski-combinator-p (first (first ski)))
(ski-combinator-p (second ski)))
(destructuring-bind ((M N) L) ski
(λ² var `(((:S ,M) ,(λ² var L)) ,N)))))
(defun λ²-rule-8 (var ski)
"λ² x. ((M L) (N L)) ≡ λ² x. (((S M) N) L), (M, N combinators)
Abstracts an entire expression L to avoid duplication."
(when (and (listp ski)
(listp (first ski))
(listp (second ski))
(equal (second (first ski))
(second (second ski)))
(ski-combinator-p (first (first ski)))
(ski-combinator-p (first (second ski))))
(destructuring-bind ((M L) (N L%)) ski
(λ² var `(((:S ,M) ,N) ,L)))))
(defun λ²-rule-9 (var ski)
"λ² x. (M N) ≡ ((S (λ² x. M)) (λ² x. N))"
(when (listp ski)
`((:S ,(λ² var (first ski))) ,(λ² var (second ski)))))
(defun λ² (var ski)
"Compact bracket abstraction from [Section 3.2; Tro18]."
(or (λ²-rule-1 var ski)
(λ²-rule-2 var ski)
(λ²-rule-3 var ski)
(λ²-rule-4 var ski)
(λ²-rule-5 var ski)
(λ²-rule-6 var ski)
(λ²-rule-7 var ski)
(λ²-rule-8 var ski)
(λ²-rule-9 var ski)))
;; Debugging helpers
(defun trace-λ²-rules ()
(trace λ²-rule-1 λ²-rule-2 λ²-rule-3 λ²-rule-4 λ²-rule-5 λ²-rule-6 λ²-rule-7
λ²-rule-8 λ²-rule-9))
(defun untrace-λ²-rules ()
(untrace λ²-rule-1 λ²-rule-2 λ²-rule-3 λ²-rule-4 λ²-rule-5 λ²-rule-6 λ²-rule-7
λ²-rule-8 λ²-rule-9))
;;; Binary ski-calculus
;; From [Section 3.1; Tro18].
;; Here I denote terms in the binary ski-calculus representation with the
;; variable BINARY.
(defun ski->binary-ski (ski-combinator)
"This is only defined for closed ski-terms, that is, ski-combinators"
(assert (ski-combinator-p ski-combinator))
(cond ((eq :S ski-combinator)
'(0 0))
((eq :K ski-combinator)
'(0 1))
((eq :I ski-combinator)
(ski->binary-ski '((:S :K) :K)))
((^application-p ski-combinator)
(append '(1)
(ski->binary-ski (first ski-combinator))
(ski->binary-ski (second ski-combinator))))))
(defun get-next-code (binary) ;=> '(code rest)
(when binary
(cond ((and (= 0 (first binary))
(= 0 (second binary)))
(list :S (subseq binary 2)))
((= 0 (first binary))
(list :K (subseq binary 2)))
;; application
((= 1 (first binary))
(destructuring-bind (operation rest-1)
(get-next-code (rest binary))
(destructuring-bind (operand rest-2)
(get-next-code rest-1)
(list (list operation operand)
rest-2)))))))
(defun add-I (ski)
"Replaces the subterm '((:S :K) :K) with :I."
(do-subterms ski
'add-I
(lambda (subterm)
(if (equal subterm '((:S :K) :K))
:I
subterm))))
(defun binary-ski->ski (binary)
(destructuring-bind (code rest)
(get-next-code binary)
(if rest
(error "This binary string does not represent a ski term: ~a
~&partial code: ~a~%unparsed rest: ~a.~%"
binary code rest)
(add-I code))))
(defun binary-ski-size (ski)
(length (ski->binary-ski ski)))
......@@ -7,11 +7,13 @@
;; So far implemented:
;; - standard->de-bruijn
;; - standard->common-lisp
;; - standard->ski
;; - ski->standard
;; - ski->binary-ski
;; - binary-ski->ski
;;
;; TODO:
;; - de-bruijn->standard
;; - standard->SKI
;; - SKI->standard
;; - standard->mogensen-scott
;; - mogensen-scott->standard
;; - standard->binary
......@@ -94,3 +96,26 @@ double recursion it might be fed either objects of λ term structure or of de
;; TODO (defun common-lisp->standard (expression) )
;; Well. At least some subset of common lisp. ^^
;;; ski-calculus, or combinatory logic
;; see also transformations-ski.lisp
;; :K ≡ '(λ x (λ y x))
;; :S ≡ '(λ x (λ y (λ z ((x z) (y z)))))
;; as seen later in encodings.lisp
(defun standard->ski (term)
(do-abstractions term
(lambda (var body) (λ² var (standard->ski body)))
'standard->ski))
(defun ski->standard (ski)
(let ((S '(λ x (λ y (λ z ((x z) (y z))))))
(K '(λ x (λ y x)))
(I '(λ x x)))
(flet ((remove-skis (term)
(cond ((eq term :S) S)
((eq term :K) K)
((eq term :I) I)
(T term))))
(do-subterms ski #'ski->standard #'remove-skis))))
......@@ -205,20 +205,18 @@ church terms."
* standard-syntax with primitives: ~a
* standard-syntax without primitives: ~(~a~)
* de Bruijn representation: ~(~a~)
* Common Lisp representation: ~(~a~)~%~%"
* Common Lisp representation: ~(~a~)
* Combinatorial Logic (SKI-calculus): ~(~a~)
* Tromp's binary SKI-calculus: ~(~a~)~%~%"
(pretty-print
(decode-encodings-in-term term (reverse *base-encodings*))
:stream nil)
term
(standard->de-bruijn term)
(standard->common-lisp term)))
(defun action-transformations-viewer (validated)
(print-term
(destructuring-bind (evalp term) validated
(if evalp
(^eval-normal term *base-encodings*)
(^substitute-environment term *base-encodings*)))))
(standard->common-lisp term)
(standard->ski term)
(ski->binary-ski (standard->ski term))))
(defun transformation-viewer (stream)
(help-transformation-viewer stream)
......