elsa alternatives and similar packages
Based on the "Language" category

haskelltoolsastfromghc
Creating the HaskellTools AST from GHC's representations
* Code Quality Rankings and insights are calculated and provided by Lumnify.
They vary from L1 to L5 with "L5" being the highest. Visit our partner's website for more details.
Do you think we are missing an alternative of elsa or a related project?
Popular Comparisons
README
ELSA
elsa
is a tiny language designed to build
intuition about how the Lambda Calculus, or
more generally, computationbysubstitution works.
Rather than the usual interpreter that grinds
lambda terms down to values, elsa
aims to be
a lightweight 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
withstack
.
That is, to say
$ curl sSL https://get.haskellstack.org/  sh
$ git clone https://github.com/ucsdprogsys/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:730: 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)  betareduce 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:520: id_zero has an invalid betareduction
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 lambdacalulus term
s
<term> ::= <id>
\ <id>+ > <term>
(<term> <term>)
and id
are lowercase 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 betareduced.)
Furthermore, a step
of the form
t =a> t'
is valid ift
andt'
are equivalent up to alpharenaming,t =b> t'
is valid ift
betareduces tot'
in a single step,t =d> t'
is valid ift
andt'
are identical after letexpansion.t =*> t'
is valid ift
andt'
are in the reflexive, transitive closure of the union of the above three relations.t =~> t'
is valid ift
normalizes tot'
.
(Due to Michael Borkowski)
The difference between =*>
and =~>
is as follows.
t =*> t'
is any sequence of zero or more steps fromt
tot'
. 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 thatt
reduces tot'
in zero or more steps and thatt'
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.