Repository navigation
Implement canonical RFSA, prime atomaton, NL*, and concrete VPA constructions (2/5) - #18
Closed
Autoplectic wants to merge 3 commits into
Closed
Autoplectic wants to merge 3 commits into
Autoplectic wants to merge 3 commits into
Conversation
…toms, and NL* - ResidualTable decides residual inclusion and union coverage exactly on the minimal DFA; canonical_rfsa_from_language builds the Denis-Lemay-Terlutte canonical RFSA (was a relabeled minimal DFA). - Maximized prime atomaton = reverse of the canonical RFSA of the reversed language (Maarand & Tamm 2022). It need not be atomic (Tamm 2015), so it now subclasses NFA rather than AtomicAutomaton; CanonicalRFSA.dual() and MaximizedPrimeAtomaton.dual() reverse between them. - ResidualFiniteStateAutomaton.validate checks every state accepts a residual. - prime_residuals, atoms, prime_atoms are exact (were bounded-length checks that tested equality instead of union, and returned quotients as atoms). - Faithful NL* (Bollig et al. 2009) learning the canonical RFSA, a reversed learner for the prime atomaton, NL*-style table extraction, and an exact AutomatonEquivalenceOracle returning shortest counterexamples. Co-authored-by: Cursor <cursoragent@cursor.com>
…and a correct canonical VPA - Normalized VPA form (explicit bottom, guarded returns); documented wildcard returns as firing on every stack symbol and on the empty stack with a bottom. - Alur-Madhusudan determinization; DeterministicVisiblyPushdownAutomaton.from_vpa determinizes nondeterministic input instead of raising. - Concrete union, intersection, complement, difference, concatenation, and Kleene star (boundary-bit construction for per-factor empty stacks); the lazy CompositeVisiblyPushdownAutomaton and the *_vpa free functions are removed. - Emptiness via well-matched summary saturation, accepted_word witnesses, is_universal, includes, equivalent, and has_unmatched_word. - to_single_entry / to_multiple_entry convert well-matched VPAs into modular form; modular minimize converts automatically when no modules are given. - CanonicalVisiblyPushdownAutomaton raises NonWellMatchedLanguageError on languages with pending calls/returns, and no longer accepts pending calls or depends on class representatives (joint top-level/nested congruence). - NestedWordAutomaton operations delegate through the tagged VPA encoding. - Property tests check every operation against brute-force reference semantics. Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
Autoplectic
force-pushed
the
sofic-missing-constructions
branch
from
October 6, 2026 21:39
cc544ca to
7ea187a
Compare
Member
Author
|
Superseded by #22, which contains the same commits as a single PR. |
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 #17.
Made with Cursor