# elsa

A tiny language for understanding the lambda-calculus http://github.com/ucsd-progsys/elsa

Latest on Hackage: | 0.2.0.1 |

This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow stackage.org to host generated Haddocks.

**Ranjit Jhala**

**jhala@cs.ucsd.edu**

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

.