feat(Automata): Two-way automaton

[crei]

This defines a (nondeterministic) two-way automaton, i.e. an automaton with an input tape that can move its input tape head in both directions, following the definition by [Vardi1989]. The purpose of introducing two-way automata is to prove the power of Turing machines with constant space following Vardi's proof of equivalence of two-way and one-way automata.

The definition is not via LTS mainly because the labels would not coincide with the input symbols, which makes it a bit more awkward. Instead, this defines a single-step relation between configurations and then List.IsChain is used to define a "Run", e.g. a sequence of configurations such that adjacent ones are Step-related and which starts at an initial configuration.

[barni120400]

Why do you want a set of starting and accepting states and not a single starting and single accpting state?

[crei]

That's just Vardi's definition. In the end, it doesn't really matter much, but this is also how NA is defined.

[ctchou]

I think you should take advantage of the LTS infrastructure in cslib. The state space of your LTS is TwoNACfg State input, the label space can be either Unit (if you don't really care about transition labels) or Symbol × SignType (if you want to expose the symbol being consumed and the head movement in transition labels), the Tr is Step a input. Then you can leverage the various notions of execution in cslib's LTS, such as LTS.MTr, LTS.Execution, and the InChainFromTo without having to develop your own.

Here's what I mean:

@[ext]
structure TwoNAState (State Symbol : Type*) (input : List Symbol) where
  state : State
  pos : Fin (input.length + 1)

def TwoNATrType (State Symbol : Type*) := State → Symbol →  SignType →  State → Prop

def TwoNALTS (input : List Symbol) (twoTr : TwoNATrType State Symbol) :
    LTS (TwoNAState State Symbol input) Unit where
  Tr c _ c' := ∃ m, ∃ _ : (c.pos : ℕ) < input.length,
    twoTr c.state input[c.pos] m c'.state ∧ (c'.pos : ℤ) = (c.pos : ℤ) + (m.cast : ℤ)

def TwoNA (input : List Symbol) (twoTr : TwoNATrType State Symbol)
    (start : Set ((TwoNAState State Symbol input))) :
    Automata.NA (TwoNAState State Symbol input) Unit where
  Tr := (TwoNALTS input twoTr).Tr
  start := start

Then you don't need TwoNA-specific notions of executions; you can just use those in LTS and NA and all the theorems which have been proved about them.

[fmontesi]

Hi @crei and @SamuelSchlesinger, what do you think of @ctchou's comment? Does it match your goals?

[crei]

I changed this so that a TwoNA is now an NA with a specific label type.

I'm still unsure if LTS is the right base here. As mentioned by @ctchou , there are two options about the label type:

1. Either Unit (i.e. an LTS without labels) or
2. Symbol \times SignType.

The first one (as done in the comment above) requires you to define an LTS on top of the configurations and then only re-use MTr, but I think there is a lot of confusion because you have two different Trs.

The second one (as done in the current state of the PR) cannot use MTr and Run, because only some of the Runs are legal.

Both of them cannot simply use the FinAcc extension of NA (although both of them are NAs) because the notion of acceptance is completely different.

In general, I have the impression that you can do this with LTS, but the question is if you should. Already the fact that there is no clear winner between the two ways to define it might be an indication that the LTS model is not really fitting. It does provide the tools, but maybe a more basic notion like IsChainFromTo could provide the same tools?

[crei]

Actually the way it is now is wrong, because it inherits Execution from LTS which is wrong, those are not the correct executions.

[crei]

I tried it differently, closer to @ctchou 's suggestion. Basically starting with an LTS on the Configurations and restricting the transitions by disallowing the illegal labels such that Execution and Run would not be wrong, but here we hit a different problem: We can only really "build" the LTS when we know the input string, because that is an input to the transition relation, so I fear that the two-way automaton actually cannot inherit from NA.
And I think it is an OK requirement to separate an automaton from its possible inputs.

[crei]

Ok, this might be getting closer to a solution we can all agree on. I now defined TwoNA outside the LTS hierarchy (because of the reasons in the above comment) but defined a function that returns a finite acceptor on the configurations (relative to an input). The acceptor does not accept the input, but we have the property that the TwoNA accepts an input if and only if the language of the acceptor is non-empty.

My main criticism still stands, you have to dig a bit into the definitions of LTS to be able to judge that this definition is equivalent to the one given in Vardi's paper.

As an alternative, I gave one that is closer to the paper and uses List.IsChainFromTo (for which, admittedly, you also have to understand IsChain).

[ctchou]

How about I give it a try myself? I don't have time right now, but should have enough time in the next 48 hours or so.

My current guess is this:

• The configurations are the correct notion of State.
• Symbol can be Unit, because the accepted word is not consumed one symbol at a time.
• We need a different acceptor and FinAcc is not appropriate.
  But only doing it will show if my guess is correct.

[ctchou]

I just pushed an alternative design of 2-way automata in a new file TwoNA/BasicAlt.lean. Please take a look and let me know what you think. It uses both the existing LTS and the Automata.Acceptor frameworks in cslib, but not Automata.NA or Automata.NA.FinAcc. The new Automata.TwoWayNA namespace is at the same level as Automata.NA.FinAcc and has its own Acceptor instance, from which we get the accepted language for free. An alternative is to put TwoWayNA under Automata.NA, but that won't make much difference in substance.

[crei]

What I like about your version is the fact that the equality on inputs is enforced on the configuration level, at the point where you restrict the transition relation. I'm not so happy about the fact that the original transition relation is not visible any more and also the initial states are not available. I also see that "TwoWayNA" makes much more sense as a name, but I won't change that for now to not complicate the diff. I agree that an LTS without labels does not really make sense. Let me try to move the input into the configurations.

[ctchou]

I see what you are doing in the via LTS section. I think it can probably work, in the sense of allowing you to leverage the results already proved for LTS. But note that the read pointer pos and the input should really be considered an integral part of the state of a 2-way automaton. But they are not part of your definition of TwoNA. You "slip them in" later in TwoNA.toCfgTr. But this is ultimately an aesthetic judgement on my part and I won't insist on it.

To make my point above more provocatively, notice that TwoNA could be interpreted as (the finite-state control of) a 1-tape Turing machine. All you have to do is to use a product type Symbol x Symbol for the Symbol in TwoNATr and interpret the first component of the product as the symbol read from the tape and the second the symbol written to the tape. Because the state of your TwoNA does not include the tape, you don't get an opportunity to state the invariant that the tape is not allowed to change in TwoNA.

[ctchou]

I would suggest you rename .toCfgTr to .toCfgLTS and .toCfgLTS to .toCfgNAFinAcc. In fact, you can make .toCfgTr to return LTS (TwoNACfg State Symbol) (Symbol × SignType) to match its new name.

[ctchou]

Personally I think it is more convenient to define pos : ℕ, because I found dealing with Fin types a pain in general. In the the transition relation you will have to somehow say that pos is within the index range of input in any case (namely, some x = c.input[c.pos]?).

[crei]

Maybe it's just an aesthetic judgment but maybe I also don't understand. To me, the input head position cannot be part of the state, it can only be part of the configuration: All possible state sets and all possible transitions (allowed by the type system) should be valid. The restriction comes in when we are talking about the "implementation details" of the automaton and what it means for it to accept a word and transition between configurations. For me, it is important to ensure in the type system that it is not possible to construct an 'illegal' TwoWayNA, because only then can we talk about what "any TwoWayNA" can do. In your alternative, twoWayNA.mk ensures that the initial and final states and the transition relation are built properly. If I see it right, in your version, you can construct a TwoWayNA where there is a single transition that moves the input head from position 0 to (say) position 10 in one step. It also does not restrict movement of the input head to (say) two positions right of the end of the input.

[ctchou]

For me, a "state" of a machine is a complete summary of the past behavior of the machine and its future behavior should not depend on anything beyond what is in the "state". Call it a "configuration" if you like, but the point is that the computing power of a machine is determined by its "state" in the above sense, not just its "finite-state control" part. For example, you cannot define the correct Acceptor without referring to the complete "state". But, as I said, this is mostly an aesthetic issue and I won't insist on it.

[ctchou]

I think it is clearer to not involve ℤ at all. For example, what happens if c.pos = 0 and m = neg? It would seem that the RHS is then -1 : ℤ. Does this force c'.pos to be 0? It takes some thinking and looking up the manual to figure that out. Why not spell it out via case splitting on m and (if necessary) c.pos?

[Edit] Actually it is worse than I thought, because you can prove this:

example (n : ℕ) (p : Fin n) : (p : ℤ) ≠ (0 : ℤ) + (SignType.neg : ℤ) := by simp

That is, if c.pos = 0 and m = neg, there is no next step. Is this what you want?

[crei]

Yes, this is exactly what I want, see the Implementation notes. This is also the way it is stated in the paper I'm formalizing here.

[ctchou]

The informal text of your implementation note allows at least two interpretations when c.pos = 0 and m = neg:
(1) there is no next configuration and hence the execution gets stuck at this point.
(2) there is a next configuration but pos stays at position 0.
Both approaches are reasonable in the sense that both will result in a regular language being accepted. Your code does (1), but that is not transparent. I had to squint hard at it and prove a theorem to be certain that my understanding is correct. You should spell out what you want either in the code or in the comment.

[crei]

I added more comments.