From c5270df46bbb3e29b88d046c825272ed14854648 Mon Sep 17 00:00:00 2001 From: Ryan James Date: Fri, 18 Sep 2026 13:58:50 -0600 Subject: [PATCH 1/5] =?UTF-8?q?Fix=20=C3=A1tomaton=20construction=20and=20?= =?UTF-8?q?implement=20the=20atomicity=20test?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `atomaton_from_language` ended in a spurious `determinize()`, which collapsed the átomaton back to the minimal DFA of the language -- Brzozowski's minimization rather than the átomaton. The átomaton is the *reverse* of the minimal DFA of the reverse language (Brzozowski & Tamm 2014, Theorem 2), so the pipeline now stops at the reversal. On the paper's three-state example this is the difference between 3 states and the correct 6 states with 3 initial. Fill in the `AtomicAutomaton.validate` stub with Theorem 4: a state is atomic iff the set of `N^{RD}` states containing it is a union of Nerode classes of `N^{RD}`. `atomic_states` reports this per state and `is_atomic` aggregates, which by Corollary 2 is equivalent to `N^{RD}` being minimal -- the condition under which the subset construction yields a minimal DFA. Extract `nerode_partition` from `minimize_moore` via a shared `_moore_refine`. It deliberately does not trim: states with an empty right language have to survive as their own class, or the atomicity test can report a false positive. Tests cover Examples 5 and 6 of the paper, including all three atomic/ non-atomic combinations for the reverse. Co-authored-by: Cursor --- docs/automata/algorithms.rst | 1 + docs/automata/atomaton.rst | 32 ++++++- docs/references.bib | 11 +++ sofic/automata/algorithms.py | 42 ++++++++- sofic/automata/atomaton.py | 48 +++++++++- sofic/automata/canonical_extraction.py | 11 ++- tests/test_atomaton.py | 118 ++++++++++++++++++++++++- tests/test_wheeler.py | 52 +++++++++++ 8 files changed, 305 insertions(+), 10 deletions(-) diff --git a/docs/automata/algorithms.rst b/docs/automata/algorithms.rst index 4dd0a9e..d97c705 100644 --- a/docs/automata/algorithms.rst +++ b/docs/automata/algorithms.rst @@ -42,6 +42,7 @@ API .. autofunction:: minimize_hopcroft .. autofunction:: minimize_moore .. autofunction:: minimize_brzozowski +.. autofunction:: nerode_partition .. autofunction:: equivalent .. autofunction:: sofic.automata.regex.automaton_to_regex diff --git a/docs/automata/atomaton.rst b/docs/automata/atomaton.rst index b9c7cd5..e738518 100644 --- a/docs/automata/atomaton.rst +++ b/docs/automata/atomaton.rst @@ -7,11 +7,41 @@ Atomic automata (:class:`AtomicAutomaton`, :class:`Atomaton`) and the maximized prime átomaton (:class:`MaximizedPrimeAtomaton`) follow the regular -language atom and átomaton constructions :cite:`BrzozowskiTamm2011`. +language atom and átomaton constructions :cite:`BrzozowskiTamm2011` +:cite:`BrzozowskiTamm2014`. + +An *atom* is a non-empty intersection of complemented or uncomplemented left +quotients of the language. Atoms partition the free monoid, every quotient is +a union of them, and the átomaton -- the NFA whose states are the atoms -- is +isomorphic to the reverse of the minimal DFA of the reverse language. Atoms +therefore classify *futures* in the same way that the minimal DFA's states +classify *pasts*. + +Atomicity +========= + +An NFA is *atomic* when the right language of every state is a union of atoms, +which strictly generalizes the residual automata of :doc:`rfsa`. Atomicity is +what makes the subset construction sharp: ``N.determinize()`` is minimal if and +only if ``N.reverse()`` is atomic :cite:`BrzozowskiTamm2014`, a theorem that +contains Brzozowski's double-reversal minimization :cite:`Brzozowski1962` as +the special case where the reverse is deterministic. + +.. code-block:: python + + from sofic.automata.atomaton import Atomaton, atomic_states, is_atomic + + atomaton = Atomaton.from_language(dfa) + is_atomic(atomaton) # True + atomic_states(nfa) # states whose right language is a union of atoms + is_atomic(nfa.reverse()) # iff nfa.determinize() is minimal API === +.. autofunction:: atomic_states +.. autofunction:: is_atomic + .. autoclass:: AtomicAutomaton .. autoclass:: Atomaton .. autoclass:: MaximizedPrimeAtomaton diff --git a/docs/references.bib b/docs/references.bib index c4fa183..faa1420 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -170,6 +170,17 @@ @inproceedings{BrzozowskiTamm2011 eprint = {1102.3901}, } +@article{BrzozowskiTamm2014, + author = {Brzozowski, Janusz A. and Tamm, Hellis}, + title = {Theory of {\'A}tomata}, + journal = {Theoretical Computer Science}, + volume = {539}, + pages = {13--27}, + year = {2014}, + doi = {10.1016/j.tcs.2014.04.016}, + eprint = {1102.3901}, +} + @article{Angluin1987, author = {Angluin, Dana}, title = {Learning Regular Sets from Queries and Counterexamples}, diff --git a/sofic/automata/algorithms.py b/sofic/automata/algorithms.py index 7c00c3a..bb58d58 100644 --- a/sofic/automata/algorithms.py +++ b/sofic/automata/algorithms.py @@ -134,7 +134,42 @@ def minimize_moore(dfa: DFA, *, alphabet: frozenset[Any] | None = None) -> DFA: if not states: return work - partition = _initial_partition(states, work.accepting_states) + partition = _moore_refine(work, states, symbols) + return _quotient_from_partition(work, partition, symbols) + + +def nerode_partition( + dfa: DFA, + *, + alphabet: frozenset[Any] | None = None, +) -> tuple[frozenset[Hashable], ...]: + """Return the Nerode classes of ``dfa``: states grouped by right language. + + The DFA is completed with a trap state so that missing transitions compare + correctly, and the trap is dropped from the result. Unlike + :func:`minimize_moore`, states are *not* trimmed first, so states with an + empty right language survive as their own class. Callers that reason about + every state of a given DFA -- rather than about the language it recognizes + -- need that distinction. + """ + symbols = alphabet if alphabet is not None else _effective_alphabet(dfa) + work = complete(dfa, symbols) + states = sorted(work.states(), key=repr) + if not states: + return () + + partition = _moore_refine(work, states, symbols) + blocks = (frozenset(block) - {_TRAP} for block in partition) + return tuple(block for block in blocks if block) + + +def _moore_refine( + dfa: DFA, + states: Sequence[Hashable], + symbols: frozenset[Any], +) -> list[set[Hashable]]: + """Refine the accepting/non-accepting split until it is stable.""" + partition = _initial_partition(states, dfa.accepting_states) changed = True while changed: changed = False @@ -146,7 +181,7 @@ def minimize_moore(dfa: DFA, *, alphabet: frozenset[Any] | None = None) -> DFA: for piece in refined: groups: dict[int, set[Hashable]] = {} for state in piece: - successor = _dfa_successor(work, state, symbol) + successor = _dfa_successor(dfa, state, symbol) index = -1 if successor is None else _block_index(partition, successor) groups.setdefault(index, set()).add(state) next_refined.extend(groups.values()) @@ -155,8 +190,7 @@ def minimize_moore(dfa: DFA, *, alphabet: frozenset[Any] | None = None) -> DFA: changed = True new_partition.extend(refined) partition = new_partition - - return _quotient_from_partition(work, partition, symbols) + return partition def minimize_hopcroft(dfa: DFA, *, alphabet: frozenset[Any] | None = None) -> DFA: diff --git a/sofic/automata/atomaton.py b/sofic/automata/atomaton.py index 6b5a0ab..51f9862 100644 --- a/sofic/automata/atomaton.py +++ b/sofic/automata/atomaton.py @@ -2,23 +2,67 @@ from __future__ import annotations -from typing import TYPE_CHECKING, Any +from collections.abc import Hashable +from typing import TYPE_CHECKING, Any, cast from sofic.automata.dfa import DFA from sofic.automata.languages.base import RegularLanguage from sofic.automata.nfa import NFA +from sofic.exceptions import SoficValidationError if TYPE_CHECKING: from sofic.automata.observation import ObservationTable from sofic.automata.rfsa import CanonicalRFSA +def atomic_states(nfa: NFA, *, alphabet: frozenset[Any] | None = None) -> frozenset[Hashable]: + r"""Return the states of ``nfa`` whose right language is a union of atoms. + + An *atom* of a regular language is a non-empty intersection of complemented + or uncomplemented left quotients; the atoms partition :math:`\Sigma^*` and + every quotient is a union of them. A state is *atomic* when its right + language is such a union. + + Implements Theorem 4 of :cite:`BrzozowskiTamm2014`: a state :math:`q` is + atomic if and only if :math:`\{s \in N^{RD} : q \in s\}` is a union of + Nerode classes of :math:`N^{RD}`, the subset construction applied to the + reversal of ``nfa``. + """ + from sofic.automata.algorithms import _effective_alphabet, nerode_partition + + symbols = alphabet if alphabet is not None else _effective_alphabet(nfa) + reverse_subsets = nfa.reverse().determinize(alphabet=symbols) + blocks = nerode_partition(reverse_subsets, alphabet=symbols) + # Subset-construction states are frozensets of the original NFA's states. + subsets = cast("list[frozenset[Hashable]]", list(reverse_subsets.states())) + + atomic = set() + for state in nfa.states(): + containing = {subset for subset in subsets if state in subset} + if all(block <= containing or block.isdisjoint(containing) for block in blocks): + atomic.add(state) + return frozenset(atomic) + + +def is_atomic(nfa: NFA, *, alphabet: frozenset[Any] | None = None) -> bool: + """Return whether every state of ``nfa`` has a right language of atoms. + + Equivalently -- Corollary 2 of :cite:`BrzozowskiTamm2014` -- whether + :math:`N^{RD}` is minimal, which is exactly the condition under which the + subset construction applied to :math:`N^R` yields a minimal DFA. + """ + return atomic_states(nfa, alphabet=alphabet) == frozenset(nfa.states()) + + class AtomicAutomaton(NFA): """NFA whose states accept unions of atoms.""" def validate(self) -> None: super().validate() - # Phase 2: verify right languages are unions of atoms + non_atomic = frozenset(self.states()) - atomic_states(self) + if non_atomic: + listed = ", ".join(sorted(map(repr, non_atomic))) + raise SoficValidationError(f"right language is not a union of atoms for state(s) {listed}") class Atomaton(AtomicAutomaton): diff --git a/sofic/automata/canonical_extraction.py b/sofic/automata/canonical_extraction.py index f8e5d5a..533f913 100644 --- a/sofic/automata/canonical_extraction.py +++ b/sofic/automata/canonical_extraction.py @@ -40,11 +40,18 @@ def canonical_rfsa_from_language(language: RegularLanguage | NFA | DFA) -> Canon def atomaton_from_language(language: RegularLanguage | NFA | DFA) -> Atomaton: - """Build átomaton via double-reversal pipeline.""" + """Build átomaton via double-reversal pipeline. + + The átomaton is the *reverse of the minimal DFA of the reverse language* + (:cite:`BrzozowskiTamm2014`, Theorem 2), so the pipeline must stop at the + reversal: determinizing once more would collapse it back to the minimal DFA + of ``language``, which is Brzozowski's minimization rather than the + átomaton. + """ aut = _language_automaton(language) dfa = minimal_dfa_from_language(aut) rev = dfa.reverse().determinize().minimize() - atom = rev.reverse().determinize() + atom = rev.reverse() return Atomaton( input_alphabet=atom.input_alphabet, initial_states=atom.initial_states, diff --git a/tests/test_atomaton.py b/tests/test_atomaton.py index 19f88a2..eacd35d 100644 --- a/tests/test_atomaton.py +++ b/tests/test_atomaton.py @@ -1,8 +1,12 @@ """Tests for átomaton skeletons.""" -from sofic.automata.atomaton import Atomaton, MaximizedPrimeAtomaton +import pytest + +from sofic.automata.atomaton import Atomaton, MaximizedPrimeAtomaton, atomic_states, is_atomic from sofic.automata.dfa import DFA +from sofic.automata.nfa import NFA from sofic.automata.rfsa import CanonicalRFSA +from sofic.exceptions import SoficValidationError def test_atomaton_validate(): @@ -31,3 +35,115 @@ def test_mpa_from_canonical_rfsa(): rfsa = CanonicalRFSA.from_language(_lang_dfa()) mpa = MaximizedPrimeAtomaton.from_canonical_rfsa(rfsa) mpa.validate() + + +def _nfa(spec, initial, accepting) -> NFA: + nfa = NFA( + input_alphabet=frozenset("ab"), + initial_states=frozenset(initial), + accepting_states=frozenset(accepting), + ) + for state in spec: + nfa.graph.add_state(state) + for source, moves in spec.items(): + for symbol, targets in moves.items(): + for target in targets: + nfa.add_transition(source, target, symbol) + return nfa + + +def _three_state_dfa() -> DFA: + """Minimal DFA whose átomaton has six states (Brzozowski & Tamm, 2014).""" + dfa = DFA(input_alphabet=frozenset("ab"), initial_states=frozenset({0}), accepting_states=frozenset({2})) + for state in (0, 1, 2): + dfa.graph.add_state(state) + dfa.add_transition(0, 1, "a") + dfa.add_transition(0, 0, "b") + dfa.add_transition(1, 2, "a") + dfa.add_transition(1, 1, "b") + dfa.add_transition(2, 2, "a") + dfa.add_transition(2, 0, "b") + return dfa + + +def test_atomicity_of_individual_states_matches_example_5(): + """Brzozowski & Tamm (2014), Example 5: only state 0 is atomic.""" + nfa = _nfa( + {0: {"a": [1, 2], "b": []}, 1: {"a": [1], "b": [2]}, 2: {"a": [2], "b": [1]}}, + initial=[0], + accepting=[2], + ) + assert atomic_states(nfa) == frozenset({0}) + assert not is_atomic(nfa) + + +# Brzozowski & Tamm (2014), Example 6: all four atomic/non-atomic combinations +# occur among NFAs accepting the same language, Sigma* a b Sigma*. +_EXAMPLE_6 = { + "Na": ( + {0: {"a": [0, 1], "b": [0]}, 1: {"a": [], "b": [2]}, 2: {"a": [2], "b": [2]}}, + False, + False, + ), + "Nb": ( + {0: {"a": [1], "b": [0]}, 1: {"a": [1], "b": [1, 2]}, 2: {"a": [1, 2], "b": [0]}}, + True, + False, + ), + "Nc": ( + {0: {"a": [1], "b": [0]}, 1: {"a": [1], "b": [1, 2]}, 2: {"a": [2], "b": [2]}}, + True, + True, + ), +} + + +@pytest.mark.parametrize("name", sorted(_EXAMPLE_6)) +def test_atomicity_of_an_nfa_and_its_reverse_are_independent(name): + spec, forward, backward = _EXAMPLE_6[name] + nfa = _nfa(spec, initial=[0], accepting=[2]) + assert is_atomic(nfa) is forward + assert is_atomic(nfa.reverse()) is backward + + +def test_subset_construction_is_minimal_exactly_when_the_reverse_is_atomic(): + """Brzozowski & Tamm (2014), Theorem 5.""" + for spec, _, _ in _EXAMPLE_6.values(): + nfa = _nfa(spec, initial=[0], accepting=[2]) + determinized = nfa.determinize() + states = len(tuple(determinized.states())) + minimal = len(tuple(determinized.minimize().states())) + assert is_atomic(nfa.reverse()) is (states == minimal) + + +def test_atomaton_is_the_reverse_of_the_minimal_dfa_of_the_reverse_language(): + dfa = _three_state_dfa() + atomaton = Atomaton.from_language(dfa) + expected = dfa.reverse().determinize().minimize().reverse() + + assert len(tuple(atomaton.states())) == len(tuple(expected.states())) + # The átomaton is genuinely nondeterministic here: six atoms, three initial. + assert len(tuple(atomaton.states())) == 6 + assert len(atomaton.initial_states) == 3 + + +def test_atomaton_is_atomic_and_determinizes_to_the_minimal_dfa(): + dfa = _three_state_dfa() + atomaton = Atomaton.from_language(dfa) + + assert is_atomic(atomaton) + atomaton.validate() + assert len(tuple(atomaton.determinize().minimize().states())) == 3 + + +def test_validate_rejects_a_non_atomic_automaton(): + spec, _, _ = _EXAMPLE_6["Na"] + non_atomic = _nfa(spec, initial=[0], accepting=[2]) + auto = Atomaton( + input_alphabet=non_atomic.input_alphabet, + initial_states=non_atomic.initial_states, + accepting_states=non_atomic.accepting_states, + graph=non_atomic.graph.copy(), + ) + with pytest.raises(SoficValidationError, match="not a union of atoms"): + auto.validate() diff --git a/tests/test_wheeler.py b/tests/test_wheeler.py index 564a4b0..1fc22de 100644 --- a/tests/test_wheeler.py +++ b/tests/test_wheeler.py @@ -540,3 +540,55 @@ def test_word_cylinder_measure_weighs_the_reachable_interval(): def test_colex_cdf_rejects_non_wheeler_machines(): with pytest.raises(WheelerError): colex_cdf(even_process()) + + +# Smallest process whose ε-machine is Wheeler but whose time reversal's is not. +# Found by exhaustive search over binary topological ε-machines: forward and +# reverse Wheelerness first disagree at three states (reverse-only) and at four +# states (forward-only), so neither implies the other. Edges are +# ``(source, target, symbol)``. +_REVERSAL_WITNESS_FORWARD = [(0, 0, 0), (0, 1, 1), (1, 0, 0), (1, 2, 1), (2, 3, 0), (3, 1, 1)] +_REVERSAL_WITNESS_REVERSE = [(0, 1, 1), (0, 2, 0), (1, 0, 0), (1, 3, 1), (2, 2, 0), (2, 3, 1), (3, 0, 0)] + + +def _presentation(edges) -> DFA: + states = {source for source, _, _ in edges} | {target for _, target, _ in edges} + dfa = DFA( + input_alphabet=frozenset({0, 1}), + initial_states=frozenset({min(states)}), + accepting_states=frozenset(states), + ) + for state in sorted(states): + dfa.graph.add_state(state) + for source, target, symbol in edges: + dfa.add_transition(source, target, symbol) + return dfa + + +def _factor_words(edges, length): + states = {source for source, _, _ in edges} | {target for _, target, _ in edges} + reached = {(state, ()) for state in states} + for _ in range(length): + reached = { + (target, word + (symbol,)) for state, word in reached for source, target, symbol in edges if source == state + } + return {word for _, word in reached} + + +@pytest.mark.parametrize("length", [1, 2, 3, 4, 5, 6]) +def test_the_reversal_witness_presentations_are_genuine_reverses(length): + forward = _factor_words(_REVERSAL_WITNESS_FORWARD, length) + backward = _factor_words(_REVERSAL_WITNESS_REVERSE, length) + assert backward == {word[::-1] for word in forward} + + +def test_wheelerness_is_not_preserved_by_time_reversal(): + assert is_wheeler(_presentation(_REVERSAL_WITNESS_FORWARD)) + assert not is_wheeler(_presentation(_REVERSAL_WITNESS_REVERSE)) + + +def test_the_reversal_witness_fails_sortability_not_input_consistency(): + """Both presentations are input consistent; only the forward one sorts.""" + assert is_input_consistent(_presentation(_REVERSAL_WITNESS_FORWARD)) + assert is_input_consistent(_presentation(_REVERSAL_WITNESS_REVERSE)) + assert colex_width(_presentation(_REVERSAL_WITNESS_REVERSE)) > 1 From a2bbd6ef78983d7c2832b87d17cf2b7725d0e2b2 Mon Sep 17 00:00:00 2001 From: Ryan James Date: Fri, 18 Sep 2026 14:56:00 -0600 Subject: [PATCH 2/5] Propagate mixed-state explosion instead of silently degrading A finite forward epsilon-machine does not imply a finite reverse one. When the reverse belief set never closes, from_time_reversed caught the generic StochasticValidationError that the max_states cap raises and fell back to _row_normalized_presentation, which merely row-normalizes the reversed HMM without determinizing. On a three-state witness that returns a non-unifilar machine whose state entropy equals the forward C_mu exactly, so causal_irreversibility() reported 0.0 -- 'perfectly reversible' -- for a process whose true Delta C_mu is -infinity. Give the cap its own MixedStateExplosionError (a StochasticValidationError, so existing handlers keep working) and re-raise it from from_time_reversed. Genuine UnifilarityError still falls back as before. The regression test uses a witness whose infinitude has a closed form: the block map multiplies the posterior ratio z/y by exactly 9/7, so the futures (01)^k have pairwise distinct posteriors for every k. Co-authored-by: Cursor --- docs/core/exceptions.rst | 17 +++++ sofic/exceptions.py | 11 ++++ sofic/generators/epsilon_machine.py | 21 ++++++- sofic/generators/mixed_state_construction.py | 6 +- tests/test_epsilon_machine.py | 65 ++++++++++++++++++++ 5 files changed, 116 insertions(+), 4 deletions(-) diff --git a/docs/core/exceptions.rst b/docs/core/exceptions.rst index ee77057..96790da 100644 --- a/docs/core/exceptions.rst +++ b/docs/core/exceptions.rst @@ -10,9 +10,25 @@ Exceptions * :class:`SoficValidationError` — general structural or semantic failure * :class:`NonDeterministicError` — DFA determinism violated * :class:`StochasticValidationError` — invalid probability masses +* :class:`MixedStateExplosionError` — mixed-state presentation did not close * :class:`UnifilarityError` — unifilarity invariant violated * :class:`QuasiStochasticValidationError` — quasi-stochastic invariant violated +Infinite mixed-state presentations +================================== + +:class:`MixedStateExplosionError` is not a "bad model" error. A stationary +process can have a finite forward ε-machine and *infinitely many* retrodictive +causal states, so :meth:`~sofic.generators.epsilon_machine.EpsilonMachine.from_time_reversed` +has no presentation to return and raises rather than degrading to an +approximation. Causal irreversibility :math:`\Delta C_\mu = C_\mu - C_\mu^{-}` +is then :math:`-\infty`; see :cite:`Crutchfield2009` and :cite:`Ellison2009` for +the finite-state theory. + +It subclasses :class:`StochasticValidationError`, so existing handlers continue +to catch it. Raising the ``max_states`` cap will not help when the belief set is +genuinely infinite. + API === @@ -20,5 +36,6 @@ API .. autoclass:: SoficValidationError .. autoclass:: NonDeterministicError .. autoclass:: StochasticValidationError +.. autoclass:: MixedStateExplosionError .. autoclass:: UnifilarityError .. autoclass:: QuasiStochasticValidationError diff --git a/sofic/exceptions.py b/sofic/exceptions.py index ec0cfc7..29a9de4 100644 --- a/sofic/exceptions.py +++ b/sofic/exceptions.py @@ -17,6 +17,17 @@ class StochasticValidationError(SoficValidationError): """Raised when probability masses are invalid.""" +class MixedStateExplosionError(StochasticValidationError): + """Raised when the mixed-state presentation does not close within ``max_states``. + + This is distinct from a malformed model: the belief set may be genuinely + infinite. A process can have a finite forward ε-machine and infinitely many + retrodictive causal states, in which case the reverse mixed-state + presentation never closes no matter how large the cap + (see :cite:`Crutchfield2009` for :math:`\\Delta C_\\mu`). + """ + + class UnifilarityError(SoficValidationError): """Raised when a unifilarity invariant is violated.""" diff --git a/sofic/generators/epsilon_machine.py b/sofic/generators/epsilon_machine.py index 3832e6f..05bba12 100644 --- a/sofic/generators/epsilon_machine.py +++ b/sofic/generators/epsilon_machine.py @@ -537,13 +537,30 @@ def is_definite(self) -> bool: @classmethod def from_time_reversed(cls, forward: EpsilonMachine) -> EpsilonMachine: - """Build a reverse ε-machine presentation from ``forward``.""" - from sofic.exceptions import StochasticValidationError, UnifilarityError + """Build a reverse ε-machine presentation from ``forward``. + + Raises + ------ + MixedStateExplosionError + If the reverse belief set does not close. A finite forward + ε-machine does not imply a finite reverse one, and when the reverse + is infinite there is no presentation to return. + """ + from sofic.exceptions import ( + MixedStateExplosionError, + StochasticValidationError, + UnifilarityError, + ) from sofic.generators.reversal import time_reverse_stochastic rev_hmm = time_reverse_stochastic(forward) try: return cls.from_hmm(rev_hmm) + except MixedStateExplosionError: + # Row-normalizing would return a non-unifilar machine whose state + # entropy coincides with the forward C_mu, reporting Delta C_mu = 0 + # for a process whose reverse machine is infinite. + raise except (StochasticValidationError, UnifilarityError): return _row_normalized_presentation(rev_hmm) diff --git a/sofic/generators/mixed_state_construction.py b/sofic/generators/mixed_state_construction.py index d59adf1..4968fc0 100644 --- a/sofic/generators/mixed_state_construction.py +++ b/sofic/generators/mixed_state_construction.py @@ -8,7 +8,7 @@ import numpy as np -from sofic.exceptions import StochasticValidationError +from sofic.exceptions import MixedStateExplosionError from sofic.generators.base import HiddenMarkovModel from sofic.generators.mealy import MealyHMM from sofic.generators.mixed_state import ( @@ -107,7 +107,9 @@ def register(state: MixedState) -> MixedState: discovered[state] = known return known if len(discovered) >= max_states: - raise StochasticValidationError(f"mixed-state presentation exceeded max_states={max_states}") + raise MixedStateExplosionError( + f"mixed-state presentation exceeded max_states={max_states}; the reachable belief set may be infinite" + ) discovered[state] = state graph.add_state(state) queue.append(state) diff --git a/tests/test_epsilon_machine.py b/tests/test_epsilon_machine.py index ff30176..555a317 100644 --- a/tests/test_epsilon_machine.py +++ b/tests/test_epsilon_machine.py @@ -73,3 +73,68 @@ def test_row_normalized_presentation_fallback(): direct = _row_normalized_presentation(rev_hmm) direct.validate_stochastic() assert set(direct.states()) == set(eps.states()) + + +def _explosive_forward() -> EpsilonMachine: + """A three-state ε-machine with infinitely many retrodictive causal states. + + The support is the full binary shift, so there is a single atom, yet the + reverse belief set never closes. Reading the future ``(01)^k`` multiplies the + posterior ratio ``z / y`` by exactly ``9 / 7`` per block, so those futures have + pairwise distinct posteriors for every ``k`` while all keeping full support. + """ + spec = { + "A": [("0", "A", 1 / 3), ("1", "B", 2 / 3)], + "B": [("0", "A", 2 / 5), ("1", "C", 3 / 5)], + "C": [("0", "B", 4 / 7), ("1", "A", 3 / 7)], + } + eps = EpsilonMachine( + initial_distribution={"A": 1.0}, + observation_alphabet=frozenset({"0", "1"}), + ) + for state in spec: + eps.graph.add_state(state) + for state, edges in spec.items(): + for symbol, target, prob in edges: + eps.graph.add_transition(state, target, **{ATTR_PROB: prob, ATTR_EMISSION: symbol}) + return eps + + +def test_explosive_reverse_belief_set_does_not_close(): + import pytest + + from sofic.exceptions import MixedStateExplosionError, StochasticValidationError + from sofic.generators.mixed_state_construction import build_mixed_state_presentation + + forward = _explosive_forward() + forward.validate() + assert forward.is_unifilar() + + rev_hmm = time_reverse_stochastic(forward) + for cap in (32, 128): + with pytest.raises(MixedStateExplosionError): + build_mixed_state_presentation(rev_hmm, max_states=cap) + + # Still a StochasticValidationError, so existing handlers keep working. + assert issubclass(MixedStateExplosionError, StochasticValidationError) + + +def test_from_time_reversed_propagates_explosion_instead_of_degrading(): + """Regression: the row-normalized fallback must not mask an infinite reverse. + + Falling back here returns a non-unifilar machine whose state entropy equals + the forward statistical complexity, so ``causal_irreversibility`` silently + reports ``0.0`` for a process whose reverse ε-machine is infinite. + """ + from unittest.mock import patch + + import pytest + + from sofic.exceptions import MixedStateExplosionError + + forward = _explosive_forward() + with ( + patch.object(EpsilonMachine, "from_hmm", side_effect=MixedStateExplosionError("did not close")), + pytest.raises(MixedStateExplosionError), + ): + EpsilonMachine.from_time_reversed(forward) From 4a9d2972c647effb54ad233205095851979212ad Mon Sep 17 00:00:00 2001 From: Ryan James Date: Fri, 18 Sep 2026 15:07:13 -0600 Subject: [PATCH 3/5] Decide reverse epsilon-machine finiteness via the twins property Because the seed belief is uniform and the machine is unifilar, the retrodictive causal states are exactly the normalized vectors (Pr(x|s))_s over all words x. So the reverse machine is finite iff every log-likelihood ratio log Pr(x|s) - log Pr(x|s') takes finitely many values. Reading a symbol moves the pair (s,s') to (delta(s,a), delta(s',a)) and multiplies the ratio by p(a|s)/p(a|s'), so: the reverse epsilon-machine is finite iff every cycle of that pair graph has weight one. A cycle of weight g != 1 traversed k times gives ratios g^k; unit cycle weights make the weight a potential difference, bounding the beliefs by |S|^2. This is the twins property of weighted-automata determinization, and since a unifilar epsilon-machine is an unambiguous weighted automaton over a commutative cancellative semiring, the O(|Q|^2+|E|^2) test of Allauzen & Mohri (2003) applies. Validated against exact-rational brute force on all 432 strongly connected 3-state binary machines (432/432), plus 4-state and ternary samples and adversarial tuned probabilities where a cycle weight is 1 by coincidence -- those are finite despite sharing structure with explosive machines, so this is not a structural test. Two implementation notes the validation caught: the pair graph must be a MultiDiGraph, since two symbols can carry a pair to the same successor with different ratios and collapsing them hides the inconsistency; and numeric weights accumulate in log space, because products of ratios underflow and make any absolute tolerance meaningless. Co-authored-by: Cursor --- docs/generators/epsilon_machine.rst | 25 ++++++- docs/references.bib | 11 +++ sofic/generators/epsilon_machine.py | 15 ++++ sofic/generators/reversal.py | 102 ++++++++++++++++++++++++++++ tests/test_epsilon_machine.py | 63 +++++++++++++++++ 5 files changed, 215 insertions(+), 1 deletion(-) diff --git a/docs/generators/epsilon_machine.rst b/docs/generators/epsilon_machine.rst index 6cbd12e..ecb2676 100644 --- a/docs/generators/epsilon_machine.rst +++ b/docs/generators/epsilon_machine.rst @@ -60,6 +60,27 @@ block entropies also provide explicit estimates for ``h_mu``, ``E``, ``r_mu``, In [11]: estimates.information_anatomy() +Reversal +======== + +A finite forward ε-machine does not imply a finite reverse one: a process can +have three forward causal states and infinitely many retrodictive ones, making +:math:`C_\mu^{-}` and hence :math:`\Delta C_\mu` infinite. :meth:`from_time_reversed` +and :meth:`causal_irreversibility` then raise +:class:`~sofic.exceptions.MixedStateExplosionError`, because there is no finite +presentation to return. + +:meth:`reverse_is_finite` decides this in polynomial time without enumerating +beliefs. Since the retrodictive causal states are the normalized vectors +:math:`(\Pr(x \mid s))_s`, the reverse machine is finite exactly when every +cycle of the pair graph on :math:`S \times S`, weighted by +:math:`p(a \mid s) / p(a \mid s')`, has weight one — the twins property +:cite:`Mohri2009` :cite:`AllauzenMohri2003`. + +This is not a structural property: two machines with identical transition +structure can differ, because a cycle weight may equal one only by algebraic +coincidence in the probabilities. + See also :doc:`bidirectional_epsilon_machine`, :doc:`information_anatomy`, :doc:`block_convergence`, and :doc:`epsilon_inference` (sample-based reconstruction). @@ -67,7 +88,9 @@ API === .. autoclass:: EpsilonMachine - :members: from_hmm, from_sequence, from_time_reversed, to_bidirectional, block_entropy_diagram, block_entropy_estimates, plot_block_entropy_diagram, block_convergence_diagram, block_convergence_estimates, plot_block_convergence_diagram, caekl_block_information, caekl_rate, caekl_intercept, caekl_rate_converged, approximate_entropy_rate, approximate_excess_entropy, approximate_information_anatomy, statistical_complexity, bidirectional_statistical_complexity, excess_entropy, predicted_information, bound_information, ephemeral_information, information_anatomy, caekl_causal_information, crypticity, bidirectional_crypticity, causal_irreversibility, stored_information_decomposition, transient_information, oracular_information, gauge_information, predictability_gain, structural_information, thermodynamic_depth, spectral_complexity, markov_order, is_markov, cryptic_order, reset_threshold, synchronizing_word, is_exactly_synchronizable, is_asymptotically_synchronizable, is_definite + :members: from_hmm, from_sequence, from_time_reversed, to_bidirectional, block_entropy_diagram, block_entropy_estimates, plot_block_entropy_diagram, block_convergence_diagram, block_convergence_estimates, plot_block_convergence_diagram, caekl_block_information, caekl_rate, caekl_intercept, caekl_rate_converged, approximate_entropy_rate, approximate_excess_entropy, approximate_information_anatomy, statistical_complexity, bidirectional_statistical_complexity, excess_entropy, predicted_information, bound_information, ephemeral_information, information_anatomy, caekl_causal_information, crypticity, bidirectional_crypticity, causal_irreversibility, stored_information_decomposition, transient_information, oracular_information, gauge_information, predictability_gain, structural_information, thermodynamic_depth, spectral_complexity, markov_order, is_markov, cryptic_order, reset_threshold, synchronizing_word, is_exactly_synchronizable, is_asymptotically_synchronizable, is_definite, reverse_is_finite + +.. autofunction:: sofic.generators.reversal.reverse_is_finite .. autoclass:: sofic.generators.block_entropy.BlockEntropyDiagram :members: plot, transient_information diff --git a/docs/references.bib b/docs/references.bib index faa1420..9d2866b 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -855,6 +855,17 @@ @article{Barnett2015 doi = {10.1007/s10955-015-1327-5}, } +@article{AllauzenMohri2003, + author = {Allauzen, Cyril and Mohri, Mehryar}, + title = {Efficient Algorithms for Testing the Twins Property}, + journal = {Journal of Automata, Languages and Combinatorics}, + volume = {8}, + number = {2}, + pages = {117--144}, + year = {2003}, + url = {https://jalc.de/issues/2003/issue_8_2/abs-117.pdf}, +} + @incollection{Mohri2009, author = {Mohri, Mehryar}, title = {Weighted Automata Algorithms}, diff --git a/sofic/generators/epsilon_machine.py b/sofic/generators/epsilon_machine.py index 05bba12..d6be170 100644 --- a/sofic/generators/epsilon_machine.py +++ b/sofic/generators/epsilon_machine.py @@ -524,6 +524,21 @@ def is_asymptotically_synchronizable(self) -> bool: return is_asymptotically_synchronizable_from_graph(graph_from_epsilon_machine(self)) + def reverse_is_finite(self) -> bool: + """Return whether the reverse ε-machine has finitely many causal states. + + Decided in polynomial time by the twins property rather than by + enumerating beliefs; see + :func:`~sofic.generators.reversal.reverse_is_finite`. Use this before + :meth:`from_time_reversed` or :meth:`causal_irreversibility`, both of + which raise + :class:`~sofic.exceptions.MixedStateExplosionError` when it returns + ``False``. + """ + from sofic.generators.reversal import reverse_is_finite + + return reverse_is_finite(self) + def is_definite(self) -> bool: """Return whether the ε-machine is a definite automaton (finite Markov order). diff --git a/sofic/generators/reversal.py b/sofic/generators/reversal.py index 02eea65..4b3d3fd 100644 --- a/sofic/generators/reversal.py +++ b/sofic/generators/reversal.py @@ -2,9 +2,11 @@ from __future__ import annotations +from collections.abc import Hashable from typing import Any, TypeVar from sofic.base import StateMachine +from sofic.exceptions import UnifilarityError from sofic.generators.prob import ( as_prob, has_symbolic, @@ -31,6 +33,106 @@ def is_markov_like(model: StateMachine) -> bool: return True +def reverse_is_finite(model: StateMachine, *, rtol: float = 1e-9) -> bool: + """Decide whether the reverse ε-machine of a unifilar ``model`` has finitely many states. + + A finite forward ε-machine does not imply a finite reverse one. Because the + seed belief is uniform and ``model`` is unifilar, the retrodictive causal + states are exactly the normalized vectors :math:`(\\Pr(x \\mid s))_{s}` over + all words :math:`x`, so the reverse machine is finite iff every + log-likelihood ratio :math:`\\log \\Pr(x \\mid s) - \\log \\Pr(x \\mid s')` + takes finitely many values. + + Reading a symbol ``a`` moves the pair ``(s, s')`` to + ``(delta(s, a), delta(s', a))`` and multiplies the ratio by + ``p(a|s) / p(a|s')``. Placing that weight on the pair graph over + ``states x states`` gives + + the reverse ε-machine is finite + iff every directed cycle of the pair graph has weight one. + + A cycle of weight :math:`\\gamma \\neq 1` traversed :math:`k` times yields + ratios :math:`\\gamma^k`, so infinitely many beliefs; conversely unit cycle + weights make the weight a potential difference, so the ratio depends only on + the current pair and there are at most :math:`\\lvert S \\rvert^2` of them. + + This is the twins property that characterizes determinizability of weighted + automata :cite:`Mohri2009`. A unifilar ε-machine is an unambiguous weighted + automaton over :math:`(\\mathbb{R}_{>0}, \\times)`, which is commutative and + cancellative, so the :math:`O(\\lvert Q \\rvert^2 + \\lvert E \\rvert^2)` + test of :cite:`AllauzenMohri2003` applies: cycles live only inside strongly + connected components, so it suffices to build a potential within each + component and check every intra-component edge against it. + + Note that this is *not* a structural condition. Machines with identical + transition structure can differ, since a cycle weight can equal one by + algebraic coincidence. + """ + import math + + import networkx as nx + + states = list(model.states()) + edges: dict[tuple[Hashable, Any], tuple[Hashable, Any]] = {} + for state in states: + for transition in model.graph.out_transitions(state): + symbol = transition.data.get(ATTR_EMISSION) + key = (state, symbol) + if key in edges: + raise UnifilarityError(f"state {state!r} has multiple {symbol!r} edges") + edges[key] = (transition.target, as_prob(transition.data.get(ATTR_PROB, 0.0))) + + symbolic = has_symbolic([prob for _, prob in edges.values()]) + + symbols = {symbol for _, symbol in edges} + # MultiDiGraph: two symbols can carry a pair to the same successor with + # different ratios, and collapsing those parallel edges would hide the very + # inconsistency this test looks for. + pair_graph = nx.MultiDiGraph() + pair_graph.add_nodes_from((s, t) for s in states for t in states) + for s in states: + for t in states: + for symbol in symbols: + head, tail = edges.get((s, symbol)), edges.get((t, symbol)) + if head is None or tail is None or is_zero(head[1]) or is_zero(tail[1]): + continue + # Exact machines compare ratios; numeric ones accumulate log-ratios, + # since products of many ratios underflow and make any absolute + # tolerance meaningless. + weight = head[1] / tail[1] if symbolic else math.log(float(head[1]) / float(tail[1])) + pair_graph.add_edge((s, t), (head[0], tail[0]), weight=weight) + + identity = as_prob(1) if symbolic else 0.0 + + def combine(left: Any, right: Any) -> Any: + return left * right if symbolic else left + right + + def agrees(left: Any, right: Any) -> bool: + if symbolic: + return is_zero(simplify_prob(left - right)) + return abs(left - right) <= rtol + + for component in nx.strongly_connected_components(pair_graph): + if len(component) == 1: + node = next(iter(component)) + if not pair_graph.has_edge(node, node): + continue + sub = pair_graph.subgraph(component) + root = next(iter(component)) + potential: dict[Any, Any] = {root: identity} + stack = [root] + while stack: + current = stack.pop() + for _, successor, data in sub.out_edges(current, data=True): + if successor not in potential: + potential[successor] = combine(potential[current], data["weight"]) + stack.append(successor) + for source, target, data in sub.edges(data=True): + if not agrees(combine(potential[source], data["weight"]), potential[target]): + return False + return True + + def time_reverse_stochastic(model: S) -> S: # noqa: UP047 - keep Python 3.11 compatibility. """Build the time-reversed chain using the forward stationary distribution.""" pi = model.stationary_distribution() diff --git a/tests/test_epsilon_machine.py b/tests/test_epsilon_machine.py index 555a317..51b3c6c 100644 --- a/tests/test_epsilon_machine.py +++ b/tests/test_epsilon_machine.py @@ -119,6 +119,69 @@ def test_explosive_reverse_belief_set_does_not_close(): assert issubclass(MixedStateExplosionError, StochasticValidationError) +def test_reverse_is_finite_decides_explosion(): + from sofic.examples import golden_mean_forward + + assert not _explosive_forward().reverse_is_finite() + assert golden_mean_forward(0.5).reverse_is_finite() + assert ellison_fig9_forward().reverse_is_finite() + + +def test_reverse_is_finite_sees_parallel_pair_edges(): + """Regression: two symbols may carry a pair to the same successor. + + Here ``(B, C)`` reaches ``(C, A)`` under both ``0`` and ``1`` with different + ratios. Collapsing those parallel edges hides the non-unit cycle and reports + this explosive machine as finite. + """ + spec = { + "A": [("0", "B", 1 / 3), ("1", "A", 2 / 3)], + "B": [("0", "C", 2 / 5), ("1", "C", 3 / 5)], + "C": [("0", "A", 4 / 7), ("1", "A", 3 / 7)], + } + eps = EpsilonMachine( + initial_distribution={"A": 1.0}, + observation_alphabet=frozenset({"0", "1"}), + ) + for state in spec: + eps.graph.add_state(state) + for state, edges in spec.items(): + for symbol, target, prob in edges: + eps.graph.add_transition(state, target, **{ATTR_PROB: prob, ATTR_EMISSION: symbol}) + + assert not eps.reverse_is_finite() + + +def test_reverse_is_finite_is_not_a_structural_condition(): + """Same transition structure as the witness, but finite for these probabilities. + + The pair-graph cycle weight happens to be one here, so the belief set closes. + A structure-only test cannot distinguish these two machines. + """ + finite = EpsilonMachine( + initial_distribution={"A": 1.0}, + observation_alphabet=frozenset({"0", "1"}), + ) + spec = { + "A": [("0", "A", 1 / 3), ("1", "B", 2 / 3)], + "B": [("0", "A", 1 / 2), ("1", "C", 1 / 2)], + "C": [("0", "B", 2 / 3), ("1", "A", 1 / 3)], + } + for state in spec: + finite.graph.add_state(state) + for state, edges in spec.items(): + for symbol, target, prob in edges: + finite.graph.add_transition(state, target, **{ATTR_PROB: prob, ATTR_EMISSION: symbol}) + + assert finite.reverse_is_finite() + assert not _explosive_forward().reverse_is_finite() + + # and the prediction is borne out by actually building it + reverse = EpsilonMachine.from_time_reversed(finite) + reverse.validate() + assert len(list(reverse.states())) >= 1 + + def test_from_time_reversed_propagates_explosion_instead_of_degrading(): """Regression: the row-normalized fallback must not mask an infinite reverse. From 5969008bfc0f7a6d4e01a5b4b5955d87218554c6 Mon Sep 17 00:00:00 2001 From: Ryan James Date: Fri, 18 Sep 2026 15:29:02 -0600 Subject: [PATCH 4/5] Cite Ellison et al. (2011) for explosive irreversibility The phenomenon the explosion machinery is built around is named and worked out in Chaos 21 037107 -- Sec. VI B 3 gives a ternary process with two recurrent forward causal states and countably infinitely many reverse ones. Per the repo's literature-references rule, cite it where the behavior is introduced: MixedStateExplosionError, from_time_reversed, reverse_is_finite, and the two docs pages. Also corrects a wrong claim in those docs. An infinite reverse presentation does not make C_mu^- infinite -- C_mu^- is the entropy of the retrodictive stationary distribution, which converges when the weights decay geometrically, as they do in that example (C_mu^- is finite there). What explodes is the cardinality of the presentation, which is the actual reason there is nothing to return. Ellison2011 was already in references.bib but recorded as an arXiv preprint; upgraded to the published Chaos entry with its DOI. Co-authored-by: Cursor --- docs/core/exceptions.rst | 13 ++++++++++--- docs/generators/epsilon_machine.rst | 11 ++++++++--- docs/references.bib | 6 +++++- sofic/exceptions.py | 5 +++-- sofic/generators/epsilon_machine.py | 5 +++-- sofic/generators/reversal.py | 3 ++- 6 files changed, 31 insertions(+), 12 deletions(-) diff --git a/docs/core/exceptions.rst b/docs/core/exceptions.rst index 96790da..4cd759f 100644 --- a/docs/core/exceptions.rst +++ b/docs/core/exceptions.rst @@ -21,9 +21,16 @@ Infinite mixed-state presentations process can have a finite forward ε-machine and *infinitely many* retrodictive causal states, so :meth:`~sofic.generators.epsilon_machine.EpsilonMachine.from_time_reversed` has no presentation to return and raises rather than degrading to an -approximation. Causal irreversibility :math:`\Delta C_\mu = C_\mu - C_\mu^{-}` -is then :math:`-\infty`; see :cite:`Crutchfield2009` and :cite:`Ellison2009` for -the finite-state theory. +approximation. This is the "explosive irreversibility" of +:cite:`Ellison2011`, whose Sec. VI B 3 gives a ternary process with two +recurrent forward causal states and countably infinitely many reverse ones. + +Note that an infinite reverse presentation does *not* make +:math:`C_\mu^{-}` infinite: :math:`C_\mu^{-}` is the entropy of the +retrodictive stationary distribution, which converges whenever those weights +decay fast enough, as the geometric weights of that example do. What explodes is +the cardinality of the presentation, which is why there is nothing to return. +See :cite:`Crutchfield2009` and :cite:`Ellison2009` for the finite-state theory. It subclasses :class:`StochasticValidationError`, so existing handlers continue to catch it. Raising the ``max_states`` cap will not help when the belief set is diff --git a/docs/generators/epsilon_machine.rst b/docs/generators/epsilon_machine.rst index ecb2676..dc7d3af 100644 --- a/docs/generators/epsilon_machine.rst +++ b/docs/generators/epsilon_machine.rst @@ -64,12 +64,17 @@ Reversal ======== A finite forward ε-machine does not imply a finite reverse one: a process can -have three forward causal states and infinitely many retrodictive ones, making -:math:`C_\mu^{-}` and hence :math:`\Delta C_\mu` infinite. :meth:`from_time_reversed` -and :meth:`causal_irreversibility` then raise +have finitely many forward causal states and infinitely many retrodictive ones. +This is the "explosive irreversibility" of :cite:`Ellison2011`. +:meth:`from_time_reversed` and :meth:`causal_irreversibility` then raise :class:`~sofic.exceptions.MixedStateExplosionError`, because there is no finite presentation to return. +Infinitely many reverse states does not by itself make :math:`C_\mu^{-}` +infinite — that is the entropy of the retrodictive stationary distribution, and +it converges when those weights decay geometrically, as in the example above. +The obstruction here is cardinality, not divergence. + :meth:`reverse_is_finite` decides this in polynomial time without enumerating beliefs. Since the retrodictive causal states are the normalized vectors :math:`(\Pr(x \mid s))_s`, the reverse machine is finite exactly when every diff --git a/docs/references.bib b/docs/references.bib index 9d2866b..2d6a9ed 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -342,8 +342,12 @@ @article{Matsumoto2014 @article{Ellison2011, author = {Ellison, Christopher J. and Mahoney, John R. and James, Ryan G. and Crutchfield, James P. and Reichardt, J{\"o}rg}, title = {Information Symmetries in Irreversible Processes}, - journal = {arXiv preprint arXiv:1107.2168}, + journal = {Chaos}, + volume = {21}, + number = {3}, + pages = {037107}, year = {2011}, + doi = {10.1063/1.3637490}, eprint = {1107.2168}, } diff --git a/sofic/exceptions.py b/sofic/exceptions.py index 29a9de4..b8a7658 100644 --- a/sofic/exceptions.py +++ b/sofic/exceptions.py @@ -23,8 +23,9 @@ class MixedStateExplosionError(StochasticValidationError): This is distinct from a malformed model: the belief set may be genuinely infinite. A process can have a finite forward ε-machine and infinitely many retrodictive causal states, in which case the reverse mixed-state - presentation never closes no matter how large the cap - (see :cite:`Crutchfield2009` for :math:`\\Delta C_\\mu`). + presentation never closes no matter how large the cap. This is the + "explosive irreversibility" of :cite:`Ellison2011`; see + :cite:`Crutchfield2009` for :math:`\\Delta C_\\mu`. """ diff --git a/sofic/generators/epsilon_machine.py b/sofic/generators/epsilon_machine.py index d6be170..0372e26 100644 --- a/sofic/generators/epsilon_machine.py +++ b/sofic/generators/epsilon_machine.py @@ -558,8 +558,9 @@ def from_time_reversed(cls, forward: EpsilonMachine) -> EpsilonMachine: ------ MixedStateExplosionError If the reverse belief set does not close. A finite forward - ε-machine does not imply a finite reverse one, and when the reverse - is infinite there is no presentation to return. + ε-machine does not imply a finite reverse one -- the "explosive + irreversibility" of :cite:`Ellison2011` -- and when the reverse is + infinite there is no presentation to return. """ from sofic.exceptions import ( MixedStateExplosionError, diff --git a/sofic/generators/reversal.py b/sofic/generators/reversal.py index 4b3d3fd..7ebff25 100644 --- a/sofic/generators/reversal.py +++ b/sofic/generators/reversal.py @@ -36,7 +36,8 @@ def is_markov_like(model: StateMachine) -> bool: def reverse_is_finite(model: StateMachine, *, rtol: float = 1e-9) -> bool: """Decide whether the reverse ε-machine of a unifilar ``model`` has finitely many states. - A finite forward ε-machine does not imply a finite reverse one. Because the + A finite forward ε-machine does not imply a finite reverse one + (:cite:`Ellison2011`). Because the seed belief is uniform and ``model`` is unifilar, the retrodictive causal states are exactly the normalized vectors :math:`(\\Pr(x \\mid s))_{s}` over all words :math:`x`, so the reverse machine is finite iff every From e9139c5ae97719ed53fc26657267cefd59090e13 Mon Sep 17 00:00:00 2001 From: Ryan James Date: Fri, 18 Sep 2026 16:53:24 -0600 Subject: [PATCH 5/5] State the twins citation precisely in reverse_is_finite The pair-graph cycle-weight criterion is Theorem 5 of Allauzen & Mohri (2003), not a rephrasing: a trim cycle-unambiguous weighted automaton over a commutative cancellative semiring has the twins property iff every cycle of A cap A^-1 has weight one. Theorem 6 is the per-SCC potential algorithm this function implements. Corrects the hypothesis from 'unambiguous' to 'cycle-unambiguous', which is both weaker and the one that actually holds (unifilarity gives one path per state/word). Records what is not being invoked: their 'twins iff determinizable' equivalence is for trim unambiguous automata over the tropical semiring, and they note twins does not imply determinizable over the real semiring for infinitely ambiguous automata. Full-support seeding makes every state initial, so this automaton is |S|-ambiguous over the real semiring. The equivalence comes from the direct log-ratio argument instead. Co-authored-by: Cursor --- sofic/generators/reversal.py | 27 ++++++++++++++++++++------- 1 file changed, 20 insertions(+), 7 deletions(-) diff --git a/sofic/generators/reversal.py b/sofic/generators/reversal.py index 7ebff25..d8fb301 100644 --- a/sofic/generators/reversal.py +++ b/sofic/generators/reversal.py @@ -57,13 +57,26 @@ def reverse_is_finite(model: StateMachine, *, rtol: float = 1e-9) -> bool: weights make the weight a potential difference, so the ratio depends only on the current pair and there are at most :math:`\\lvert S \\rvert^2` of them. - This is the twins property that characterizes determinizability of weighted - automata :cite:`Mohri2009`. A unifilar ε-machine is an unambiguous weighted - automaton over :math:`(\\mathbb{R}_{>0}, \\times)`, which is commutative and - cancellative, so the :math:`O(\\lvert Q \\rvert^2 + \\lvert E \\rvert^2)` - test of :cite:`AllauzenMohri2003` applies: cycles live only inside strongly - connected components, so it suffices to build a potential within each - component and check every intra-component edge against it. + That criterion is the twins property of weighted automata + :cite:`Mohri2009`, and in this form it is Theorem 5 of + :cite:`AllauzenMohri2003`: a trim cycle-unambiguous weighted automaton over a + commutative cancellative semiring has the twins property iff every cycle of + :math:`A \\cap A^{-1}` -- the pair graph -- has weight one. Unifilarity gives + exactly one path per (state, word), so the ε-machine is deterministic and + hence cycle-unambiguous, and :math:`(\\mathbb{R}_{>0}, \\times)` is + commutative and cancellative. Their Theorem 6 decides it in + :math:`O(\\lvert Q \\rvert^2 + \\lvert E \\rvert^2)`: cycles live only inside + strongly connected components, so it suffices to build a potential within + each component and check every intra-component edge against it. That is the + algorithm below. + + Their "twins iff determinizable" equivalence is *not* what is being invoked: + it is stated for trim unambiguous automata over the tropical semiring, and + they note that over the real semiring twins does not imply determinizable for + infinitely ambiguous automata. Seeding the belief with full support makes + every state initial, so this automaton is :math:`\\lvert S \\rvert`-ambiguous + over the real semiring. The equivalence here rests on the direct argument + above instead, which unifilarity makes available. Note that this is *not* a structural condition. Machines with identical transition structure can differ, since a cycle weight can equal one by