# Lambda Calculus: an Elm CLI

## A Lambda Calculator

`\$ lambdaWelcome! type :help for help> (\x.x) (\y.y)λy.y`
`> :let id = \x.xadded id as λx.x> id idλx.x`
`# Standard Libary# Booleanstrue      \x.\y.xfalse     \x.\y.yand       \p.\q.p q por        \p.\q.p p qnot       \p.p (false) true# Church numeralszero      \s.\z.zone       \s.\z.s ztwo       \s.\z.s s zthree     \s.\z.s s s zisZero    \n.n (\x.zero) truesucc      \n.\f.\x.f(n f x)`
`> and true trueλx.λy.x> and true falseλx.λy.y> and false falseλx.λy.y`

## Implementing the Calculator in Elm

`type Expr    = Var String    | Lambda String Expr    | Apply Expr Expr`
`> :parse xOk (Var "x")> :parse \x.xOk (Lambda "x" (Var "x"))> :parse (\x.x) \y.yOk (Apply (Lambda "x" (Var "x")) (Lambda "y" (Var "y")))`
`(\p.\q.p q p) (\x.\y.x) (\x.\y.y)`

# Addenda

## Output options

`> and true falsefalse> :pretty> and true falseλx.λy.y> :raw> and true false\x.\y.y> :named> and true falsefalse`

## :beta command

`> :beta (succ zero) onetrue`
`> :beta (\x.x) (\a.a)true`
`> OmegaTOO MANY SUBSTITUTIONS (size2 > 100000). Term may be divergent> :beta Omega OmegaLHS may be divergent`

--

--

## More from James Carlson

jxxcarlson on elm slack, http://jxxcarlson.github.io