Ordinal notations and QPF

Stream: Type theory

[Palalansoukî]

I noticed from #mathlib4 > ZFSet and computability that QPF is not only a good tool for defining large objects such as universes, but is also well suited for defining ordinal notations, since these are defined as certain fixed points of functions on ordinals. For example, one can give an ordinal notation system for ordinals below $\epsilon_0$ as follows:

import Mathlib

namespace List

variable {α}

theorem ofFn_getElem' {k} (l : List α) (hk : k = l.length) :
    (ofFn fun i : Fin k ↦ l[(i : ℕ)]) = l := by
  rcases hk; simp

end List

namespace OrdinalNotation

abbrev NotationFunctor (α : Type*) := Multiset α

noncomputable instance : QPF NotationFunctor where
  P := ⟨ℕ, Fin⟩
  abs {α} s := Multiset.map s.2 Finset.univ.val
  repr {α} s := ⟨s.card, fun i : Fin s.card ↦ s.toList[i]⟩
  abs_repr {α} s := by
    simp only [Fin.getElem_fin, Fin.univ_val_map]
    rw [List.ofFn_getElem'] <;> simp
  abs_map {α β f i} := by
    let ⟨n, φ⟩ := i
    simp [PFunctor.map, Function.comp_def]

def Epsilon0 : Type := QPF.Fix NotationFunctor

noncomputable def mk (s : Multiset Epsilon0) : Epsilon0 := QPF.Fix.mk s

noncomputable def dest (o : Epsilon0) : Multiset Epsilon0 := QPF.Fix.dest o

noncomputable instance : Zero Epsilon0 := ⟨mk 0⟩

/-- Notice that this is not an usual ordinal sum; rather sum of multiset ordered by $\ge$. -/
noncomputable instance : Add Epsilon0 := ⟨fun o₁ o₂ ↦ mk (dest o₁ + dest o₂)⟩

noncomputable def exp (o : Epsilon0) : Epsilon0 := mk {o}

scoped notation "ω^[" o "]" => exp o

noncomputable instance : One Epsilon0 := ⟨ω^[0]⟩

noncomputable def omega : Epsilon0 := ω^[1]

end OrdinalNotation

Compared with the existing definition in mathlib, this definition looks simpler and more elegant, except that it is noncomputable. How could one make this definition computable?

By the way, in proof theory there is a tool for treating ordinal notations in an abstract way, namely dilators. These were introduced by Girard as certain endofunctors on the category of ordinals satisfying specific conditions, and they are often used in settings that involve large ordinals. I suspect that QPF is essentially a dilator (or a ptyx?), or at least a restricted version of one. I am not an expert on either notion, so I cannot judge ... but does anyone know about this?

[Aaron Liu]

I'm currently working on a way to make QPF work without having to give an explicit repr function, I think this would solve your computability issue