Stream: coq-community devs & users

Topic: Languages and Chomsky hierarchy


view this post on Zulip 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 -> bool to represent languages, rather than word -> Prop as we do, and then go on to prove Myhill-Nerode constructively. In a certain sense this begs the question, however.

(Coq code is here)

view this post on Zulip 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: )

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Nov 25 2021 at 14:47):

OK to open an issue maybe? I might dig into it at some point.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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: Jun 06 2023 at 22:01 UTC