λ-Calculus Interpreter

An interactive web interface for lambda calculus expressions

λ TRUE FALSE AND OR NOT ZERO ONE TWO THREE PLUS MULT

Predefined Variables

Define a Variable

What is Lambda Calculus?

Lambda calculus is a formal system in mathematical logic for expressing computation based on function abstraction and application. It was introduced by Alonzo Church in the 1930s as part of his research into the foundations of mathematics.

Despite its simplicity, lambda calculus is Turing-complete, meaning it can express any computation that a Turing machine can perform.

Lambda Calculus Syntax

  • Variables: Single letters like x, y, z that represent values or functions
  • Abstractions (λx.M): Functions with a parameter x and body M
  • Applications (M N): Applying function M to argument N
  • Parentheses: Used for explicit grouping of expressions

Note: You can type abstractions using either the lambda symbol (λ) or backslash (\). For example: λx.x or \x.x

Redex and β-reduction

A term of the form (λx.M) N is called a β-redex. The act of evaluating lambda calculus terms is called β-reduction, which replaces (λx.M) N with M[N/x] (substituting N for x in M).

A term without β-redexes is said to be in β-normal form.

Evaluation Strategies

  • β-reduction: Perform a single beta-reduction step
  • Normal Order: Reduce leftmost, outermost redex first (favored by Church-Rosser theorem)
  • Call-by-value: Evaluate arguments before applying functions (used in most programming languages)

Church Encodings

Church encodings are ways to represent data and operations using only lambda expressions:

Booleans

  • TRUE: λx.λy.x
  • FALSE: λx.λy.y
  • AND: λp.λq.p q p
  • OR: λp.λq.p p q
  • NOT: λp.λa.λb.p b a

Church Numerals

  • ZERO: λf.λx.x
  • ONE: λf.λx.f x
  • TWO: λf.λx.f (f x)
  • THREE: λf.λx.f (f (f x))

Arithmetic Operations

  • SUCC: λn.λf.λx.f (n f x)
  • PLUS: λm.λn.λf.λx.m f (n f x)
  • MULT: λm.λn.λf.m (n f)
  • POW: λm.λn.n m

Using this Application

  • Input: Type lambda expressions in the input field
  • Evaluation: Choose your evaluation strategy (β-reduction, Normal Order, or Call-by-value)
  • Variables: Define your own variables in the Variables tab
  • Dark Mode: Toggle between light and dark themes with the moon/sun button

Example Expressions

  • Identity function: λx.x
  • Application to a variable: (λx.x) y
  • Constant function: λx.λy.x
  • Boolean AND: (AND TRUE FALSE)
  • Addition: (PLUS TWO THREE)
  • Y combinator: λf.(λx.f (x x)) (λx.f (x x))