Elsa is a lambda calculus evaluator
elsais 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,
elsaaims 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
elsaonline at this link
You can locally build and run
elsaby
elsawith
stack.
That is, to say
$ curl -sSL https://get.haskellstack.org/ | sh $ git clone https://github.com/ucsd-progsys/elsa.git $ cd elsa $ stack install
elsaprograms look like:
-- id_0.lc let id = \x -> x let zero = \f x -> xeval 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
elsaon the above, you should get the following output:
$ elsa ex1.lcOK 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
elsawill complain that
$ elsa ex2.lcex2.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,
elsarejects the following program,
-- id_0_bad.lc let id = \x -> x let zero = \f x -> xeval id_zero : id zero =b> (\f x -> x) =d> zero
with the error
$ elsa ex4.lcex4.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.lcabove.
elsaPrograms
An
elsaprogram has the form
-- definitions [let = ]+-- reductions []*
where the basic elements are lambda-calulus
terms
::= \ + -> ( )
and
idare lower-case identifiers
::= x, y, z, ...
A
is a sequence ofterms chained together with a
::= eval : ( )*::= =a> -- alpha equivalence =b> -- beta equivalence =d> -- def equivalence =*> -- trans equivalence =~> -- normalizes to
elsaprograms
A
reductionof the form
t_1 s_1 t_2 s_2 ... t_nis valid if
t_i s_i t_i+1is valid, and
t_nis in normal form (i.e. cannot be further beta-reduced.)
Furthermore, a
stepof the form
t =a> t'is valid if
tand
t'are equivalent up to alpha-renaming,
t =b> t'is valid if
tbeta-reduces to
t'in a single step,
t =d> t'is valid if
tand
t'are identical after let-expansion.
t =*> t'is valid if
tand
t'are in the reflexive, transitive closure of the union of the above three relations.
t =~> t'is valid if
tnormalizes to
t'.
(Due to Michael Borkowski)
The difference between
=*>and
=~>is as follows.
t =*> t'is any sequence of zero or more steps from
tto
t'. So if you are working forwards from the start, backwards from the end, or a combination of both, you could use
=*>as a quick check to see if you're on the right track.
t =~> t'says that
treduces to
t'in zero or more steps and that
t'is in normal form (i.e.
t'cannot be reduced further). This means you can only place it as the final step.
So
elsawould accept these three
eval ex1: (\x y -> x y) (\x -> x) b =*> beval ex2: (\x y -> x y) (\x -> x) b =~> b
eval ex3: (\x y -> x y) (\x -> x) (\z -> z) =*> (\x -> x) (\z -> z) =b> (\z -> z)
but
elsawould not accept
eval ex3: (\x y -> x y) (\x -> x) (\z -> z) =~> (\x -> x) (\z -> z) =b> (\z -> z)
because the right hand side of
=~>can still be reduced further.