Skip to content

Latest commit

 

History

History
26 lines (19 loc) · 1.3 KB

README.md

File metadata and controls

26 lines (19 loc) · 1.3 KB

Cactus Environment Machine

We implement call by need using shared environments, targeting GNU as and ld on x64 Linux. No libc dependencies to run the resulting programs, which do nothing but leak memory and print a lambda term if they terminate succesfully.

For a description of the approach, the functional pearl document is in paper/

For the implementation, see code/. The compiled program cem takes a file that should be a closed lambda term, and produces an executable prog, which when run will print the term of the resulting closure (if there is one) in lambda calculus with deBruijn indices. For example, the program λt.t will print λ0.

There is one discrepancy between the paper and the code. The paper uses Barendregt syntax, but the implementation uses a more lispy syntax, where every sequences of applications is wrapped in parentheses. We also create a simple let rule, which is compiled to pure lambda terms, where { is the standard let and } is the usual in. See the code/examples/ for examples of the syntax, but formally:

t ::= λx.t | (t .. t t) | x | { x = t y = t ... z = t } t

So instead of (λx.a x) λy.y, we would write (λx.(a x) λy.y). Parentheses are used to define applications, not to disambiguate. This has the nice property that when a term ends is unambiguous.