Showing termination for the semantics of infinite joins

Stream: new members

[Fernando Chu]

Lean will reject the definition interpret below. This seems reasonable to me, but also I'm unsure how to instruct lean that this is fine.

import Mathlib

open CategoryTheory Limits

inductive Formula : Type where
  | t : Formula
  | infdisj : (ℕ → Formula) → Formula

variable {C : Type u} [Category.{v} C] [(X : C) → HasCoproductsOfShape ℕ (Subobject X)]

-- fail to show termination for interpret
def interpret {X : C} : Formula → Subobject X
  | .t => ⊤
  | .infdisj f => ∐ (interpret ∘ f)

What is the right way to do this?

[Aaron Liu]

-- fail to compile definition
def interpret {X : C} : Formula → Subobject X
  | .t => ⊤
  | .infdisj f => ∐ fun i => interpret (f i)

[Aaron Liu]

Originally you had

-- fail to show termination for interpret
def interpret {X : C} : Formula → Subobject X
  | .t => ⊤
  | .infdisj f => ∐ ((fun i => interpret i) ∘ f)

and it's not clear that this terminates.

[Aaron Liu]

Remember that your functions will get eta expanded until they are fully applied

[Fernando Chu]

Aaron Liu said:

Remember that your functions will get eta expanded until they are fully applied

What does "fully applied" mean here? I'm a bit confused; I would have thought thatfun i => interpret (f i) is defeq to (fun i => interpret i) ∘ f. Is this not? By the way the first suggestion now works by adding noncomputable, thanks!

[Fernando Chu]

I guess the termination checker probably doesn't work up to defeq then?

[Aaron Liu]

The termination checker look for recursive applications and tries to prove that the arguments are decreasing

[Aaron Liu]

With fun i => interpret (f i) the argument is f i which is decreasing but with (fun i => interpret i) ∘ f the argument is i which is not decreasing.

[Adrian Marti]

Edit: I just realized that the issue was about termination and not computability :sweat_smile: but maybe it is still interesting..

The whole HasLimit machinery in mathlib does not provide you with a way to compute limits (or colimits). Recall that colimits get computed in mathlib with

/-- Use the axiom of choice to extract explicit `ColimitCocone F` from `HasColimit F`. -/
def getColimitCocone (F : J ⥤ C) [HasColimit F] : ColimitCocone F :=
  Classical.choice <| HasColimit.exists_colimit

which sits inside a noncomputable section since it uses the axiom of choice.

The issue is that HasColimit is a property and not data, and thus we cannot computably extract a colimit (there might also be distinct isomorphic choices of colimits). Interestingly, in the case of colimit operations in posets, there is always a unique choice and it corresponds to iSup or sSup. Still, even if there is a unique choice, I don't think that there is a way to compute it (which is less intuitive). So if one were to insist on making things computable, one would have to store colimits as data.

The interesting thing is that wlog, given a category $C$ which has colimits, there is a way to replace it with an equivalent category $D$ that has all colimits and also a specified way to compute them, so we are not really losing generality by requiring colimits to have data.

This works the following way: Recall that in $\textup{Set}$ we do have specific constructions of colimits (for example by representing them as a coequalizer of coproducts) and thus in every presheaf category the same is true. Now define $D$ to be the essential image of the Yoneda embedding $C \to \textup{Set}^{C^{op}}$. This is equivalent to $C$ and has concrete computable colimits.

Note: Variations of this trick can be used to prove strictification theorems for monoidal categories (or bicategories).