Implement canonical RFSA, prime atomaton, NL*, and concrete VPA constructions (2/5)

docs/automata/atomaton.rst

@@ -36,6 +36,17 @@ the special case where the reverse is deterministic.
     atomic_states(nfa)           # states whose right language is a union of atoms
     is_atomic(nfa.reverse())     # iff nfa.determinize() is minimal
 
+Maximized prime átomaton
+========================
+
+The maximized prime átomaton (:class:`MaximizedPrimeAtomaton`) is the dual of
+the canonical RFSA :cite:`MaarandTamm2022`: the reverse of the canonical RFSA of
+the reversed language, just as the átomaton is the reverse of the minimal DFA of
+the reversed language. Its states are the maximized prime atoms, and the right
+language of each lies between its atom and its maximized atom :cite:`Tamm2015`.
+Unlike the átomaton it need not be atomic, so it is a plain
+:class:`~sofic.automata.nfa.NFA` subclass.
+
 API
 ===
 
@@ -45,3 +56,6 @@ API
 .. autoclass:: AtomicAutomaton
 .. autoclass:: Atomaton
 .. autoclass:: MaximizedPrimeAtomaton
+   :members: from_language, from_canonical_rfsa, dual
+
+.. autofunction:: sofic.automata.canonical_extraction.maximized_prime_atomaton_from_language

docs/automata/learning.rst

@@ -10,11 +10,21 @@ Learning
 Active learning (NL\*)
 ======================
 
-Active learning of maximized prime átomatons via NL\* with a membership
-teacher, following Angluin-style learning and its nondeterministic extension
-:cite:`Angluin1987,Bollig2009`:
-
-.. autofunction:: sofic.automata.learning.learn_maximized_prime_atomaton
+NL\* :cite:`Bollig2009` extends Angluin's L\* :cite:`Angluin1987` to
+nondeterministic automata. It keeps an RFSA-closed, RFSA-consistent observation
+table whose prime rows become the hypothesis states, and adds every suffix of a
+counterexample as a new experiment. When the equivalence oracle accepts, the
+hypothesis is the canonical RFSA of the target (:doc:`rfsa`). Running NL\* on
+the reversed target and reversing the result learns the maximized prime
+átomaton (:doc:`atomaton`).
+
+:class:`~sofic.automata.active.AutomatonEquivalenceOracle` answers equivalence
+queries exactly against a target automaton, returning a shortest
+counterexample.
+
+.. autofunction:: sofic.automata.learning.learn_rfsa_nlstar
+.. autofunction:: sofic.automata.learning.learn_prime_atomaton_nlstar
+.. autofunction:: sofic.automata.learning.learn_rfsa_from_language
 
 Active learning (L\*, TTT, Mealy)
 =================================
@@ -65,6 +75,7 @@ equivalence test:
    :members:
 .. autoclass:: sofic.automata.active.LanguageMembershipOracle
 .. autoclass:: sofic.automata.active.FunctionMembershipOracle
+.. autoclass:: sofic.automata.active.AutomatonEquivalenceOracle
 .. autoclass:: sofic.automata.active.ExhaustiveEquivalenceOracle
 .. autoclass:: sofic.automata.active.RandomWalkEquivalenceOracle
 .. autoclass:: sofic.automata.active.TransducerOutputOracle

docs/automata/nwa.rst

@@ -53,13 +53,20 @@ visible roles. Use :meth:`NestedWordAutomaton.to_vpa` to encode an NWA as a VPA;
 by default symbols are tagged with their role so overlapping NWA alphabets still
 become a disjoint visible alphabet.
 
+The closure operations (``union``, ``intersection``, ``complement``,
+``difference``, ``concat``, ``kleene_star``) and decision procedures
+(``is_empty``, ``is_universal``, ``includes``, ``equivalent``) run on the tagged
+VPA encoding (see :doc:`vpa`) and are translated back to an NWA.
+
 API
 ===
 
 .. autoclass:: NestedWord
    :members: from_visible_word, validate
 
 .. autoclass:: NestedWordAutomaton
-   :members: add_call_transition, add_return_transition, add_internal_transition, recognizes, recognizes_visible, from_vpa, to_vpa
+   :members: add_call_transition, add_return_transition, add_internal_transition, recognizes, recognizes_visible,
+             from_vpa, to_vpa, union, intersection, complement, difference, concat, kleene_star, is_empty,
+             is_universal, includes, equivalent
 
 .. autofunction:: sofic.automata.nwa_simulation.recognizes_nwa

docs/automata/observation_table.rst

@@ -17,4 +17,5 @@ API
 
 .. autofunction:: sofic.automata.canonical_extraction.observation_to_canonical_rfsa
 .. autofunction:: sofic.automata.canonical_extraction.observation_to_atomaton
+.. autofunction:: sofic.automata.canonical_extraction.observation_to_maximized_prime_atomaton
 .. autofunction:: sofic.automata.canonical_extraction.observation_to_minimal_dfa

docs/automata/rfsa.rst

@@ -5,15 +5,39 @@
 RFSA
 ***
 
-Residual finite state automata (:class:`ResidualFiniteStateAutomaton`) and their
-canonical form (:class:`CanonicalRFSA`) follow the residual-language theory of
-Denis, Lemay, and Terlutte :cite:`Denis2002`. The extraction helpers documented
-here expose RFSA-oriented entry points without claiming a fully minimized RFSA
-pipeline beyond the implemented automata-backed construction.
+Residual finite state automata (:class:`ResidualFiniteStateAutomaton`) are NFAs
+whose every state accepts a residual (left quotient) of the language
+:cite:`Denis2002`. :meth:`ResidualFiniteStateAutomaton.validate` checks this
+exactly against the minimal DFA.
+
+The canonical RFSA (:class:`CanonicalRFSA`) has one state per *prime*
+residual -- a non-empty residual that is not the union of the residuals strictly
+inside it -- with initial states the primes contained in the language, accepting
+states the primes containing the empty word, and a transition
+:math:`p \xrightarrow{a} p'` whenever :math:`L_{p'} \subseteq a^{-1} L_p`
+:cite:`Denis2002`. It is never larger than the minimal DFA and can be
+exponentially smaller: for :math:`\Sigma^* a \Sigma^n` the minimal DFA has
+:math:`2^{n+1}` states and the canonical RFSA :math:`n + 2`.
+
+Reversing a canonical RFSA gives the maximized prime átomaton of the reversed
+language (:meth:`CanonicalRFSA.dual`; see :doc:`atomaton`). NL\* learns the
+canonical RFSA from queries (:doc:`learning`).
+
+.. code-block:: python
+
+    from sofic.automata.rfsa import CanonicalRFSA
+
+    rfsa = CanonicalRFSA.from_language(nfa)
+    rfsa.validate()               # every state accepts a residual
+    rfsa.dual()                   # maximized prime átomaton of the reverse
 
 API
 ===
 
 .. autoclass:: ResidualFiniteStateAutomaton
 .. autoclass:: CanonicalRFSA
-   :members: from_language, from_observation_table
+   :members: from_language, from_observation_table, dual
+
+.. autofunction:: sofic.automata.canonical_extraction.canonical_rfsa_from_language
+.. autoclass:: sofic.automata.canonical_extraction.ResidualTable
+   :members: includes, is_covered, prime_states

docs/automata/vpa.rst

@@ -6,107 +6,116 @@ Visibly Pushdown Automata
 *************************
 
 :class:`VisiblyPushdownAutomaton` partitions the alphabet into call, return,
-and internal symbols. Call transitions push a stack symbol, return transitions
-may either be guarded by a stack symbol or left unguarded as a wildcard over
-ordinary stack entries, and internal transitions leave the stack untouched.
-The model and its nested-word connection follow Alur and Madhusudan
-:cite:`AlurMadhusudan2009`.
+and internal symbols :cite:`AlurMadhusudan2009`. Call transitions push a stack
+symbol, internal transitions leave the stack alone, and return transitions pop
+it. A return guarded by a stack symbol fires only when that symbol is on top; a
+wildcard return (no stack symbol) fires on every stack symbol, and also on the
+empty stack when the VPA has a ``bottom_stack_symbol``. A return on the empty
+stack is a *pending return*; it is possible only with a bottom symbol and leaves
+the stack empty. Acceptance is by final state, so words may end with *pending
+calls* still on the stack.
+
+Operations and decisions
+========================
+
+Every closure operation returns a concrete automaton:
+
+* ``union`` (disjoint sum) and ``intersection`` (synchronized product);
+* ``determinize`` -- the summary construction of :cite:`AlurMadhusudan2009`,
+  whose states pair a summary relation with the set of current states. The
+  result is a complete :class:`DeterministicVisiblyPushdownAutomaton`, and
+  :meth:`DeterministicVisiblyPushdownAutomaton.from_vpa` uses it whenever its
+  input is nondeterministic;
+* ``complement`` (determinize, then flip accepting states) and ``difference``;
+* ``concat`` and ``kleene_star``. Each factor is read from an empty stack of its
+  own: the finite control records whether the current factor's stack is empty
+  and pushes that bit with every symbol, so a return that would pop a pending
+  call of an earlier factor counts as a pending return of the current one.
+
+Emptiness is decided by saturating the relation of well-matched summaries and
+then searching states reachable with pending calls or pending returns;
+``accepted_word`` returns a witness. ``is_universal``, ``includes``,
+``equivalent``, and ``has_unmatched_word`` build on it.
+:class:`~sofic.automata.nwa.NestedWordAutomaton` exposes the same operations by
+delegating through :meth:`~sofic.automata.nwa.NestedWordAutomaton.to_vpa`.
 
-Canonical forms
-===============
+.. code-block:: python
+
+   balanced.union(other).equivalent(other.union(balanced))   # True
+   balanced.complement().complement().equivalent(balanced)   # True
+   balanced.concat(balanced).accepted_word()                 # e.g. ('(', ')')
+
+Canonical and modular forms
+===========================
+
+General visibly pushdown languages have no unique minimal deterministic VPA, and
+exact unrestricted minimization is NP-complete :cite:`Gauwin2020`. Canonical
+forms exist for well-matched languages, or once calls are assigned to modules
+:cite:`AlurKumarMadhusudanViswanathan2005`.
 
-The VPA module includes four deterministic canonical forms:
+``CanonicalVisiblyPushdownAutomaton``
+   The Myhill-Nerode canonical deterministic VPA of a well-matched language.
+   Its states are classes of the finite algebra of well-matched summaries,
+   refined jointly for top-level contexts and for contexts inside a pending
+   call. With an empty call alphabet it is the minimal DFA. Languages with a
+   pending call or return raise
+   :exc:`~sofic.exceptions.NonWellMatchedLanguageError`.
 
 ``SingleEntryVisiblyPushdownAutomaton``
    A k-module SEVPA. Modules partition the states, calls are assigned to
-   modules by ``call_partition``, every non-base module has one entry state in
-   ``entry_states``, and every call pushes ``(caller_state, call_symbol)``.
+   modules by ``call_partition``, every non-base module has one entry state, and
+   every call pushes ``(caller_state, call_symbol)``.
 
 ``MultipleEntryVisiblyPushdownAutomaton``
-   A k-module MEVPA. Calls are still assigned to modules, but a module may have
-   several entries. The pushed call stack symbol must depend only on the source
-   state.
+   A k-module MEVPA. A module may have several entries, and the pushed symbol
+   depends only on the caller state.
 
 ``CallDrivenAutomaton``
-   A CDA, used here as the shared modular generalization. The target of a call
-   transition is determined by the call symbol, independent of the source state.
-
-``CanonicalVisiblyPushdownAutomaton``
-   The Myhill-Nerode canonical deterministic VPA. It is constructed from the
-   finite algebra of well-matched summaries induced by a deterministic VPA and
-   quotiented by finite right-context acceptance signatures. If the call
-   alphabet is empty, this construction specializes to the usual minimal DFA
-   right congruence.
-
-The modular ``minimize`` constructors require deterministic input and fixed
-module/call metadata. They intentionally do not attempt arbitrary VPA
-minimization: visibly pushdown automata do not have unique minimum recognizers
-in general, and exact unrestricted minimization is NP-complete.
-
-Operations
-==========
-
-Finite automata expose the usual regular operations directly on ``DFA`` and
-``NFA`` instances: ``union``, ``intersection``/``intersect``, ``complement``,
-``difference``, ``concat``/``concatenate``, and ``kleene_star``/``star``.
-
-VPAs expose the same operation names. These return
-``CompositeVisiblyPushdownAutomaton`` instances, which are exact VPA language
-expressions with a ``recognizes`` method. This keeps concatenation and Kleene
-star correct even when an operand accepts with pending stack content; concrete
-graph normalization for those composite VPAs is intentionally left separate
-from the operation API.
-
-Constructor sketch
-==================
+   The shared modular generalization: a call's target depends only on the call
+   symbol.
+
+:func:`~sofic.automata.vpa_constructions.to_single_entry` and
+:func:`~sofic.automata.vpa_constructions.to_multiple_entry` convert any VPA of a
+well-matched language into these forms (default: one module per call symbol).
+On a call the state resets to the module's entry and the caller is pushed, so
+the automaton forgets its caller; that is why pending calls -- and hence
+non-well-matched languages, which raise
+:exc:`~sofic.exceptions.NonWellMatchedLanguageError` -- are out of scope. The
+modular ``minimize`` constructors call these conversions when no modules are
+given, and otherwise quotient the supplied module structure.
 
 .. code-block:: python
 
+   SingleEntryVisiblyPushdownAutomaton.minimize(vpa)                     # convert, then minimize
    SingleEntryVisiblyPushdownAutomaton.minimize(
-       vpa,
-       call_partition={"call": "module"},
-       modules={"main": {"q0"}, "module": {"entry", "body"}},
-       entry_states={"module": "entry"},
-   )
-
-   MultipleEntryVisiblyPushdownAutomaton.minimize(
-       vpa,
-       modules={"main": {"q0"}, "module": {"entry0", "entry1"}},
-       call_partition={"call0": "module", "call1": "module"},
-   )
-
-   CallDrivenAutomaton.minimize(
-       vpa,
-       modules={"main": {"q0"}, "module": {"entry"}},
-       call_partition={"call": "module"},
+       sevpa, call_partition={"call": "module"}, modules=sevpa.modules,
    )
-
    CanonicalVisiblyPushdownAutomaton.from_vpa(vpa)
 
-References
-==========
-
-The summary and SEVPA constructions follow Alur, Kumar, Madhusudan, and
-Viswanathan :cite:`AlurKumarMadhusudanViswanathan2005`. The unrestricted
-minimization limitation follows Gauwin, Muscholl, and Raskin
-:cite:`Gauwin2020`.
-
 API
 ===
 
 .. autoclass:: VisiblyPushdownAutomaton
-   :members: union, intersection, intersect, complement, difference, concat, concatenate, kleene_star, star
+   :members: union, intersection, complement, difference, concat, kleene_star, determinize, is_empty,
+             accepted_word, is_universal, includes, equivalent, has_unmatched_word
 
 .. autoclass:: DeterministicVisiblyPushdownAutomaton
-
-.. autoclass:: CompositeVisiblyPushdownAutomaton
+   :members: from_vpa
 
 .. autoclass:: SingleEntryVisiblyPushdownAutomaton
+   :members: minimize
 
 .. autoclass:: MultipleEntryVisiblyPushdownAutomaton
+   :members: minimize
 
 .. autoclass:: CallDrivenAutomaton
+   :members: minimize
 
 .. autoclass:: CanonicalVisiblyPushdownAutomaton
+   :members: from_vpa
+
+.. automodule:: sofic.automata.vpa_constructions
+   :members: normalize, determinize, complement, concat, kleene_star, well_matched_summaries, accepted_word,
+             has_unmatched_word, to_single_entry, to_multiple_entry
 
 .. autofunction:: sofic.automata.vpa_simulation.recognizes_vpa

docs/references.bib

@@ -158,6 +158,28 @@ @article{Denis2002
   doi     = {10.3233/FUN-2002-51402},
 }
 
+@inproceedings{Tamm2015,
+  author    = {Tamm, Hellis},
+  title     = {Generalization of the Double-Reversal Method of Finding a Canonical Residual Finite State Automaton},
+  booktitle = {Descriptional Complexity of Formal Systems},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {9118},
+  pages     = {268--279},
+  publisher = {Springer},
+  year      = {2015},
+  doi       = {10.1007/978-3-319-19225-3_23},
+}
+
+@inproceedings{MaarandTamm2022,
+  author    = {Maarand, Hendrik and Tamm, Hellis},
+  title     = {Yet Another Canonical Nondeterministic Automaton},
+  booktitle = {Descriptional Complexity of Formal Systems},
+  series    = {Lecture Notes in Computer Science},
+  publisher = {Springer},
+  year      = {2022},
+  doi       = {10.1007/978-3-031-13257-5_14},
+}
+
 @inproceedings{BrzozowskiTamm2011,
   author    = {Brzozowski, Janusz A. and Tamm, Hellis},
   title     = {Theory of {\'A}tomata},