# lambda #### A toy interpreter and compiler of the untyped λ calculus, written in common lisp. 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 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 (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. ## Try it! Requirements - Common Lisp REPL (SBCL and CCL tested) with Quicklisp installed Clone this repository to a directory where Quicklisp can find it, for example in `quicklisp/local-projects/` or in whatever `(:tree ...)` you have in `~/.config/common-lisp/repos.conf`. In your Common Lisp REPL evaluate: ``` (ql:quickload "lambda") (in-package :lambda.ui) (main) ``` You'll be prompted: ``` Input which UI to use: 3 for the transformation viewer 2 for the church REPL 1 for the base REPL 0 to exit Anything else will return help instructions. ``` The UI help instructions include the BNF of the standard syntax of this λ calculus, and a short description of each menu options. Each UI mode starts with help instructions specific to the UI mode, examples of usage, and the set of self encoded primitives, such as `:ID :TRUE :FALSE :S :AND :OR :IF :Y :OMEGA`, which you can use when entering a λ term. #### Examples of λ terms, without and with primitives, and of reductions. Note that only single variable abstractions are allowed. Without primitives: ``` d (x y) (λ a (λ b (a b)) ``` With primitives: ``` ((:or :true) a) (((:if :false) a ) b) ``` 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 (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. - 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))`. + 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. - Lazy, normal order, and applicative order reducers, with respective steppers and self-evaluation loop catchers. - A λ calculus interpreter in common-lisp and a compiler to common lisp lambda abstractions. - Compiler transformations and simplifications are currently only β-reducing in normal order with loop-catching and maximum allowed steps, closing possibly open terms, full renaming of bound variables, then switching to common-lisp syntax and returning the resulting common-lisp closure. For the base of this implementation I just followed Barendrecht and Barendsen's 1994 book "Introduction to Lambda Calculus" [BarBar84]. TBA representations come with respective papers (see references below), which I am currently implementing. #### Tested 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]. Extensive manually written tests are performed as well. 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 I used the principle of literal programming, with comments in plain text format. The beginning of each file should be informative of the file contents. # TODO Immediate TODO goals, in my priority order, starting from highest priority. - 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) - Compile to my computer's assembly (with the help of disassembly). - 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 In several places in documentation and in comments, I refer to the following publications, in LaTeX bibtex-style alpha. - [Bar84] **The Lambda Calculus: Its Syntax and Semantics**, H.P. Barendregt, *Elsevier (1984)* - [BarBar84] **Introduction to lambda calculus**, H.P. Barendregt and E.Barendsen, *Nieuw archief voor wisenkunde 4, 337-372 (1984)* - [Tro18] **Functional Bits : Lambda Calculus based Algorithmic Information Theory**, J. Tromp, * (2018)* - [Mog94] **Efficient Self-Interpretation in Lambda Calculus**, T. Mogensen, *Journal of Functional Programming 2, (1994)*