(\{\                                                  \\
    { { \ ,~,                                              \\
   { {   \)))  *                                            \\
    { {  (((  /                                             /\\
     {/{/; ,\/                                             // \\
        (( '                                              //   \\
         \` \                                            //     \\
         (/  \                                          //       \\
 ejm     `)  `\                                        //         \\

Lambda Shell

GithubDocumentation

A simple REPL shell for untyped lambda expressions. It provides provides named terms, reduction strategies and capture-avoiding substitution and extends lambda calculus by macros and directives.

Examples

There are builtin terms SUCC and NIL to create natural numbers using church numerals:

[λ] @usestd
@usestd

[λ] one := SUCC NIL
one := SUCC NIL

[λ] two := SUCC (SUCC NIL)
two := SUCC (SUCC NIL)

[λ] !normalize (ADD one two)
\f . \x . f (f (f x))

You can select different reduction strategies at runtime:

[λ] @usestd
@usestd

[λ] !vnormalize (AND TRUE FALSE)
AND TRUE FALSE
(\q . TRUE q TRUE) FALSE
(\q . (\y . q) TRUE) FALSE
(\q . q) FALSE
FALSE

[λ] @set strategy normal
@set strategy normal

[λ] !vnormalize (AND TRUE FALSE)
AND TRUE FALSE
(\q . TRUE q TRUE) FALSE
TRUE FALSE TRUE
(\y . FALSE) TRUE
FALSE