On Propositional Program Equivalence (extended abstract)
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866916836711333888 |
|---|---|
| author | Kappé, Tobias |
| author_facet | Kappé, Tobias |
| contents | General program equivalence is undecidable. However, if we abstract away the semantics of statements, then this problem becomes not just decidable, but practically feasible. For instance, a program of the form "if $b$ then $e$ else $f$" should be equivalent to "if not $b$ then $f$ else $e$" - no matter what $b$, $e$ and $f$ are. This kind of equivalence is known as propositional equivalence. In this extended abstract, we discuss recent developments in propositional program equivalence from the perspective of (Guarded) Kleene Algebra with Tests, or (G)KAT. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_07480 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | On Propositional Program Equivalence (extended abstract) Kappé, Tobias Programming Languages General program equivalence is undecidable. However, if we abstract away the semantics of statements, then this problem becomes not just decidable, but practically feasible. For instance, a program of the form "if $b$ then $e$ else $f$" should be equivalent to "if not $b$ then $f$ else $e$" - no matter what $b$, $e$ and $f$ are. This kind of equivalence is known as propositional equivalence. In this extended abstract, we discuss recent developments in propositional program equivalence from the perspective of (Guarded) Kleene Algebra with Tests, or (G)KAT. |
| title | On Propositional Program Equivalence (extended abstract) |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2507.07480 |