Type theory and propositions as types

Se basa en

Requisitos previos obligatorios, hasta el fondo: 17

Aprenderás a

• Type-check terms of the simply typed λ-calculus and read them as proofs in intuitionistic propositional logic.
• Explain dependent function (Π) and dependent pair (Σ) types and use them to express ∀ and ∃.
• Define the natural numbers and lists as inductive types and derive their induction principles.
• Contrast a type-theoretic foundation, where every term has a type, with ZFC, where everything is a set and membership is global.

Definición

• A typing judgement t : A asserts that the term t has type A.
• Curry–Howard correspondence: propositions correspond to types and proofs to terms; implication corresponds to function types.
• An element of a dependent function type Π (x : A), B(x) sends each a : A to an element of B(a).
• An inductive type is freely generated by its constructors; for example ℕ is generated by zero and succ.

Teorema

• The simply typed λ-calculus is strongly normalising.
• Normalisation of proofs in intuitionistic natural deduction corresponds to β-reduction of typed λ-terms.
• Lean's logic is a dependent type theory in the tradition of the calculus of inductive constructions, with a hierarchy of universes; classical principles such as choice are added as explicit axioms.

Errores frecuentes

• Thinking type theory and set theory are interchangeable; they have different primitive notions and are related by interpretations, not identical.
• Treating types as sets: a term has its type as part of its meaning, whereas a set may belong to many unrelated sets.
• Assuming every program is a meaningful proof; in a consistent type theory, non-terminating terms are excluded.

Conduce a

Descubrimientos opcionales

• Proof theory Normalisation of typed λ-terms corresponds to removing detours in natural-deduction proofs, a central theme of proof theory.
• Formal methods Dependent types let programs carry machine-checked proofs of their own specifications.
• ← Propositional logic and truth tables
• ← Russell's paradox and why sets need axioms
• ← First steps in Lean
• ← Formalising mathematics in Lean and Mathlib
• ← ZFC: axiomatic set theory

Itinerarios de aprendizaje

• Computer science and formal methods

Lecturas complementarias

• Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, Theorem Proving in Lean 4
• Jean-Yves Girard, Yves Lafont and Paul Taylor, Proofs and Types (1989)
• Rob Nederpelt and Herman Geuvers, Type Theory and Formal Proof: An Introduction (2014)