Computability

Lambda Calculus and Computability

A Turing machine is not the only way to formalize computation. In the same year, 1936, Church proposed lambda calculus - a rewriting system with no state and no memory. Both approaches turned out to be equivalent, and this discovery reshaped the understanding of what computation fundamentally is.

**Haskell, ML, Lisp** - functional languages grew directly from lambda calculus
**Type systems** - System F and simply-typed lambda calculus underlie Haskell, Scala, Rust
**Proof assistants** (Coq, Agda) - use dependently-typed lambda calculus
**Compilers** - CPS and A-normal form are standard lambda expression transformations

Lambda Calculus: Syntax and Reductions

In 1936, Alonzo Church proposed a completely different answer to the question 'what does it mean to compute?' - not a machine with a tape, but a system of expression rewriting. No state, no memory cells - only functions and their application. Lambda calculus is built from three rules and fits on a single page.

Computation is reduction. Three kinds: **alpha** (variable renaming), **beta** (substituting an argument into the function body), and **eta** (eliminating redundant wrapping). Beta-reduction is the central one:

**Normal form** - an expression to which no beta-reduction can be applied. The omega combinator `(λx. x x)(λx. x x)` reduces to itself - the analog of an infinite loop. Not every lambda expression has a normal form.

What is the result of fully beta-reducing `(λx. λy. x) a b`?

The Church-Turing Thesis

In 1936, Church and Turing independently reached the same conclusion by different paths. Church formalized computability through lambda calculus. Turing - through tape machines. When they compared results, the classes of functions matched. This led to a hypothesis that cannot be proved formally.

The thesis says nothing about speed. A Turing machine may solve a problem in exponential time while a real computer solves it in linear time. Computability and computational complexity are separate questions.

The **physical Church-Turing thesis** is a stronger and more controversial claim: any physical process in the universe can be simulated by a Turing machine. Quantum computing does not refute it - quantum computers change complexity, but not the class of computable functions.

The Church-Turing thesis is a thesis (not a theorem) because:

Equivalence of Computational Models

Lambda calculus and Turing machines describe the same set of functions. The proof of equivalence requires a translation in both directions. Church numerals show how natural numbers and arithmetic arise from pure functions without any numeric primitives.

**Church numerals** are one of the most elegant constructions in computability theory: the numeral n is the function 'apply f exactly n times'. Arithmetic emerges from pure functional composition - without any special numeric primitives.

Church numeral `two = λf. λx. f(f(x))`. What does `two(λx. x+1)(0)` return?

Combinators S, K, I

Haskell Curry posed a provocative question in the 1920s: are variables needed at all? He showed that three basic combinators - S, K, I - suffice to express any lambda expression. This is combinatory logic: lambda calculus without variables.

**SKI calculus is Turing-complete** - from just two primitives S and K, any Turing-computable function can be expressed. This is the minimal universal computational basis. The esoteric languages Unlambda and Iota are built on this principle.

What does `K x y` return for any x and y?