Efficient coinduction

Stream: general

[Paul A. Reichert]

I'm currently toying around with implementing a small functional reactive programming library in Lean (similar to Yampa).
To do this, I need a coinductive type representing a "signal function", i.e. a nonterminating infinite computation, taking an input and returning an output and a successor signal function. Conceptually, using coinductive types,

codata SF (α β : Type) : Type
| succ : (α → β) → (α → SF) → SF

I was able to translate this into actual Lean code and the above code directly works with Jeremy Avigad's Quotients of Polynomial Functors library.

However, my own implementation and the referenced one both do not seem to meet two reasonable performance requirements:

• inserting n inputs should cost O(n) time
• if I pass an input to a signal function, store its succeeding signal function and forget the original one, the old one should be deleted to avoid memory leaks when the program runs for an indefinite time.
  At least I believe so. For example, using Jeremy Avigad's library, I analyzed the performance of a signal function that counts tt boolean inputs using trace in the accumulation function. The following code is just for reference, you can safely skip it if my problem is clear without it -- I'm more interested in ways to construct this coinductive type efficiently, meeting the above criteria.

def output {α β} (s : stream α β) (a : α) : β :=
begin
  refine stream.cases_on s _,
  exact λ f _, f a,
end

def succ {α β} (s : stream α β) (a : α) : stream α β :=
begin
  refine stream.cases_on s _,
  exact λ _ f, f a,
end

def succ_many {α β} : stream α β → list α → stream α β
| s [] := s
| s (a :: as) := succ_many (succ s a) as

def fold {α β : Type} (f : β → α → β) (init : β) : stream α β :=
stream.corec α β β (λ b, stream.shape.succ (f b) (f b)) init

def accumulator : stream bool ℕ := fold
  (λ ctr e, trace "Hi" (ite (e = tt) (ctr + 1) ctr)) 0

-- This prints too many "Hi"s!
#eval output (succ_many accumulator [tt, tt, tt, tt]) tt

Here is what I myself came up with (in Lean 4):

def multiInput (α β : Type) : Nat → Type
| Nat.zero => α → β
| Nat.succ n => α → multiInput α β n

def SF (α β : Type) := ∀ n : Nat, multiInput α β n

def succ {α β : Type} (s : SF α β) (a : α) : SF α β :=
λ n => s (n + 1) a

def output {α β : Type} (s : SF α β) (a : α) : β := s 0 a

The problems are the same as with the previous construction.

If anyone had an idea how to do this more efficiently, I'd be very happy. (I believe general to be the correct category because it's not about program verification, I hope I'm right...)

Edit: Although it won't resolve the memory leak issue, memoization, if it is possible in Lean, may help with the first issue.

[Paul A. Reichert]

I guess I found a solution using quotient types that basically takes the corecursion property as the definition. For those that are interested in the details:

def SF' (α β : Type u) := Σ σ : Type, σ × (σ → α → β × σ)

namespace SF'

def output {α β} (s : SF' α β) (a : α) : β :=
  (s.2.2 s.2.1 a).1

def succ {α β} (s : SF' α β) (a : α) : SF' α β :=
  ⟨s.1, ((s.2.2 s.2.1 a).2, s.2.2)⟩

def succ_many {α β} (s : SF' α β) : List α → SF' α β
| [] => s
| a :: as => (s.succ a).succ_many as

def r {α β} (s t : SF' α β) : Prop :=
  ∀ as a, (s.succ_many as).output a = (t.succ_many as).output a

instance equivalence {α β} : Equivalence (@r α β) :=
⟨λ _ _ _ => rfl, λ h _ _ => (h _ _).symm, λ h₁ h₂ as a => Eq.trans (h₁ as a) (h₂ as a)⟩

instance instanceSetoid (α β) : Setoid (SF' α β) := by
  exact Setoid.mk r equivalence

end SF'

def SF (α β : Type u) := Quotient (inferInstance : Setoid (SF' α β))
def SF'.quot (s : SF' α β) : SF α β := Quotient.mk' s

namespace SF

variable {α β γ σ}

def quotRecOn (s : SF α β) (f : SF' α β → γ)
  (h : ∀ s t : SF' α β, s ≈ t → f s = f t) : γ := by
  refine Quotient.hrecOn s f ?_
  intros s t hh
  rw [h s t hh]
  exact HEq.refl _

def output (s : SF α β) (a : α) : β := by
  exact s.quotRecOn (λ s' => s'.output a) (λ _ _ h => h [] a)

def succ (s : SF α β) (a : α) : SF α β := by
  refine s.quotRecOn (λ s' => Quotient.mk' (s'.succ a))
                 (λ _ _ h => Quotient.sound (λ as a' => h (a :: as) a'))

def corec (f : σ → α → β × σ) (init : σ) : SF α β := SF'.quot ⟨σ, (init, f)⟩

end SF

[Mario Carneiro]

Note that the QPF implementation was never intended for actual computation; it doesn't have the right properties for that. We had imagined that it would be replaced using some implementedBy tricks into something more like an ill-founded unsafe inductive type, but the work on this was never done, in part because a lot of it either depends on lean 4 or would need to be significantly redesigned for lean 4. So coinductive types are still on the "todo list" for lean 4 I would say

[Mario Carneiro]

One thing that I think we don't want to change is that coinductive types are not known to the kernel - they are only simulated using some tactic magic. I think there is still some work to be done to ensure that it is possible for user code to present an "inductive interface" that can interact correctly with all the builtin tactics, but most likely it won't actually see progress until we try to implement coinductive types for real