elsa: A tiny language for understanding the lambda-calculus

[ language, library, mit, program ] [ Propose Tags ]

elsa is a small proof checker for verifying sequences of reductions of lambda-calculus terms. The goal is to help students build up intuition about lambda-terms, alpha-equivalence, beta-reduction, and in general, the notion of computation by substitution.

[Skip to Readme]
Versions [RSS] [faq],,,,,,
Dependencies array, base (==4.*), dequeue, directory, elsa, filepath, hashable, json, megaparsec, mtl, unordered-containers [details]
License MIT
Author Ranjit Jhala
Maintainer jhala@cs.ucsd.edu
Category Language
Home page http://github.com/ucsd-progsys/elsa
Source repo head: git clone https://github.com/ucsd-progsys/elsa/
Uploaded by ranjitjhala at 2019-03-31T04:34:43Z
Distributions NixOS:
Executables elsa
Downloads 3707 total (43 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs available [build log]
Last success reported on 2019-03-31 [all 1 reports]


[Index] [Quick Jump]


Maintainer's Corner

For package maintainers and hackage trustees


Readme for elsa-

[back to package description]


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


You can locally build and run elsa by

  1. Installing stack
  2. Cloning this repo
  3. 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


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

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 <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'.