Why is Stream' called Stream'?

Stream: mathlib4

[Ching-Tsun Chou]

Why is Stream' (https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Stream/Defs.html) called Stream'? I understand there is already a Stream type. But wouldn't Sequence or Seq be a more appropriate and informative name? Stream'.Seq can be called Sequence.Stream instead. Isn't the intuitive idea that a "stream" is a finite or infinite list?

[Violeta Hernández]

I'd love to get rid of these primed names. And I agree that Sequence would be more understandable to the average Mathlib user.

[Wrenna Robson]

Would agree with this. Primed names bad!

[Wrenna Robson]

I am not sure I love this definition of Steam' but it might be the simplest possible choice in the circumstances. IIRC the !proper" definition of this sort of type uses coinduction which Lean does not (?) support well?

[Ching-Tsun Chou]

In my automata theory development (#announce > Automata theory in Lean4 ), I use types of the form ℕ → X to model infinite words/sequences. I would like to use Strem', but am really put off by its awful name. I'm not sure coinduction is strictly needed, because the automata theory papers I've read just directly index into infinite (or finite) words in their definitions and proofs. This is not to say coinduction cannot be useful, but I think we should first have some evidence of its usefulness.

[Vasilii Nesterov]

Violeta Hernández said:

I'd love to get rid of these primed names. And I agree that Sequence would be more understandable to the average Mathlib user.

But we also have Stream'.Seq for possibly finite sequences :)

[Vasilii Nesterov]

Ching-Tsun Chou said:

In my automata theory development (#announce > Automata theory in Lean4 ), I use types of the form ℕ → X to model infinite words/sequences. I would like to use Strem', but am really put off by its awful name. I'm not sure coinduction is strictly needed, because the automata theory papers I've read just directly index into infinite (or finite) words in their definitions and proofs. This is not to say coinduction cannot be useful, but I think we should first have some evidence of its usefulness.

Coinduction for Stream'.Seq was very useful in my tactic #announce > New tactic: `compute_asymptotics` @ 💬

[Ching-Tsun Chou]

I suggest above that we rename Stream' to Sequence or Seq and Stream'.Seq to Sequence.Stream. I assume the informal notion of a "stream" means a finite or infinite sequence.

[Vasilii Nesterov]

I feel the opposite way: "stream" is infinite, "sequence" is possibly finite

[Ching-Tsun Chou]

I'm not sure that that agrees with Stream (without the prime):
https://leanprover-community.github.io/mathlib4_docs/Init/Data/Stream.html#Stream
I wouldn't mind if we rename Stream' to (for example) InfSeq. The current name Stream' is just confusing.

[Ching-Tsun Chou]

As it now stands, we have:

• Finite sequences: List
• Infinite sequences: Stream'
• Finite or infinite sequences: Stream'.Seq and Stream.
  It just doesn't make sense.

[Ching-Tsun Chou]

If anything should be called Stream', it should be what is currently Stream'.Seq.

[Niels Voss]

I wouldn't call it InfSeq, since to me Inf means "infimum"

[Ching-Tsun Chou]

Personally I prefer Sequence or even Seq. My suggestion of InfSeq was in response to Vasilii's comment. Another option is OmegaSeq or ωSeq.

[Yury G. Kudryashov]

Answering the question in the title, not the question "how should it be called?": it was called stream in Lean 3, but Lean 4 got something else called Stream, so we had to rename. Adding ' was the easiest way to go forward with porting Mathlib to Lean 4.

[Chris Henson]

Ching-Tsun Chou said:

Personally I prefer Sequence or even Seq. My suggestion of InfSeq was in response to Vasilii's comment. Another option is OmegaSeq or ωSeq.

Seq is maybe confusing because of docs#Seq

[Ching-Tsun Chou]

Yury G. Kudryashov said:

Answering the question in the title, not the question "how should it be called?": it was called stream in Lean 3, but Lean 4 got something else called Stream, so we had to rename. Adding ' was the easiest way to go forward with porting Mathlib to Lean 4.

That's really an unfortunate decision. If Stream'.Seq had existed when Stream was stream, the new Stream should have been called Sequence to be consistent with Stream'.Seq. Now we end up with a Stream' that's really not similar to Stream which in turn is more similar to Stream'.Seq.

[Ruben Van de Velde]

It was certainly a reasonable decision, if perhaps one with an undesirable outcome. Probably a PR to rename it (with deprecations) would be acceptable, if the new name is a significant improvement

[Vasilii Nesterov]

Stream' was probably named after Coq's Stream: https://rocq-prover.org/doc/v8.10/stdlib/Coq.Lists.Streams.html

[Vasilii Nesterov]

In Agda, our Stream' is also called Stream, but our Stream'.Seq is called Colist. That was the word I had been searching for when trying to find this type. I only came across it later, after I had already made my own version. So yes, discoverability is probably not great.

[Bryan Gin-ge Chen]

It doesn't seem like there are strong arguments in favor of the current name(s), so if someone would like to guide us to consensus on which new names we should go with, I agree that a PR would be welcome. In any case, improvements to docs to help discoverability (including mentioning alternative names / analogous types in other widely-used systems for basic definitions) are always welcome!

[Ching-Tsun Chou]

I suggested above that Stream' and Stream'.Seq be renamed to Sequence and Stream', respectively. Another option for the latter is Colist, as Vasilii pointed out.

[Ching-Tsun Chou]

If people feel strongly that Sequence should encompass both finite and infinite sequences, then Stream' can renamed to ωSequence.

[Vasilii Nesterov]

I usually see the coinductive type of infinite sequences referred to as a "stream" (Coq, Agda, Haskell, nlab). Could you point me to a source where the term ωSequence is used?

[Ching-Tsun Chou]

Your view is a programmer's view. In normal mathematics, the current Stream' is just called sequences, infinite sequence, or ω-sequences.

[Ching-Tsun Chou]

For example, the page attached below is taken from:
Thomas, Wolfgang (1990). "Automata on infinite objects". In Van Leeuwen (ed.). Handbook of Theoretical Computer Science. Elsevier. pp. 133–164.
automata on infinite words.pdf

[Ching-Tsun Chou]

As you can see, even in some parts of theoretical computer science, people talk about "words", "sequences", or "ω-sequences", and never use the word "stream".

[Snir Broshi]

Or ω-words

[Ching-Tsun Chou]

Renaming Stream' to ωWords would be fine with me. But I suspect the term "word" is more limited to automata theory and related fields than the more generic term "sequence".

[Vasilii Nesterov]

Is this type used in context of normal mathematics? I think most results about it treats this as a coinductive type. The only place where it's used outside Data is for continued fractions where it again represents a corecursive computation.

[Vasilii Nesterov]

My opinion is that we should treat Stream' as a coinductive type, and its definition as ℕ → α is just an implementation detail, since Lean doesn't support coinduction internally

[Ching-Tsun Chou]

As it now stands, Stream' is not defined coinductively. It is defined as sequences!
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Stream/Defs.html#Stream'

[Vasilii Nesterov]

Yes, because there is no way to define things coinductively in Lean

[Ching-Tsun Chou]

And I want to use it as sequences in my project on automata theory, where no one uses the term "stream".

[Vasilii Nesterov]

What does it give to you compared to using ℕ → α?

[Ching-Tsun Chou]

First, I don't want to reprove already proved theorems. Second, ℕ → α does not let me use the dot-notation.

[Vasilii Nesterov]

I think it's the right spelling when you need regular sequences and don't need coinduction, for example: docs#TopologicalSpace.denseSeq

[Ching-Tsun Chou]

I don't think how a data type is defined should be an issue at all. What matters is the API of the data type. I do want to use many of the existing APIs of Stream', like get, take, drop, append etc. I don't want to define a separate version of them and reprove the theorems. That defeats the whole point of having mathlib.

[Ching-Tsun Chou]

In fact, I've redefined and reproved quite a few of them in terms of ℕ → α:
https://github.com/ctchou/AutomataTheory/blob/main/AutomataTheory/Sequences/Basic.lean
I don't want to continue doing that. I want to use a better-named Stream' and contribute to its API.

[Ching-Tsun Chou]

By the way, even leaving aside the issue of whether "sequences' and "ω-sequences" are reasonable names, the way that the term "stream" is used in Lean is just inconsistent: Stream' is always infinite, but Stream and Stream'.Seq can be either finite or infinite. Why? If we consistently use "stream" to refer to infinite sequences (as in Rocq), that would be OK with me. But are we going to rename Stream (without the prime) to Colist or something else?

[Yury G. Kudryashov]

I've explained the source of this inconsistency above: Stream' and Stream'.Seq come from Lean 3 while Stream is a completely different concept introduced in Lean 4. You don't have to convince people that the current naming is bad (I guess, everyone involved agrees with this). You should convince people that the new names you propose are good.

[Ching-Tsun Chou]

I have already stated my reasons above. Sequence is a name any mathematician can understand and is literally what Stream' is currently defined to be. Stream'.Seq can be renamed to Stream' for its resemblance to Stream (without the prime).

[Vasilii Nesterov]

@Mario Carneiro What do you think as the author of these files?

[Yury G. Kudryashov]

@Ching-Tsun Chou Could you please summarize different proposals (pairs of new names for Stream' and Stream'.Seq) with main pros and cons?

[Ching-Tsun Chou]

My proposal is literally just 2 message above your message. I have stated it several times in this thread.

[Ching-Tsun Chou]

(deleted)

[Ching-Tsun Chou]

Namely, I propose that (Stream'. Stream'.Seq) be renamed to (Sequence, Stream').

[Yury G. Kudryashov]

There were other proposals in this topic. Some of them don't use ' in the names. Could you please explain what's wrong with them?

[Ching-Tsun Chou]

I'm not sure which proposal you are referring to. Please quote the message.

[Yury G. Kudryashov]

Here I'm trying to quote most messages that mention other names. It looks like you've discarded most of them. It would be nice if you summarize why they're worse than having Stream and Stream' in the library.

Ching-Tsun Chou said:

Personally I prefer Sequence or even Seq. My suggestion of InfSeq was in response to Vasilii's comment. Another option is OmegaSeq or ωSeq.

Ching-Tsun Chou said:

I suggested above that Stream' and Stream'.Seq be renamed to Sequence and Stream', respectively. Another option for the latter is Colist, as Vasilii pointed out.

Ching-Tsun Chou said:

If people feel strongly that Sequence should encompass both finite and infinite sequences, then Stream' can renamed to ωSequence.

Ching-Tsun Chou said:

Renaming Stream' to ωWords would be fine with me. But I suspect the term "word" is more limited to automata theory and related fields than the more generic term "sequence".

[Yury G. Kudryashov]

Also, I would wait for Mario before starting a PR that actually renames definitions.

[Ching-Tsun Chou]

My fundamental problem with the current naming scheme is that it does not make sense. I copy the definition of Stream' below:

/-- A stream `Stream' α` is an infinite sequence of elements of `α`. -/
def Stream' (α : Type u) := ℕ → α

Why is it called Stream', not simply Sequence or ωSequence (as its own comment points out)? How is it related to the Stream type without the prime?

As to Stream'.Seq, I suggest it be renamed Stream' because it is the type of sequences which can be finite or infinite and hence resembles Stream, so the prime will actually make some sense.

[Yury G. Kudryashov]

Generally, we're trying to avoid primes in the names, especially in type names. As I wrote above, you don't need to convince people that the current names are bad (assuming that Stream isn't going anywhere). Their purpose was to go ahead with porting, and they served this purpose. OTOH, if we're renaming them, then it's better to make sure that we won't rename them again in a few months. So, you should explain what do you think about, e.g., pros and cons of Sequence + Stream' vs Sequence + Colist.

[Ching-Tsun Chou]

OK, I propose that (Stream',Stream'.Seq) be renamed to (Sequence, Colist).

[Wrenna Robson]

I really like Sequence as a name for that (though I do think having it be a one-element structure rather than literally a function might be good.

[Mario Carneiro]

My opinion is that the definition should be named Stream, that's why it was called stream in the first place. Lean 4 introduced another thing called Stream which IMO has less claim to the name, and they are already working on something else that seems likely to replace it, so I'm not sure how worthwhile it is to try to avoid the word in the first place. AFAICT setting aside lean 4 core issues there is no reason why the names of Stream and Seq should be swapped.

[Mario Carneiro]

I don't mind the name Colist as an alternative to Seq, but I think Seq/Sequence is a more common name. But Colist and Sequence should both be in the docstring for docs#Stream'.Seq

[Mario Carneiro]

And re: why is it not coinductive, it's about as coinductive as it can be. There is a commented out pretend coinductive declaration right next to the real declaration, and the entire API is coinductive-inspired. You won't find very many corec definitions in mathlib other than that one

[Markus Himmel]

Yes, it's likely that core will no longer need its Stream at some point, but if you want you can have the name even before then: lean4#10645

[Ching-Tsun Chou]

First, I think dropping the prime from Stream' would already be a big improvement, especially if the current Stream can be done away with and there is no confusion about whether "streams" refer to both finite and infinite sequences or only infinite sequences.

Second, I do not understand why "stream" is an appropriate name for infinite sequences. I searched the PDFs of quite a few mathematical textbooks on my drive. Almost all of them talk about sequences (Cauchy sequences, for instance) and none of them even contains the word "stream". In fact, the only exception I can find, Moschovakis's "Notes on Set Theory", defines "streams" to comprise both finite and infinite sequences, as you can see from the excerpt attached below:
p84-of-notes-on-set-theory.pdf
So, why is "stream" an appropriate name for plain, old infinite sequences?

Third, even if infinite sequences can be viewed as a coinductive datatype, is there anything wrong with the naive view of thinking of them as plain, old infinite sequences? Even List, which is defined inductively, also has APIs which basically view a list as a function on the domain Fin n (where n is the length of the list) , such as ofFn and the various flavors of get, and you can prove properties about List using them without ever thinking about induction at all.

[Mario Carneiro]

There is a distinction one can make between a stream and an infinite sequence. An infinite sequence is a map Nat -> A which is indexed i.e. $a_0,a_1,\dots$. You will often see these showing up in mathematics, e.g. taking the limit of a sequence in topology, or summing an infinite sequence. A stream is a coinductive data structure which you can pull elements from, it has a head and a tail. These come up in CS contexts, such as stream algorithms or state machines. It happens that these two types are isomorphic, but the APIs for them are not the same, and maybe one day Stream will get the data representation overhaul it's always yearned for when the compiler is ready for it, at which point they will have to be different types.

[Ching-Tsun Chou]

I'm not sure I understand this argument. I have already given the example of List. On the one hand, List is an inductive datatype. On the other hand, a list can be viewed as a function with a Fin domain (in other words, it is a finite sequence). Are you arguing that these two APIs should be on two different types, instead of sharing the same type List? What's the advantage in doing that?

In the past few days, I ported my automata theory project:
https://github.com/ctchou/AutomataTheory
from using ℕ → _ to represent infinite sequences to using Stream' _, because there is really no point in defining my own versions of Stream'.appendStream' and Stream'.drop (which I use a lot) and I want to use the dot-notation. I was pleasantly surprised by how easy the porting was. In my theory I never thought of infinite sequences as a coinductive datatype (after all, I was using ℕ → _). But the presumably "coinductive style" API of Stream' still works. So, even if Lean acquires the capability to do proper coinductive definitions in the future, why do you want to have a separate type which you know is isomorphic to infinite sequences?

For an analogy, consider the real numbers. You can define them using Cauchy sequences or using Dedekind cuts (and perhaps other means). Do you want to have two versions of the reals depending on how they are defined?

[Violeta Hernández]

I agree. What's stopping us from just defining all the Stream' API for ℕ → α? We lose dot notation, sure, but then we don't have to bikeshed about names.

[Ching-Tsun Chou]

That's what I was doing. But after a while I realized that it was just silly to repeat stuffs that are already in the Stream' API and the dot-notation really helps to make expressions readable and beautiful. I started this bike-shedding thread because I could not figure out why an exotic name "stream" was given to something that's called "sequence" in every mathematical text I've read.

[Mario Carneiro]

Ching-Tsun Chou said:

I'm not sure I understand this argument. I have already given the example of List. On the one hand, List is an inductive datatype. On the other hand, a list can be viewed as a function with a Fin domain (in other words, it is a finite sequence). Are you arguing that these two APIs should be on two different types, instead of sharing the same type List? What's the advantage in doing that?

It's basically the same reason Array A and List A exist as separate types even though they are isomorphic. If there is a difference in data representation then there has to be a separate type

[Mario Carneiro]

Ching-Tsun Chou said:

For an analogy, consider the real numbers. You can define them using Cauchy sequences or using Dedekind cuts (and perhaps other means). Do you want to have two versions of the reals depending on how they are defined?

If we had both versions, yes they would be separate types and we'd prove they are isomorphic

[Mario Carneiro]

If you just want a Nat function, you should not be using Stream'. This is (minor) abuse of the type and things will probably be more complicated if/when it becomes properly coinductive.

[Mario Carneiro]

the fact that Stream' is implemented as a nat function is an implementation detail

[Ching-Tsun Chou]

@Mario Carneiro, I find what you wrote above very surprising. The distinction between Array and List is meaningful only when Lean code is run as a computer program. Here we are proving theorems involving infinite sequences, not writing or reasoning about computer programs. Why should we care about the internal implementation of a datatype once the appropriate API has been defined and proved?

As it happens, there is an alternative implementation of the reals , Bourbakiℝ, in mathlib:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/UniformSpace/CompareReals.html
If I now re-prove a bunch of analysis theorems in terms of Bourbakiℝrather than ℝand submit a mathlib PR, will you approve that PR?

Furthermore, to follow your own logic, since the internal implementation matters, you should have agreed with me in the first place that the current Stream' should be renamed Sequence (because it is literally implemented as sequences) and the name Stream should be used only after the appropriate coinductive implementation is in place. Isn't that so? (If in the future coinduction is used to define executable infinite list in Lean, then I would agree completely that it should be called Stream, but not before it is actually done.)

[Mario Carneiro]

Yes, Stream' is intended to be a computational data type that can be used in programs

[Mario Carneiro]

Ching-Tsun Chou said:

you should have agreed with me in the first place that the current Stream' should be renamed Sequence (because it is literally implemented as sequences) and the name Stream should be used only after the appropriate coinductive implementation is in place. Isn't that so?

No, because API changes are more disruptive than internal implementation changes. Keep in mind that stream has been around with the same API since lean 3, and there have been many many implementation detail changes since then. Changing the API to track the internal changes would only make it that much harder to keep up with lean. Suffice it to say, Stream' is a coinductive API for a type which is awaiting compiler support. If you use it today you will face performance issues but those issues can at least be reported as a bug and tracked, whereas if we were to pretend that Stream was intended to be natural number functions all along then there would be no issue to track in the first place. (And there would also be a good chance that people would argue that there is no need for the Sequence type since it is just a wrapper around functions with no API changes so we would end up with nothing at all.)

[Mario Carneiro]

Also, Stream is one in a family of definitions including Stream'.Seq and Stream'.WSeq which are also coinductive types but require more complicated simulations using subtypes of functions. These types are intended to work together and it would be awkward if one of them was missing.

[Ching-Tsun Chou]

Are you saying that I should define my own Sequence type to wrap ℕ → _ and duplicate all relevant theorems from Stream' on it? I do want to use the dot-notation and follow the same naming convention as List and Stream'.

[Mario Carneiro]

Yes, if you want. Obviously that would need to go through review if you want it in mathlib, I have already foreshadowed some critiques I can predict

[Mario Carneiro]

You can use dot notation on functions BTW, you put them in the Function.* namespace

[Mario Carneiro]

You could also put them in Sequence.Function.*; I think if you open Sequence then that will also work as dot notation for functions

[Ching-Tsun Chou]

But does it make sense to define API functions like take, drop, extract, append on general functions?

[Mario Carneiro]

the latter approach avoids that issue since it's namespaced so it only works when you open the scope

[Mario Carneiro]

but the reason I suggest that is because mathlib already uses sequences all over the place and the official spelling for sequences is to use unadorned function types

[Ching-Tsun Chou]

Still, a new namespace does not force the domain of a function to be N.

[Mario Carneiro]

I know it's not a perfect solution, I think we both understand the pros and cons of the options here

[Mario Carneiro]

if you can live without dot notation you can also just have reasonably named free functions

[Mario Carneiro]

but if you insist on a new type then you will have to deal with conversion to and from functions for all the places where people use functions to mean sequences (or specialize a theorem about functions to sequences)

[Mario Carneiro]

and it's not even the case that all sequences are indexed by Nat, some are Int or Ordinal or whatever

[Mario Carneiro]

I'm not sure it can actually be interpreted as anything other than "word mathematicians like to use for functions on a discrete domain"

[Ching-Tsun Chou]

I was using naked ℕ → _ functions and I ended up not liking it. In particular, I want to re-use names like take, drop, extract, append and keep their approximate meanings. (After all, infinite sequences have many similarities to finite ones.)

One option is to call the new type OmegaWord or ωWord to avoid entanglement with the many meanings of "sequence" in normal math.

[Mario Carneiro]

Seems fine to me. I will abstain from making an editorial decision on whether that should be in mathlib, but if it works for you and you can argue your case then great

[Mario Carneiro]

...append?

[Mario Carneiro]

what does it mean to append two infinite sequences

[Aaron Liu]

probably append a finite sequence at the front of an infinite one

[Ching-Tsun Chou]

Sorry, I was being brief: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Stream/Defs.html#Stream'.appendStream'

[Yury G. Kudryashov]

(deleted)

[Violeta Hernández]

Mario Carneiro said:

It's basically the same reason Array A and List A exist as separate types even though they are isomorphic. If there is a difference in data representation then there has to be a separate type

As I understand it, Array is internally backed by an array, while List is internally backed by a linked list. That is the only difference, and from a theorem proving perspective both types are exactly the same.

[Violeta Hernández]

Ching-Tsun Chou said:

For an analogy, consider the real numbers. You can define them using Cauchy sequences or using Dedekind cuts (and perhaps other means). Do you want to have two versions of the reals depending on how they are defined?

Funny you mention this, since one of my PRs introduces the Dedekind completion to Mathlib! Of course, the only theorem I'm really interested in proving about DedekindCut ℚ is that it's order-isomorphic to ℝ. It seems like a complete waste of time to reintroduce all the API about arithmetic just to prove that the fields end up isomorphic.