ELSA
elsa
is a tiny language designed to build
intuition about how the Lambda Calculus, or
more generally, computationbysubstitution works.
Rather than the usual interpreter that grinds
lambda terms down to values, elsa
aims to be
a lightweight proof checker that determines
whether, under a given sequence of definitions,
a particular term reduces to to another.
Online Demo
You can try elsa
online at this link
Install
You can locally build and run elsa
by
 Installing stack
 Cloning this repo
 Building
elsa
with stack
.
That is, to say
$ curl sSL https://get.haskellstack.org/  sh
$ git clone https://github.com/ucsdprogsys/elsa.git
$ cd elsa
$ stack install
Editor Plugins
Overview
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.
Partial Evaluation
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:730: 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)  betareduce 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:520: id_zero has an invalid betareduction
7  =b> (\f x > x)
^^^^^^^^^^^^^^^
You can fix the error by inserting the appropriate
intermediate term as shown in id_0.lc
above.
Syntax of elsa
Programs
An elsa
program has the form
 definitions
[let <id> = <term>]+
 reductions
[<reduction>]*
where the basic elements are lambdacalulus term
s
<term> ::= <id>
\ <id>+ > <term>
(<term> <term>)
and id
are lowercase 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
Semantics of elsa
programs
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 betareduced.)
Furthermore, a step
of the form
t =a> t'
is valid if t
and t'
are equivalent up to alpharenaming,
t =b> t'
is valid if t
betareduces to t'
in a single step,
t =d> t'
is valid if t
and t'
are identical after letexpansion.
t =*> t'
is valid if t
and t'
are in the reflexive, transitive closure
of the union of the above three relations.
t =~> t'
is valid if t
normalizes to t'
.
(Due to Michael Borkowski)
The difference between =*>
and =~>
is as follows.

t =*> t'
is any sequence of zero or more steps from t
to 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 t
reduces 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 elsa
would accept these three
eval ex1:
(\x y > x y) (\x > x) b
=*> b
eval 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 elsa
would 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.