feat(Automata, LTS, TM): Introduce LTS.SMTr and LTS.mapLabel, generalise TM tapes to arbitrary universes, fix EpsilonNA, and introduce their single-accept transformation#625
Conversation
fmontesi
changed the title
fmontesi
changed the title
ctchou
left a comment
ctchou
left a comment
There was a problem hiding this comment.
Overall comment: I think the changes related to Turing machines and their tapes should be separated out to a different PR. Currently they are indpendent of the changes related to LTS and EpsilonNA.
| /-- Extensional equality for LTS. -/ | ||
| theorem ext {lts₁ lts₂ : LTS State Label} | ||
| (h : ∀ s μ s', lts₁.Tr s μ s' ↔ lts₂.Tr s μ s') : lts₁ = lts₂ := by | ||
| rcases lts₁ with ⟨Tr₁⟩ | ||
| rcases lts₂ with ⟨Tr₂⟩ | ||
| grind only [mk.injEq] |
There was a problem hiding this comment.
You don't need to prove this theorem yourself. Adding the @[ext] attribute to the definition of LTS suffices.
| /-- `setImage` on `HasTau.τ` preserves membership. -/ | ||
| @[scoped grind .] | ||
| lemma mem_saturate_setImage_τ [HasTau Label] (lts : LTS State Label) (h : s ∈ S) : | ||
| s ∈ lts.saturate.setImage S HasTau.τ := by | ||
| simp only [setImage, Set.mem_iUnion, exists_prop] | ||
| exists s | ||
| grind |
There was a problem hiding this comment.
Given the theorem subset_saturate_setImage_τ below, do we really need this lemma? They are practically identical.
| /-- `τClosure` preserves membership. -/ | ||
| @[scoped grind .] | ||
| lemma τClosure_mem [HasTau Label] (lts : LTS State Label) (h : s ∈ S) : | ||
| s ∈ lts.τClosure S := by grind [= τClosure] |
| theorem saturate_mTr_sMTr_not_nil_iff [HasTau Label] {lts : LTS State Label} | ||
| (hμs : μs ≠ []) : lts.saturate.MTr s μs s' ↔ lts.SMTr s μs s' := by |
There was a problem hiding this comment.
Why not take this as the definition of LTS.SMTr? I think the properties of LTS.SMTr proved above are all easy consequences of this alternative definition.
|
|
||
|
|
||
| /-! | ||
| # Map operation for LTS. |
There was a problem hiding this comment.
Unless you plan to add other kinds of map operations in the future, I think this file should be renamed to MapLabel.lean and this comment should be more specific.
| Accepts (a : FinAcc State Symbol) (xs : List Symbol) := | ||
| ∃ s ∈ a.start, ∃ s' ∈ a.accept, a.SMTr s (xs.map Option.some) s' |
There was a problem hiding this comment.
I think the old indentation pattern is the correct one.
| end Automata.εNA.FinAcc | ||
|
|
||
| end Cslib | ||
| apply Iff.intro <;> intro h <;> rcases h with ⟨s, hs, s', hs', h⟩ |
There was a problem hiding this comment.
The intro and rcases can be merged into rintro.
| /-! # Translation of εNA into εNA with a single accept state | ||
|
|
||
| Defines the transformation `toSingleAccept` for `εNA.FinAcc` and proves correctness | ||
| results in terms of language equivalence and correspondences between the two transition systems. | ||
| -/ |
There was a problem hiding this comment.
Is this file necessary for this PR? Its contents don't seem to be used anywhere else now.
Also, the stand construction in textbooks:
https://en.wikipedia.org/wiki/Thompson%27s_construction
uses EpsilonNA with a single start state and a single accept state. Perhaps they should be the target of formalization.
2 participants
This PR:
mapLabeloperation for LTS and its properties.toSingleAcceptfor EpsilonNA.FinAcc, which transforms the automaton into an equivalent one that has a single accept state with no outgoing transitions.