Operations on Fixpoint Equation Systems
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2023
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866917741523369984 |
|---|---|
| author | Neele, Thomas van de Pol, Jaco |
| author_facet | Neele, Thomas van de Pol, Jaco |
| contents | We study operations on fixpoint equation systems (FES) over arbitrary complete lattices. We investigate under which conditions these operations, such as substituting variables by their definition, and swapping the ordering of equations, preserve the solution of a FES. We provide rigorous, computer-checked proofs. Along the way, we list a number of known and new identities and inequalities on extremal fixpoints in complete lattices. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2304_07162 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Operations on Fixpoint Equation Systems Neele, Thomas van de Pol, Jaco Logic in Computer Science We study operations on fixpoint equation systems (FES) over arbitrary complete lattices. We investigate under which conditions these operations, such as substituting variables by their definition, and swapping the ordering of equations, preserve the solution of a FES. We provide rigorous, computer-checked proofs. Along the way, we list a number of known and new identities and inequalities on extremal fixpoints in complete lattices. |
| title | Operations on Fixpoint Equation Systems |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2304.07162 |