Is there a better definition of L^ω ?

Stream: computer science

[Ching-Tsun Chou]

Let L : Set (List A) be a "language" in the automata theory sense, where A : Type*. We can define L^ω : Set (ℕ → A) to be the set of infinite sequences each of which is an infinite concatenation of words from L:

L^ω := { as : ℕ → A | ∃ φ : ℕ → ℕ, StrictMono φ ∧ φ 0 = 0 ∧ ∀ m, as ⇊ (φ m) (φ (m + 1)) ∈ L }

where as ⇊ i j is the finite word consisting of as i, as (i + 1), ..., as (j - 1). (That is, ⇊ is the analogue of List.extract for infinite sequences.). The above definition works and I've proved quite a few results involving it in my automata theory development (see https://github.com/ctchou/AutomataTheory). But I've found that it is very, very painful to work with the above definition. For example, I'm now trying to prove the intuitively obvious result:

(L∗)^ω = L^ω

where L∗ is the Kleene-star of L. I'm finding the going very tough and unpleasant. Hence my question: Is there a better and more usable definition of L^ω? I have not been able to think of any.

[Matt Diamond]

ah, so φ basically lists the indices of the "stitches" (so to speak) in the concatenation for each sequence

[Matt Diamond]

or even simpler, it just lists the starting indices for each concatenated word

[Matt Diamond]

yeah, it does seem a bit difficult to express "as is an infinite concatenation of finite lists"

[Ching-Tsun Chou]

Yes, that's right. The L^ω ⊆ (L∗)^ω direction is easy to prove. But the other direction (L∗)^ω ⊆ L^ω is nasty and I can't think of an alternative definition or an intermediate lemma to make it easier.

[Ching-Tsun Chou]

Toward the end of this file:
https://github.com/ctchou/AutomataTheory/blob/work-1/AutomataTheory/Languages/Basic.lean
you can find my current incomplete proof. It is not pretty and I had to use notions and results from this file:
https://github.com/ctchou/AutomataTheory/blob/work-1/AutomataTheory/Sequences/Segments.lean
which are rather unwieldy, although the intuitive idea is very simple.

[Matt Diamond]

btw, not sure if you're aware but a lot of the sequence API you've written is also covered by docs#Stream'

[Matt Diamond]

(if you wanted to create your own API that's fine too, just thought I would mention it)

[Ching-Tsun Chou]

Yes, I've looked at Stream' and may change my code to use it later. But as far as I can tell, Stream' does not have the sort of results that I use. In particular, Stream' seems to try hard to avoid talking about explicit indices, while I need to directly reason about indices all the time (which is why the omega tactic is used all over the place in my code).

[Ching-Tsun Chou]

BTW, why is it called Stream'? Wouldn't Sequence be a better name? This is especially confusing when there is also Stream which is different from Stream'.

[Matt Diamond]

yeah I have no idea, it was called stream in mathlib3

[Matt Diamond]

and then of course there's docs#Stream'.Seq which is referred to as a "sequence"

[Matt Diamond]

to be fair, getting terminology right can be hard

[Matt Diamond]

one thought would be to have φ be a list of word lengths rather than indices, from which you could then derive the indices by summing up previous lengths... however, I have no idea if that would make things harder or easier

[Matt Diamond]

I only know that it would remove the need for the StrictMono and φ 0 = 0 requirements

[Matt Diamond]

but the lists would contain the same information, so it probably wouldn't buy you anything

[Ching-Tsun Chou]

I doubt it. The difficulty in the proof of (L∗)^ω ⊆ L^ω is that the LHS has two levels of indices (or lengths) and it is a pain in the *** to somehow "flatten" them into a single level when one can't use a recursive formulation of the flattening operation. (At least I don't know how to do that.)

[Ching-Tsun Chou]

Imagine that we want to prove (L∗)∗ = L∗. One could define the Kleene-star L∗ using a definition like that for L^ω. (Indeed, there is a theorem IterStar_seg_exists in Languages/Basic.lean showing you how that can be done.). But we probably won't use that approach. Instead, we will try to exploit the recursive definition of L ^ n and do an inductive proof. It would be nice if I know how to do that with L^ω.

[Thomas Waring]

Ching-Tsun Chou said:

It would be nice if I know how to do that with L^ω.

I think the equivalent version for L^ω would be a coinductive definition, but that's a guess based on the fact that infinite streams over A are a final coalgebra for the functor

$$X \mapsto A \times X$$

Lean support for coinduction is I think fairly nascent so this might not help even if it is true.

[Aaron Liu]

The docs#Stream' API should have some coinductive things

[Aaron Liu]

docs#Stream'.head docs#Stream'.tail docs#Stream'.corec

[Dexin Zhang]

I guess it will be nicer if we create APIs and lemmas on (ℕ → List α) → ℕ → α

[Ching-Tsun Chou]

Aaron Liu said:

The docs#Stream' API should have some coinductive things

It would be great if someone can show me how to define L^ω using the Stream' API. I looked at the API and it is not clear to me how to do so. In fact, we can start with something even simpler: the concatenation of a language of finite words and an ω-language of infinite words:

def ConcatInf (L0 : Set (List A)) (L1 : Set (ℕ → A)) : Set (ℕ → A) :=
  { as | ∃ al0 as1, al0 ∈ L0 ∧ as1 ∈ L1 ∧ as = al0 ++ as1 }

where ++ is a notation for appending a finite word and an infinite word:

def AppendListInf (xl : List X) (xs : ℕ → X) : ℕ → X :=
  fun k ↦ if h : k < xl.length then xl[k] else xs (k - xl.length)

If ℕ → A is replaced by Stream' A, can the Stream' API be used to define the above?

[Ching-Tsun Chou]

I can see how to define AppendListInf using the Stream' API by recursing on the first argument, but I don't see how to do ConcatInf. How do you get the existential quantifiers?

[Aaron Liu]

What's wrong with ConcatInf?

[Ching-Tsun Chou]

Nothing wrong with it. But if the Stream' API is limited to defining AppendListInf and everything else is kept the same, then I don't see how the Stream' API is going to improve the definition of L^ω.

[Aaron Liu]

I didn't say it was going to improve anything I just mentioned about the coinductive things

[Matt Diamond]

I believe AppendListInf already exists as docs#Stream'.appendStream'

[Matt Diamond]

(and it comes with the ++ₛ notation which is nice)

[Ching-Tsun Chou]

Thanks for pointing it out. I'll use it if I ever switch to using Stream'.

[Ching-Tsun Chou]

I finished the proof of (L∗)^ω = L^ω. It's not pretty, but it works:

https://github.com/ctchou/AutomataTheory/blob/f209ad388f87c737598cb59376a17157c077e34d/AutomataTheory/Languages/Basic.lean#L259