══════════════════════════════════════════════════════════════════════════════
Termination checking using well-founded typing derivations
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
by Rodolphe Lepigre (Inria, LSV, CNRS, ⋯)
Checking the termination of programs is a very difficult and important problem
in contexts where consistency is critical (e.g., in proof assistants). One way
of ensuring termination is to rely on well-known, Ramsey-based techniques such
as the size change principle of Lee, Jones and Ben Amram. They roughly consist
in analysing the recursive calls throughout programs, to ensure that there is
some structural decrease (usually based on the subterm order). In this talk, I
will present a new technique based on circular typing derivations, in which we
rather analyse the “call structure” of circular typing derivations (also using
a variant of the size change principle).
This is joint work with Christophe Raffalli.
Links:
- https://lepigre.fr/files/docs/lepigre2017_subml.pdf (paper)
- https://github.com/rlepigre/subml (git repository of SubML)
- https://github.com/rlepigre/pml (git repository of PML₂ )
══════════════════════════════════════════════════════════════════════════════
══════════════════════════════════════════════════════════════════════════════
Introduction
━━━━━━━━━━━━
Termination checking is useful:
- Termination is (generally) desirable for programs.
- It is required for the consistency of non-trivial proof systems.
There are several techniques:
- Keywords: ranking function, dependency pair, sized types, ⋯
- Many techniques are based (more or less explicitely) on Ramsey's theorem.
- Example: the size change principle of Lee, Jones and Ben Amram.
Idea of this work:
- Use Ramsey-based techniques in a singular way.
- The termination argument is not directly related to terms.
- We use circular typing derivations.
Advantages of our approach:
- Well-typed programs are terminating.
- The termination argument is local.
- We achieve compositionality through size annotations.
map : ∀α, (A ⇒ B) ⇒ List(α,A) ⇒ List(α,B)
split : ∀α, (A ⇒ Bool) ⇒ List(α,A) ⇒ List(α,A) × List(α,A)
1/12
══════════════════════════════════════════════════════════════════════════════
══════════════════════════════════════════════════════════════════════════════
Syntax of the language
━━━━━━━━━━━━━━━━━━━━━━
Terms:
t,u ∷= x | λx.t | t u (usual λ-calculus)
| 0 | t+1 | [t | 0 → u₀ | x+1 → u₁] (zero, successor, case analysis)
| ∙∈A (some element of type A)
Types:
A,B ∷= N(s) (sized natural numbers)
| A ⇒ B (function type)
Ordinals (sizes):
s,o ∷= α (ordinal variable)
| ω (limit ordinal)
| ∙