Source-linked AI summary
Embedding Pure Type Systems in the lambda-Pi-calculus modulo
Denis Cousineau, Gilles Dowek
TL;DR
The paper asks whether the computation-rule extension λΠ-calculus modulo can express theories that are commonly represented by richer typing rules. It constructs embeddings of all functional Pure Type Systems into λΠ-calculus modulo and establishes soundness, termination preservation, confluence, and conditional conservativity results.
Problem
The paper addresses how to represent Pure Type Systems and their proofs using the λΠ-calculus modulo rather than additional typing rules.
Method
It defines an appropriate rewrite system, called the universe-reduction rules, and translates Pure Type System contexts, terms, and types into λΠ-calculus modulo.
Results
All functional Pure Type Systems embed in λΠ-calculus modulo; the embedding preserves typing, reflects reduction termination, and yields confluence.
Takeaways & Limitations
The λΠ-calculus modulo is sufficiently expressive to encode functional Pure Type Systems using computation rules instead of their additional typing rules.
Takeaways & Limitations
Conservativity is established for weak η-long normal terms, while unrestricted conservativity fails in general, including cases involving polymorphic identity and universe terms.
Abstract
from arXiv · showhide
The lambda-Pi-calculus allows to express proofs of minimal predicate logic. It can be extended, in a very simple way, by adding computation rules. This leads to the lambda-Pi-calculus modulo. We show in this paper that this simple extension is surprisingly expressive and, in particular, that all functional Pure Type Systems, such as the system F, or the Calculus of Constructions, can be embedded in it. And, moreover, that this embedding is conservative under termination hypothesis.
1 The λΠ-calculus
The λΠ-calculus is a dependently typed lambda-calculus with dependent products, abstractions, conversion, and separate Type and Kind sorts. Its reduction properties support proof representation and metatheoretic results for minimal predicate logic.
- Dependent types: Dependent products let types and function results depend on terms, such as arrays indexed by natural numbers.An application substitutes the argument for the bound variable in the dependent result type.
- Syntax and typing: The calculus includes terms, Type, Kind, dependent products, abstractions, and applications, with α-equivalence and β-reduction defined as usual.The typing rules include product formation, abstraction, and conversion modulo β-equivalence.
- Syntax and typing: Type-family abstraction and conversion allow a functionally computed type, such as array (2 × n), to type the corresponding term.These extensions add abstraction and conversion rules involving terms whose types may be Kind.
- Metatheory: Types are preserved by β-reduction, β-reduction is confluent and strongly terminating, and each term has a unique type modulo β-equivalence.These properties provide the calculus’s principal metatheoretic guarantees.
- Proof representation: Minimal predicate-logic formulas and proofs translate into terms and typed terms in the λΠ-calculus.Strong termination yields cut elimination, and atomic conclusions have no proofs when they lack cut-free proofs.
2 The λΠ-calculus modulo
The λΠ-calculus modulo extends the λΠ-calculus by replacing β-conversion with conversion generated by β-reduction and a well-typed rewrite system. This internalizes theory-specific computation while preserving typing under rewriting.
- Motivation: Theory axioms can be replaced by rewrite rules, avoiding open proof terms whose termination benefits may be lost in the Logical Framework.This is the Deduction modulo route to expressing theories in the λΠ-calculus.
- Rewrite systems: A rewrite rule consists of β-normal left and right terms, a context, and a type, and it must be well-typed in the surrounding context.Typed substitutions preserve the common type of the rewritten terms.
- Rewrite systems: The congruence generated by a rewrite system identifies terms connected by rewriting and is combined with β-equivalence.The congruence is the smallest one containing each rewrite step.
- Definition: The λΠ-calculus modulo replaces β-conversion in the conversion rules with conversion generated by β and rewrite rules.The resulting relation is written ≡βR.
- Examples: The calculus can extend even the λΠ−-calculus with rewrite-based conversion; for example, rewriting P to Q ⇒ Q types a function from P.The example uses the rule P −→ (Q ⇒ Q).
3 The Pure Type Systems
Pure Type Systems specify sorts, axioms, and product and abstraction rules, providing a common framework for systems such as the λΠ-calculus, Calculus of Constructions, F, and Fω. Functional systems retain strong structural properties needed for comparison with λΠ-calculus modulo.
- Definition: A Pure Type System is defined by sorts, axioms between sorts, and rules assigning a sort to products and abstractions.Its typing rules include product formation, abstraction, and conversion.
- Examples: The λΠ-calculus and Calculus of Constructions arise by adding different sort rules to the same basic sorts and axiom.The Calculus of Constructions includes the additional Kind-based rules.
- Examples: The simply typed λ-calculus is the system with sorts Type and Kind, axiom ⟨Type, Kind⟩, and rule ⟨Type, Type, Type⟩.This provides the base example in the schematic presentation of Pure Type Systems.
- Metatheory: Functional Pure Type Systems include systems such as the λΠ-calculus, Calculus of Constructions, F, and Fω, where uniqueness of types holds.β-reduction terminates in these listed systems, while termination is not asserted for all Pure Type Systems.
4 Embedding functional Pure Type Systems in the λΠ-calculus modulo
The paper embeds every functional Pure Type System into the λΠ-calculus modulo by encoding sorts and dependent products with universes, decoding functions, and rewrite rules. The translation is sound, preserves β-reduction, and supports termination and confluence results for the target system.
- Embedding construction: Functional Pure Type Systems can be embedded in the λΠ-calculus modulo using an appropriate rewrite system.The construction is motivated by Deduction modulo and Tarski-style universes.
- Embedding construction: Each sort s is represented by a universe Us together with a decoding function εs that turns universe elements into types.The universe-reduction rules define how encoded products decode to dependent products.
- Translation: The translation maps variables and sorts directly, encodes dependent products through ˙Π constructors, and translates abstractions and applications homomorphically.The product translation records the source and target sorts used by the corresponding rewrite rules.
- Soundness: The translation preserves substitution and maps every β-reduction in the source system to a β-reduction in the λΠ-calculus modulo.These properties are established by induction on terms and by observing that translated β-redexes remain β-redexes.
- Soundness: If Γ ⊢t : B in a functional Pure Type System, then the translated judgment ∥Γ∥⊢|t| : ∥B∥ holds in λΠP.This is the stated soundness proposition for the embedding.
- Termination: Source reduction sequences translate to target reduction sequences, so termination of a well-typed term in the Pure Type System implies termination of its translation.The proof combines soundness with preservation of β-reduction.
- Confluence: Parallel reduction is strongly confluent, its reflexive-transitive closure matches ordinary reduction, and ordinary reduction in λΠP is confluent.The confluence proof uses parallel reduction and the canonical parallel reduct M†.
5 Conservativity
The paper establishes conservativity of the embedding for functional Pure Type Systems, first for weak η-long normal terms and then, under termination, for closed inhabitants. It also identifies why unrestricted conservativity fails and how back translation supports the proof.
- Scope and obstruction: Unrestricted conservativity fails: translated typability in λΠP does not generally guarantee an exactly corresponding term in P.The paper gives counterexamples, including polymorphic identity in the simply-typed lambda calculus and a rule constructor that is typable but is not itself a translation.
- Back translation: The proof introduces a back translation from λΠP to P that erases encoding constructs and maps translated terms back to their P counterparts.The translation is defined recursively over products, abstractions, encoded products, universe operators, and applications.
- Back translation: The back translation is a right inverse of the forward translations, so translating a term and back-translating it recovers the original term.This right-inverse property is established structurally and is used to relate typing and conversion across the two systems.
- Proof correspondence: Back translation preserves the relevant reduction and conversion structure, while translated Pure Type System terms retain β-equivalence relationships.The propositions establish preservation for β-reduction, collapse of rewrite steps under back translation, and correspondence of equivalence judgments.
- Conservativity proof: For weak η-long normal terms, every inhabitant of a translated type can be back-translated to a term inhabiting the original Pure Type System type.The induction analyzes products, abstractions, applications, variables, and encoded Pure Type System constructors; weak η-long form ensures encoded products occur η-expanded.
- Conservativity theorem: If λΠP is terminating, the embedding is conservative for closed inhabitation: ∥A∥ has a closed inhabitant in λΠP exactly when A has one in P.Termination reduces an arbitrary closed inhabitant to weak η-long normal form, after which the conservativity proposition applies.