Partial Reductions for Kleene Algebra with Linear Hypotheses
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911387300659200 |
|---|---|
| author | Chung, Liam Kappé, Tobias |
| author_facet | Chung, Liam Kappé, Tobias |
| contents | Kleene algebra (KA) is an important tool for reasoning about general program equivalences, with a decidable and complete equational theory. However, KA cannot always prove equivalences between specific programs. For this purpose, one adds hypotheses to KA that encode program-specific knowledge. Traditionally, a map on regular expressions called a reduction then lets us lift decidability and completeness to these more expressive systems. Explicitly constructing such a reduction requires significant labour. Moreover, due to regularity constraints, a reduction may not exist for all combinations of expression and hypothesis.
We describe an automaton-based construction to mechanically derive reductions for a wide class of hypotheses. These reductions can be partial, in which case they yield partial completeness: completeness for expressions in their domain. This allows us to automatically establish the provability of more equivalences than what is covered in existing work. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_14114 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Partial Reductions for Kleene Algebra with Linear Hypotheses Chung, Liam Kappé, Tobias Programming Languages Kleene algebra (KA) is an important tool for reasoning about general program equivalences, with a decidable and complete equational theory. However, KA cannot always prove equivalences between specific programs. For this purpose, one adds hypotheses to KA that encode program-specific knowledge. Traditionally, a map on regular expressions called a reduction then lets us lift decidability and completeness to these more expressive systems. Explicitly constructing such a reduction requires significant labour. Moreover, due to regularity constraints, a reduction may not exist for all combinations of expression and hypothesis. We describe an automaton-based construction to mechanically derive reductions for a wide class of hypotheses. These reductions can be partial, in which case they yield partial completeness: completeness for expressions in their domain. This allows us to automatically establish the provability of more equivalences than what is covered in existing work. |
| title | Partial Reductions for Kleene Algebra with Linear Hypotheses |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2601.14114 |