Email Gateway (Nov 18 2025 at 14:22): Email Gateway (Nov 18 2025 at 14:22):From: Peter Lammich <lammich@in.tum.de>
Dear all,
I'm happy to announce a new AFP entry:
Pre*: The Predecessors of a Regular Language w.r.t. a Context-Free
Grammar, with Applications
by Tassilo Lemke and Tobias Nipkow
Abstract:
Let $L$ be a language, $G$ a context-free grammar
and let $pre^*(L)$ be the language of all predecessors (w.r.t.\ $G$) of
words in $L$.
The following fact has been rediscovered in the literature repeatedly:
If $L$ is regular, so is $pre^*(L)$. Moreover, given an NFA $M$ for $L$,
an NFA $M'$ for $pre^*(L)$
can be computed very elegantly from $M$. Starting from a suitable $M$,
simple checks on $M'$
provide solutions to many elementary decision problems concerning $G$,
such as the word-problem, emptiness problem, and more.
We formalize two algorithms to compute $pre^*(L)$ for a regular $L$
(using NFAs as representation).
The first one is very simple and elegant and works for any CFG, while
the second one is
more efficient but is restricted to CFGs in in extended-CNF.
All our algorithms are executable,
allowing many elementary problems on context-free grammars to be solved
automatically.
https://www.isa-afp.org/entries/Pre_Star_CFG.html
Enjoy!
--
Peter
Last updated: Dec 02 2025 at 16:32 UTC