Skip to content

stelleg/cem_pearl

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

25 Commits
 
 
 
 
 
 

Repository files navigation

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.

About

Cactus environment machine

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published