Normal Forms for Elements of ${}^*$-Continuous Kleene Algebras Representing the Context-Free Languages
Abstract
Within the tensor product $K \mathop{\otimes_{\cal R}} C_2'$ of any ${}^*$-continuous Kleene algebra $K$ with the polycyclic ${}^*$-continuous Kleene algebra $C_2'$ over two bracket pairs there is a copy of the fixed-point closure of $K$: the centralizer of $C_2'$ in $K \mathop{\otimes_{\cal R}} C_2'$. Using an automata-theoretic representation of elements of $K\mathop{\otimes_{\cal R}} C_2'$ à la Kleene, with the aid of normal form theorems that restrict the occurrences of brackets on paths through the automata, we develop a foundation for a calculus of context-free expressions without variable binders. We also give some results on the bra-ket ${}^*$-continuous Kleene algebra $C_2$, motivate the ``completeness equation'' that distinguishes $C_2$ from $C_2'$, and show that $C_2'$ already validates a relativized form of this equation. final version. 42 pages, 4 figures. References sorted alphabetically
Fields of Study & Subjects
Formal Methods in Verification
Logic
programming
and type systems
semigroups and automata theory
Publication details
- Journal / source
- Fundamenta Informaticae
- Volume
- Volume 195, Issues 1-4:...
- Publication date
- 14 January 2026
- Language
- EN