elsa alternatives and similar packages
Based on the "Language" category
* 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?
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.
You can try
elsa online at this link
You can locally build and run
- Installing stack
- Cloning this repo
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.
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)
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
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
elsa program has the form
-- definitions [let <id> = <term>]+ -- reductions [<reduction>]*
where the basic elements are lambda-calulus
<term> ::= <id> \ <id>+ -> <term> (<term> <term>)
id are lower-case identifiers
<id> ::= x, y, z, ...
<reduction> is a sequence of
terms chained together
<reduction> ::= eval <id> : <term> (<step> <term>)* <step> ::= =a> -- alpha equivalence =b> -- beta equivalence =d> -- def equivalence =*> -- trans equivalence =~> -- normalizes to
reduction of the form
t_1 s_1 t_2 s_2 ... t_n is valid if
t_i s_i t_i+1is valid, and
t_nis in normal form (i.e. cannot be further beta-reduced.)
step of the form
t =a> t'is valid if
t'are equivalent up to alpha-renaming,
t =b> t'is valid if
t'in a single step,
t =d> t'is valid if
t'are identical after let-expansion.
t =*> t'is valid if
t'are in the reflexive, transitive closure of the union of the above three relations.
t =~> t'is valid if
(Due to Michael Borkowski)
The difference between
=~> is as follows.
t =*> t'is any sequence of zero or more steps from
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'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.
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)
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.