OmegaLanguage

Stream: CSLib

[Ching-Tsun Chou]

I started a PR cslib#92 on ωLanguage, which is the infinite-word analogue of Mathlib.Computability.Language. If anyone has a better idea for the definition of omegaPower, please let me know. One of my goals is to port the theorems in:
https://github.com/ctchou/AutomataTheory/blob/main/AutomataTheory/Languages/Basic.lean
some of which are pretty nasty to prove. I can definitely use some better ideas.

[Thomas Waring]

Is it true that L^ω = (L∗)↗ω? — that might not be easier to work with as a definition but it is at least cleaner (or seems so to me)

[Ching-Tsun Chou]

L^ω ⊆ (L∗)↗ω is certainly true, but I'm not too sure about the other direction. I'm working on an alternative definition of L^ω that uses an ωSequence version of flatten, in a manner analogous to how L∗ is defined in Mathlib.Computability.Language. We will see whether this makes the proofs easier

[Ching-Tsun Chou]

The PR cslib#92 for OmegaLanguage is now ready for review. The proofs of the harder results have been much improved relative to:
https://github.com/ctchou/AutomataTheory/blob/main/AutomataTheory/Languages/Basic.lean
We now have enough results about OmegaLanguage to start developing the theory of ω-automata.
CC: @Chris Henson , @Fabrizio Montesi

[Fabrizio Montesi]

That looks pretty good to me. I'd just like to point out this PR creates the Computability/Languages/ directory with this (containing Language and OmegaLanguage), which seems ok to me, in case anybody wants to comment on that.

[Chris Henson]

That did pass my notice, but I think it's fine? Maybe Languages.Languages is mildly confusing, but it's probably okay.

[Ching-Tsun Chou]

Actually the names of leaf files are in singular, not plural, forms. I expect Computability/Languages/ to get more files, such as OmegaRegularLanguage.lean.

[Pieter Cuijpers]

On a related note, I noticed there is now a LTS.$\omega$ Tr definition, but it looks more like a definition of an $\omega$-run to me than a $\omega$-transition. In comparison, the LTS.MTr definition looses the 'intermediate states' along a path, while the LTS.$\omega$ Tr definition keeps them. I think this is confusing.

Is there a place where we talk about runs/walks/whatever we should call it, instead of transitions?
And should this definition not go there?

(In the context of Zeno behavior, or in the context of Buchi-like automata, it makes sense to have an infinite series of transitions "end" in some final state. In that context, $\omega$ Tr would make sense to me.)

[Ching-Tsun Chou]

I don't have a strong view about the name. But we will need such a definition, whatever we choose to call it. For, in automata theory on infinite words, we need to express such notions as "some accepting states appear infinitely many times" and "the set of states that appear infinitely many times is such and such".

[Fabrizio Montesi]

My current vision is that all of the following might be relevant, long-term:

• LTS.Execution, which is the finite version of our current LTS.ωTr (using Lists instead of ωSequences). It models a finite sequence of transitions.
• LTS.MTr, basically what we have now. It's a multi-step transition from a state to another.
• LTS.OmegaExecution, which is our current LTS.ωTr. It's an (omega-)infinite sequence of transitions.
• LTS.ωTr, which is the LTS.MTr equivalent for OmegaExecution.

with theorems connecting all of these.

There's some thinking to do and I really wanted to unlock the link-up between LTS and the automata work, so in the spirit of 'good is better than perfect' I added LTS.ωTr and postponed thinking about this.

[Ching-Tsun Chou]

I'm not sure there is a useful infinite counterpart of LTS.MTr. LTS.OmegaExecution is useful. But once you get rid of the infinite sequence of states, I don't think what remains is very useful.

[Pieter Cuijpers]

Ching-Tsun Chou said:

I'm not sure there is a useful infinite counterpart of LTS.MTr. LTS.OmegaExecution is useful. But once you get rid of the infinite sequence of states, I don't think what remains is very useful.

My feeling as well. I think renaming the current LTS.ωTr to LTS.ωExecution and introducing LTS.Execution is a natural first step. (I'll put it on my todo list, so keep me posted if anyone wants to start on it as well.)

There are conceivable infinite counterparts of LTS.MTr, but those require that one comes up with a "cluster point" or "convergence point" of an infinite sequence of states. On metric or topological labeled transition systems, this is done. But without additional structure, indeed, it does not make sense (to me at least).

[Ching-Tsun Chou]

Actually it is not very clear what a definition for LTS.Execution should look like. Fabrizio and I thought about this but have not reached a definite conclusion. The closest thing we have now is the theorem LTS.MTr.exists_states in LTS/Basic.lean. Also, in PR cslib#249, we have a series of theorems relating LTS.MTr and LTS.ωTR in the section ωMultiStep in the same file.

[Fabrizio Montesi]

Here's the current status on that:

I have a local branch with a ready-to-PR proposal for Execution and related theorems. I never made a PR simply because I haven't found a use for it yet.

It looks like this:

/-- An execution is a (possibly-empty) sequence of transitions from a start state. -/
inductive IsExecution : State → List Label → List State → State → Prop where
  | refl {s : State} : IsExecution s [] [] s
  | stepL {s1 : State} {μ : Label} {s2 : State} {μs : List Label} {ss : List State} {s3 : State} :
    lts.Tr s1 μ s2 → IsExecution s2 μs ss s3 →
    IsExecution s1 (μ :: μs) (s2 :: ss) s3

This construction is similar to what people do in 'execution systems', where you have a start state and then a List (Label x State). However, @Ching-Tsun Chou and I discussed that working with such lists that pack together labels and states is a bit of a pain, so we've been sticking to having two lists (one for labels and one for states) instead.

In infinite executions (currently OmegaTr), the formulation is easier/more elegant because you just need two omega-sequences, as you don't need to cover the case where the execution has no transitions.

IsExecution comes with some basic properties and a correspondence to MTr:

/-- Correspondence between multistep transitions and executions. -/
theorem mTr_isExecution_iff : lts.MTr s1 μs s2 ↔ ∃ ss, lts.IsExecution s1 μs ss s2 := by grind

I'm not sure how to refactor, if at all, theorem MTr.exists_states if we introduce this. We need something like that to enable reasoning with indexes.

[Pieter Cuijpers]

I like that definition quite a lot! It solves some of the problems I've had in the past as well, at first sight.

I think, actually, that the correspondence theorem you now use is really the definition of LTS.MTr
I would just prove all the composition theorems on IsExecution first, and then derive them for LTS.MTr

In a few weeks time, I get four students who want to do a Lean4 project. I'm planning to leave it a bit open to them what kind of problems to take on, but such a refactoring could be part of the work? (No promisses, they also have to want it, and it has to be interesting enough from an educational point of view.)

[Pieter Cuijpers]

MTr.exists_states sounds like a connection to me between walks in a graph and executions over an LTS.
A walk in a graph would be a "list of edges" that are appropriately connected.
Each edge, in case of an LTS, is a transition.

[Fabrizio Montesi]

Well, an lts is essentially a graph -- with minimal assumptions (can have infinite states, have infinite edges getting out of a state, etc.). So MTr/IsExecution is a walk. In introduction to choreographies, I have a background chapter on inference systems where I use exactly graph walks as an example, because then it translates directly to an inference system for multistep transitions in lts.

[Fabrizio Montesi]

the key difference with MTr.exists_states is just ergonomics, iiuc, i.e., whether you wanna reason by structural induction on the walk or you wanna reason on the indexes of the 'list(s) of transitions'.

it might be that we can elegantly refactor the proofs that use MTr.exists_states to use IsExecution instead, but we should really check. :-)

[Ching-Tsun Chou]

Why not just take the right-hand side of LTS.MTr.exists_states as the definition of LTS.IsExecution? Namely:

def LTS.IsExecution (lts : LTS State Label)
    (s1 : State) (μs : List Label) (ss : List State) (s2 : State) : Prop :=
  ∃ _ : ss.length = μs.length + 1, ss[0] = s1 ∧ ss[μs.length] = s2 ∧
    ∀ k, ∀ _ : k < μs.length, lts.Tr ss[k] μs[k] ss[k + 1]

The current proof of LTS.MTr.exists_states already proves the → direction of mTr_isExecution_iff and a simple induction on ℕ will prove the ← direction. In general, I find it much more pleasant to work with explicit indices over ℕ than with custom inductive types, because Lean has very strong support for such reasoning in grind and omega tactics and also has an enormous library about Lists.

[Chris Henson]

I mentioned this in a review I just left, but could you explain to me this pattern of having existentials like ∃ _ : ss.length = μs.length + 1 ? It feels very odd for things whose type is in Prop.

[Ching-Tsun Chou]

The weird ∃ _ and ∀ _ patterns are there to enable Lean to automatically infer that all indexing operations in the expression are within bounds. Once you get familiar with it, it is very easy to use.

[Ching-Tsun Chou]

In informal math, you would write something like:

def LTS.IsExecution (lts : LTS State Label)
    (s1 : State) (μs : List Label) (ss : List State) (s2 : State) : Prop :=
  ss.length = μs.length + 1 ∧ ss[0] = s1 ∧ ss[μs.length] = s2 ∧
    ∀ k < μs.length, lts.Tr ss[k] μs[k] ss[k + 1]

But Lean is not smart enough (yet) to supply the in-bound proofs in this case.

[Chris Henson]

As I noted in the review for cslib#241 for the ∀ _ you can instead write ∀ k, (_ : k < μs.length) → ..., which I think is a bit more legible.

Not sure about the existential though. Is this sort of thing common upstream for proofs using indexing? It all seems to work fine, I just want to make sure we're doing whatever is most standard.

[Ching-Tsun Chou]

We can use whatever form that is considered standard. By Curry-Howard isomorphism, I suspect they are literally identical to Lean.

[Ching-Tsun Chou]

BTW, there is another advantage of using explicit list indexing over an inductive definition: the latter biases you toward doing induction from the left end of the list while the former doesn't. For example, in many automata theory textbooks, a multi-step execution is defined by induction on the right end of the list, which is the opposite of how induction on lists is typically done in Lean. So the translation from the textbook to the Lean code is not exactly straightforward. By using explicit list indexing, when you do an induction on ℕ, you can choose to decompose the list either on the left end or on the right end and you can always find appropriate API functions and theorems in mathlib to support your reasoning.

[Fabrizio Montesi]

Ching-Tsun Chou said:

Why not just take the right-hand side of LTS.MTr.exists_states as the definition of LTS.IsExecution? Namely:

def LTS.IsExecution (lts : LTS State Label)
    (s1 : State) (μs : List Label) (ss : List State) (s2 : State) : Prop :=
  ∃ _ : ss.length = μs.length + 1, ss[0] = s1 ∧ ss[μs.length] = s2 ∧
    ∀ k, ∀ _ : k < μs.length, lts.Tr ss[k] μs[k] ss[k + 1]

The current proof of LTS.MTr.exists_states already proves the → direction of mTr_isExecution_iff and a simple induction on ℕ will prove the ← direction. In general, I find it much more pleasant to work with explicit indices over ℕ than with custom inductive types, because Lean has very strong support for such reasoning in grind and omega tactics and also has an enormous library about Lists.

This was an idea I did consider, actually, also because it matches what we'd do for OmegaExecution (now called OmegaTr). I guess my main qualm for not doing it right now is that it looks a bit weird. I'll spend some more time trying to make it look what one would write on paper... I remember I had some problems making the proofs go through though -- probably connected to what you mention about grind and omega.

[Ching-Tsun Chou]

I should point out that a theorem like LTS.MTr.exists_states will always be needed, no matter how we define LTS.IsExecution, for the simple reason that we need to relate finite executions and infinite executions somehow. So my suggestion is that we may as well just use the RHS of LTS.MTr.exists_states as the definition. In fact, we can probably live without a definition for LTS.IsExecution at all. This is the situation now, and I don't feel we lack anything when proving theorems.

Having said all that, here's yet another possible definition of `LTS.MTr.exists_states: we can make the state sequence always infinite as follows:

def LTS.IsExecution (lts : LTS State Label) (μs : List Label) (ss : ωSequence State) : Prop :=
    ∀ k, (_ : k < μs.length) → lts.Tr (ss k) μs[k] (ss (k + 1))

theorem LTS.mTr_isExecution_iff :
    lts.MTr s1 μs s2 ↔ ∃ ss, lts.IsExecution μs ss ∧ ss 0 = s1 ∧ ss μs.length = s2 := by
  sorry

This way we can dispense with all the pesky assertions about the lengths of state sequences and related list indexing in-bound proofs, though we still need to reason about those about label sequences. Also note that lts.IsExecution μs ss doesn't need to mention s1 and s2, because they are simply ss 0 and ss μs.length. In the proof of the → direction of LTS.mTr_isExecution_iff we need to extend finite sequences to infinite sequence. But that would not be a problem because we can always repeat s1 forever. We probably should also prove theorems saying that lts.IsExecution μs ss depends only on the first μs.length + 1 states of ss, though my experience suggests that such theorems are never actually used in the development of automata theory.

[Fabrizio Montesi]

I managed to clean up the list stuff quite a bit. See cslib#258 for a possible definition of execution.

@Ching-Tsun Chou I agree that maybe we can do without, but it's nice to give it a name in theorems about it. We'll see how useful it can be though..

Anyway, if we go ahead with this, I should probably add to the PR a renaming of OmegaTr to IsOmegaExecution.

I'm using the Is-prefix because it might make sense to have a bundled version as well with 'methods' like 'start', 'final', 'labels', etc. But I don't wanna introduce that now, since I don't see any proof that needs it yet.

[Ching-Tsun Chou]

@Fabrizio Montesi I have commented on cslib#258. I think you want to include the beginning and ending states among the arguments of LTS.IsExecution. That will make the statements of several theorem shorter and prettier. (In particular, the condition ss.length = μs.length + 1 won't need to be mentioned again and again.)

I'm fine with renaming OmegaTR to IsOmegaExecution. But perhaps we can shorten Execution to Exec everywhere? I think we should not use the Greek letter ω for Omega, because it is hard to notice.

[Fabrizio Montesi]

Re naming and Omega: I agree, it's also a pain to search. Do I understand correctly you mean renaming ωTr into OmegaExecution?

[Fabrizio Montesi]

Re the length thing, I've replied in the PR.

[Ching-Tsun Chou]

I would prefer OmegaExec for brevity. But OmegaExecution is fine, too.