Divergence monad

Stream: Is there code for X?

[Niels Voss]

Since all Lean functions, excepting a few pathological ones, terminate, I was wondering if it was possible to represent partial functions with a type

$$\text{Diverging}(X) = X \cup \{\bot\}$$

where ⊥ represents a computation that loops forever. This would be classically equivalent to both Option and Part, but it would sit between Option and Part computationally. The reason why Part and particularly PFun.fix is not sufficient is that Part encodes for a much wider range of computations, including those that could overflow the end of arrays or perform unsafe casts, which makes it too general.

I am asking this for my own curiosity rather than because I need it for a specific project. However, I could imagine it might have some uses, because it is possible to prove things about possibly-diverging computations, in contrast to partial. So looping computations could be reasoned about, and only converted to partial "total" functions when actually needed.

[Daniel Weber]

Part encodes for a much wider range of computations, including those that could overflow the end of arrays or perform unsafe casts, which makes it too general.

could you explain this? I'm not sure I understand

[Niels Voss]

Right now, we can build potentially non-terminating functions without "meta-features" like partial by using PFun.fix. Then, when we actually want to run the function, we must first prove that it terminates for the specific input. Alternatively, we can use Part.unwrap, which is an unsafe function. For Part in general, this function can lead to crashes (or possibly even undefined behavior), because it basically is equivalent to running code with a sorry. For example, the following crashes the Lean server:

import Mathlib.Control.Fix

def myList : List ℕ := [1,2,3]
def myVal : Part ℕ where
  Dom := False
  get h := myList[5]

#eval myVal.unwrap

However, I'm pretty sure that if you just run .unwrap on values of the form PFun.fix f (where the f is a total function) then it can't actually crash. However, because Mathlib doesn't actually distinguish between general Part values and the result of PFun.fix, we don't have a way to run values of type PFun.fix in a safe, opaque way.

[Niels Voss]

So the idea would be to have two separate concepts, Part which represents computations that might perform undefined behavior (bad), and Diverge, which represents computations that might loop forever (less bad):

• Part is what we currently have in mathlib. Unwrapping is an unsafe operation that can crash Lean or worse.
• Diverge would be a new type. Unwrapping is a partial (and therefore opaque) operation that can enter an infinite loop. Also, properties of Diverge stuff could in theory be proven.
• Option can be interpreted as computations that might crash, using the .get! operation. This is less bad than Diverge because you would find out in finite time whether or not your program has crashed.

[Niels Voss]

I was originally thinking of something like

import Mathlib.Data.PFun
private def Comps.{u,v} (α : Type u) : Set (Part α) :=
    { PFun.fix f g | (γ : Type v) (f : γ →. α ⊕ γ) (g : γ) } -- Maybe f here should be total?
def DivM.{u,v} (α : Type u) : Type u := Comps.{u,v} α

But then I don't think you can actually get the source PFun back, making this useless for computation (Trunc over Sigma would need to be used instead of Exists, I think). Plus, I'm not sure I like the way it handles universes.

[Niels Voss]

I did find docs#Fix, which seems to be of interest, but it's a class and not a usable structure

[Edward van de Meent]

so iiuc, you'd like a version of Part where you also prove that outside of the given domain, f is not sensibly defined?

[Edward van de Meent]

or something like this?

import Mathlib

structure Loop (α β γ : Type*) where
  start : α → β
  step : β → β
  cond : β → Prop -- maybe use Bool?
  stop : (b:β) → cond b → γ

def Loop.dom (f:Loop α β γ) (a:α) : Prop := ∃ n, f.cond <| f.step ^[n] (f.start a)

def Loop.eval (f:Loop α β γ) [DecidablePred f.cond] : (a:α) → f.dom a → γ := fun a ha =>
  f.stop (f.step^[Nat.find ha] (f.start a)) (Nat.find_spec ha)

[nrs]

might be worth looking at https://www.sciencedirect.com/science/article/abs/pii/S2352220824000531 and the corresponding coq code

[Trebor Huang]

One possible interpretation is restricting Part to using propositions of the form (n : Nat) -> p n where p is decidable. Intuitively this does correspond to possibly non-terminating computations, where p n means the calculation terminates after n steps (obviously should be decidable).

[Niels Voss]

Or alternatively, just a Stream of Options, or a Stream'.Seq. I think this would need to be quotiented to have the right notion of equality.

[Niels Voss]

Edward van de Meent said:

so iiuc, you'd like a version of Part where you also prove that outside of the given domain, f is not sensibly defined?

I'm not really sure what you mean. Part is just a single value, not a function.

Your Loop example seems like the most general way to do it, which is probably good (though I would replace Prop with Bool, or at least a decidable proposition, as you considered). However, it seems that what would really be best is to have DivM be Loop quotiented by returning the same value, which probably requires a universe bump.

[Edward van de Meent]

Niels Voss said:

However, it seems that what would really be best is to have DivM be Loop quotiented by returning the same value

that seems counterproductive? i thought the whole goal was to have a type for functions which may or may not loop? if you quotient out the intermediate steps, you miss out on the whole looping part...

[Niels Voss]

Not necessarily. It would still let you write infinite loops, it's just that equality wouldn't care about the specific way in which an infinite loop was obtained.

[Edward van de Meent]

then i don't see what this adds compared to functions to Partial? since i suspect that these will then be very close to equivalent?

[Edward van de Meent]

since a proof saying "this program terminates on this input" should allow you to evaluate the program on the input and return the value, and in the other direction, you can make a program loop on "non-valid" inputs

[Niels Voss]

I don't think a quotient wrapper would remove your ability to evaluate the program on inputs you proved that terminate. A function would be represented as A -> DivM B, and whether or not a function terminates in a given input is a predicate that respects the equivalence relation

[Niels Voss]

I do kind of see your point though, in that you could already do that with Part. I still think it would be useful to have an operation with a partial unwrap operation rather than an unsafe unwrap operation

[Edward van de Meent]

unfortunately, i don't think there is a good way to do this in lean

[Edward van de Meent]

as in, afaik there is no way to "unwrap" a partial operation in a pure way

[Asei Inoue]

@Niels Voss

You could want to read this:
relevant monad appears in this paper.

https://arxiv.org/abs/1810.08380

[Asei Inoue]

679B84B8-C984-4278-8051-E33F6561667A.jpg

[Niels Voss]

Isn't this the Part monad that already exists in Mathlib?

[Matt Diamond]

yes, I believe it is... that's @Mario Carneiro's paper that explains the design of mathlib's Computability library, which uses Part to model partial recursive functions

[Niels Voss]

Funnily enough, I actually saw paper for the first time today a few hours before Asei Inoue suggested it because I was looking through Mathlib's computability API and it was linked.

Anyways, the reason that this doesn't work for my suggestion is that I was curious if there was a monad for functions that were safe to run with partial without causing undefined behavior, but you could still reason about when they do terminate. The current Part is too general for that.

[Edward van de Meent]

The WIP partial_fixpoint feature might interest you

[Edward van de Meent]

Coming soon to a Lean release near you

[Mario Carneiro]

I don't see why Part doesn't satisfy that requirement @Niels Voss , except that the partial keyword is unrelated to mathematical modeling of partial functions

[Mario Carneiro]

I advocated for partial functions to get compiled to things returning Part way back when it was introduced, but we got something that is not really sound to reason about instead, and partial_fixpoint is as I understand it finally implementing something sound, although it still isn't using the Part monad

[Mario Carneiro]

I don't know what the API of partial_fixpoint actually looks like

[Niels Voss]

Running a general Part function can cause undefined behavior, if I understand correctly (see the unwrap example above). However, a certain subset of Part values are safe to run and might only cause infinite loops instead of undefined behavior.

Anyways, this was just something I was curious about rather than something I personally need.

[Mario Carneiro]

running a Part function doesn't cause undefined behavior, ignoring proof obligations causes undefined behavior

[Mario Carneiro]

running a Part function requires first proving that it will terminate

[Niels Voss]

Yeah, running a Part by proving termination first is perfectly safe. But Part.unwrap is unsafe because it ignores proof obligations. Whereas if we had a SafePart then we could either run it normally by first proving termination, or without proving termination by using a partial function. The difference is that running Part without proving termination can only be done in an unsafe, whereas running SafePart without proving termination could be done in a partial.

[Mario Carneiro]

neither one is safe, the only reason partial functions are safe to run is because the compiler specifically turns off some optimizations around them and also proves independently that the target type is inhabited

[Mario Carneiro]

there is no way to do that kind of reasoning in the logic

[Niels Voss]

So you mean that running a SafePart type in a partial def could still cause undefined behavior?

[Mario Carneiro]

I don't think SafePart can be defined at all in a way which is logically distinct from Part or Id

[Mario Carneiro]

if it's an opaque wrapper, perhaps you can express those semantics (that's kind of what partial is) but you can't reason about it

[Niels Voss]

I was thinking something like this:

import Mathlib.Data.PFun
set_option autoImplicit false

structure SafePart.{u,v} (α : Type u) where
  σ : Type v -- The type of auxillary data used by the computation
  current : σ
  next : σ → α ⊕ σ

partial def SafePart.run {α : Type*} [Inhabited α] (v : SafePart α) : α :=
  match v.next v.current with
  | .inl a => a
  | .inr s => SafePart.run ⟨v.σ, s, v.next⟩

def SafePart.toPart {α : Type*} (v : SafePart α) : Part α :=
PFun.fix (pure ∘ v.next) v.current

-- Number of steps for hailstones/Collatz conjecture
def countSteps (n : Nat) : SafePart Nat where
  σ := Nat × Nat
  current := (0, n)
  next := fun (steps, k) =>
    if k ≤ 1 then .inl steps
    else if k % 2 = 0 then .inr (steps + 1, k / 2)
    else .inr (steps + 1, 3 * k + 1)

#eval SafePart.run (countSteps 211) -- 39

[Aaron Liu]

This looks like docs#Computation.corec

[Matt Diamond]

that's a good point... and Computation.toPart is very simple

import Mathlib

set_option autoImplicit false

def Computation.toPart {α : Type*} (c : Computation α) : Part α :=
{
  Dom   := c.Terminates
  get _ := c.get
}

partial def Computation.run' {α : Type*} [Nonempty α] (c : Computation α) : α :=
match destruct c with
| Sum.inl a => a
| Sum.inr ca => run' ca

def collatz : Nat × Nat → Nat ⊕ (Nat × Nat) :=
fun (steps, k) =>
  if k ≤ 1 then .inl steps
  else if k % 2 = 0 then .inr (steps + 1, k / 2)
  else .inr (steps + 1, 3 * k + 1)

-- Number of steps for Collatz conjecture
def countSteps (n : Nat) : Computation Nat :=
Computation.corec collatz (1, n)

#eval (countSteps 27).run'

[Matt Diamond]

though docs#Computation.run already exists in an unsafe version

[Matt Diamond]

I think Computation is basically the divergence monad that @Niels Voss was curious about... it allows you to prove things about intermediate steps in a potentially infinite loop

[Mario Carneiro]

I think you probably want to quotient the type by the relation of skipping a 'think' step, since otherwise Computation A has classically A + Nat values instead of A + 1

[Niels Voss]

Yes, this seems pretty much to fit what I was looking for. I was thinking of quotienting by something, as Mario Carneiro suggested, but then I'm not entirely sure if we can still use a partial function to run it

[Mario Carneiro]

get can still be defined on the quotient type, in fact it's basically the only thing you can define

[Matt Diamond]

oh right, because the result is the same across equivalent computations

[Mario Carneiro]

but you may indeed have troubles lifting it to satisfy the requirements of partial without just cheating the proof

[Niels Voss]

Here's one way it could be defined:

import Mathlib.Data.Seq.Computation

def computationSetoid (α : Type*) : Setoid (Computation α) where
  r := Computation.Equiv
  iseqv := Computation.Equiv.equivalence

def Divergence {α : Type*} := Quotient (computationSetoid α)

[Mario Carneiro]

ah, thanks past me for having already thought of this :)

[Matt Diamond]

yeah I guess you would have trouble proving that Computation.run' (as a partial function) respects the Quotient relation since you can't really prove anything about it

[Mario Carneiro]

you can make it an element of a singleton type

[Matt Diamond]

sorry, what does "it" refer to

[Niels Voss]

The return value of Computation.run', I think

[Mario Carneiro]

i.e. Computation.run' (c : Computation A) : { a // (\exists h, a = c.get h) \/ !c.Terminates /\ a = default }

[Matt Diamond]

ah, I see

[Niels Voss]

Sorry, what does a.get refer to? Doesn't a in the {} have type A?

[Mario Carneiro]

typo

[Niels Voss]

oh i see now. I think a ∈ c is probably the cleaner way of saying it

[Niels Voss]

I got it working, although it took me much longer than I expected. Sorry for the messy code right now; this is mainly just a proof-of-concept:

import Mathlib.Data.PFun
import Mathlib.Data.Seq.Computation

set_option autoImplicit false

partial def Computation.run' {α : Type*} [Nonempty α] (c : Computation α) : α :=
match destruct c with
| Sum.inl a => a
| Sum.inr ca => run' ca

def Constrain {α : Type*} (c : Computation α) [Inhabited α] :=
  {a : α // a ∈ c ∨ (¬c.Terminates ∧ a = default)}

def Constrain.mk {α : Type*} [Inhabited α] (c : Computation α) : Computation (Constrain c) where
  val (n : ℕ) :=
    (c.val.get n).attach.map fun ⟨a, ha⟩ =>
      ⟨a, Or.inl ⟨n, _⟩⟩ -- Sometimes need to replace _ with "by simp_all" when editing the below proof
  property n a h := by
    simp_all only [Option.map_eq_some', Option.attach_eq_some_iff, Subtype.exists, Option.mem_def,
      exists_and_left]
    rcases h with ⟨a, h₁, h₂, h₃⟩
    have := c.property h₁
    use a
    apply And.intro this
    use this
    simp_all

def Constrain.val_eq {α : Type*} [Inhabited α] {a b : Computation α} (h : a.Equiv b)
  (c : Constrain a) (d : Constrain b) : c.val = d.val := by
  by_cases ha : a.Terminates
  · have hb : b.Terminates := (Computation.terminates_congr h).mp ha
    apply Computation.mem_unique
    · simpa [ha] using c.property
    · have : d.val ∈ b := by simpa [hb] using d.property
      exact (h d.val).mpr this
  · have hb : ¬b.Terminates := fun h' => absurd ((Computation.terminates_congr h).mpr h') ha
    have h₁ : c.val ∉ a := fun t => absurd (Computation.terminates_of_mem t) ha
    have h₂ : d.val ∉ b := fun t => absurd (Computation.terminates_of_mem t) hb
    have := c.property
    have := d.property
    simp_all

instance {α : Type*} [Inhabited α] (c : Computation α) : Subsingleton (Constrain c) := by
  apply Subsingleton.intro
  intro a b
  unfold Constrain
  ext
  by_cases h : c.Terminates
  · apply Computation.mem_unique
    · simpa [h] using a.property
    · simpa [h] using b.property
  · have h₁ : a.val ∉ c := fun t => absurd (Computation.terminates_of_mem t) h
    have h₂ : b.val ∉ c := fun t => absurd (Computation.terminates_of_mem t) h
    have := a.property
    have := b.property
    simp_all

-- For some reason defining this above the Subsingleton instance causes the simp_all to no longer
-- finish, so we define this down here.
def Constrain.val {α : Type*} [Inhabited α] {c : Computation α} : Constrain c → α := Subtype.val

open Classical in
instance {α : Type*} (c : Computation α) [Inhabited α] : Nonempty (Constrain c) :=
  if h : c.Terminates then
    h.term.elim (fun a ha ↦ Nonempty.intro (⟨a, Or.inl ha⟩ : Constrain c))
  else
    Nonempty.intro (⟨default, Or.inr ⟨h, rfl⟩⟩ : Constrain c)

noncomputable instance {α : Type*} (c : Computation α) [Inhabited α] : Inhabited (Constrain c) :=
  Classical.inhabited_of_nonempty (by infer_instance)

def computationSetoid (α : Type*) : Setoid (Computation α) where
  r := Computation.Equiv
  iseqv := Computation.Equiv.equivalence

def Divergence (α : Type*) := Quotient (computationSetoid α)

lemma Constrain.eq {α : Type*} {a b : Computation α} [Inhabited α] (h : a.Equiv b)
  : Constrain a = Constrain b := by
  unfold Constrain
  congr
  funext x
  congr 1
  · exact propext (h x)
  · congr 2
    exact propext (Computation.terminates_congr h)

def Divergence.run {α : Type*} [Inhabited α] : Divergence α → α :=
  Quotient.lift (fun c : Computation α => Constrain.val (Computation.run' (Constrain.mk c))) <| by
    intro a b h
    apply Constrain.val_eq
    exact h

def collatz : Nat × Nat → Nat ⊕ (Nat × Nat) :=
fun (steps, k) =>
  if k ≤ 1 then .inl steps
  else if k % 2 = 0 then .inr (steps + 1, k / 2)
  else .inr (steps + 1, 3 * k + 1)

-- Number of steps for Collatz conjecture
def countSteps (n : Nat) : Computation Nat :=
Computation.corec collatz (1, n)

def countStepsDiv (n : Nat) : Divergence Nat := ⟦countSteps n⟧

#eval Divergence.run (countStepsDiv 27) -- 112

[Mario Carneiro]

Here's some proof golfing applied to that:

import Mathlib.Data.PFun
import Mathlib.Data.Seq.Computation

def Constrain {α : Type*} (c : Computation α) [Nonempty α] :=
  {a : α // a ∈ c ∨ (¬c.Terminates ∧ a = Classical.choice ‹_›)}

instance {α : Type*} (c : Computation α) [Nonempty α] : Nonempty (Constrain c) :=
  match em c.Terminates with
  | .inl _ => ⟨_, .inl c.get_mem⟩
  | .inr h => ⟨_, .inr ⟨h, rfl⟩⟩

partial def Computation.run' {α : Type*} [Nonempty α] (c : Computation α) : Constrain c :=
  match h : destruct c with
  | .inl a => ⟨a, .inl (destruct_eq_pure h ▸ ret_mem _)⟩
  | .inr ca => by
    refine let ⟨a, h'⟩ := run' ca; ⟨a, ?_⟩
    rw [destruct_eq_think h]
    match h' with
    | .inl h' => exact .inl (think_mem h')
    | .inr ⟨h1, h2⟩ => exact .inr ⟨mt of_think_terminates h1, h2⟩

theorem Constrain.val_eq {α : Type*} [Nonempty α] {a b : Computation α} (h : a.Equiv b) :
  ∀ (c : Constrain a) (d : Constrain b), c.val = d.val
  | ⟨_, .inl hc⟩, ⟨_, .inl hd⟩ => Computation.mem_unique ((h _).1 hc) hd
  | ⟨_, .inr ⟨hc, _⟩⟩, ⟨_, .inl hd⟩ => nomatch hc ⟨_, (h _).2 hd⟩
  | ⟨_, .inl hc⟩, ⟨_, .inr ⟨hd, _⟩⟩ => nomatch hd ⟨_, (h _).1 hc⟩
  | ⟨_, .inr ⟨_, hc⟩⟩, ⟨_, .inr ⟨_, hd⟩⟩ => hc.trans hd.symm

def computationSetoid (α : Type*) : Setoid (Computation α) where
  r := Computation.Equiv
  iseqv := Computation.Equiv.equivalence

def Divergence (α : Type*) := Quotient (computationSetoid α)

def Divergence.run {α : Type*} [Nonempty α] : Divergence α → α :=
  Quotient.lift (fun c : Computation α => (Computation.run' c).1)
    fun _ _ h => Constrain.val_eq h _ _

def collatz : Nat × Nat → Nat ⊕ (Nat × Nat) :=
  fun (steps, k) =>
    if k ≤ 1 then .inl steps
    else if k % 2 = 0 then .inr (steps + 1, k / 2)
    else .inr (steps + 1, 3 * k + 1)

-- Number of steps for Collatz conjecture
def countSteps (n : Nat) : Computation Nat :=
  Computation.corec collatz (1, n)

def countStepsDiv (n : Nat) : Divergence Nat := ⟦countSteps n⟧

#eval Divergence.run (countStepsDiv 27) -- 112

[Niels Voss]

I am going to try placing a Monad instance of Divergence once I can figure out how to get the bind operator working properly

[Niels Voss]

Do you know if it would be possible to implement similar to Haskell's fix operator? If so, would such an operator be useful given that Lean isn't as "lazy" as Haskell?

[Niels Voss]

One disadvantage of the current approach is that because the single value of Constrain empty (where empty is the non-halting computation) is Classical.choice _, we have no way to tell what it is. This means that if we have two computations c1, c2 where c1 converges and c2 diverges, it is impossible to determine whether or not c1.run = c2.run. There are also some other problems, such as not being able to distinguish between a converging and diverging computation based on .run alone.

Because of this, I think it's better to define Constrain to be an Option instead. This also makes things cleaner, and the old value can always be recovered with Divergence.run.getD default, possibly replacing default with an infinite loop if all you have is a Nonempty instance and don't want to mark the definition as noncomputable.

import Mathlib.Data.PFun
import Mathlib.Data.Seq.Computation
import Mathlib.Control.Fix
import Mathlib.Tactic

set_option autoImplicit false

def Option.toComputation {α : Type*} : Option α → Computation α
| .some a => .pure a
| .none => .empty α

theorem Option.eq_of_equiv_toComputation {α : Type*} (a b : Option α)
  (h : a.toComputation.Equiv b.toComputation) : a = b :=
  match a, b with
  | .some x, .some y => by
    congr
    exact (Computation.eq_of_pure_mem <| (h x).mp (Computation.ret_mem x))
  | .some x, .none => absurd (h x |>.mp (Computation.ret_mem x)) (Computation.not_mem_empty x)
  | .none, .some y => absurd (h y |>.mpr (Computation.ret_mem y)) (Computation.not_mem_empty y)
  | .none, .none => rfl

structure Computation.Result {α : Type*} (c : Computation α) where
  val : Option α
  constraint : c.Equiv val.toComputation

instance {α : Type*} (c : Computation α) : Nonempty c.Result :=
  match em c.Terminates with
  | .inl _ => ⟨c.get, Computation.equiv_pure_of_mem (Computation.get_mem c)⟩
  | .inr h => ⟨none, fun s => iff_of_false (fun h' => h ⟨s, h'⟩) (Computation.not_mem_empty s)⟩

partial def Computation.run' {α : Type*} (c : Computation α) : c.Result :=
match h : destruct c with
| .inl a => ⟨some a, by rw [destruct_eq_pure h]; rfl⟩
| .inr ca => by
  refine let ⟨a, h'⟩ := run' ca; ⟨a, ?_⟩
  rw [destruct_eq_think h]
  intro s
  constructor <;> intro h
  · simp [←h' s, Computation.of_think_mem h]
  · simp [h' s, h, Computation.think_mem]

theorem Computation.Result.val_eq {α : Type*} {a b : Computation α} (h : a.Equiv b)
  (r : a.Result) (s : b.Result) : r.val = s.val := by
  apply Option.eq_of_equiv_toComputation
  exact Computation.Equiv.trans (Computation.Equiv.trans r.constraint.symm h) s.constraint

def Computation.toOption {α : Type*} (c : Computation α) : Option α := c.run'.val

def computationSetoid (α : Type*) : Setoid (Computation α) where
  r := Computation.Equiv
  iseqv := Computation.Equiv.equivalence

def Divergence (α : Type*) := Quotient (computationSetoid α)

def Divergence.run {α : Type*} : Divergence α → Option α :=
  Quotient.lift (fun c => (Computation.run' c).val) fun _ _ h => Computation.Result.val_eq h _ _

def collatz : Nat × Nat → Nat ⊕ (Nat × Nat) :=
fun (steps, k) =>
  if k ≤ 1 then .inl steps
  else if k % 2 = 0 then .inr (steps + 1, k / 2)
  else .inr (steps + 1, 3 * k + 1)

-- Number of steps for Collatz conjecture
def countSteps (n : Nat) : Computation Nat :=
Computation.corec collatz (1, n)

def countStepsDiv (n : Nat) : Divergence Nat := ⟦countSteps n⟧

#eval Divergence.run (countStepsDiv 27) -- some 112

[Niels Voss]

In this code, I basically took your golfed versions of the proofs and rewrote them to use Option. This code also avoids the need for a [Nonempty α] instance

[Mario Carneiro]

Niels Voss said:

Do you know if it would be possible to implement similar to Haskell's fix operator? If so, would such an operator be useful given that Lean isn't as "lazy" as Haskell?

Yes, Computation definitely supports fix, as does Part

[Mario Carneiro]

All of these implementations are passable for demo purposes but not great from a performance standpoint. There are lean compiler changes needed to make it possible to implement better data representations for coinductive types

[Miyahara Kō]

You can see the example of coinductive override here.

[Miyahara Kō]

This example uses the not merged feature:opaque_repr.

[Niels Voss]

So my understanding of the issue is that we want a different runtime representation of Computation than how it is represented in math, but there's a bug in the compiler right now that prevents us from doing that. So, we need an opaque_ref attribute, which is introduced in the PR, which fixes the bug?

How much worse is the performance of Computation and Divergence than partial (is it a constant multiple different, or of worse time complexity?) and where does the slowdown come from? I could imagine how Stream'.tail ends up building a bunch of 1 +s that have to be tracked, but is there a more fundamental reason why Computations are slow?

[Mario Carneiro]

A Computation is a function where you give it the number of steps to compute and it computes the output to that approximation. If it turns out you didn't give enough fuel, you call it again with more steps and it runs the computation from the beginning again with more fuel. This is very different from the destructor function approach, where the result of a partial computation is a value in an existentially quantified type, and you can just call the destructor function again to continue the computation if the partial computation was not enough

[Mario Carneiro]

If you use every step of computation, this is an O(n^2) computation instead of the ideal O(n). You can make it into a constant overhead by exponentially growing the step counts

[Mario Carneiro]

This is relevant for the recent Computable reals discussion, since computable reals are also morally a coinductive type and you don't want to have to redo the computation from the beginning again every time (although some real numbers need to be computed from scratch anyway since you have to adjust the bounds on various quantities)

[Niels Voss]

I think I ran into a similar problem with computational complexity when I tried to see if I could make a Semidecidable typeclass for deciding things like < on real numbers. But, what prevents us from just "storing" the result of running the computation for n steps so that when you want to later run it for n+k steps you can skip the first n?

[Mario Carneiro]

I think we need mutable quotients for the storage part to work, unless you use a monadic representation

[Niels Voss]

Oh, so the problem is not with Computation, but with Divergence

[Mario Carneiro]

no, this is something else

[Mario Carneiro]

the idea of mutable quotients is that you can modify values in place (not just returning the new value, actually changing the input and returning nothing) as long as there is a quotient that hides the fact that you did anything

[Mario Carneiro]

Lean supports only one specific mutable quotient, namely Thunk

[Mario Carneiro]

which is effectively Thunk A = MutQuot (A + (Unit -> A)) where the quotient relation is inl a ~ inr (fun _ => a)

[Niels Voss]

I was about to ask if it was related to Thunk. So right now, Computation doesn't use quotients, but if we wanted to speed it up to better time complexity, we would need a MutQuot?

[Mario Carneiro]

right

[Mario Carneiro]

you might be able to do it with nested Thunks if you are sufficiently clever

[Niels Voss]

I feel like this is something which could be implemented within Lean code, probably by using something like IO.Ref. But it would increase the trusted codebase for the compiler

[Mario Carneiro]

I think there is a haskell library that does something like that (although since it's haskell the thunks come for free)

[Mario Carneiro]

IO.Ref (or ST.Ref) would still need monads though

[Mario Carneiro]

and you would lose the ability to reason about the object

[Niels Voss]

I mean in theory I think there's' a way to run IO code in an unsafe block that isn't monadic. I don't think this is a good idea though

[Mario Carneiro]

That's ST, it's already in lean

[Mario Carneiro]

but it's still monadic at the point where you do the writes

[Mario Carneiro]

so it's not really possible to hide the refs away in an encapsulation in a library

[Niels Voss]

I guess what I don't understand is that if Computation is a Nat -> (Option _) behind the scenes, why can't we just run for n steps, check if it has terminated, and then start our next run at n+1

[Mario Carneiro]

you can, the trouble is that the f : Nat -> Option A in question also has its own state, and when you call f n and later f (n+1), those two calls are independent and f will have to run through n+1 steps of computation in the second call even if the first n steps are the same as the prior call to f n which has been forgotten

[Mario Carneiro]

for example, imagine f is running a turing machine for n steps, those two calls will independently build the machine and step through n or n+1 steps

[Niels Voss]

Ohhh that makes more sense. So it isn't so much that every Computation suffers from this poor time complexity, but that most practically usable Computations will be recursive and thus require recomputing, unless the intermediate results are memoized somehow

[Mario Carneiro]

right

[Mario Carneiro]

and since the intended interface of Computation is the coinductive one, most Computations will be constructed using the corecursor, which is recursive

[Niels Voss]

How does this compare with the SafePart defined above (which I've repasted below):

import Mathlib.Data.PFun
set_option autoImplicit false

structure SafePart.{u,v} (α : Type u) where
  σ : Type v -- The type of auxillary data used by the computation
  current : σ
  next : σ → α ⊕ σ

partial def SafePart.run {α : Type*} [Inhabited α] (v : SafePart α) : α :=
  match v.next v.current with
  | .inl a => a
  | .inr s => SafePart.run ⟨v.σ, s, v.next⟩

def SafePart.toPart {α : Type*} (v : SafePart α) : Part α :=
PFun.fix (pure ∘ v.next) v.current
-- Number of steps for hailstones/Collatz conjecture
def countSteps (n : Nat) : SafePart Nat where
  σ := Nat × Nat
  current := (0, n)
  next := fun (steps, k) =>
    if k ≤ 1 then .inl steps
    else if k % 2 = 0 then .inr (steps + 1, k / 2)
    else .inr (steps + 1, 3 * k + 1)

#eval SafePart.run (countSteps 211) -- 39

Does the extra state stored in SafePart help in any way?

[Mario Carneiro]

yes it does

[Niels Voss]

Of course, it requires a universe bump, which could be a problem

[Mario Carneiro]

SafePart is the representation that Computation would prefer to have

[Mario Carneiro]

but there is a universe issue

[Mario Carneiro]

not just that there is a bump, there is a second level argument

[Mario Carneiro]

you can't collect up a list of computations from different sources if they use types at different levels

[Niels Voss]

right, because if that argument goes up, more functions become computable. So for any given v, it will never encode all the computations

[Mario Carneiro]

The ideal coinductive interface lets you choose the level independently from the coinductive type itself, similar to how the recursor of an inductive type has an additional level argument

[Mario Carneiro]

we can accomplish that logically using this function of options representation, but we lose the good computational structure

[Niels Voss]

Maybe there's a way to memoize the intermediate results of Computation? Like if we instead had Nat -> Thunk (Option _) (not sure if that's sufficient)

[Mario Carneiro]

the fact that it's behind a function would make the thunk useless

[Mario Carneiro]

it would still get created anew even if you called it twice on the same n

[Mario Carneiro]

There is a HashMemo thingy in lean core IIRC but it's not suitable for reasoning

[Niels Voss]

Out of curiosity, how does https://github.com/alexkeizer/QpfTypes handle this problem?

[Mario Carneiro]

In the original QPF formalization, we did something similar to the Computation representation (but generalized to arbitrary coinductives)

[Mario Carneiro]

it basically suffers from the same tradeoffs

[Mario Carneiro]

I'm not sure about Alex's work, I'll take a look

[Mario Carneiro]

It seems to make use of mathlib's QPF library, which is a direct port of the lean 3 library in our paper

[Niels Voss]

So, to be clear, if MutQuot could be implemented (possibly requiring C++ code), then it would allow for optimal coinductive representations, and both fix the Computation and provide a tool that the ComputableReal project could use?

[Mario Carneiro]

the actual type definition is src#MvPFunctor.M, which hides some details in a coercion to function instance, but if you combine src#MvPFunctor.mp and src#MvPFunctor.Obj you see that it is a function from paths (the equivalent of Nat in Computation) to partial outputs

[Mario Carneiro]

yes

[Mario Carneiro]

and now you see why I've been frustrated that an easy PR which fixes the issue has been blocked for almost 2 years for no reason

[Niels Voss]

Is that https://github.com/leanprover/lean4/pull/2292 that you linked above?

[Mario Carneiro]

yes

[Matt Diamond]

were you given any rationale for why it was blocked? that sounds really annoying

[Shreyas Srinivas]

Can this divergence monad be used in the formalisation of the greedy method in the equational theories project?

[Mario Carneiro]

you can see everything I know on the issue itself

[Mario Carneiro]

I'm pretty sure it was killed by the P-low

[Shreyas Srinivas]

Shreyas Srinivas said:

Can this divergence monad be used in the formalisation of the greedy method in the equational theories project?

There we also have a semi decidable procedure where we backfill values in a function

[Mario Carneiro]

because the FRO priority mechanism not a fair scheduler, it will just starve anything which is not high prio

[Niels Voss]

This is going to sound like a stupid idea, but we just pass like a really, really large value into the fuel function?

[Mario Carneiro]

for real number computations, that's a bad idea, since various bits of the internal computation will make use of the fuel to decide how big to make the intermediates

[Mario Carneiro]

but for a plain corecursor application, that's usually a fine way to compute partial functions

[Niels Voss]

If the real number computations make use of the fuel to decide how large to make the intermediates, does that mean that even if we get a way to memoize intermediate results, it will have to recompute them anyways?

[Johan Commelin]

Yes:

Mario Carneiro said:

This is relevant for the recent Computable reals discussion, since computable reals are also morally a coinductive type and you don't want to have to redo the computation from the beginning again every time (although some real numbers need to be computed from scratch anyway since you have to adjust the bounds on various quantities)

[Niels Voss]

Would getting an efficient representation using the MutQuot and other approaches suggested here even help for the ComputableReals project, given that it has to recompute with different bounds anyways?

[Mario Carneiro]

This is not always the case though. Some exact real computations are just stream transformers and can make use of prior information, while others actually need to do some math on the target precision to decide what subcomputations to run, and these may or may not gain an advantage from caching. The papers Bas mentioned seem to indicate that in general it's important for caching to be a component of an efficient exact real computation system, although I'm sure the details matter

[Niels Voss]

To confirm, all this discussion is mainly relevant for compiled code, not kernel reduction, right? Afaik Thunk doesn't help in the kernel, so neither would MutQuot?

[Mario Carneiro]

that's right

[Mario Carneiro]

the kernel has completely different performance characteristics