Decide reverse ε-machine finiteness via the twins property - #10
Merged
Autoplectic merged 5 commits intoSep 19, 2026
Merged
Conversation
`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 <cursoragent@cursor.com>
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 <cursoragent@cursor.com>
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 <cursoragent@cursor.com>
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 <cursoragent@cursor.com>
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 <cursoragent@cursor.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacked on #9 — the reversal test needs the Wheeler module, so this targets
cursor/wheeler-automatarather thanmain. Retarget once #9 lands.Five commits, all downstream of one question: is the reverse ε-machine of a
finite unifilar machine itself finite? Answering it turned up a silent
correctness bug.
Fix the átomaton construction, add the atomicity test
atomaton_from_languageended in a spurious.determinize(), so it returned aminimal DFA instead of the átomaton — three states where Brzozowski & Tamm's
Example 5 wants six. Removed.
Adds
atomic_states/is_atomic(Theorem 4 and Corollary 2 of Brzozowski &Tamm 2014), which fills in the
AtomicAutomaton.validatestub. Supporting thatmeant factoring the Moore refinement out of
minimize_mooreinto a shared_moore_refineand exposingnerode_partition.Propagate mixed-state explosion instead of silently degrading
EpsilonMachine.from_time_reversedcaughtStochasticValidationError— whichis also what the mixed-state construction raised on hitting
max_states— andfell back to a row-normalized presentation. For a process whose reverse machine
is genuinely infinite, that returned a plausible-looking 3-state non-unifilar
machine whose state entropy happens to equal the forward
causal_irreversibility()reportedwrong in the direction that hides the interesting phenomenon.
New
MixedStateExplosionErrorseparates "the belief set may be infinite" from"the model is malformed", and the former now propagates. Regression test pins it.
Decide finiteness in polynomial time
reversal.reverse_is_finiteanswers the question without enumerating beliefs.Because the seed is uniform and the machine is unifilar, retrodictive causal
states are exactly the normalized
finite iff every log-likelihood ratio takes finitely many values — iff every
directed cycle of the pair graph over
That criterion is Theorem 5 of Allauzen & Mohri (2003) (twins property for$|S|$ -ambiguous over the reals. Only the
trim cycle-unambiguous weighted automata over a commutative cancellative
semiring); the per-SCC potential algorithm is their Theorem 6. The docstring is
explicit that their "twins iff determinizable" equivalence is not being
invoked — that is stated for unambiguous automata over the tropical semiring,
and full-support seeding makes this one
reduction is new.
Two implementation notes worth reviewing:
meaningless — an early float version disagreed with exact arithmetic on 18
cases. Numeric inputs now accumulate log-ratios; symbolic ones stay exact.
MultiDiGraph, notDiGraph. Two symbols can carry a pair to the samesuccessor with different ratios. Collapsing those parallel edges hides the
very inconsistency the test looks for, classifying an explosive machine as
finite. Regression test
test_reverse_is_finite_sees_parallel_pair_edges.Note this is not structural: machines with identical transition graphs differ,
since a cycle weight can hit one by algebraic coincidence.
Attribution
"Explosive irreversibility" is named in Ellison et al. (2011), not new here, and$C_\mu^-$ can stay finite over countably$\Delta C_\mu = -\infty$ ; corrected.
it concerns presentation cardinality —
many states. Earlier docstrings claimed
docs/references.bibgains the published Chaos entry with DOI.Testing
1031 passed. Validated
reverse_is_finiteagainst brute-force exact-arithmeticenumeration on all 432 strongly-connected 3-state binary unifilar machines, plus
adversarial tuned-probability cases, 4-state samples, and ternary alphabets.
ruffandruff formatclean;tydiagnostics unchanged from base at 158.