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/core/exceptions.rst b/docs/core/exceptions.rst index ee77057..4cd759f 100644 --- a/docs/core/exceptions.rst +++ b/docs/core/exceptions.rst @@ -10,9 +10,32 @@ 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 === @@ -20,5 +43,6 @@ API .. autoclass:: SoficValidationError .. autoclass:: NonDeterministicError .. autoclass:: StochasticValidationError +.. autoclass:: MixedStateExplosionError .. autoclass:: UnifilarityError .. autoclass:: QuasiStochasticValidationError diff --git a/docs/generators/epsilon_machine.rst b/docs/generators/epsilon_machine.rst index 6cbd12e..dc7d3af 100644 --- a/docs/generators/epsilon_machine.rst +++ b/docs/generators/epsilon_machine.rst @@ -60,6 +60,32 @@ 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). @@ -67,7 +93,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 c4fa183..2d6a9ed 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}, @@ -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}, 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/sofic/exceptions.py b/sofic/exceptions.py index ec0cfc7..b8a7658 100644 --- a/sofic/exceptions.py +++ b/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.""" diff --git a/sofic/generators/epsilon_machine.py b/sofic/generators/epsilon_machine.py index 3832e6f..0372e26 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). @@ -537,13 +552,31 @@ 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 -- the "explosive + irreversibility" of :cite:`Ellison2011` -- 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/sofic/generators/reversal.py b/sofic/generators/reversal.py index 02eea65..d8fb301 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,120 @@ 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 + (: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 + 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. + + 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 + 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_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_epsilon_machine.py b/tests/test_epsilon_machine.py index ff30176..51b3c6c 100644 --- a/tests/test_epsilon_machine.py +++ b/tests/test_epsilon_machine.py @@ -73,3 +73,131 @@ 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_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. + + 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) 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