Untyped

An untyped lambda calculus parser, evaluator, and REPL, written in Haskell.

Build & Run

The REPL can be invoked with either docker or stack.

docker

Build

docker build -t lambda-calculus .

Launch REPL

docker run -it lambda-calculus

stack

Build

stack build

Launch REPL

stack exec lambda-calculus-exe

REPL Commands

• let
• ?
• βnf
• trace
• η-equivalance
• fv

let bindings

Syntax

let {var} = {expr}

Examples

λ> let q = λx.x
q := λx.x

λ> let y = (λxyz.xz(yz))(λx.z)(λx.a)
y := (λx.λy.λz.xz(yz))(λx.z)(λx.a)

Show context

Syntax

?

Examples

λ> ?
y := (λx.λy.λz.xz(yz))(λx.z)(λx.a)
q := λx.x

Evaluate to β-normal-form

Syntax

! {expr}

Examples

λ> ! (λxyz.xz(yz))(λx.z)(λx.a)
λw.za

λ> let y = (λxyz.xz(yz))(λx.z)(λx.a)
λ> ! y
λw.za

Trace β-normal-form evaluation

Syntax

trace {expr}

Examples

λ> trace (λxyz.xz(yz))(λx.z)(λx.a)
Γ, a, z, (λx.λy.λz.xz(yz))(λx.z)(λx.a)
--------------------------------------
(λx.λy.λz.xz(yz))(λx.z)(λx.a)
-----------------------------
(λy.λw.(λx.z)w(yw))(λx.a)
-------------------------
λw.(λx.z)w((λx.a)w)
-------------------
λw.z((λx.a)w)
-------------
λw.za

η-equivalance

(evaluate to β-normal-form and check α-equivalence)

Syntax

= {expr} {expr}

Examples

λ> let z = λx.x
λ> let y = λq.q
λ> = z y
True
  via α?.β
    λx.x
    λq.q

λ> let z = (λz.z)(λz.zz)(λz.zy)
λ> let w = (λx.λy.xyy)(λy.y)y
λ> = z w
True
  via α?.β
    yy
    yy

Free Variables

Syntax

fv {expr}

Examples

λ> fv (λxyz.xz(yz))(λx.z)(λx.a)
{a,z}