LTS: multistep transitions and executions

Stream: CSLib

[Fabrizio Montesi]

@Ching-Tsun Chou I've been playing around with different defs of executions and multistep transitions. I wonder if there are opportunities to simplify some things, or at least clarify them. These are just semi-random thoughts for now:

I think we have similar insights regarding potentially-infinite executions. For example, if you look at how I defined divergent executions in LTS/Basic.lean, you'll see I used Stream' at the time. (This can/should just become OmegaSequence, btw.)
We could easily adopt OmegaSeq for modelling any execution in general for LTS, as you did in Run and some of your other developments.

However, for finite executions, it can be annoying not to just have an inductive/a list/etc. In particular, I'd still keep MTr around (also because it's an established concept in the literature), but we might want to make it a Type (max u v) instead of a Prop? This is similar to what they do for graphs in mathlib, IIUC. It'd then be how we represent a 'finite execution' and allow us to compute the set of intermediate states whenever we need it.

[Fabrizio Montesi]

My major reason for keeping it a Prop so far is to treat it like a (ternary) relation.. @Chris Henson do you think you're gonna have a similar thing for rewriting systems? If you use ReflTransGen for a multistep reduction, how do you get out the set of intermediate states?

[Chris Henson]

I'm not quite sure I follow. Do you mean essentially wanting a version of ReflTransGen that is in Type instead of Prop? I have not anticipated a need for this.

[Ching-Tsun Chou]

@Fabrizio Montesi You mean something like the following? This way t : lts.MRTr' s μs t will carry the state sequence t.ss and its properties, all uses ofLTS.MTr will be replaced by LTS.MTr', and proofs that currently use the inductive definition of LTS.MTr will be replaced by proofs in terms of lists (for which mathlib has excellent support). LTS.InfMTr can replace (most of) the current definition of NA.Run.

structure LTS.MTr' (lts : LTS State Label) (s : State) (μs : List Label) (t : State) where
  ss : List State
  ss_len : ss.length = μs.length + 1
  ss_beg : ss[0] = s
  ss_end : ss[μs.length] = t
  ss_run : ∀ k, ∀ _ : k < μs.length, lts.Tr ss[k] μs[k] ss[k + 1]

structure LTS.InfMtr (lts : LTS State Label) (s : State) (μs : ωSequence Label) where
  ss : ωSequence State
  ss_beg : ss 0 = s
  ss_run : ∀ k, lts.Tr (ss k) (μs k) (ss (k + 1))

[Ching-Tsun Chou]

BTW, I've checked that the above does type-check.

[Fabrizio Montesi]

Chris Henson said:

I'm not quite sure I follow. Do you mean essentially wanting a version of ReflTransGen that is in Type instead of Prop? I have not anticipated a need for this.

Re type instead of prop: yes.

[Fabrizio Montesi]

Ching-Tsun Chou not exactly. My ideas was to just change MTr to finish in Type instead of Prop, while keeping the rest the same, like this:

inductive LTS.MTr (lts : LTS State Label) : State → List Label → State → Type (max u v) where

I can then define states, labels, start, final, and whatever other information we'd like simply by defining appropriate functions, e.g.,

def LTS.Tr.start (_ : lts.Tr s1 μ s2) : State := s1

def LTS.MTr.states (mtr : lts.MTr s1 μs s2) : List State :=
  match mtr with
  | refl => []
  | stepL tr mtr =>
    tr.start :: mtr.states

[Ching-Tsun Chou]

I think this will lead us to the type-checking hell. Eventually we will need to existentially quantified out the State type in order to define regular and ω-regular languages. The following is a mock-up of the process. It does not type-check even though I have limited State to Type 0 (as is done in the current definitions of regular and ω-regular languages).

inductive LTS.MTr' (lts : LTS State Label) : State → List Label → State → Type _ where
  | refl {s : State} : lts.MTr' s [] s
  | stepL {s1 : State} {μ : Label} {s2 : State} {μs : List Label} {s3 : State} :
    lts.Tr s1 μ s2 → lts.MTr' s2 μs s3 →
    lts.MTr' s1 (μ :: μs) s3

def foo (μs : List Label) :=
  ∃ (State : Type), ∃ (lts : LTS State Label), ∃ (s1 s2 : State), lts.MTr' s1 μs s2

Now that I think about it, I'm not sure the LTS.MTr' I proposed above won't have a similar problem.

[Fabrizio Montesi]

Uh, oh.

[Fabrizio Montesi]

I think I had a similar problem in the past..

[Fabrizio Montesi]

I'm your case, you're interested in defining 'there exists an automaton that accepts this (set of) string(s)', right?

[Ching-Tsun Chou]

But how do you say that? "there exists an automaton" ultimately boils down to "there exists an LTS".

[Fabrizio Montesi]

Yes, I'm just curious about why you're interested in 'foo'.

[Fabrizio Montesi]

That one, for example, you could write as:

def foo (μs : List Label) := Σ State, Σ lts : LTS State Label, Σ s1 s2 : State, lts.MTr s1 μs s2

(I guess. I haven't used Sigma quite a bit.)

[Ching-Tsun Chou]

After thinking more, I think the problem is more basic. At some point you'll have to define a predicate LTS.trans (lts : LTS State Label) (s1 : State) (μs : List Label) (s2 : State) : Prop to mean what the current LTS.MTr means, for otherwise I don't see how you can talk about the language accepted by an automaton. But how do you define LTS.trans?

[Ching-Tsun Chou]

Note that Sigma produces a Type _, not a Prop. A language is a set (over words), which needs a defining predicate. So there is no escape from the need for somehow defining the equivalent of the current LTS.MTr. But how?

[Ching-Tsun Chou]

Furthermore, note that the function LTS.MTr.states above is not very useful by itself. Not only do we need to get a sequence of states out of mtr : LTS.MTr, but we also need to relate that sequence with s1, s2, and μs in order to do anything useful. But that's exactly what the current theorem LTS.MTr.exists_states does for you. So I don't see what making LTS.MTr into a Type buys for you which we don't already have.

[Fabrizio Montesi]

Ching-Tsun Chou said:

Furthermore, note that the function LTS.MTr.states above is not very useful by itself. Not only do we need to get a sequence of states out of mtr : LTS.MTr, but we also need to relate that sequence with s1, s2, and μs in order to do anything useful. But that's exactly what the current theorem LTS.MTr.exists_states does for you. So I don't see what making LTS.MTr into a Type buys for you which we don't already have.

That's less of a problem, it's a matter of proving properties about states and the other defs about MTr. But the problem about defining predicates you mention right before is critical.

[Fabrizio Montesi]

This probably means that MTr + theorems to 'flatten' the list of states/labels make sense for finite stuff, and what we're missing is the infinite counterpart.
Please see cslib#232, where I define in LTS/Basic.lean

def LTS.ωTr (lts : LTS State Label) (ss : ωSequence State) (μs : ωSequence Label) : Prop :=
  ∀ n, lts.Tr (ss n) (μs n) (ss (n + 1))

and then prove

/-- Any finite execution extracted from an infinite execution is valid. -/
theorem LTS.ωTr_mTr {lts : LTS State Label} {n m : ℕ} {hnm : n ≤ m}
    (h : lts.ωTr ss μs) : lts.MTr (ss n) (μs.extract n m) (ss m)

[Fabrizio Montesi]

We could use that as common base for my defs of divergent executions and your def of infinite run.

I was hoping, for example, to rewrite

/-- Infinite run. -/
def Run (na : NA State Symbol) (xs : ωSequence Symbol) (ss : ωSequence State) :=
  ss 0 ∈ na.start ∧ ∀ n, na.Tr (ss n) (xs n) (ss (n + 1))

into

/-- Infinite run. -/
def Run (na : NA State Symbol) (xs : ωSequence Symbol) (ss : ωSequence State) :=
  ss 0 ∈ na.start ∧ na.ωTr ss xs

but this made grind explode in a couple of proofs because apparently the search space increases for reasons still unknown to me -- this is likely me being dumb with something.

[Fabrizio Montesi]

Ok, I've managed to port Run to ωTr now. Some proofs required adding a line here or there. I think it's because we need to generalise some theorems about runs to ωTr.