Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Bidirectional Interpolation for the Lambda-Calculus -- Revisiting and Formalising Craig-Čubrić Interpolation

Meven Lennon Bertrand, Alexis Saurin

TL;DR

A new proof of Craig's Interpolation theorem is given by building on principles of bidirectional typing, and formalise it in Rocq.

Abstract

Craig's Interpolation theorem has a wide range of applications, from mathematical logic to computer science. Proof-theoretic techniques for establishing interpolation usually follow a method first introduced by Maehara for the Sequent Calculus and then adapted by Prawitz to Natural Deduction. The result can be strengthened to a proof-relevant version, taking proof terms into account: this was first established by Čubrić in the simply-typed lambda-calculus with sums and more recently in linear, classical and intuitionistic sequent calculi. We give a new proof of Čubrić's proof-relevant interpolation theorem by building on principles of bidirectional typing, and formalise it in Rocq.

Bidirectional Interpolation for the Lambda-Calculus -- Revisiting and Formalising Craig-Čubrić Interpolation

TL;DR

A new proof of Craig's Interpolation theorem is given by building on principles of bidirectional typing, and formalise it in Rocq.

Abstract

Craig's Interpolation theorem has a wide range of applications, from mathematical logic to computer science. Proof-theoretic techniques for establishing interpolation usually follow a method first introduced by Maehara for the Sequent Calculus and then adapted by Prawitz to Natural Deduction. The result can be strengthened to a proof-relevant version, taking proof terms into account: this was first established by Čubrić in the simply-typed lambda-calculus with sums and more recently in linear, classical and intuitionistic sequent calculi. We give a new proof of Čubrić's proof-relevant interpolation theorem by building on principles of bidirectional typing, and formalise it in Rocq.
Paper Structure (18 sections, 15 theorems, 8 equations, 4 figures)

This paper contains 18 sections, 15 theorems, 8 equations, 4 figures.

Table of Contents

  1. Introduction
  2. The simply-typed $\lambda$-calculus with sums
  3. Syntax
  4. Reduction and equations
  5. Bidirectional typing, normal forms and the subformula property
  6. A bidirectional characterisation of normal forms
  7. Normalisation for STLC+
  8. Interpolation
  9. ⋅
  10. Γ_1
  11. Γ_1.(x : A)
  12. Γ_1
  13. Γ_1
  14. Constant-free theorem
  15. Constants and equations
  16. ...and 3 more sections

Key Result

Theorem 4

Reduction is confluent: if $t \rightsquigarrow^* u$ and $t \rightsquigarrow^* u'$, then there exists $v$ such that $u \rightsquigarrow^* v$ and $u' \rightsquigarrow^* v$.

Figures (4)

  • Figure 1: Types and terms of STLC+ with respect to a language $\mathcal{L} = (\mathcal{B},\mathcal{C},\mathop{\mathrm{ty}}\nolimits)$
  • Figure 2: https://anonymous.4open.science/r/interpolation-stlc/code/theories/Typing.v#L164 Substitutions and their typing (excerpt)
  • Figure 3: https://anonymous.4open.science/r/interpolation-stlc/code/theories/Reduction.v#L50 Reduction (congruence rules omitted)
  • Figure 4: https://anonymous.4open.science/r/interpolation-stlc/code/theories/Bidir.v#L11 Bidirectional typing for the STLC+, with respect to a language $\mathcal{L} = (\mathcal{B},\mathcal{C},\mathop{\mathrm{ty}}\nolimits)$

Theorems & Definitions (25)

  • Definition 1: https://anonymous.4open.science/r/interpolation-stlc/code/theories/BasicAst.v#L18 Language
  • Definition 2: https://anonymous.4open.science/r/interpolation-stlc/code/theories/Typing.v#L16 Types and terms
  • Definition 3: https://anonymous.4open.science/r/interpolation-stlc/code/theories/Reduction.v#L121 Reductions
  • Theorem 4: https://anonymous.4open.science/r/interpolation-stlc/code/theories/ReductionConfluence.v#L173 Confluence
  • Lemma 5: https://anonymous.4open.science/r/interpolation-stlc/code/theories/Equations.v#L720 Subject reduction
  • Lemma 6: https://anonymous.4open.science/r/interpolation-stlc/code/theories/MetaTheory.v#L56 Normality
  • Theorem 7: https://anonymous.4open.science/r/interpolation-stlc/code/theories/MetaTheory.v#L29 Progress
  • Definition 8: https://anonymous.4open.science/r/interpolation-stlc/code/theories/MetaTheory.v#L97 Covering
  • Definition 9: https://anonymous.4open.science/r/interpolation-stlc/code/theories/MetaTheory.v#L135 Values
  • Definition 10: https://anonymous.4open.science/r/interpolation-stlc/code/theories/MetaTheory.v#L128 Reducibility
  • ...and 15 more