Source-linked AI summary
Domain Theory Meets Interaction Trees in Rocq
David Nowak, Vlad Rusu
TL;DR
Rocq’s built-in coinduction complicates interaction-tree reasoning with artificial silent steps and weak-bisimulation proofs. This paper uses a domain-theoretic formalization and an inductive equivalence relation for effectful computations. It proves the relation correct under a base-relation assumption and demonstrates it on equivalent Syracuse-sequence programs.
Problem
Earlier Rocq interaction-tree formalizations rely on built-in coinduction, which brings artificial silent steps and weak-bisimulation reasoning into program equivalence proofs.
Source: §1 · p. 2Method
The paper formalizes interaction trees using domain theory and defines an inductive equivalence by closing a base relation on primitive effects under monadic structure and least upper bounds.
Source: §1 · p. 2, §4.1 · p. 6Results
Equivalent computations have equal denotations in monads implementing their effects, assuming the base relation is correct; the framework also proves two Syracuse-sequence programs equivalent.
Source: §1 · p. 2Takeaways & Limitations
The Syracuse example shows the relation can establish equivalence for possibly non-terminating programs without deciding whether the sequence terminates.
Source: §5 · p. 12The paper does not prove completeness of the equivalence relation.
Source: §4.3 · p. 11
Abstract
from arXiv · showhide
We present a domain-theoretical formalization of interaction trees in the Rocq prover. Unlike existing formalizations, ours does not rely on Rocq's built-in coinduction. Hence, we avoid complications occurring in earlier works, such as artificially including silent steps to comply with Rocq's productivity checker, treating monad laws as weak bisimulations, and coinductive bisimulation reasoning. We define an inductive program equivalence relation as the congruence closure of a base relation on primitive effects with respect to action sequencing and least upper bounds. This enables reasoning about possibly non-terminating programs by reducing their equivalences to equivalences of their terminating approximations, which are then proved by induction. This relation is proved correct: provided the base relation is correct, equivalent computations have equal denotations in any monad that faithfully implements the effects. We illustrate the framework by showing the equivalence of two programs encoding the Syracuse sequence, whose termination is an open mathematical conjecture.
1 Introduction
The paper formalizes interaction trees in Rocq through domain theory rather than built-in coinduction, avoiding complications associated with earlier coinductive formalizations. It defines a correct inductive equivalence for effectful computations and illustrates it with two Syracuse-sequence programs.
1 Introduction
- The formalization avoids Rocq’s built-in coinduction, and thus the artificial silent steps and weak-bisimulation reasoning associated with earlier approaches.Earlier proofs could require traversing trees with a corecursive function and then proving weak bisimilarity of the results.Source: §1 · pp. 1–2
- The equivalence relation closes a base relation on primitive effects under monadic structure and least upper bounds, reducing non-terminating equivalence proofs to induction on terminating approximations.Its correctness is established once, assuming the base relation is correct, independently of proofs for particular programs.Source: §1 · p. 2
- The framework proves equivalent computations have equal denotations in monads implementing their effects, provided the base relation is correct.The correctness proof is independent of proofs of equivalence for specific programs.Source: §1 · p. 2
- The authors show two programs encoding the Syracuse sequence are equivalent, without resolving the conjecture about whether that sequence terminates.The example demonstrates equivalence for a sequence whose termination remains an open mathematical conjecture.Source: §1 · p. 2
2 Background
The background develops domain-theoretic tools for representing partial and coinductive structures. It uses completions of finite labelled partial containers to construct coinductive types with definition orders.
2 Background
- Domain theory orders elements by how defined they are, providing the ordering perspective used in the paper’s construction.The paper adapts a specific construction from earlier work.Source: §2 · p. 2
2.1 Elements of Domain Theory
- Kleene’s fixpoint theorem defines possibly partial functions in Rocq as least fixpoints of continuous functionals; greatest fixpoints supply coinductive objects.The paper also uses the coinduction principle associated with greatest fixpoints.Source: §2.1 · p. 3
2.2 Coinductive Types as Labelled Partial Containers
- The paper encodes coinductive types as completions of finite labelled partial containers, whose trees admit partially defined approximations as well as fully defined terms.The resulting coinductive types inherit a definition order and a bisimulation relation equivalent to equality.Source: §2.2 · pp. 4–5
3 CPO-valued Monads
This section defines CPO-valued monads and develops a state transformer that augments an existing monad with state effects. These structures provide the monadic setting used by the paper’s interaction trees and Syracuse example.
3 CPO-valued Monads
- A CPO-valued monad organizes computation values as complete partial orders and provides return and bind operations satisfying monadic laws.The definition also requires continuity properties for bind.Source: §3 · p. 5
- The state transformer augments an existing CPO-valued monad with state and lifts operations from the original monad into the augmented one.Its bind sequences computations while threading state through them.Source: §3 · p. 6
- The state primitives read the current state with get and replace it with put.The transformer combined with the option monad yields the StateS monad used in the Syracuse example.Source: §3 · p. 6
4 Interaction Trees
The paper constructs interaction trees through domain-theoretic completion, then equips them with monadic operations and an inductive congruence for equational reasoning. The congruence handles non-terminating programs by reducing equivalence to finite approximations.
4.1 Interaction Trees: Definition and Basic Properties
- Interaction trees are formed by completing finite trees encoded as Labelled Partial Containers, yielding a CPO with a coinductive structure and bisimulation equal to equality.Their nodes represent effects and continuations; leaves may be bottom or returned values.Source: §4.1 · pp. 6–8
Definition 9 (Trigger)
- Trigger wraps one uninterpreted primitive effect in a tree as a single effect node whose immediate continuation returns purely.It is the most basic way to inject an effect such as get.Source: Definition 9 (Trigger) · p. 8
4.2.1 Ret, Bind, and Monadic Laws
- Bind is defined as the least fixpoint of a continuous functional on an uncurried pair of arguments, then curried to obtain the sequencing operation.The monad laws are proved using coinduction, and equality–bisimulation equivalence makes them Rocq equalities.Source: §4.2 · p. 8, §4.1 · p. 8, §4.2.1 · p. 9
4.2.2 Fold
- Fold interprets tree effects into a CPO-valued result, and its definition requires each effect handler to be continuous.Using fold ret g traverses a tree and applies g to its effects, producing a value in a concrete monad.Source: §4.2.2 · p. 10
4.3 Congruence for Equational Reasoning on Interaction Trees
- Closure under least upper bounds lets the inductive congruence reduce equivalence of non-terminating programs to equivalences of finite approximations, which can be proved by induction.The relation is generated from effect-specific axioms and is closed under bind as well as least upper bounds.Source: §4.3 · p. 11
5 Example
The example proves equivalence between two Syracuse programs by comparing fuel-bounded approximations. It handles input zero separately and aligns the programs’ loop iterations for positive inputs.
5 Example
- The single-loop program uses one while-loop, whereas the double-loop program uses nested loops to repeatedly divide even state values by 2.The double-loop version is described as an optimized version of the single-loop program.Source: §5 · p. 12, Figure 3 · p. 12, Figure 4 · p. 12
- The programs are equivalent: if they terminate, both return 1; for n=0 both diverge, while positive-input equivalence follows by fuel induction.The induction compares corresponding fuel-bounded computations.Source: §5 · pp. 13–14
- Kleene’s theorem represents each while-loop as the least upper bound of its fuel-bounded iterations.The fuel-indexed function gives the i-th iteration of the while-loop functional.Source: §5 · p. 13
- For positive x, the double program’s inner loop reaches its least upper bound after nb zeroes x iterations and updates the state to x/(2^nb zeroes x).At x=0, the inner loop diverges instead.Source: §5 · p. 13
- For n=0, divergence propagates from the double program’s inner loop to the whole program, and the single program also diverges; reflexivity proves their equivalence.Source: §5 · p. 13
- For n>0, each double-program outer-loop iteration matches one or more single-program iterations that produce the same state; the proof aligns their fuel counts and proceeds by induction.The correspondence uses iter n k, and the proof uses congruence for least upper bounds and the base relation in the inductive step.Source: §5 · pp. 13–14
6 Conclusions, Additional Related Work, and Future Work
The domain-theoretic formalization supports reasoning about effectful, potentially non-terminating computations, demonstrated by proving equivalence between two Syracuse-sequence implementations. It avoids silent transitions and weak bisimulation used in closely related work.
6 Conclusions, Additional Related Work, and Future Work
- The framework proves equivalence between two implementations of the possibly nonterminating Syracuse sequence.Source: §6 · p. 14
- Grounding interaction trees in domain theory eliminates the need for silent transitions and weak bisimulation that complicate related work.Source: §6 · p. 14
- FreeSpec and Monae consider only finite program executions, unlike this work's focus on potentially non-terminating computations.Source: §6 · p. 14
- The algebraic-effects framework of Hyland, Plotkin, and Power gives a semantic and categorical account, while this work represents effectful computation through interaction trees in Rocq.Source: §6 · p. 14
- Prior work studies effectful program equivalence through logical relations, applicative bisimilarity, and modal logic.Source: §6 · p. 14
- A future coproduct operation for interaction trees could support reasoning about programs with combined effects.Source: §6 · p. 15
- Future work could add specialized tactics for effect-specific reasoning and coproduct manipulation using Rocq rewriting.Source: §6 · p. 15
- Combining domain-theoretic interaction trees with Hoare or separation logic could support mixed equational and logical reasoning.Source: §6 · p. 15