Evaluate untyped λ-calculus

Choose a β‑reduction strategy, evaluate, and inspect the reduction steps.

How to use

Write a program with the following format:

  • any let bindings
  • one final expression to be evaluated

Then choose a beta-reduction strategy, optionally enable logging of beta reduction steps, and evaluate.

To understand more about the beta-reduction strategies, see the "About λ-Calculus" section.

A prelude with a few useful definitions (combinators, church numbers, etc) can be included.

When the prelude is included, user's definitions can overwritte prelude's when they share the same name.

Now, regarding lambda syntax: the lambda symbol can be written as either \ or λ as in λx.x or λx.x

Equational referencing

As already mentioned, it includes equational referencing, so instead of writing one big lambda expression, expressions can be "assigned" to names (as let id = λx.x) and reused anywhere.

Before evaluation, references will be replaced by their pure lambda expression representation.

PS: let definitions can not be recursive.
Thus let f = λx. f x is not allowed.

After evaluation, we also replace the final expression with a loaded reference if any is alpha-equivalent .

Possible confusion point: if prelude is included, the resultant expression can be something unexpected: a term defined in the prelude (such as zero which is λf.λx.x).

Final notes

  • Limited to 2^12 beta-reduction steps
  • Call-by-value (Weak, Strict) and Call-by-need (Weak, Lazy) to be implemented yet.
  • It does not feature eta-reductions.
  • It's not possible to indent code. Use multiple lines for big expressions or simplify with more let bindings.
About λ-calculus

Lambda calculus is a formal system for representing computation created by Alonzo Church in 1930s. If you think as a programming language, it's turing complete.

As a rewriting system, untyped lambda calculus is not strongly normalizing. Meaning that there are terms with no normal form such as: (λx.x x) (λx.x x)

Lambda calculus builds terms from three pieces: variables, abstractions, and applications.

A variable is a name like x.

An abstraction λx. t is an anonymous function that binds x in the body t.

And application t s means "apply t to s" (left-associative, so f a b means (f a) b).

β-reduction

A redex (reducible expression) is any application where the left side is an abstraction: (λx. t) s.

Now, β-reduction is the substitution step upon a redex: (λx. t) s -> t[x := s]

t[x := s] means: replace all occurrences of s for the free occurrences of x in t.

Free occurence refers to a variable that is not bound to any previous abstraction.

The replacement process includes something called capture-avoiding substitution. You may check out more about it in the "Learn more here" section's links.

Example:

(λx. x y) z -- a redex
-- one β-reduction
z y -- an application between two free variables

Normal Form

A term is in normal form when no beta-reduction applies, i.e. it has no subexpression of the form (λx. t) s, meaning it has no redexes.

For example, (λx. x) y -> y, and y is in normal form.

Weak Head Normal Form (WHNF)

A term is in WHNF when its head is not a beta-redex. Redexes may still appear inside arguments or inside lambda bodies.

Head: the leftmost term in a left-associative application chain.
Example: f a b means ((f a) b), so the head is f. 

-- WHNF:
λx. (λy. y) x
f ((λx. x) y)
x y z

-- Not WHNF (head redex):
(λx. x) y
((λx. x) y)
((λx. x) y) z

Reduction strategies

Reduction strategies differ in how they choose which redex to reduce first.

They can be strong or weak.

Strong: it reduces under lambdas. It can reach normal form if it terminates.

Weak: it does NOT reduce under lambdas. It's still possible to find the normal form if the expression doesn't require reducing under lambdas). Otherwise, the last weak reduction results in the Weak Head Normal Form (WHNF) of the expression

A few reduction strategies are: Normal Order, Applicative, Call-by-name, and Call-by-value.

Note: beta‑reduction is confluent (Church–Rosser), so if a term has a normal form, it is unique.
Any strategy that terminates reaches the same normal form.

Normal Order (Strong, Non-Strict):

It reduces first the leftmost outermost redex.

Arguments are substituted into the abstraction body before being reduced. 

let f = λa. a b c
let arg = (λx.x) y -- not in normal form, it can be reduced

f arg

-- ONE beta-reduction step outputs:

arg b c
-- or
((λx.x) y) b c

Normal Order reduction is normalizing, meaning it's guaranteed to reduce until normal form if one exists.

Applicative (Strong, Strict):

It reduces first the leftmost innermost redex.

Arguments are reduced first, and then substituted.

let f = λa. a b c
let arg = (λx.x) y -- not in normal form, it can be reduced

f arg

-- ONE beta-reduction step outputs:

f y
-- or
(λa. a b c) y
Applicative is not normalizing

Applicative does not guarantee reduction until normal form even if one exists. 

let const = λx. λy. x
let omega = (λx. x x) (λx. x x)

const ok omega

Normal order fully normalizes the expression as it does not try to reduce omega.

Applicative does not terminate because it tries to reduce omega first, getting stuck in infinite recursion.

Call-by-name (Weak, non-strict but it may recompute reductions)

It reduces only the leftmost outermost expression until it's a lambda, and then it applies the arguments without reducing them. 

let const = λx. λy. x
let arg = (λz. z) w

const arg

-- ONE beta-reduction step outputs:

λy. arg
-- or
λy. ((λz. z) w)

-- This stops at WHNF (a lambda), even though the body still has a redex.
-- Thus, for Call-by-Name, there are no more reductions be applied.
Call-by-value (Weak, strict)

It reduces the leftmost outermost redex only after first reducing the argument to a value. It does NOT reduce under lambdas as Call-by-Name. 

let f = λx. λy. (λz. z) y
let arg = (λu. u) (λv. v)

f arg

-- one step: call-by-value reduces the argument first
(λx. λy. (λz. z) y) (λv. v) -- or f (λv.v)
-- one step: then applies
λy. (λz. z) y -- WHNF
-- stops at WHNF (lambda head), even though the body still has a redex.

Learn more here:

Reduction strategy: