# 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
```

## 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: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.

## Syntax of `elsa`

Programs

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
```

## 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 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 =~> t'`

is valid if `t`

normalizes to `t'`

.