A monad for partial computations

Stream: mathlib4

[Anthony Vandikas]

Inspired by @Aaron Liu's comments in #mathlib4 > deprecate Mathlib.Data.Nat.PartENat? @ 💬 and #Is there code for X? > Divergence monad @ 💬 I made an attempt at constructing a monad for partial computations with a computable OmegaCompletePartialOrder instance (neither Option nor Part support this use case). My solution consists of three parts.

A computable version of Quotient.choice. As mentioned in #lean4 > Quot.lift for dependent products @ 💬 , the "obvious" computational interpretation of Quotient.choice : (∀i:I, @Quotient (A i) …) → @Quotient (∀i:I, A i) is not sound. However, we _can_ provide a sound computational interpretation when we restrict I to ℕ:

unsafe def Quotient.countableChoice_impl {α : Nat → Type*} {S : ∀ i, Setoid (α i)}
    (f : ∀ i, Quotient (S i)) :
    @Quotient (∀ i, α i) (by infer_instance) :=
  Quotient.lift₂
    (fun z s ↦ ⟦fun | .zero => z | .succ n => s n⟧)
    (fun z₁ s₁ z₂ s₂ h₁ h₂ ↦ by
      apply sound
      rintro ⟨_|n⟩
      · apply h₁
      · apply h₂)
    (f 0)
    (countableChoice_impl (fun n ↦ f n.succ))

@[implemented_by Quotient.countableChoice_impl]
def Quotient.countableChoice {α : Nat → Type*} {S : ∀ i, Setoid (α i)}
    (f : ∀ i, Quotient (S i)) :
    @Quotient (∀ i, α i) (by infer_instance) :=
  Quotient.choice f

My justification for the soundness of this implementation comes from the fact that only uses existing (sound and computable) functions + general recursion. The implementation is found here (it uses unquot instead of recursion for performance reasons, but should be equivalent).

A type of semi-computable propositions. Next, I define a type of semi-computable propositions ΩProp as a quotient of the type of boolean sequences (ℕ → Bool) / ≈, where p ≈ q ≝ (∃n, p n) ↔ (∃n, q n). A sequence is interpreted as "true" if at least one element in the sequence is true, and the quotient relation ensures that we cannot observe the difference between different "true" sequences. The ΩProp type has a (computable) OmegaCompletePartialOrder, and Quotient.countableChoice is used in the implementation of ωSup.

The implementation of this type is here.

A type of semi-computable computations. Finally, I define the type ΩPart A of semi-computable computations returning a value of type A. The definition of ΩPart is the same as Part with ΩProp swapped for Prop. Again, ΩPart A has a (computable) OmegaCompletePartialOrder instance. The implementation can be found here.

This was mainly just a fun experiment and the code is not ready to be (or perhaps should not be) put in mathlib. I thought I should post it here to see if 1) there is any interest or 2) an implementation already exists that has escaped my notice.

[Eric Wieser]

Since you've written this in mathlib itself, it would probably be easiest to look at if you opened a draft PR; you can make it clear in the description that you don't actually intend it to be merged.

[Anthony Vandikas]

Eric Wieser said:

Since you've written this in mathlib itself, it would probably be easiest to look at if you opened a draft PR; you can make it clear in the description that you don't actually intend it to be merged.

Good idea! I have made a PR at #34291.