Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Operations on Fixpoint Equation Systems

Thomas Neele, Jaco van de Pol

TL;DR

This work presents a unified, machine-checked treatment of operations on fixpoint equation systems (FES) over arbitrary complete lattices, focusing on when substitutions and reordering preserve the solution. It develops foundational lattice theory, defines a semantic FES framework, and establishes both equalities and inequalities for unfolding, substitution, and swapping, including new results such as Bekič-type inequalities and forward substitution under indirect-dependency constraints. A key contribution is the systematic use of dependency graphs to capture indirect dependencies and guide safe reordering and substitution of equations, enabling modular solving and potential reductions in mu/nu alternations. The results generalize known BES/PBES techniques to the broader FES setting and are formalised in Coq and PVS, underscoring their rigor and potential applicability to parity games and related logical systems.

Abstract

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.

Operations on Fixpoint Equation Systems

TL;DR

This work presents a unified, machine-checked treatment of operations on fixpoint equation systems (FES) over arbitrary complete lattices, focusing on when substitutions and reordering preserve the solution. It develops foundational lattice theory, defines a semantic FES framework, and establishes both equalities and inequalities for unfolding, substitution, and swapping, including new results such as Bekič-type inequalities and forward substitution under indirect-dependency constraints. A key contribution is the systematic use of dependency graphs to capture indirect dependencies and guide safe reordering and substitution of equations, enabling modular solving and potential reductions in mu/nu alternations. The results generalize known BES/PBES techniques to the broader FES setting and are formalised in Coq and PVS, underscoring their rigor and potential applicability to parity games and related logical systems.

Abstract

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.
Paper Structure (27 sections, 30 theorems, 58 equations, 2 tables)

This paper contains 27 sections, 30 theorems, 58 equations, 2 tables.

Table of Contents

  1. Introduction
  2. Well-known instances of FES
  3. Contributions
  4. Overview
  5. Fixpoint Laws in Complete Lattices
  6. Fixpoint Equation Systems
  7. Definition of Fixpoint Equation Systems
  8. Semantics of FES and Basic Results
  9. The Dependency Graph between Variables
  10. Substituting in FES Equations
  11. Unfolding Definitions
  12. Substituting a Partial Solution
  13. Swapping Variables in FES specifications
  14. Swapping Equations with the same Sign
  15. Migrating Independent Blocks of Equations
  16. ...and 12 more sections

Key Result

Lemma 2.1

Let $(U,\leq,glb)$ be a complete lattice. Let $\sigma\mathrel{ \hbox{${\mathrel{ \hbox{${\in}$}}}$}}\{\mu,\nu\}$, $A\mathrel{ \hbox{${\mathrel{ \hbox{${\in}$}}}$}} U$, and let $F,G\mathrel{ \hbox{${\mathrel{ \hbox{${\in}$}}}$}} U\to U$ and $H,K\mathrel{ \hbox{${\mathrel{ \hbox{${\in}$}}}$}} U\times

Theorems & Definitions (68)

  • Lemma 2.1
  • proof
  • Lemma 2.2
  • proof
  • Example 3.1
  • Example 3.2
  • Example 3.3
  • Remark 3.4
  • Example 3.5
  • Lemma 3.6
  • ...and 58 more