Infinite, lazy stream

Stream: general

[Mark Christiaens]

I'm trying to make an infinite, lazy stream of constant values:

inductive MyStream.{u} (α : Type u) where
  | inf (a : α) (t : Unit -> MyStream α) : MyStream α

def constStream.{u} {α : Type u} (a : α) : MyStream α :=
  MyStream.inf a (fun () => constStream a)

Lean rejects this:

fail to show termination for constStream

I've tried some variants but I fail to get this right. Any suggestions?

[Vasilii Nesterov]

Lean doesn't allow infinite recursion, and you can't create "infinite objects" using just inductive types. What you need is a coinductive type and a corecursive function. Lean's kernel doesn't support such types directly, but they can be modeled using functions. For infinite streams, see docs#Stream'.

[Robin Arnez]

You can add partial to constStream (as long as you don't care about proving stuff). Also, MLList works well as a monadic lazy list (import Batteries.Data.MLList.Basic, again, forget about proving stuff).

[Robin Arnez]

If you do care about proving things, then Nat -> α (under the mathlib alias Stream'). However note that that gets rid of good performance

[Paul Reichert]

Another alternative would be to make the state of the stream explicit and to carry around a transition function on the state type:

structure MyStream (α : Type u) where
  σ : Type u
  value : α
  state : σ
  nextInternal : σ → α × σ

def MyStream.next (s : MyStream α) : MyStream α :=
  let p := s.nextInternal s.state
  ⟨s.σ, p.1, p.2, s.nextInternal⟩

def constStream (a : α) : MyStream α where
  σ := PUnit
  value := a
  state := .unit
  nextInternal _ := (a, .unit)

This way you get relatively efficient streams that you can actually prove things about. You can think of it as a bundled version of the docs#Stream typeclass together with its state type.

(Note that constStream is stateless, so it doesn't use any state, but sigma is there to accomodate cases where your stream does have some state.)

The main downside of this approach is that MyStream α lives in Type (u + 1), not Type u like α. If you can live with that and are fine with having to explicitly provide some state type and transition function when creating a stream, this might be an option.

[Mark Christiaens]

Making the state explicit works! Thanks.

Could you explain a bit more about why this does work and my attempt did not?

Maybe first about my attempt. My reasoning was this. In Lean, I cannot make types that would have infinite terms (since it's a strict language). So, let's make a type that holds one value and a way to continue generating more values from that. That will require 2 fields: a value and function. Seems fine to me. Also, it's not "infinite recursion": the function that is embedded is not executed until I fetch another value. Seems fine to me too.

So it seems that Lean is fundamentally not happy with me using the _type_ recursively. Is that because it would break the proof system?

I tried making my function partial:

  inductive MyStream.{u} (α : Type u) where
    | inf (a : α) (t : Unit -> MyStream α) : MyStream α

  partial def constStream.{u} {α : Type u} (a : α) : MyStream α :=
    MyStream.inf a (fun () => constStream a)

But then Lean4 complains about:

failed to compile 'partial' definition 'Attempt2.constStream', could not prove that the type
  {α : Type u} → α → MyStream α
is nonempty.

So then I thought, let's try to convince Lean that this type is nonempty.

instance [Inhabited α]: Inhabited (MyStream α) where
  default := .inf (default : α) (fun () => default)

Lean doesn't like that:

failed to synthesize
  Inhabited (MyStream α)

From a logical point of view, that kind of makes sense to me. I'm trying to convince Lean that my type is nonempty through a circular reasoning. That indeed is nonsense.

So I guess that my question is whether I'm right in thinking that the fundamental problem is that I cannot prove the nonemptiness?

And a related question, how come the solution with the explicit state field doesn't suffer this nonemptiness faith?

As another data point, I've added a nil constructor to MyStream. So MyStream is definitely inhabited.

  inductive MyStream.{u} (α : Type u) where
    | inf (a : α) (t : Unit -> MyStream α) : MyStream α
    | nil
  deriving Inhabited

  partial def constStream.{u} {α : Type u} (a : α) : MyStream α :=
    MyStream.inf a (fun () => constStream a)

This does compile. From this I conclude that using MyStream inside the definition of MyStream is allowed but it messes with termination checking (hence the need for the partial keyword).

So, I guess I'm a bit confused about what I'm fighting against here. Is it recursive types, nonemptiness, or the need for a higher universe?

[Aaron Liu]

Mark Christiaens said:

  inductive MyStream.{u} (α : Type u) where
    | inf (a : α) (t : Unit -> MyStream α) : MyStream α

This type is actually empty

[Aaron Liu]

import Mathlib.Logic.IsEmpty

inductive MyStream.{u} (α : Type u) where
  | inf (a : α) (t : Unit -> MyStream α) : MyStream α

instance {α : Type u} : IsEmpty (MyStream α) where
  false := MyStream.rec fun _ _ ih => ih ()

[Paul Reichert]

Mark Christiaens said:

So, I guess I'm a bit confused about what I'm fighting against here. Is it recursive types, nonemptiness, or the need for a higher universe?

When you write down your inductive definition for MyStream, MyStreamas a type is a type such that:

• there is a function MyStream.inf : {α} -> (a : α) (t : Unit -> MyStream α) : MyStream α,
• MyStream.inf is injective in the sense that each pair (a, t) produces a different element in MyStream α ("no confusion"),
• and (since inf is the only constructor available,) every element of MyStream α can be obtained from MyStream.inf -- in other words, MyStream.inf is surjective.

In a somewhat hand-wavy way, this is a fixpoint equation for the type MyStream α, but most importantly, it defines MyStream with reference to itself. Such "impredicative" definitions are tricky because it's neither clear that such a type MyStream α exists nor that it is unique in any way.

some examples for fixpoint problems

In general, a fixpoint of a function F is some x such that F x = x.

• If F : Nat -> Nat, F x := x, then every x : Nat is a fixpoint, so there's no unique fixpoint.
• If F : Nat -> Nat, F x := x + 1, then there is no fixpoint because F x = x is always false.

In the case of inductive types, we are considering fixpoints of types, not numbers, but the basic problem is the same.

For inductive types that are allowed in Lean, there doesn't need to be a unique fixpoint, but there always exists one, and in face, there even exists a smallest fixpoint. Let's see what this means in practice.

Consider your original definition of MyStream:

inductive MyStream.{u} (α : Type u) where
  | inf (a : α) (t : Unit -> MyStream α) : MyStream α

I claim that the empty type (False) satisfies our fixpoint conditions:

• MyStream.inf : {α} -> (a : α) -> (t : Unit -> False) -> False is easy to construct as inf a t := t (). (This is more or less what Aaron did to show that MyStream is empty.)
• MyStream.inf is bijective, since there are no pairs (a, t) and there are no elements x : False, in both cases because False is empty.

However, the fixpoint solution you apparently hoped for is that of infinite streams. To see that it also satisfies the fixpoint conditions, let's model it (inefficiently) as MyStream α := Nat -> α:

First, define:

MyStream.inf (a : α) (t : Unit -> Nat -> α) (n : Nat) := match n with
  | 0 => a
  | m + 1 => t () m

Also in this case, inf is bijective! So the fixpoint equation implied by the definition isn't unique.

In order to make MyStream well-defined, inductive types in Lean are always the smallest possible fixpoint -- in this case, the empty type. Note that Lean is totally capable to construct coinductive types "by hand", for example as Nat -> α, and there doesn't seem to be anything about Lean's type theory that would make coinductive types impossible. However, in practice, Lean lacks built-in support for them in analogy to inductive types and it can sometimes be hard to construct them in an efficient and convenient way.

The higher universe is also just an artifact of practical limitations: From the type theory perspective, Nat -> α is a perfectly valid model of your coinductive type, it's just not efficient. In contrast, my construction is more efficient but requires a universe bump. Right now there doesn't seem to be a way to achieve both goals at once (except for the case of coinductive predicates!).

relation to termination conditions

I think that the termination requirement that you walked into ensures that the constructed element is actually contained in your inductive (smallest-fixpoint) type.

For simplicity, let's first consider Nat.

inductive Nat where
  | nil : Nat
  | succ : Nat -> Nat

Since Nat is the smallest possible fixpoint, we need to be stingy with regard to elements of Nat -- only those elements that must exist are allowed.

1. Using the first constructor, 0 = Nat.nil definitely exists.
2. Using the second constructor and (1.), 1 = Nat.succ 0 definitely exists.
3. Using the second constructor and (2.), 2 = Nat.succ 1 definitely exists.
4. ...

The important thing to note is that "circular reasoning" isn't allowed: (3.) cannot refer to (3.) itself, it can only refer to (2.). Otherwise, we could say (perhaps a bit hand-wavy, but this is the idea):

(inf) Using the second constructor and (inf), \inf = Nat.succ \inf definitely exists.

But Nat definitely should not contain infinity since it's the smallest-possible fixpoint. Hence we also need to forbid the following definition, which is similar to your constStream definition:

def infiniteNat : Nat :=
  Nat.succ infinite_nat

The termination checker tries to find a "termination measure" that strictly decreases with every recursive call and that is well-founded: There's no infinite decreasing sequence w.r.t. the termination measure. This decreasing condition can be thought to ensure that we never construct an element of an inductive type in a circular way like with infiniteNat and (inf). But you can also think of this check as a termination check: Since the well-founded termination measure decreases with every recursive call, the recursion must end after finitely many steps.

</wall of text>

I hope this was readable and helps a bit to understand the fundamental problem with defining MyStream as an inductive type.

[Vasilii Nesterov]

Mark Christiaens said:

Also, it's not "infinite recursion": the function that is embedded is not executed until I fetch another value. Seems fine to me too.

When you define a function foo recursively, i.e., referring to foo in its own body, the definition is valid only if, in each recursive call, the arguments passed to foo decrease in some sense.

In your definition above, constStream a "calls" constStream a, which is not allowed. I'm putting "call" in quotes here because it has nothing to do with the actual computation; it's just a syntactic thing here.

[Vasilii Nesterov]

partial and nonemptiness are a completely different matter here. The partial keyword is used when we don't want to prove anything about the function being defined—we only need to use it for computations. When partial is used, Lean only requires a proof that the target type of the function is inhabited, because no function can exist with an empty target type (since such a function would immediately lead to a contradiction, allowing one to prove False). Then function becomes opaque from a logical point of view: you can use it in computations, but you can't reason about it or prove properties of it within Lean's logic.