Karl Palmskog (Nov 25 2021 at 14:09): Karl Palmskog (Nov 25 2021 at 14:09):@Christian Doczkal regarding languages in general what do you think about this?
Dockzal et al. [12] use the Coq type
word -> boolto represent languages, rather thanword -> 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)
Christian Doczkal (Nov 25 2021 at 14:34):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: )
Karl Palmskog (Nov 25 2021 at 14:37):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?
Christian Doczkal (Nov 25 2021 at 14:45):Okay, with Myhill-Nerode the situation was complicated, I don't remember from the top of my head.
Karl Palmskog (Nov 25 2021 at 14:47):OK to open an issue maybe? I might dig into it at some point.
Christian Doczkal (Nov 25 2021 at 14:49):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.
Christian Doczkal (Nov 25 2021 at 14:51):Here a "classifier" is a "data" object providing access to the finitely many equivalence classes and a decider decides language membership.
Christian Doczkal (Nov 25 2021 at 14:59):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)
Karl Palmskog (Nov 25 2021 at 15:01):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