Lambda Calculus & Type Theory

Functions all the way down → types as proofs

1:00

How three syntactic forms — variable, abstraction, application — define a Turing-complete model of computation, and how adding types turns programs into proofs.

By the end, you can

Name the three syntactic forms of lambda calculus and give an example of each.
Perform beta reduction by substituting an argument into a function body.
Explain alpha conversion and distinguish free variables from bound variables.
Define what it means for a term to be in normal form.
Encode the Church booleans TRUE and FALSE as functions and trace an IF expression by reduction.
Encode small Church numerals and evaluate one by supplying a concrete function and starting value.
State the Church-Turing thesis and explain what Turing completeness means for lambda calculus.
Explain what the Y combinator does and why the Z combinator is needed in strict languages.
Describe why Omega has no normal form and what this illustrates about the halting problem.
State the typing rules for abstraction and application in simply-typed lambda calculus.
Explain the trade-off: simply-typed lambda calculus guarantees termination but is not Turing complete.
Build a simple type derivation tree and interpret it as a logical proof.
Articulate the Curry-Howard correspondence with at least three matched pairs.
Describe what Hindley-Milner inference achieves and why it is remarkable.
Explain what dependent types add and name at least two languages that use them.

Up next in Advanced Algorithms, Math & PL Theory