Need help with elsa?
Click the “chat” button below for chat support from the developer who created it, or find similar developers for support.

About the developer

ucsd-progsys
134 Stars 9 Forks MIT License 57 Commits 2 Opened issues

Description

Elsa is a lambda calculus evaluator

Services available

!
?

Need anything else?

Contributors list

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

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  = ]+

-- reductions []*

where the basic elements are lambda-calulus

term
s
 ::=  
          \ + -> 
            ( )

and

id
are lower-case identifiers
   ::= x, y, z, ...

A

 is a sequence of 
term
s chained together with a

 ::= eval  :  ( )*

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

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

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.