@Christian Doczkal regarding languages in general what do you think about this?
Dockzal et al.  use the Coq type
word -> boolto represent languages, rather than
word -> Propas we do, and then go on to prove Myhill-Nerode constructively. In a certain sense this begs the question, however.
(Coq code is here)
Well, for the paper they cite, the criticism is indeed valid. This is the reason why we started distinguishing languages and decidable languages in later versions of the development. (And I don't know what to think about them not being able to spell my name. :shrug: )
ah OK, just to confirm, so Myhill-Nerode in Reglang and the JAR paper doesn't rely on
word -> bool? Or can it be generalized if it is?
Okay, with Myhill-Nerode the situation was complicated, I don't remember from the top of my head.
OK to open an issue maybe? I might dig into it at some point.
Well, here is the precise statement from the journal paper:
Theorem 5.9 A language is regular if and only if it has both a decider and a classifier.
Here a "classifier" is a "data" object providing access to the finitely many equivalence classes and a decider decides language membership.
This is part of the reason why the title is about "representations" of regular languages: We always have some kind of "data" objects that we do translations/constructions on. In fact,
regular L is a Sigma-type, not a proposition, although we do sometimes use
inhabited (regular L)
OK, so one takeway might be that reusing all Reglang results in some general formalization of the Chomsky hierarchy is not completely straightforward
Last updated: Feb 05 2023 at 15:03 UTC