elsa
is a tiny language designed to build
intuition about how the Lambda Calculus, or
more generally, computation-by-substitution works.
Rather than the usual interpreter that grinds
lambda terms down to values, elsa
aims to be
a light-weight proof checker that determines
whether, under a given sequence of definitions,
a particular term reduces to to another.
You can try elsa
online at this link
You can locally build and run elsa
by
- Installing stack
- Cloning this repo
- Building
elsa
withstack
.
That is, to say
$ curl -sSL https://get.haskellstack.org/ | sh
$ git clone https://github.com/ucsd-progsys/elsa.git
$ cd elsa
$ stack install
elsa
programs look like:
-- id_0.lc
let id = \x -> x
let zero = \f x -> x
eval id_zero :
id zero
=d> (\x -> x) (\f x -> x) -- expand definitions
=a> (\z -> z) (\f x -> x) -- alpha rename
=b> (\f x -> x) -- beta reduce
=d> zero -- expand definitions
eval id_zero_tr :
id zero
=*> zero -- transitive reductions
When you run elsa
on the above, you should get the following output:
$ elsa ex1.lc
OK id_zero, id_zero_tr.
If instead you write a partial sequence of reductions, i.e. where the last term can still be further reduced:
-- succ_1_bad.lc
let one = \f x -> f x
let two = \f x -> f (f x)
let incr = \n f x -> f (n f x)
eval succ_one :
incr one
=d> (\n f x -> f (n f x)) (\f x -> f x)
=b> \f x -> f ((\f x -> f x) f x)
=b> \f x -> f ((\x -> f x) x)
Then elsa
will complain that
$ elsa ex2.lc
ex2.lc:11:7-30: succ_one can be further reduced
11 | =b> \f x -> f ((\x -> f x) x)
^^^^^^^^^^^^^^^^^^^^^^^^^
You can fix the error by completing the reduction
-- succ_1.lc
let one = \f x -> f x
let two = \f x -> f (f x)
let incr = \n f x -> f (n f x)
eval succ_one :
incr one
=d> (\n f x -> f (n f x)) (\f x -> f x)
=b> \f x -> f ((\f x -> f x) f x)
=b> \f x -> f ((\x -> f x) x)
=b> \f x -> f (f x) -- beta-reduce the above
=d> two -- optional
Similarly, elsa
rejects the following program,
-- id_0_bad.lc
let id = \x -> x
let zero = \f x -> x
eval id_zero :
id zero
=b> (\f x -> x)
=d> zero
with the error
$ elsa ex4.lc
ex4.lc:7:5-20: id_zero has an invalid beta-reduction
7 | =b> (\f x -> x)
^^^^^^^^^^^^^^^
You can fix the error by inserting the appropriate
intermediate term as shown in id_0.lc
above.
An elsa
program has the form
-- definitions
[let <id> = <term>]+
-- reductions
[<reduction>]*
where the basic elements are lambda-calulus term
s
<term> ::= <id>
\ <id>+ -> <term>
(<term> <term>)
and id
are lower-case identifiers
<id> ::= x, y, z, ...
A <reduction>
is a sequence of term
s chained together
with a <step>
<reduction> ::= eval <id> : <term> (<step> <term>)*
<step> ::= =a> -- alpha equivalence
=b> -- beta equivalence
=d> -- def equivalence
=*> -- trans equivalence
=~> -- normalizes to
A reduction
of the form t_1 s_1 t_2 s_2 ... t_n
is valid if
- Each
t_i s_i t_i+1
is valid, and t_n
is in normal form (i.e. cannot be further beta-reduced.)
Furthermore, a step
of the form
t =a> t'
is valid ift
andt'
are equivalent up to alpha-renaming,t =b> t'
is valid ift
beta-reduces tot'
in a single step,t =d> t'
is valid ift
andt'
are identical after let-expansion.t =*> t'
is valid ift
andt'
are in the reflexive, transitive closure of the union of the above three relations.t =~> t'
is valid ift
normalizes tot'
.