Master Lambda Calculus: Syntax, Reductions, and the Y Combinator Explained

Introduction

Lambda calculus is a formal system derived from mathematical logic that studies function abstraction, application, and recursion using variable binding and substitution rules. It was first published by Alonzo Church in the 1930s and serves as a universal model of computation equivalent to a single‑tape Turing machine.

Syntax Rules

Variable : x – a name representing a value.

Function (abstraction) : λx.x – defines a function with parameter x and body x.

Application : M N – applies function M to argument N.

Free and Bound Variables

In λx.xy, x is a bound variable while y is free.

Reduction Rules

α‑Conversion

Renames bound variables to avoid name clashes (e.g., λx.x ≡ λy.y).

λx.x ≡ λy.y

// js
(x => x) === (y => y)

β‑Reduction

Replaces a function’s parameter with the actual argument, effectively performing a function call.

(λx.x)y ≡ y
(λx.x y)(a(b)) ≡ a b y

// js
(x => x)(y) === y
(x => x)(a(b)) === a(b)

Complex expressions can be reduced in any order because all functions are pure.

η‑Conversion

Eliminates redundant abstractions: if λx.M x does not use x inside M, it can be simplified to M.

let fn  = (a) => ((b) => 'foo'))(a)
let fn2 = () => 'foo'

fn(1) // 'foo'
fn2() // 'foo'

Avoiding Ambiguity

Expressions like λx.x y can be parsed as (λx.x) y or λx.(x y). Two conventions are used:

The function body extends as far to the right as possible, so λx.x y means λx.(x y).

Application is left‑associative: X Y Z means (X Y) Z, not X (Y Z).

Currying

Since lambda calculus functions take a single argument, multi‑argument functions are expressed by nesting abstractions. For example, addition can be written as:

λa.λb.PLUS a b
// js
const fn = a => b => PLUS(a, b)

Conditional Branching

Booleans are encoded as functions: TRUE = λx y.x, FALSE = λx y.y. An IF construct can be defined as IF = λc t f.c t f, and logical operators as:

AND = λx y.x y FALSE
OR  = λx y.x TRUE y
NOT = λx.x FALSE TRUE

Church Numerals

Natural numbers are represented using the successor function S. Zero and successors are defined as:

ZERO = λs z.z
ONE  = λs z.s(z)
TWO  = λs z.s(s(z))
THREE = λs z.s(s(s(z)))

In JavaScript these correspond to:

let ZERO = (s, z) => z
let ONE  = (s, z) => s(z)
let TWO  = (s, z) => s(s(z))
let THREE= (s, z) => s(s(s(z)))

Addition

PLUS = λx y s z.x s (y s z)
// js
const PLUS = (x, y) => (s, z) => x(s, y(s, z))

// example
let FIVE = PLUS(TWO, THREE)
convert(FIVE) // 5

Multiplication

MULTIPLY = λx y s.x (y s)
// js
const MULTIPLY = (x, y) => s => x(y(s))

let SIX = MULTIPLY(TWO, THREE)
convert(SIX) // 6

Loops and Recursion

All loops can be expressed via recursion. In lambda calculus, recursion is achieved with the Y combinator, which computes a fixed point of a higher‑order function, allowing an anonymous function to refer to itself.

Fixed‑Point Combinator

The Y combinator is defined as λf.λx.(f (x x)) (λx.f (x x)). In JavaScript it can be written as:

function Y(f) {
  return (function (x) {
    return f(x(x));
  })(function (x) {
    return f(x(x));
  });
}

// arrow‑function version
const Y = f => (x => f(x(x)))(x => f(x(x)));

Using Y, a factorial function can be defined without naming itself:

const factorial = Y(f => n => n === 1 ? 1 : n * f(n - 1));
factorial(5); // 120

References

λ演算(Lambda Calculus)入门基础（一）：定义与归约

阿隆佐·丘奇的天才之作——lambda演算中的数字

Church encoding – Wikipedia

Lambda Calculus – Learn X in Y minutes

You Can Explain Functional Programming Using Emojis

Y‑Combinator推导的Golang描述

Fixed Point Combinator – Wikipedia