Type-theoretically what is a termination proof?

Stream: lean4

[nrs]

Intuitively a termination proof means a function eventually stops, but type-theoretically, what is it we're proving about a term of a function type? (Or is it at all correct to say that a termination proof is a proof about a property of a term of a function type?)

[Kevin Buzzard]

You're proving that it is a term of a function type. i.e. that term doesn't even exist until you've finished the termination proof.

[nrs]

Kevin Buzzard said:

You're proving that it is a term of a function type. i.e. that term doesn't even exist until you've finished the termination proof.

Ah I see! So a termination proof means we're showing that a term does indeed follow from the introduction rules for the types of our type theory?

[Kevin Buzzard]

I guess you can write a computer program which contains a "function" which sometimes loops on an input, but mathematically this isn't a function, it's a "partially-defined function" or something. In mathematics if you say $f:X\to Y$ then this means that given an element of $X$ you must get an element of $Y$ out at the end of it, and that's what Lean's function type represents. I don't know anything about introduction rules, apologies. You're proving that something is a well-defined term.

[nrs]

Kevin Buzzard said:

I guess you can write a computer program which contains a "function" which sometimes loops on an input, but mathematically this isn't a function, it's a "partially-defined function" or something. In mathematics if you say $f:X\to Y$ then this means that given an element of $X$ you must get an element of $Y$ out at the end of it, and that's what Lean's function type represents. I don't know anything about introduction rules, apologies. You're proving that something is a well-defined term.

Ty I will be thinking about this!

[Edward van de Meent]

the way i look at it, is that you're proving that the description you're giving is sufficient to completely determine the behaviour and values of the function

[Joachim Breitner]

The way I look at it is that you are helping lean prove that there exists a function (a value in the given type) that satisfies the given equations, and then lean constructs that value for you, and proves that it satisfies the equations.

This may not even completely determine the behavior, something like https://github.com/leanprover/lean4/issues/3119 with the value being not uniquely determines for some inputs is totally fine (and the aeneas people have implemented that).

This extensional point of view mostly ignores questions about the reduction behavior of the function.

[Giacomo Stevanato]

The way I see it, in type theory you can't define recursive functions like you would do in functional programming, instead you define functions that use eliminators on some of their inputs, which kinda emulates recursion. These are however restricted to getting the result of the recursive call only for structurally smaller values. Often the compiler can fit your function definition with this limitation automatically, but sometimes it can't. Termination proofs add extra parameters to the function on which the compiler can trivially eliminate on while still being able to get the recursive results it needs and hence allows it to write a term for your function.

[Kevin Buzzard]

One of the things I've always found fascinating about this community is that because it has such a diverse mix of people, there are sometimes lots of ways to look at it :-)

[Trebor Huang]

The general technique (Bove–Capretta) is to look at the recursion, construct another helper proposition that says "this input can be reached recursively from the base case". Now you trivially have a function f that takes an input, and a proof of the proposition at this input, and returns the output, by recursion on the proof (not the input!). The termination proof is simply proving that the proposition is true for all inputs, which you can feed into the second argument of f. This proposition is called Acc in Lean.

Though Acc being a proposition in Lean does raise some type theoretic complications, so you can probably view it as an ordinary type first, which doesn't change anything except maybe computational efficiency.

[nrs]

def someFunc (x : A) (y : B) : C := (body) is type-theoretically the assertion: (x : A), (y : B) |- someFunc x y : C. Since a term is well-formed only if it has finitely many symbols, a termination proof consists of the proof that someFunc x y is a term with finitely many symbols (this is effectively what people were saying above but I couldn't properly understand it at the time)

[Edward van de Meent]

I don't think that's right? def loop (a : Unit) : Unit := loop a has finitely many symbols, but doesn't terminate

[Edward van de Meent]

Or maybe I am misunderstanding what you mean by "symbols"?

[nrs]

hm you're right. instead the right statement is: a termination proof consists of the proof that someFunc x y denotes at least one symbol and at most finitely many symbols, i.e. that (x : A), (y : B) |- someFunc x y : C is a syntactically well-formed judgment

[Soundwave]

Kevin and Giacomo's perspectives are two sides of the same coin in the following way: Consider a recursive function trivially terminating if its termination follows from structural induction on one of its arguments. Such a function, is, in particular, the result of applying the recursor of the type inducted on with a suitable motive (It's a good exercise to show this). This is how recursive functions are constructed internally (type theoretically speaking).

Then, for a general recursive function, a termination proof is a part of the definition in the following way: for an arbitrary recursive definition f : X₁ × ... × Xₙ with a termination proof, there exists an inductive type I and g : X₁ × ... × Xₙ → I and h : X₁ × ... × Xₙ × I such that h is trivially terminating w.r.t. I and h x₁ ... xₙ (g x₁ ... xₙ) = f x₁ ... xₙ in the natural way (made precise with operational semantics).

You can think of the termination proof as an ergonomic way of specifying I and g. In particular Lean works in terms of an order relationship equivalent to the structural order on I.

Coq somewhat infamously lacked a feature for general termination proofs for most of its life because, well, by this theorem, it didn't need it!

[Alok Singh]

Kevin Buzzard said:

One of the things I've always found fascinating about this community is that because it has such a diverse mix of people, there are sometimes lots of ways to look at it :-)

How I feel about math in general