Decide reverse ε-machine finiteness via the twins property

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
 

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

docs/core/exceptions.rst

@@ -10,15 +10,39 @@ 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. 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
+genuinely infinite.
+
 API
 ===
 
 .. autoclass:: SoficError
 .. autoclass:: SoficValidationError
 .. autoclass:: NonDeterministicError
 .. autoclass:: StochasticValidationError
+.. autoclass:: MixedStateExplosionError
 .. autoclass:: UnifilarityError
 .. autoclass:: QuasiStochasticValidationError

docs/generators/epsilon_machine.rst

@@ -60,14 +60,42 @@ 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 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
+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).
 
 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

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},
@@ -331,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},
 }
 
@@ -844,6 +859,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},

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:

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):

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,

sofic/exceptions.py

@@ -17,6 +17,18 @@ 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. This is the
+    "explosive irreversibility" of :cite:`Ellison2011`; see
+    :cite:`Crutchfield2009` for :math:`\\Delta C_\\mu`.
+    """
+
+
 class UnifilarityError(SoficValidationError):
     """Raised when a unifilarity invariant is violated."""