0.0.0.1 Keywords.

Reversible computation; causal-consistent reversibility; reversible causal nets (RCN);
reversible prime event structures (rPES); semantic rate–distortion; closure-preserving fidelity;
irredundant core decomposition; hypergraph entropy; rollback safety; Blahut–Arimoto algorithm.

1 Introduction↩︎

1.0.0.1 Rollback is not free.

Reversible computation studies models in which executed actions may be undone, motivated by fault recovery, debugging, and reversible views of concurrent or biochemical dynamics [1]–[4]. A recurring observation is that safe rollback requires auxiliary information about the forward run: to decide which reverse steps are legal and in what order, a system (or debugger) must retain enough evidence of causal dependencies, conflicts, prevention, and sometimes reverse-causality constraints [5]–[7]. This makes reversibility inherently discipline-sensitive: changing the reversing discipline changes what must be remembered.

1.0.0.2 A quantitative question.

While operational and axiomatic frameworks provide crisp correctness criteria (e.g., causal consistency and related safety properties), an orthogonal and practically central question remains: how many bits are necessary to represent a history so that the reconstructed history preserves rollback-relevant consequences? Classical information theory addresses “how many bits” questions via rate–distortion theory: given a source and a fidelity criterion, Shannon’s rate–distortion function characterizes the minimum rate needed to achieve a prescribed average distortion [8]–[10]. However, the fidelity criterion for rollback is not symbolwise (e.g., not Hamming distance on logged atoms): what matters is whether the decoder can answer the same rollback-relevant queries, such as which undo steps are blocked and which precedence obligations hold. A symbolwise distortion can over-penalize semantically redundant facts and under-represent global logical effects of local edits.

1.0.0.3 Closure-preserving fidelity as a semantic interface.

To align compression with rollback semantics, we adopt a closure-based interface. A single run is represented as a finite fact base \(S_O\subseteq\mathbb{S}\), and rollback-relevant semantics are modeled by a monotone closure operator \(\mathrm{Cn}_{\mathrm{rev}}\) induced by an effective rule system (e.g., function-free Horn rules / Datalog) [11], [12]. Rollback capability is then a closure observable, \(\mathsf{RB}(S)=\mathrm{Cn}_{\mathrm{rev}}(S)\cap\mathbb{Q}_{\mathrm{rb}}\), for a designated set \(\mathbb{Q}_{\mathrm{rb}}\) of rollback-relevant facts. Within this interface, a reconstruction \(\hat{S}_O\) is perfectly faithful for rollback if it preserves closure (\(\mathrm{Cn}_{\mathrm{rev}}(\hat{S}_O)=\mathrm{Cn}_{\mathrm{rev}}(S_O)\)), or more minimally preserves the rollback observable. We instantiate this at the single-symbol level by editing one fact at a time and measuring the induced closure change via a Jaccard-type distance, yielding a bounded finite-alphabet distortion suitable for Shannon rate–distortion analysis.

1.0.0.4 Key mechanism: redundancy becomes information-theoretically invisible.

Closure-preserving fidelity makes redundancy explicit. Many logged facts are consequences of others under \(\mathrm{Cn}_{\mathrm{rev}}\) and can be deleted (or replaced) without changing rollback semantics. We formalize this by a deterministic deletion scan that decomposes \(S_O\) into an irredundant core \(A\) and a redundant remainder \(J\). Under an admissible reconstruction alphabet \(\hat{\mathbb{S}}\subseteq \mathrm{Cn}_{\mathrm{rev}}(S_O)\), every redundant fact \(j\in J\) has zero distortion against every admissible reconstruction. As a result, both the zero-distortion limit and the full rate–distortion curve reduce to a core-only optimization problem scaled by the core mass \(P_A=P_O(A)\). This “core reduction” viewpoint is closely related in spirit to closure-based rate–distortion for deductive sources [13], and we show that it yields a natural quantitative frontier for reversible logging.

1.0.0.5 Endpoint law at \(D=0\): hypergraph entropy.

At zero distortion, the relevant object is not always Shannon entropy. If distinct core symbols admit overlapping sets of zero-distortion reconstructions, the \(D=0\) limit becomes a structured confusability problem. We capture this structure by a confusability hypergraph \(\Gamma_0\) induced by overlaps of zero-distortion reconstruction sets, and obtain an exact hypergraph-entropy characterization of the perfect-fidelity rate \(R_{\mathrm{sem}}(0)\). We further introduce a rollback-task loss that counts how many rollback judgments change under an edit, giving a task-aligned alternative rate–distortion function with the same core-only reduction principle.

1.0.0.6 Discipline-indexed instantiation on RCN/rPES.

We instantiate \(\mathrm{Cn}_{\mathrm{rev}}\) on reversible causal nets (RCN) and reversible prime event structures (rPES) by defining a family of discipline-indexed monotone closures for causal, cause-respecting, and inverse-causal semantics [7], [14]. This makes discipline sensitivity quantitative: different closures induce different cores, hence different zero-distortion rates and different rate–distortion trade-offs. We complement the theory with numerical evidence obtained by constructing finite alphabets/distortion matrices and computing finite-alphabet rate–distortion curves via Blahut–Arimoto [15], [16].

1.0.0.7 Contributions.

1. Semantic rate–distortion for reversible logging. We formulate reversible logging as a Shannon rate–distortion problem where fidelity is measured by preserving a reversible semantic closure \(\mathrm{Cn}_{\mathrm{rev}}\), and define a bounded single-symbol closure distortion \(d_{\mathrm{Cn}}\) aligned with rollback semantics.

2. Canonical core decomposition and redundancy invisibility. We prove a deterministic core decomposition \(S_O=A\uplus J\) with \(\mathrm{Cn}_{\mathrm{rev}}(A)=\mathrm{Cn}_{\mathrm{rev}}(S_O)\), and show that under admissibility \(\hat{\mathbb{S}}\subseteq\mathrm{Cn}_{\mathrm{rev}}(S_O)\) the redundant part \(J\) is distortion-free against all reconstructions. Consequently, \(R_{\mathrm{sem}}(D)\) factorizes into a core-only rate–distortion problem scaled by \(P_A\).

3. Exact zero-distortion law via hypergraph entropy. We characterize \(R_{\mathrm{sem}}(0)\) as a hypergraph-entropy quantity induced by overlaps of zero-distortion reconstruction sets on the core.

4. Rollback-task RD and discipline-indexed RCN/rPES instantiation. We introduce a rollback-task loss \(\ell_{\mathrm{rb}}\), derive a parallel core-only reduction principle, and instantiate the full framework on RCN/rPES under multiple reversing disciplines, with numerical verification of endpoint identities and factorization predictions.

1.0.0.8 Organization.

Section 2 defines the fact-base interface, reversible closure, and rollback observables. Section 3 develops semantic rate–distortion under closure-preserving fidelity. Section 4 connects semantic distortion to rollback safety and introduces rollback-task rate–distortion. Section 5 instantiates discipline-indexed closures on RCN/rPES and analyzes induced cores. Section 6 reports numerical evidence (enumeration, Blahut–Arimoto curves, and Monte Carlo sweeps). Section 7 reviews related work, and Section 8 concludes.

2 Preliminaries: Fact Bases, Proof Systems, and Rollback Semantics↩︎

This section fixes the semantic interface used throughout the paper. A single execution history is represented as a finite fact base \(S_O\subseteq\mathbb{S}\), and rollback-relevant semantics are expressed via invariance of a monotone closure operator \(\mathrm{Cn}_{\mathrm{rev}}\) induced by an effective proof system. Figure 1 depicts how this closure interface overlays a standard reversible logging pipeline and supports an application-level rate–distortion (RD) design loop. In the rest of the paper, preserving the full closure \(\mathrm{Cn}_{\mathrm{rev}}(S_O)\) is used as a sufficient fidelity criterion for rollback, while \(\mathsf{RB}(S)\) (Definition 3) captures the minimal rollback observable of interest. Our instantiations follow standard causal-consistent reversibility frameworks (e.g., RCCS/LTSI and reversible Petri-net/event-structure accounts) and reversible message-passing logs; see, e.g., [5], [7], [17].

2.0.0.1 Design choice (semantic interface).

Throughout, rollback-relevant semantics are treated as (projections of) closure consequences \(\mathrm{Cn}_{\mathrm{rev}}(S)\). Accordingly, we adopt closure preservation \(\mathrm{Cn}_{\mathrm{rev}}(\hat{S})=\mathrm{Cn}_{\mathrm{rev}}(S)\) as a principled and sufficient semantic fidelity criterion for reversible logging, aligning the reversible setting with closure-based compression.

2.1 Fact universe and log fact bases↩︎

2.1.0.1 Event vocabulary.

Fix a finite set \(\mathcal{E}\) of forward events. Let \(\underline{\mathcal{E}}\) be a disjoint set of corresponding reverse events; we write \(\underline{e}\) for the reverse of \(e\in\mathcal{E}\). In Petri-net settings, events may be transition occurrences; in process-calculus settings, events may be equivalence classes of transitions (as in LTSI/event-based accounts); in message-passing settings, events may be log primitives.

2.1.0.2 From events to constants.

We assume each event identifier \(e\in \mathcal{E}\cup \underline{\mathcal{E}}\) is represented by a corresponding constant symbol, so that event occurrences and relations can be recorded as ground facts in \(\mathbb{S}\).

2.1.0.3 Relations (model-agnostic interface).

We assume the target reversible model induces (possibly partially defined) relations on events:

• Causality \(<\;\subseteq \mathcal{E}\times \mathcal{E}\);

• Conflict \(\#\;\subseteq \mathcal{E}\times \mathcal{E}\);

• Reverse-causality \(\prec\;\subseteq \mathcal{E}\times \underline{\mathcal{E}}\) (“\(e\) is a cause of undoing \(u\)”);

• Prevention \(\triangleright\;\subseteq \mathcal{E}\times \underline{\mathcal{E}}\) (“presence of \(e\) blocks undoing \(u\)”);

• Optionally, sustained causation \(\ll\;\subseteq \mathcal{E}\times \mathcal{E}\), used in axiomatic frameworks to tie \(<\) to prevention constraints.

The concrete meaning of these relations is instantiated in Section 5.

2.1.0.4 Fact signature and ambient universe.

Let \(\Sigma_{\mathrm{rev}}\) be a finite relational signature containing at least the predicate symbols: \[\mathsf{Fwd}(\cdot),\;\mathsf{Rev}(\cdot),\;\mathsf{Occurs}(\cdot),\; \mathsf{Cause}(\cdot,\cdot),\;\mathsf{Conflict}(\cdot,\cdot),\; \mathsf{RevCause}(\cdot,\cdot),\;\mathsf{Prevent}(\cdot,\cdot).\] (Concrete instantiations may add, e.g., \(\mathsf{Key}(k,\cdot,\cdot)\), FIFO order facts, place/marking facts, etc.) Fix a finite set of constants containing all event identifiers for the execution under study (and any auxiliary identifiers such as keys). Let \(\mathbb{S}\) denote the set of all ground atoms over \(\Sigma_{\mathrm{rev}}\) and these constants. Since both the signature and the constant set are finite, the ambient universe \(\mathbb{S}\) is finite.

2.1.0.5 Background theory vs.logged facts.

For readability, we allow two equivalent presentations:

• All-in-log: \(S_O\) contains both dynamic and static facts relevant to the run.

• Fixed background: a fixed finite set \(\mathcal{B}\subseteq\mathbb{S}\) encodes the static semantics for the program/model, and \(S_O\) contains only dynamic history facts; then reasoning is performed over \(\mathcal{B}\cup S_O\).

All definitions below work in either view; when needed we will write \(\mathrm{Cn}_{\mathrm{rev}}(S)\) as shorthand for \(\mathrm{Cn}_{\mathrm{rev}}(\mathcal{B}\cup S)\) in the “fixed background” view.

2.2 A monotone reversible proof system and semantic closure↩︎

We now define the semantic closure operator that serves as the fidelity target for compression.

2.2.0.1 Proof system.

We assume an effective monotone proof system \(\mathsf{PS}_{\mathrm{rev}}\) over ground facts. In the concrete instantiations in this paper, \(\mathsf{PS}_{\mathrm{rev}}\) is given as a function-free Horn rule system (Datalog), so that \(\mathrm{Cn}_{\mathrm{rev}}(S)\) is the least fixed point of the associated immediate-consequence operator. The concrete rules are model-dependent, but conceptually they (i) propagate derived consequences of history facts and background structure, and (ii) derive rollback-relevant judgments (e.g., blocking evidence and precedence obligations). Crucially, we require that the induced closure operator satisfy the Tarski axioms (Assumption 2 below). For background on Datalog/Horn-rule inference and least-fixed-point semantics, see standard database references (e.g., [11]).

2.2.0.2 Least-fixed-point reading.

When \(\mathsf{PS}_{\mathrm{rev}}\) is given as function-free Horn rules (Datalog), we take \(\mathrm{Cn}_{\mathrm{rev}}(S)\) to be the least fixed point of the immediate-consequence operator induced by the rules, which coincides with Horn derivability [11], [18].

2.2.0.3 Remark (negative enabling conditions and monotone closures).

Many operational presentations of reversibility phrase enabling conditions negatively (e.g., “\(\underline{u}\) is enabled only if no preventer is present”). Such conditions are non-monotone if encoded directly as logical inference. In this paper, \(\mathrm{Cn}_{\mathrm{rev}}\) is required to be a monotone closure operator, so we do not derive conclusions from the absence of facts inside \(\mathrm{Cn}_{\mathrm{rev}}\). Instead, we encode evidence of blocking as positive derived facts, e.g., \[\mathsf{Prevent}(e,\underline{u}) \wedge \mathsf{Occurs}(e) \Rightarrow \mathsf{Blocked}(\underline{u}),\] and we choose rollback-relevant observables \(\mathbb{Q}_{\mathrm{rb}}\) so that rollback capability can be expressed using such positive evidence (e.g., blockers and precedence obligations). This keeps \(\mathrm{Cn}_{\mathrm{rev}}\) within the standard monotone Horn/Datalog setting while still capturing rollback constraints.

2.3 Rollback semantics and closure invariance↩︎

The role of \(\mathrm{Cn}_{\mathrm{rev}}\) is to provide a semantic interface for rollback. Concretely, we select a set \(\mathbb{Q}_{\mathrm{rb}}\subseteq \mathbb{S}\) of rollback-relevant query facts and define rollback capability as the closure projected to \(\mathbb{Q}_{\mathrm{rb}}\).

2.3.0.1 Rollback-relevant query vocabulary.

Let \(\mathbb{Q}_{\mathrm{rb}}\subseteq \mathbb{S}\) be a designated set of rollback-relevant ground facts. Typical examples include \[\mathsf{Blocked}(\underline{e}),\quad \mathsf{MustUndoBefore}(\underline{e},\underline{u}),\quad \mathsf{Maximal}(e),\quad \mathsf{NonMax}(e),\] depending on the chosen reversible model. Since \(\mathbb{S}\) is finite (Assumption 1) and \(\mathbb{Q}_{\mathrm{rb}}\subseteq \mathbb{S}\), the query set \(\mathbb{Q}_{\mathrm{rb}}\) is finite.

2.3.0.2 Closure invariance.

The next statement explains when rollback-equivalence coincides with full closure equivalence.

2.3.0.3 Interpretation and instantiation.

In applications (Section 5), we choose \(\mathbb{Q}_{\mathrm{rb}}\) so that \(\mathsf{RB}(S)\) captures the rollback-relevant consequences that are representable by positive evidence in a monotone setting (e.g., blocking evidence and precedence obligations). Thus, preserving \(\mathrm{Cn}_{\mathrm{rev}}(S_O)\) is a sufficient condition for preserving rollback capability, while preserving \(\mathsf{RB}(S_O)\) is the minimal requirement when only rollback observables matter. With this interface in place, we can apply closure-preserving rate–distortion ideas in the spirit of [13].

3 Semantic Rate–Distortion under Closure-Preserving Fidelity↩︎

This section instantiates a Shannon-style rate–distortion problem where distortion is measured by preservation of reversible semantic closure. The construction is in the same spirit as closure-based compression for finite deductive systems (cf.[13]), with the reversible closure \(\mathrm{Cn}_{\mathrm{rev}}\) playing the role of deductive closure.

3.1 Closure fidelity and single-symbol distortion↩︎

We follow the “single stored log” viewpoint: a finite log \(S_O\subseteq\mathbb{S}\) is given, and a random symbol is sampled from it.

3.1.0.1 Interpretation.

Admissibility says reconstructions are drawn from what is already semantically entailed by the original log. This matches the reversible-logging intuition: we only reconstruct facts that are semantically compatible with the original run.

3.1.0.2 Zero distortion.

By Lemma 3, \(d_{\mathrm{Cn}}(s,\hat{s})=0\) exactly when the single-symbol replacement preserves the full closure.

3.1.0.3 Remark (why single-symbol replacement).

The distortion \(d_{\mathrm{Cn}}(s,\hat{s})\) measures the semantic impact of modifying a log by one symbol while keeping the remaining facts fixed. This is the natural “local” perturbation in closure-based compression: although the edit is local at the syntactic level, its effect is global at the semantic level through \(\mathrm{Cn}_{\mathrm{rev}}\). This matches the reversible-logging viewpoint where a small change in the recorded history may enable/disable many rollback-relevant consequences.

3.2 Irredundant core and redundant part↩︎

3.3 Zero-distortion hypergraph and entropy law↩︎

This quantity is a hypergraph-valued analogue of confusability-based graph entropy (Körner) for zero-error settings [20], [21].

3.3.0.1 Witness-hyperedge view.

For each reconstruction symbol \(\hat{s}\in \hat{\mathbb{S}}\), define the induced witness set \[W_{\hat{s}}\mathrel{\vcenter{:}}= \{a\in A:\;\hat{s}\in R_0(a)\}.\] Then \(W_{\hat{s}}\in \Gamma_0\) whenever it is nonempty, since \(\hat{s}\in\bigcap_{a\in W_{\hat{s}}}R_0(a)\). Conversely, \(W\in\Gamma_0\) iff there exists some \(\hat{s}\in\hat{\mathbb{S}}\) such that \(W\subseteq W_{\hat{s}}\). Thus \(\Gamma_0\) is downward closed, and it can be visualized by representative witness hyperedges \(W_{\hat{s}}\) (cf.Figure 2, right).

3.3.0.2 Operational interpretation.

We interpret \(R_{\mathrm{sem}}(D)\) as the single-letter rate–distortion function of the memoryless extension in which \((S_1,\dots,S_n)\) are drawn i.i.d.from \(P_O\), and the encoder/decoder operates on blocks of length \(n\) with average distortion constraint. Under this standard setting, \(R_{\mathrm{sem}}(D)\) gives the optimal asymptotic rate; see, e.g., [9], [10].

The next theorem gives the exact zero-distortion rate in terms of a confusability hypergraph induced by the closure-preserving zero-distortion sets.

Figure 2 visualizes the key structural invariants: the partition \(S_O=A\uplus J\) with \(\mathrm{Cn}_{\mathrm{rev}}(A)=\mathrm{Cn}_{\mathrm{rev}}(S_O)\), and the way overlaps of \(R_0(a)\) over \(a\in A\) induce \(\Gamma_0\) and hence \(R_{\mathrm{sem}}(0)\).

3.3.0.3 From \(D=0\) to \(D>0\).

We now extend the zero-distortion law (Theorem 4) to general \(D\ge 0\) and show that, under admissibility, the full curve \(R_{\mathrm{sem}}(D)\) reduces to a core-only problem scaled by \(P_A=P_O(A)\).

3.4 General distortion: core-only factorization of the semantic rate–distortion function↩︎

3.4.0.1 Remark (effective distortion range).

Since \(d_{\mathrm{Cn}}\in[0,1]\) and \(d_{\mathrm{Cn}}(j,\hat{s})=0\) for all \(j\in J\) under admissibility (Proposition 3), the maximum achievable average distortion for the full source is \(D_{\max}=P_A\). Hence \(R_{\mathrm{sem}}(D)=0\) for all \(D\ge P_A\).

For convenience, let \(\mathsf{B}\mathrel{\vcenter{:}}= \mathbf{1}[S\in A]\) denote the indicator of whether the source symbol lies in the core.

4 Rollback Safety via Semantic Rate–Distortion↩︎

Section 3 gives a semantic RD theory under closure-preserving fidelity. Here we connect it to rollback computing in two steps: (i) we show that controlling the semantic distortion \(d_{\mathrm{Cn}}\) already yields exact and computable rollback-safety guarantees; (ii) we then introduce a rollback-task loss \(\ell_{\mathrm{rb}}\) that provides tighter, task-aligned guarantees and a refined RD tradeoff.

4.1 Rollback safety induced by closure-preserving fidelity↩︎

We work with the same single-symbol edit model as in Section 3.

4.2 Rollback-task loss and rollback-task rate–distortion↩︎

Closure-preserving fidelity yields conservative guarantees. We now introduce a task-aligned loss that measures how many rollback-relevant judgments change.

4.2.0.1 Admissibility and redundancy invisibility.

As in Section 3, admissibility (\(\hat{\mathbb{S}}\subseteq \mathrm{Cn}_{\mathrm{rev}}(S_O)\), Assumption 4) eliminates the redundant part \(J\) from the information-theoretic tradeoff.

4.3 Perfect rollback: hypergraph law and comparison with perfect closure preservation↩︎

4.3.0.1 Implication for computable design loops.

The finite-alphabet pipeline of Section 5.3.3 applies to both objectives: one may compute \(R_A(\delta)\) using \(d_{\mathrm{Cn}}\), or compute \(R_{\mathrm{rb},A}(\lambda)\) using \(\ell_{\mathrm{rb}}\), via the same Blahut–Arimoto machinery after constructing the corresponding distortion/loss matrix.

5 RCN/rPES Instantiation: Discipline-Indexed Closures and Core Structure↩︎

This section instantiates closure-preserving semantic rate–distortion on the reversible causal nets (RCN) and reversible prime event structures (rPES) correspondence of [7]. Our goal here is theoretical: define a discipline-indexed family of monotone closures capturing rollback-relevant semantics, and derive the resulting closure cores and zero-distortion confusability structure. Section 6 then reports the numerical and Monte Carlo evidence.

5.0.0.1 Link to rollback safety (Section 4).

The discipline-indexed closures defined in this section are not merely modeling choices: combined with the safety theorems of Section 4, they induce discipline-indexed lower bounds on the minimum logging rate required for perfect rollback safety and computable rate budgets for prescribed rollback-violation probability targets. In particular, once \(\mathrm{Cn}_{\mathrm{rev}}\) is instantiated as \(\mathrm{Cn}^{\mathrm{disc}}_{\mathrm{rcn}}\), Theorem 6 identifies the exact perfect-safety rate \(R_{\mathrm{sem}}(0)\), while Corollary 2 and Lemma 6 turn RD design objectives into explicit (conservative or tight) rollback-safety guarantees.

5.1 RCN/rPES background, logging interface, and discipline-indexed closures↩︎

We adopt the rcn setting of [7]. Let \(\overline{T}\) be the finite set of forward transitions and \(\underline{T}\) the set of backward transitions, with pairing \(\mathsf{pair}:\underline{T}\to\overline{T}\). Forward causality is induced by inhibitor arcs: \[t\;\ell\;t' \quad\Longleftrightarrow\quad {^\bullet t}\cap {^\circ t'}\neq\emptyset,\] and forward conflict is induced by shared preset: \[t\;\#\;t' \quad\Longleftrightarrow\quad {^\bullet t}\cap {^\bullet t'}\neq\emptyset.\] As in Sections 2–4, an execution state is logged as a finite fact base.

5.1.0.1 Configuration and log.

A (forward) configuration is a finite set \(X\subseteq \overline{T}\) of forward transitions currently present. The run-specific fact base is \[S_O^{\mathrm{rcn}}(X)\;\mathrel{\vcenter{:}}=\;\{\mathsf{In}(t): t\in X\}.\] Static net structure facts (preset/inhibitor/pairing) live in a background theory \(\mathcal{B}_{\mathrm{rcn}}\) [7]. Concretely, \(\mathcal{B}_{\mathrm{rcn}}\) contains ground facts for \(\mathsf{Pre}(p,t)\), \(\mathsf{Inhib}(p,t)\), and the pairing map (e.g., a predicate \(\mathsf{Pair}(\underline{t},t)\) encoding \(\mathsf{pair}(\underline{t})=t\)), so that \(\mathrm{Cn}_{\mathrm{rev}}(S)\) reasons over \(\mathcal{B}_{\mathrm{rcn}}\cup S\) rather than requiring these structural facts to be logged per run.

A central message of [7] is that different reversing disciplines (causal, cause-respecting, inverse causal, out-of-causal-order) change which facts are rollback-relevant. To capture this systematically within our closure-preserving interface, we define a discipline-indexed family of monotone Horn systems \(\mathsf{PS}^{\mathrm{disc}}_{\mathrm{rcn}}\) inducing closures \(\mathrm{Cn}^{\mathrm{disc}}_{\mathrm{rcn}}\).

5.1.1 Common structural rules: causality and conflict evidence↩︎

We use the following shared predicates in \(\Sigma_{\mathrm{rev}}\): \[\mathsf{Pre}(p,t),\;\mathsf{Inhib}(p,t),\;\mathsf{In}(t),\; \mathsf{Cause}(t,t'),\;\mathsf{Cause}^\star(t,t'),\; \mathsf{Conf}(t,t').\] All ground \(\mathsf{Pre}(\cdot,\cdot)\) and \(\mathsf{Inhib}(\cdot,\cdot)\) facts are assumed to be part of the background theory \(\mathcal{B}_{\mathrm{rcn}}\). We write \(\mathsf{Conf}(\cdot,\cdot)\) as a shorthand for the conflict predicate \(\mathsf{Conflict}(\cdot,\cdot)\) introduced in Section 2. Rules (R1)–(R2) provide a fact-level encoding of the structural relations \(t\;\ell\;t'\) and \(t\;\#\;t'\) introduced above: \(\mathsf{Cause}(t,t')\) captures inhibitor-induced causality, and \(\mathsf{Conf}(t,t')\) captures shared-preset conflict.

5.1.1.1 (R1) Inhibitor-induced causality and its transitive closure.

\[\mathsf{Pre}(p,t)\wedge \mathsf{Inhib}(p,t')\Rightarrow \mathsf{Cause}(t,t'), \qquad \mathsf{Cause}(t,t')\Rightarrow \mathsf{Cause}^\star(t,t'),\] \[\mathsf{Cause}^\star(t,u)\wedge \mathsf{Cause}^\star(u,t')\Rightarrow \mathsf{Cause}^\star(t,t').\]

5.1.1.2 (R2) Conflict evidence (structural).

\[\mathsf{Pre}(p,t)\wedge \mathsf{Pre}(p,t')\wedge (t\neq t')\Rightarrow \mathsf{Conf}(t,t').\] We treat \(t\neq t'\) as a built-in inequality predicate on constants (standard in Datalog-style presentations).

5.1.2 Causal-consistent (“causal”) discipline closure↩︎

5.1.2.1 (CC1) Semantic downward closure of presence.

\[\mathsf{In}(t)\wedge \mathsf{Cause}^\star(u,t)\Rightarrow \mathsf{In}(u).\]

5.1.2.2 (CC2) Non-maximality and rollback blockers.

\[\mathsf{In}(t)\wedge \mathsf{Cause}^\star(t,u)\wedge \mathsf{In}(u)\Rightarrow \mathsf{NonMax}(t), \qquad \mathsf{NonMax}(t)\Rightarrow \mathsf{Blocked}(\underline{t}).\] Optionally record order constraints: \[\mathsf{In}(t)\wedge \mathsf{In}(u)\wedge \mathsf{Cause}^\star(t,u)\Rightarrow \mathsf{MustUndoBefore}(\underline{t},\underline{u}).\]

5.1.2.3 Closure and rollback query set.

Let \(\mathsf{PS}^{\mathrm{causal}}_{\mathrm{rcn}}\) be the Horn system comprising (R1)–(R2) plus (CC1)–(CC2). Define \[\mathrm{Cn}^{\mathrm{causal}}_{\mathrm{rcn}}(S)\;\mathrel{\vcenter{:}}=\;\{s\in\mathbb{S}:\;\mathcal{B}_{\mathrm{rcn}}\cup S\vdash_{\mathsf{PS}^{\mathrm{causal}}_{\mathrm{rcn}}} s\}, \quad \mathbb{Q}^{\mathrm{causal}}_{\mathrm{rb}}\mathrel{\vcenter{:}}= \{\mathsf{Blocked}(\underline{t}),\mathsf{NonMax}(t),\mathsf{MustUndoBefore}(\underline{t},\underline{u})\}.\]

5.1.3 Cause-respecting discipline closure↩︎

5.1.3.1 Sustained causation evidence.

We introduce \(\mathsf{Sust}(t,u)\), intended to represent the sustained causation relation \(\ll\) in [7]. For our purposes it is sufficient to treat \(\mathsf{Sust}\) as either (i) a background predicate in \(\mathcal{B}_{\mathrm{rcn}}\), or (ii) a derived predicate computed by a fixed (finite) Horn rule set.

5.1.3.2 (CR1) Sustained-nonmaximality and blockers.

\[\mathsf{In}(t)\wedge \mathsf{Sust}(t,u)\wedge \mathsf{In}(u)\Rightarrow \mathsf{NonMax}^{\ll}(t), \qquad \mathsf{NonMax}^{\ll}(t)\Rightarrow \mathsf{Blocked}(\underline{t}).\]

5.1.3.3 Closure and query set.

Let \(\mathsf{PS}^{\mathrm{cr}}_{\mathrm{rcn}}\) be (R1)–(R2) plus (CC1) plus (CR1). Define \[\mathrm{Cn}^{\mathrm{cr}}_{\mathrm{rcn}}(S)\mathrel{\vcenter{:}}= \{s:\mathcal{B}_{\mathrm{rcn}}\cup S\vdash_{\mathsf{PS}^{\mathrm{cr}}_{\mathrm{rcn}}} s\}, \quad \mathbb{Q}^{\mathrm{cr}}_{\mathrm{rb}}\mathrel{\vcenter{:}}= \{\mathsf{Blocked}(\underline{t}),\mathsf{NonMax}^{\ll}(t)\}.\]

5.1.4 Inverse causal discipline closure↩︎

5.1.4.1 Why (CC1) is not assumed under inverse-causal reversibility.

In causal-consistent settings, forward presence is downward closed: if a consequence is present, then its causes are present as well, which is precisely what (CC1) captures in a monotone proof system. In contrast, inverse-causal (and more generally out-of-causal-order) reversibility may admit states in which a cause has been undone while some of its former consequences remain present. Therefore downward closure of \(\mathsf{In}(\cdot)\) is not a discipline-invariant semantic law, and we do not include (CC1) in \(\mathsf{PS}^{\mathrm{inv}}_{\mathrm{rcn}}\). This is exactly the mechanism by which inverse-causal rollback evidence can force additional log atoms into the closure core (Section 5.2).

Inverse causal reversibility changes rollback gating: undoing is prevented by the presence of causes rather than consequences [7].

5.1.4.2 (IC1) Blockers from causes present.

\[\mathsf{In}(u)\wedge \mathsf{Cause}^\star(u,t)\Rightarrow \mathsf{CausePresent}(u,t), \qquad \mathsf{CausePresent}(u,t)\Rightarrow \mathsf{Blocked}(\underline{t}).\]

5.1.4.3 Closure and query set.

Let \(\mathsf{PS}^{\mathrm{inv}}_{\mathrm{rcn}}\) be (R1)–(R2) plus (IC1). Define \[\mathrm{Cn}^{\mathrm{inv}}_{\mathrm{rcn}}(S)\mathrel{\vcenter{:}}= \{s:\mathcal{B}_{\mathrm{rcn}}\cup S\vdash_{\mathsf{PS}^{\mathrm{inv}}_{\mathrm{rcn}}} s\}, \quad \mathbb{Q}^{\mathrm{inv}}_{\mathrm{rb}}\mathrel{\vcenter{:}}= \{\mathsf{Blocked}(\underline{t}),\mathsf{CausePresent}(u,t)\}.\]

5.2 Core computation depends on the rollback discipline↩︎

The closure-based core \(A=\mathrm{Atom}_{\mathrm{rev}}(S_O)\) (Definition 7) is discipline-dependent through the chosen \(\mathrm{Cn}_{\mathrm{rev}}\). We now characterize the causal and cause-respecting cores as frontier-shaped, and give an explicit counterexample for inverse causal semantics.

5.2.1 Causal discipline: frontier-core result↩︎

5.2.2 Inverse causal discipline: frontier can be insufficient↩︎

5.2.3 Cause-respecting discipline: frontier core under downward-closed presence↩︎

5.2.3.1 Running example (Fig. 8 in [7]).

Figure 3 visualizes, on the Fig. 8 instance of [7], how the closure interface \(\mathrm{Cn}_{\mathrm{rev}}\) makes redundancy invisible and reduces logging complexity to the frontier-shaped core. Starting from \(S_O=\{\mathsf{In}(a),\mathsf{In}(b),\mathsf{In}(c),\mathsf{In}(d)\}\), the deletion scan (Definition 7) deletes \(\mathsf{In}(a)\) and \(\mathsf{In}(b)\) because, in that instance, they are derivable from \(\{\mathsf{In}(c),\mathsf{In}(d)\}\) under the downward-closure rule (CC1), while \(\mathsf{In}(c)\) and \(\mathsf{In}(d)\) are irredundant. Thus the core coincides with the frontier: \(A=S_O^{\mathrm{rcn}}(\mathop{\mathrm{Fr}}(X))\). The bottom row of the figure also previews why inverse-causal closures can force additional causes into the core to preserve blocker evidence (cf.Proposition 11).

5.3 Rates, reconstruction alphabets, and computability↩︎

5.3.0.1 Discipline-indexed logging rates for rollback safety.

We now make explicit how the general safety theorems of Section 4 specialize to the RCN instantiation. These discipline-indexed quantities are exactly what we compute in Section 6 to obtain the BA curves and core sizes.

5.3.0.2 Approximate safety budgets.

For a target rollback-violation probability \(\varepsilon\), Corollary 2 yields the conservative design rule \[\mathbb{E}[d_{\mathrm{Cn}}(S,\hat{S})]\le \varepsilon/|\mathbb{S}| \quad\Longrightarrow\quad \Pr[\mathsf{Viol}(S,\hat{S})=1]\le \varepsilon,\] and hence a computable rate budget \(\text{rate}\ge R_{\mathrm{sem}}(\varepsilon/|\mathbb{S}|)\). Alternatively, the task loss \(\ell_{\mathrm{rb}}\) yields the tighter guarantee \(\Pr[\mathsf{Viol}(S,\hat{S})=1]\le \mathbb{E}[\ell_{\mathrm{rb}}(S,\hat{S})]\) (Lemma 6), which motivates computing the rollback-task RD function \(R_{\mathrm{rb}}(L)\) on the same RCN instance.

5.3.1 Rollback-task instantiation on RCN: \(\ell_{\mathrm{rb}}\), \(R_{\mathrm{rb}}(L)\), and perfect-rollback rates↩︎

Throughout this subsubsection, fix a discipline \(\mathrm{disc}\in\{\mathrm{causal},\mathrm{cr},\mathrm{inv}\}\). We write \(\mathrm{Cn}_{\mathrm{rev}}=\mathrm{Cn}^{\mathrm{disc}}_{\mathrm{rcn}}\) and \(\mathbb{Q}_{\mathrm{rb}}=\mathbb{Q}^{\mathrm{disc}}_{\mathrm{rb}}\) for the corresponding closure operator and rollback query set defined in Section 5.1. All closures \(\mathrm{Cn}^{\mathrm{disc}}_{\mathrm{rcn}}(\cdot)\) are computed over the fixed background theory \(\mathcal{B}_{\mathrm{rcn}}\).

5.3.1.1 Rollback observable for RCN.

For any run-specific fact base \(S\subseteq \mathbb{S}\), define the discipline-indexed rollback observable \[\mathsf{RB}^{\mathrm{disc}}(S)\;\mathrel{\vcenter{:}}=\;\mathrm{Cn}^{\mathrm{disc}}_{\mathrm{rcn}}(S)\;\cap\;\mathbb{Q}^{\mathrm{disc}}_{\mathrm{rb}}.\] (As usual, \(\mathrm{Cn}^{\mathrm{disc}}_{\mathrm{rcn}}(S)\) is computed over \(\mathcal{B}_{\mathrm{rcn}}\cup S\).)

5.3.1.2 Rollback-task loss for RCN (single-symbol edit).

Fix a configuration \(X\subseteq \overline{T}\) and its log \(S_O=S_O^{\mathrm{rcn}}(X)=\{\mathsf{In}(t):t\in X\}\). For \(s\in S_O\) and \(\hat{s}\in \hat{\mathbb{S}}\), write \[S_O[s\leftarrow \hat{s}]\;\mathrel{\vcenter{:}}=\;(S_O\setminus\{s\})\cup\{\hat{s}\}.\] Define the discipline-indexed rollback-task loss \[\ell^{\mathrm{disc}}_{\mathrm{rb}}(s,\hat{s}) \;\mathrel{\vcenter{:}}=\; \bigl|\mathsf{RB}^{\mathrm{disc}}(S_O[s\leftarrow \hat{s}])\;\Delta\;\mathsf{RB}^{\mathrm{disc}}(S_O)\bigr|.\] Thus \(\ell^{\mathrm{disc}}_{\mathrm{rb}}(s,\hat{s})=0\) if and only if the edit preserves all rollback-relevant judgments in \(\mathbb{Q}^{\mathrm{disc}}_{\mathrm{rb}}\) (for the chosen discipline).

5.3.1.3 Rollback-task RD function for RCN.

Let \(S\sim P_O\) be a random fact symbol supported on \(S_O\) (Assumption 3), and let \(\hat{S}\in\hat{\mathbb{S}}\subseteq \mathrm{Cn}^{\mathrm{disc}}_{\mathrm{rcn}}(S_O)\) be generated by a test channel \(P_{\hat{S}\mid S}\). Define \[R^{\mathrm{disc}}_{\mathrm{rb}}(L) \;\mathrel{\vcenter{:}}=\; \inf_{P_{\hat{S}\mid S}:\;\mathbb{E}[\ell^{\mathrm{disc}}_{\mathrm{rb}}(S,\hat{S})]\le L}\;I(S;\hat{S}).\]

5.3.1.4 Core-only factorization (RCN specialization).

This paragraph specializes Theorem 7 to the RCN setting. Recall that the deletion-scan core \(\mathrm{Atom}_{\mathrm{rev}}(S_O)\) depends on the chosen closure operator; here it is computed using \(\mathrm{Cn}^{\mathrm{disc}}_{\mathrm{rcn}}\). Let \(A^{\mathrm{disc}}\mathrel{\vcenter{:}}= \mathrm{Atom}_{\mathrm{rev}}(S_O)\) denote the deletion-scan core of \(S_O\) computed with respect to the closure \(\mathrm{Cn}^{\mathrm{disc}}_{\mathrm{rcn}}\) (Definition 7). Let \(A^\star\sim \pi_A^{\mathrm{disc}}\) denote a random core symbol.

5.3.1.5 Perfect rollback (RCN form of Theorem 8).

Define the zero-loss reconstruction sets \[R^{\mathrm{rb},\mathrm{disc}}_0(s)\;\mathrel{\vcenter{:}}=\;\{\hat{s}\in\hat{\mathbb{S}}:\;\ell^{\mathrm{disc}}_{\mathrm{rb}}(s,\hat{s})=0\},\] and the induced rollback confusability hypergraph on the core: \[\Gamma^{\mathrm{rb},\mathrm{disc}}_0 \;\mathrel{\vcenter{:}}=\; \Bigl\{W\subseteq A^{\mathrm{disc}}:\;W\neq\emptyset,\;\bigcap_{a\in W}R^{\mathrm{rb},\mathrm{disc}}_0(a)\neq\emptyset\Bigr\}.\] Let \(H_{\Gamma^{\mathrm{rb},\mathrm{disc}}_0}(\pi_A^{\mathrm{disc}})\) be the corresponding hypergraph entropy as in Definition 17 (with \(A=A^{\mathrm{disc}}\) and \(\pi_A=\pi_A^{\mathrm{disc}}\)).

5.3.1.6 Computability and experimental pipeline.

The same finite-alphabet pipeline used to compute \(R_A(\delta)\) from the distortion matrix \(d(a,\hat{s})=d_{\mathrm{Cn}}(a,\hat{s})\) applies to rollback-task RD as well: one explicitly computes the loss matrix \(\ell(a,\hat{s})=\ell^{\mathrm{disc}}_{\mathrm{rb}}(a,\hat{s})\) (by recomputing \(\mathsf{RB}^{\mathrm{disc}}(\cdot)\) under single-symbol edits), and then runs Blahut–Arimoto to obtain \(R^{\mathrm{disc}}_{\mathrm{rb},A}(\lambda)\). Overall rates are recovered by the scaling in Corollary 3.

5.3.2 Nontrivial hyperedges via admissible summaries↩︎

If the reconstruction alphabet contains only concrete presence facts \(\mathsf{In}(t)\), then zero-distortion sets \(R_0(a)\) are often singletons, making \(\Gamma_0\) trivial. We introduce admissible summary atoms that (i) remain in the closure of the original log, and (ii) create overlaps among the \(R_0(a)\), yielding strict hypergraph-entropy gains.

5.3.2.1 Admissible summary atoms as a fixed rule schema.

To preserve Assumption 4 under a fixed public proof system, we avoid introducing run-specific symbols that depend on private encoder choices. Instead, we use a public, canonical naming scheme in which all summary constants are determined solely by the finite transition-ID set of the run and the shared order \(\prec\).

Concretely, for each ordered pair \((t,u)\) with \(t\prec u\), we allow a summary constant \(\sigma_{t,u}\) and a predicate \(\mathsf{Summ}(\sigma_{t,u})\). We then include the following fixed Horn-rule schema in the background theory (or, equivalently, in \(\mathsf{PS}^{\mathrm{disc}}_{\mathrm{rcn}}\)): \[\mathsf{In}(t)\wedge \mathsf{In}(u)\wedge \mathsf{Conc}(t,u)\Rightarrow \mathsf{Summ}(\sigma_{t,u}),\] \[\mathsf{Summ}(\sigma_{t,u})\Rightarrow \mathsf{In}(t), \qquad \mathsf{Summ}(\sigma_{t,u})\Rightarrow \mathsf{In}(u).\] Here \(\mathsf{Conc}(t,u)\) is a public (static) concurrency predicate, e.g., derivable from the net structure as “not related by \(\mathsf{Cause}^\star\) in either direction and not in conflict (\(\mathsf{Conf}\)).” We treat \(\mathsf{Conc}(\cdot,\cdot)\) as an extensional background predicate (precomputed from the net structure), rather than as a predicate derived inside \(\mathrm{Cn}^{\mathrm{disc}}_{\mathrm{rcn}}\) using negation, in order to preserve monotonicity. With this schema, whenever \(t,u\in X\) are concurrent, we have \(\mathsf{Summ}(\sigma_{t,u})\in \mathrm{Cn}^{\mathrm{disc}}_{\mathrm{rcn}}(S_O^{\mathrm{rcn}}(X))\) for every fixed discipline \(\mathrm{disc}\in\{\mathrm{causal},\mathrm{cr},\mathrm{inv}\}\) that includes the summary-rule schema in its background theory (or proof system). Therefore such summary atoms are admissible reconstruction symbols under Assumption 4 and can create nontrivial overlaps among the sets \(R_0(a)\) (and analogously among the zero-loss sets \(R^{\mathrm{rb}}_0(a)\) defined via \(\ell_{\mathrm{rb}}\)).

In our experiments we restrict to pair summaries (i.e., summaries over two concurrent transitions), which already yield nontrivial overlaps while keeping the alphabet size manageable.

5.3.3 Computability: finite-alphabet BA evaluation↩︎

Fix a finite core alphabet \(A\) and finite reconstruction alphabet \(\hat{\mathbb{S}}\) (e.g., concrete facts plus summaries). Define the distortion matrix \(d(a,\hat{s})\mathrel{\vcenter{:}}= d_{\mathrm{Cn}}(a,\hat{s})\).

5.3.3.1 Core-only curves vs.overall rates.

Recall from Theorem 5 that the overall semantic RD function satisfies \(R_{\mathrm{sem}}(D)=P_A\cdot R_A(\min\{D/P_A,1\})\). Accordingly, in the RCN experiments we report the core-only curves \(R_A(\cdot)\) (which capture the nontrivial part of the tradeoff), and recover the overall per-symbol rate for the full source via the scaling factor \(P_A=P_O(A)\).

5.3.3.2 Practical pipeline.

Given a discipline closure \(\mathrm{Cn}^{\mathrm{disc}}_{\mathrm{rcn}}\), one can: (i) compute the deletion-scan core \(A\); (ii) generate an admissible alphabet \(\hat{\mathbb{S}}\) (e.g., pair summaries); (iii) compute the distortion matrix by explicit closure computations under single-symbol edits; and (iv) run BA to obtain \(R_A(\delta)\). The next section reports results produced by this pipeline.

6 Experiments: Ablation on Reconstruction Alphabet and Factorization Verification↩︎

6.0.0.1 Experimental scope and what is verified.

Using the RCN instantiation of Section 5, we report four types of numerical evidence computed by a local Python verifier: (i) an ablation at zero semantic distortion comparing a facts-only reconstruction alphabet to an augmented admissible alphabet; (ii) an exact endpoint verification at \(D=0\) of the perfect-safety statement and the zero-distortion hypergraph-entropy identity (Theorem 6 and Theorem 4); (iii) a Monte Carlo verification of the core-only factorization for rollback-task RD (Theorem 7); and (iv) an exact endpoint verification at \(L=0\) of the rollback hypergraph-entropy identity together with the comparison \(R_{\mathrm{rb}}(0)\le R_{\mathrm{sem}}(0)\) (Theorem 8 and Proposition 9).

6.0.0.2 Source distribution convention.

Unless explicitly stated otherwise, we take \(P_O\) to be the uniform distribution over the fixed log fact base \(S_O\) (i.e., \(S\sim P_O\) samples a fact symbol uniformly from \(S_O\)). Accordingly, when \(P_A>0\), the conditional core distribution \(\pi_A(\cdot)=P_O(\cdot\mid A)\) is uniform over \(A\).

6.0.0.3 Medium-scale instance (ablation summary at \(D=0\)).

As a sanity check on the role of the reconstruction alphabet \(\hat{\mathbb{S}}\), Table 1 reports, for a representative medium instance (\(B=4\), depth \(d=3\)), the instance size \(|X|\), frontier size \(|\mathop{\mathrm{Fr}}|\), core size \(|A|\), and the core-only zero-distortion rates \(R_A(0)\) under a facts-only vs.facts+summary admissible reconstruction alphabet.

6.0.0.4 Observed ablation outcome.

In this run, the gain \(\Delta R_A(0)\) is numerically \(0\) for all three disciplines (to six decimal places), i.e., the currently implemented admissible summaries do not reduce the \(D=0\) rate. This suggests that, for this instance and summary-rule schema, the added symbols do not create additional useful overlaps among the core zero-distortion sets \(\{R_0(a)\}_{a\in A}\) beyond numerical precision. Accordingly, the rest of Section 6 focuses on validating the key structural theorems linking closure-based RD to rollback safety and discipline-dependent cores.

6.1 Zero-distortion endpoint check (\(D=0\)): safety and hypergraph-entropy identity↩︎

This subsection provides an exact endpoint (\(D=0\)) numerical check for the two key \(D=0\) implications proved in Section 4–Section 3: (i) perfect safety from perfect closure preservation (Theorem 6); and (ii) the zero-distortion hypergraph-entropy law (Theorem 4). All results are computed on the medium instance \((B=4,d=3)\) used in Section 6. We sample a fact symbol \(S\sim P_O\) from the fixed log \(S_O\) (Assumption 3), use an admissible reconstruction alphabet \(\hat{\mathbb{S}}\subseteq \mathrm{Cn}_{\mathrm{rev}}(S_O)\) (Assumption 4), and instantiate \(\mathrm{Cn}_{\mathrm{rev}}=\mathrm{Cn}^{\mathrm{disc}}_{\mathrm{rcn}}\) and \(\mathbb{Q}_{\mathrm{rb}}=\mathbb{Q}_{\mathrm{rb}}^{\mathrm{disc}}\) as in Section 5.

6.1.0.1 Safety check by full enumeration.

We enumerate all pairs \((s,\hat{s})\in S_O\times\hat{\mathbb{S}}\) and verify the pointwise implication \[d_{\mathrm{Cn}}(s,\hat{s})=0 \;\Longrightarrow\;\mathsf{Viol}(s,\hat{s})=0,\] where \(d_{\mathrm{Cn}}\) is the closure Jaccard distortion (Definition 6) and \(\mathsf{Viol}\) is the rollback-violation indicator (Definition 12). Table 2 reports the total number of zero-distortion pairs and the number of violations among them. In all disciplines the number of violations is \(0\), consistent with Theorem 6.

6.1.0.2 Why the number of zero-distortion pairs differs across disciplines.

The count in Table 2, \[\#\bigl\{(s,\hat{s})\in S_O\times\hat{\mathbb{S}}:\;d_{\mathrm{Cn}}(s,\hat{s})=0\bigr\},\] equals \(\sum_{s\in S_O}|R_0(s)|\), where \(R_0(s)=\{\hat{s}\in\hat{\mathbb{S}}:d_{\mathrm{Cn}}(s,\hat{s})=0\}\). Under admissibility (Assumption 4), every redundant symbol \(j\in J\) satisfies \(|R_0(j)|=|\hat{\mathbb{S}}|\) by Proposition 3. Hence \[\#\{(s,\hat{s}): d_{\mathrm{Cn}}(s,\hat{s})=0\} = |J|\cdot|\hat{\mathbb{S}}| + \sum_{a\in A} |R_0(a)|.\] Therefore the counts differ across disciplines because the induced core/redundant split \((A,J)\) and the admissible reconstruction alphabet size \(|\hat{\mathbb{S}}|\) are discipline-dependent. In particular, in this instance the observed zero-distortion pair counts are \(324\) (causal), \(228\) (cause-respecting), and \(12\) (inverse-causal), reflecting that inverse-causal closure typically reduces the redundant mass \(|J|\) and thus removes the dominant \(|J|\cdot|\hat{\mathbb{S}}|\) contribution.

6.1.0.3 Hypergraph-entropy identity at \(D=0\).

We next check the equality of Theorem 4: \[R_{\mathrm{sem}}(0)=P_A\,H_{\Gamma_0}(\pi_A), \qquad P_A\mathrel{\vcenter{:}}= P_O(A),\quad \pi_A(\cdot)\mathrel{\vcenter{:}}= P_O(\cdot\mid A),\] by explicitly constructing the core \(A=\mathrm{Atom}_{\mathrm{rev}}(S_O)\), the zero-distortion sets \(\{R_0(a)\}_{a\in A}\), the induced confusability hypergraph \(\Gamma_0\), and the hypergraph entropy \(H_{\Gamma_0}(\pi_A)\). We then compare \(H_{\Gamma_0}(\pi_A)\) against an independent endpoint computation of the core-only perfect-reconstruction rate \(R_A(0)\) (i.e., minimizing rate subject to the hard constraint \(d_{\mathrm{Cn}}(A^\star,\hat{S})=0\) almost surely). Table 3 reports the resulting values. In all disciplines, \(H_{\Gamma_0}(\pi_A)\) and \(R_A(0)\) coincide to numerical precision, and the scaled quantities \(P_AH_{\Gamma_0}(\pi_A)\) and \(P_AR_A(0)\) match exactly as predicted.

6.1.0.4 Interpretation (discipline sensitivity through the core).

Under causal and cause-respecting closures, only \(|A|=4\) out of \(|S_O|=12\) facts are core-relevant on this instance, hence \(P_A=|A|/|S_O|=1/3\) under a uniform source over \(S_O\), yielding \(R_{\mathrm{sem}}(0)=\tfrac{1}{3}\cdot 2=\tfrac{2}{3}\) bits/symbol. Under inverse-causal closure the core expands to the full log (\(|A|=|S_O|\)), so \(P_A=1\) and the endpoint rate increases accordingly. This numerically illustrates the central message of Section 5: changing the reversing discipline changes the closure, thereby changing the core and the information-theoretic logging frontier.

6.2 Rollback-task RD factorization verification (core-only reduction)↩︎

This subsection provides numerical evidence for the core-only factorization of the rollback-task rate–distortion function stated in Theorem 7 (and its RCN specialization Corollary 3). Concretely, under admissibility \(\hat{\mathbb{S}}\subseteq \mathrm{Cn}_{\mathrm{rev}}(S_O)\), redundant symbols \(J\) are loss-invisible (Lemma 7), and the overall rollback-task RD function satisfies \[R_{\mathrm{rb}}(L) = \begin{cases} 0, & P_A=0,\\[1mm] P_A\cdot R_{\mathrm{rb},A}\!\Bigl(\min\bigl\{L/P_A,\;|\mathbb{Q}_{\mathrm{rb}}|\bigr\}\Bigr), & P_A>0, \end{cases}\] where \(A=\mathrm{Atom}_{\mathrm{rev}}(S_O)\) is the deletion-scan core, \(P_A=P_O(A)\), \(R_{\mathrm{rb},A}(\cdot)\) is the rollback-task RD function of the core sub-source \(A^\star\sim \pi_A\), and \(\mathbb{Q}_{\mathrm{rb}}\) is the rollback query set.

6.2.0.1 What is being checked numerically.

For each discipline and each randomized instance/seed, we compute (i) a core-only BA curve \(R_{\mathrm{rb},A}(\lambda)\) on a budget grid \(\lambda\in[0,|\mathbb{Q}_{\mathrm{rb}}|]\), (ii) the overall curve \(R_{\mathrm{rb}}(L)\) on a corresponding overall budget grid \(L\in[0,P_A|\mathbb{Q}_{\mathrm{rb}}|]\), and report a mean absolute deviation (“mean factor.err.”) between the two sides of the factorization after rescaling: \[\text{factorization error} \;\mathrel{\vcenter{:}}=\; \frac{1}{|\mathcal{G}|}\sum_{L\in\mathcal{G}} \Bigl|\,R_{\mathrm{rb}}(L)\;-\;P_A\cdot R_{\mathrm{rb},A}\!\bigl(\min\{L/P_A,|\mathbb{Q}_{\mathrm{rb}}|\}\bigr)\Bigr|,\] for the evaluation grid \(\mathcal{G}\) used by the program.¹ Values close to \(0\) indicate exact agreement up to numerical precision, thus validating the factorization identity.

6.2.0.2 Evaluation grid \(\mathcal{G}\).

To make the factorization check fully reproducible, we specify the evaluation grid explicitly. Throughout, we use the same Blahut–Arimoto sweep parameter grid \[\mathcal{B}\;\mathrel{\vcenter{:}}=\;\{0,\;0.5,\;1,\;2,\;4,\;8,\;16\}.\] For each instance and discipline, the program runs BA at each \(\beta\in\mathcal{B}\) and records the corresponding achieved overall loss budget \(L(\beta)\) and rate \(R_{\mathrm{rb}}(L(\beta))\). We then define the evaluation grid used in the mean absolute deviation as \[\mathcal{G}\;\mathrel{\vcenter{:}}=\;\{\,L(\beta):\;\beta\in\mathcal{B}\,\}, \qquad |\mathcal{G}|=|\mathcal{B}|=7,\] and evaluate the factorization identity on these grid points. (Using a denser grid yields the same qualitative conclusion; we report the \(\beta\)-grid results since it is the one directly produced by the BA sweep and shared by all experiments.)

6.2.1 Medium instance: core BA curves (semantic vs.rollback-task)↩︎

Figure 4 reports the core-only BA curves on a medium instance (\(B=4\), \(d=3\)). The left panel is the semantic core RD curve \(R_A(D)\) induced by the closure distortion \(d_{\mathrm{Cn}}\), and the right panel is the rollback-task core RD curve \(R_{\mathrm{rb},A}(L)\) induced by \(\ell_{\mathrm{rb}}\). These curves serve two purposes: (i) they confirm that the BA pipeline over the computed distortion/loss matrices is numerically stable on the core, and (ii) they provide the core-level tradeoff objects that enter the factorization formula via the scaling \(P_A\).

6.2.1.1 Interpretation of the medium curves.

On this instance and evaluation grid, the two BA sweeps produce essentially identical rate values (up to printing precision), suggesting that the chosen rollback query set \(\mathbb{Q}_{\mathrm{rb}}\) and the implementation of \(\ell_{\mathrm{rb}}\) are, in this setting, nearly as stringent as full closure preservation on the core. Importantly for the present subsection, factorization does not require the two objectives to differ; it requires only that the overall rollback-task RD curve is a \(P_A\)-scaled version of the core curve, which we test next.

6.2.2 Monte Carlo sweep: mean factorization error across depths↩︎

Table 4 reports a Monte Carlo sweep over depths \(d\in\{2,3,4,5\}\) (with \(B=4\) and seeds \(1\)–\(20\)). The key column for Theorem 7 is “mean factor.err.”: for all reported depths and disciplines, the factorization error is on the order of \(10^{-12}\) (or exactly \(0\) in some cases), which is consistent with floating-point numerical precision. This provides strong evidence that the computed \(R_{\mathrm{rb}}(L)\) matches the predicted scaling of the core-only curve \(R_{\mathrm{rb},A}(\cdot)\) by the factor \(P_A=P_O(A)\), as stated by the theorem.

6.2.2.1 Core structure vs.factorization (separate roles).

Note that \(|A|\) varies substantially across disciplines (frontier-sized for causal/cause-respecting, depth-scaling for inverse-causal), but the factorization identity holds uniformly regardless of the core size. This is consistent with the theorem: once admissibility holds, redundancy invisibility and the indicator split \(\mathsf B=\mathbf{1}[S\in A]\) enforce the \(P_A\)-scaled reduction structurally, independent of the particular RCN instance.

6.2.3 Plots of factorization error vs.depth (inlined data)↩︎

For completeness, Figure 6 visualizes the mean factorization error on a log scale, confirming that errors remain at numerical-noise level across depths. (We also include Figure 5 for the ablation gain \(\Delta R_A(0)\) reported in the opening paragraphs of Section 6.)

6.2.3.1 Takeaway for Theorem 7.

Across disciplines and depths, the observed factorization error stays at (or below) floating-point noise level. This is consistent with the theoretical prediction that, under admissibility, the redundant part of the log contributes neither rollback-task loss nor rate, and the overall rollback-task RD function reduces exactly to a \(P_A\)-scaled core-only optimization.

6.3 Zero-loss endpoint check (\(L=0\)): rollback hypergraph entropy and comparison with closure preservation↩︎

This subsection provides an exact endpoint (\(L=0\)) numerical check for the perfect-rollback statement proved in Section 4.3. Recall that the rollback-task loss \(\ell_{\mathrm{rb}}(s,\hat{s})\) counts how many rollback-relevant judgments change under the single-symbol edit \(S_O[s\leftarrow \hat{s}]\) (Definition 13). Perfect rollback in the task sense corresponds to the hard constraint \(\ell_{\mathrm{rb}}(S,\hat{S})=0\) almost surely, and Theorem 8 predicts the endpoint identity \[R_{\mathrm{rb}}(0)=P_A\,H_{\Gamma^{\mathrm{rb}}_0}(\pi_A),\] where \(\Gamma^{\mathrm{rb}}_0\) is induced by the zero-loss sets \(R^{\mathrm{rb}}_0(a)=\{\hat{s}\in\hat{\mathbb{S}}:\ell_{\mathrm{rb}}(a,\hat{s})=0\}\) (Definition 17).

6.3.0.1 Rollback hypergraph entropy vs.independent core endpoint computation.

On the same medium instance \((B=4,d=3)\) as in Section 6.1, we compute the core \(A\), explicitly construct \(\Gamma^{\mathrm{rb}}_0\), and compute \(H_{\Gamma^{\mathrm{rb}}_0}(\pi_A)\). We then compare it with an independent core-only endpoint computation of \(R_{\mathrm{rb},A}(0)\) (minimizing rate subject to \(\ell_{\mathrm{rb}}(A^\star,\hat{S})=0\) almost surely). Table 5 reports the results. Across disciplines the two values coincide up to numerical precision; in particular, the inverse-causal deviation is at floating-point noise level (\(\approx 2.13\times 10^{-12}\)).

4pt

6.3.0.2 Comparison with perfect closure preservation.

Proposition 9 predicts \(R_{\mathrm{rb}}(0)\le R_{\mathrm{sem}}(0)\). The last column of Table 5 confirms this on the instance for all disciplines. Moreover, in the inverse-causal discipline we observe a strict separation: \[R_{\mathrm{rb}}(0)=2.0 \quad<\quad R_{\mathrm{sem}}(0)=\log_2(12)\approx 3.585,\] showing that (for the chosen query set \(\mathbb{Q}_{\mathrm{rb}}^{\mathrm{inv}}\)) preserving all rollback-task judgments can be strictly easier than preserving the full closure.

6.3.0.3 Remark (reduced query sets as a general mechanism).

Section 4.3 also explains how shrinking the rollback query set \(\mathbb{Q}_{\mathrm{rb}}\) enlarges the feasible family \(\Gamma^{\mathrm{rb}}_0\), and by Lemma 8 can only decrease \(H_{\Gamma^{\mathrm{rb}}_0}(\pi_A)\), potentially further reducing \(R_{\mathrm{rb}}(0)\) while leaving \(R_{\mathrm{sem}}(0)\) unchanged. We do not include additional numerical tables for this variant here, since the goal of this section is to validate the endpoint identities and the inequality relationship on the fixed Section 5 instance.

7 Related Work↩︎

Our work sits at the intersection of (i) reversible computation and its operational/denotational models, (ii) Petri nets and event structures for concurrency with reversibility, and (iii) Shannon rate–distortion theory under nonstandard, semantics-driven fidelity criteria. We emphasize that our contribution is not to introduce a new reversible semantics for RCN/rPES, but to make reversible rollback capability quantitative via closure-preserving rate–distortion.

7.1 Reversible computation and causal-consistent reversibility↩︎

Reversible computation is classically motivated by thermodynamic considerations. Landauer’s principle links information erasure to heat dissipation, and Bennett showed that computations can be made logically reversible by retaining suitable history information, establishing a foundational connection between reversibility and stored auxiliary data [22]–[24]. Early reversible models include reversible Turing machines and reversible cellular automata, as well as conservative/reversible logic constructions [1], [2], [25].

In concurrent and distributed settings, reversibility is discipline-sensitive: the set of backward steps that are admissible depends on causal dependencies, conflict, and additional relations such as reverse causality and prevention evidence. Process-calculus developments (e.g., RCCS and key-based variants) make this dependence explicit via memories/keys and causal bookkeeping [3], [4], [26]. Recent work provides an axiomatic account of causal-consistent reversibility (including the Parabolic Lemma and related safety/liveness properties), clarifying the role of independence and causal equivalence in combined forward/backward transition systems [5], [6]. Tool support has also begun to emerge for the axiomatic approach [27].

Our paper is aligned with this literature in that the semantic object of interest is not a syntactic trace but the discipline-indexed rollback consequences of a run. The difference is that we quantify the information content needed for perfect or approximate rollback via closure-preserving rate–distortion, rather than only proving qualitative safety properties.

7.2 RCN/rPES, Petri nets with inhibitor arcs, and reversible event structures↩︎

Event-structure and Petri-net semantics provide non-interleaving accounts of concurrency; incorporating reversibility requires handling both forward and backward moves and the additional evidence that governs when undo steps are legal. Reversible prime event structures (rPES) capture causality, conflict, reverse causality, and prevention at an abstract level, while net-based models provide operational realizations of these relations [4].

A key recent contribution is the operational correspondence developed in [7], which introduces reversible causal nets (RCN), a disciplined class of Petri nets with inhibitor arcs capable of encoding the dependency evidence needed to support rich reversing disciplines. Subsequent work further relates rPES and net-based models, clarifying the interplay between operational and denotational views and how different reversing disciplines manifest in the underlying structures [14].

Our work builds directly on this semantic foundation: rather than proposing a new reversible operational semantics, we treat the discipline-indexed rollback reasoning as a monotone closure \(\mathrm{Cn}_{\mathrm{rev}}\) and ask how its induced redundancy structure (the closure core) determines the compression frontier for reversible logging.

7.3 Rate–distortion, semantic/source coding, and zero-error confusability↩︎

Classical rate–distortion theory characterizes the minimum rate needed to represent a source under an average fidelity constraint, and is one of the central pillars of information theory [8]–[10], [28]. For finite alphabets, the rate–distortion function can be computed numerically via the Blahut–Arimoto algorithm once the source distribution and distortion matrix are fixed [15], [16].

When the fidelity criterion is structural rather than symbolwise, zero-distortion (or zero-error) limits are often governed by a confusability object, leading to graph- or hypergraph-based entropic characterizations. In particular, Körner’s graph entropy formalizes the rate of zero-error source coding under confusability constraints, and serves as a key reference point for structured zero-distortion problems [10], [20].

In our setting the distortion is induced by closure preservation under a monotone proof system, so the relevant confusability object becomes a hypergraph induced by overlaps of zero-distortion reconstruction sets on the irredundant core. This connects reversible logging to a zero-distortion regime that is genuinely combinatorial, while still admitting computable finite-alphabet curves beyond the endpoint via Blahut–Arimoto.

7.4 Closure-based rate–distortion and deductive-source viewpoints↩︎

A closely related information-theoretic viewpoint is to model the source alphabet as statements inside a fixed deductive environment and to measure fidelity by preservation of deductive closure. In that setting, the proof system induces a canonical decomposition of the stored source into an irredundant core and a redundant part of re-derivable consequences, and redundancy becomes information-theoretically invisible under admissible reconstructions (those lying inside the original closure).

The companion closure-based rate–distortion framework in [13] develops this idea for deductive sources and yields exact core-only decompositions of both the zero-distortion rate and the full rate–distortion function. Our paper can be read as a reversible-computation instantiation of that closure-based source model: the reversible proof system \(\mathsf{PS}_{\mathrm{rev}}\) and its induced closure \(\mathrm{Cn}_{\mathrm{rev}}\) encode rollback semantics, so that \(\mathrm{Cn}_{\mathrm{rev}}(\cdot)\)-preservation becomes the fidelity criterion for reversible logging.

What is specific to the reversible RCN/rPES setting is that the closure (hence the core) is discipline-dependent: causal and cause-respecting semantics lead to frontier-shaped cores under a downward-closed presence interface, while inverse-causal semantics can force the core to expand to include causal ancestors as rollback evidence. This discipline dependence is not a minor modeling choice; it directly determines the achievable compression gains.

7.4.0.1 Positioning.

In summary, the related-work threads above provide (i) discipline-indexed reversible semantics and rollback correctness criteria, and (ii) classical information-theoretic tools for rate–distortion and confusability. Our contribution is to connect these two lines via closure-preserving fidelity: reversible rollback consequences are treated as closure observables, which induces a canonical core/redundant decomposition and yields both exact endpoint laws and computable finite-alphabet rate–distortion curves for reversible logging.

8 Conclusion↩︎

We presented a semantic rate–distortion theory for reversible logging under a closure-preservation fidelity criterion. Modeling rollback-relevant semantics as a monotone closure \(\mathrm{Cn}_{\mathrm{rev}}\) yields a distortion notion that matches the operational goal: a reconstruction is faithful if it preserves closure consequences (or a designated rollback observable), not if it reproduces log atoms verbatim.

The closure interface induces a canonical structural simplification. A deterministic deletion scan decomposes any finite log fact base \(S_O\) into an irredundant core \(A\) and a redundant remainder \(J\) such that \(\mathrm{Cn}_{\mathrm{rev}}(A)=\mathrm{Cn}_{\mathrm{rev}}(S_O)\). Under admissible reconstructions \(\hat{\mathbb{S}}\subseteq \mathrm{Cn}_{\mathrm{rev}}(S_O)\), the redundant part \(J\) becomes information-theoretically invisible: it contributes neither rate nor distortion. Consequently, the full semantic rate–distortion function factorizes into a core-only problem scaled by the core mass \(P_A\).

At the perfect-fidelity endpoint \(D=0\), we identified the exact minimum rate as a hypergraph-entropy quantity \(R_{\mathrm{sem}}(0)=P_A\,H_{\Gamma_0}(\pi_A)\), where \(\Gamma_0\) captures zero-distortion confusability on the core. We also introduced a rollback-task loss \(\ell_{\mathrm{rb}}\) that directly measures how many rollback judgments change under an edit, and established parallel endpoint and factorization laws for the rollback-task rate–distortion function \(R_{\mathrm{rb}}(L)\). Together, these results provide a quantitative complement to qualitative rollback-correctness criteria: they separate what must be logged (the core) from what can be reconstructed semantically (the redundant closure consequences), and they quantify the price of exact or approximate rollback.

We instantiated the framework on reversible causal nets and reversible prime event structures via discipline-indexed monotone closures. The instantiation makes discipline sensitivity explicit and measurable: different reversing disciplines induce different closures, hence different cores and different information-theoretic logging frontiers. Our numerical evidence (enumeration checks, Blahut–Arimoto curves, and Monte Carlo sweeps) supports the predicted endpoint identities and core-only factorizations and illustrates the gap between causal/cause-respecting and inverse-causal disciplines on medium-scale instances.

8.0.0.1 Limitations and future work.

The present formulation adopts a “single stored log” viewpoint and a single-symbol edit distortion, which yields a clean finite-alphabet rate–distortion problem and transparent structural theorems. Natural next steps include: (i) extending the source model from sampling symbols from a fixed \(S_O\) to streaming and time-evolving logs; (ii) designing explicit coding schemes that approach the derived limits while respecting admissibility and decoder-side closure computation; (iii) enriching admissible reconstruction alphabets with principled summary atoms that provably create useful core confusability in concrete reversible semantics; and (iv) extending the closure interface to settings that require controlled forms of non-monotonicity (e.g., negative enabling conditions) while retaining computable safety guarantees. Finally, applying the same closure-based quantitative lens to other reversible frameworks (e.g., process calculi and message-passing logs) is a promising direction for developing discipline-aware, rate-optimal reversible debuggers and rollback mechanisms.

References↩︎

---

1. If your implementation uses a slightly different grid or normalization, only this display should be updated; the interpretation remains the same.↩︎