Email Gateway (Jul 07 2025 at 09:32): Email Gateway (Jul 07 2025 at 09:32):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
I’m happy to announce another AFP entry that became available today:
Parikh's theorem
by Fabian Lehr
Abstract:
In formal language theory, the Parikh image of a language L is the set of
multisets of the words in L: the order of letters becomes irrelevant, only the
number of occurrences is relevant. Parikh's Theorem states that the Parikh image
of a context-free language is the same as the Parikh image of some regular
language. This formalization closely follows Pilling's proof: It describes a
context-free language as a minimal solution to a system of equations induced by
a context free grammar for this language. Then it is shown that there exists a
minimal solution to this system which is regular, such that the regular solution
and the context-free language have the same Parikh image.
https://www.isa-afp.org/entries/Parikh.html
Enjoy,
René
Last updated: Jul 26 2025 at 12:43 UTC