ELSA
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.
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/ucsd-progsys/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.
Elsa supports several operators with optional normal form checking:
Basic Operators
=a> - alpha equivalence
=b> - single beta reduction
=e> - single eta reduction
=d> - definition expansion
=n> - normal order beta reduction
=p> - applicative order beta reduction
=*> - transitive closure of reductions
All operators can be extended with normal form checks:
=op:s> - check strong normal form after operation
=op:w> - check weak normal form after operation
=op:h> - check head normal form after operation
Examples:
-- nf_0.lc
let id = \z -> z
-- Check beta reduction to weak normal form
conf example1:
(\x y -> x (\w -> w w)) id
=b:w> (\y -> id (\w -> w w))
-- Check beta reduction to head normal form
conf example2:
((\x -> x) Z) (\x y -> x (\w -> w w)) id
=b:h> Z (\x y -> x (\w -> w w)) id
-- Normal order reduction to strong normal form
conf example3:
(\x y -> x) id
=n:s> \y -> id
Strategy-Specific Transitive Reductions
=n*> - normal order transitive reductions
=p*> - applicative order transitive reductions
Example:
-- sptr_0.lc
-- The numbers 0, 1, 3, 6 in church encoding
let c0 = \f x -> x
let c1 = \f x -> f x
let c3 = \f x -> f (f (f x))
let c6 = \f x -> f (f (f (f (f (f x)))))
-- Boolean functions
let true = \x y -> x
let false = \x y -> y
-- Number operations
let iszero = \n -> n (\x -> false) true
let pred = \n f x -> n (\g h -> h (g f)) (\u -> x) (\u -> u)
let mult = \m n f x -> m (n f) x
-- Fixed-point combinator and recursive function
let Y = \g -> (\x -> g (x x)) (\x -> g (x x))
let G = \f n -> iszero n c1 (mult n (f (pred n)))
let fact = Y G
eval factorial:
fact c3
-- The next line shows that we can show specific intermediate steps and leave out the rest
=n*> iszero c3 c1 (mult c3 (((\x -> G (x x)) (\x -> G (x x))) (pred c3)))
=n*> c6 --In this case, using =~> also works
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: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
Or you can change evaluation method, by changing
eval to conf (see also next section)
-- succ_1_alt.lc
let one = \f x -> f x
let two = \f x -> f (f x)
let incr = \n f x -> f (n f x)
conf 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)
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.
Confirmation Statements
The conf statement works like eval but
doesn't require the final term to be in normal
form. This is useful for infinite reductions
or intermediate proofs.
Example:
-- om_0.lc
let omega = (\x -> x x) (\x -> x x)
conf omega_reduces_to_self:
omega
=d> (\x -> x x) (\x -> x x)
=b> (\x -> x x) (\x -> x x)
=d> omega
Syntax of elsa Programs
An elsa program has the form
-- definitions and evaluations can be mixed
([let <id> = <term>] | [<reduction>])*
where the basic elements are lambda-calulus terms
<term> ::= <id>
\ <id>+ -> <term>
(<term> <term>)
and id are lower-case identifiers
<id> ::= x, y, z, ...
A <reduction> is a sequence of terms chained together
with a <step>
<reduction> ::= (eval | conf) <id> : <term> (<step> <term>)*
<step> ::= =, <equivtype>, [:, <nfcheck>], >
<equivtype> ::= a -- alpha equivalence
b -- beta equivalence
e -- eta equivalence
d -- def equivalence
* -- trans equivalence
n -- normal order beta equivalence
p -- applicative order beta equivalence
n* -- normal order trans beta equivalence
p* -- applicative order trans beta equivalence
~ -- normalizes to
<nfcheck> ::= s -- strong normal form check
w -- weak normal form check
h -- head normal form check
Semantics of elsa programs
An eval 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 if t and t' are equivalent up to alpha-renaming,
t =b> t' is valid if t beta-reduces to t' in a single step,
t =d> t' is valid if t and t' are identical after let-expansion.
t =*> t' is valid if t and t' are in the reflexive, transitive closure
of the union of the above three relations,
t =n> t' is valid if t beta-reduces using normal order to t' in
a single step,
t =p> t' is valid if t beta-reduces using applicative order to t'
in a single step,
t =n*> t' is valid if t and t' are in the reflexive, transitive closure
of the union of the =a>, =d> and =n> operator relations,
t =p*> t' is valid if t and t' are in the reflexive, transitive closure
of the union of the =a>, =d> and =p> operator relations,
t =~> t' is valid if t normalizes to t',
t =e> t' is valid if t eta-reduces to t' in a single step.
A conf reduction of the form t_1 s_1 t_2 s_2 ... t_n is similar to the
eval reduction of the same form, except that t_n does not have to be
in normal form.
Each reduction supports an optional nfcheck, which specifically checks
whether the operator is in the requested normal form, in addition to checking
the functionality of the operator. For example, t =b:w> t' not only checks
whether t can be reduced to t' in a single step, but also whether the
result is in weak normal form.
(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.