commit b18949321d32a1a8738a70ef0896a5e63edd8188 parent 7c28387bf75853ec9178c91ac7bef758f319616a Author: Antoine Amarilli <a3nm@a3nm.net> Date: Wed, 25 Jun 2025 13:45:51 +0200 commit with codex Diffstat:
32 files changed, 234 insertions(+), 63 deletions(-)
diff --git a/automata_classes b/automata_classes @@ -9,6 +9,8 @@ - [automata_acyclic] - [automata_weakly_acyclic] - [automata_self_verifying] +- [automata_one_way] + - [automata_two_way] - [DFAs] diff --git a/automata_deterministic b/automata_deterministic @@ -1,9 +1,9 @@ # Automata deterministic -[automata] where for each [state] and [letter] there is at most one outgoing [transition] +[one_way_word_automaton] where for each [state] and [letter] there is at most one outgoing [transition] - possibly none for [incomplete_automata] -Up: [automata_types], [determinism_language] +Up: [one_way_word_automaton], [determinism_language] Aliases: automaton deterministic, deterministic automaton, deterministic automata, DFA, DFAs, automaton determinism, automata determinism diff --git a/automata_multitape b/automata_multitape @@ -0,0 +1,12 @@ +# Automata multitape + +An [automaton] with multiple [tapes] to read multiple [words] +- each tape can advance independently from the others, unlike [synchronous_automata] + +Defines a [rational_relation] + +Can be seen as an automaton reading symbols of the form (a, padding) or (padding, a), and looking at its semantics under erasure of the padding symbols + +Up: [automata_types] + +Aliases: multitape automaton, multitape automata diff --git a/automata_nondeterministic b/automata_nondeterministic @@ -1,13 +1,13 @@ # Automata nondeterministic (NFA) -An [automaton] which is [nondeterministic] +A [one_way_automaton] which is [nondeterministic] There are known upper bounds on the size of the smallest [DFA] corresponding to an NFA Special case: [automata_nondeterministic_dense] -Up: [nondeterministic], [automata_types] +Up: [one_way_automaton], [nondeterministic] See also: [epsilon_transition] -Aliases: nondeterministic automaton, nondeterministic automata, NFA, NFAs, automaton nondeterministic +Aliases: nondeterministic automaton, nondeterministic automata, NFA, NFAs, automaton nondeterministic, word automaton nondeterministic diff --git a/automata_one_way b/automata_one_way @@ -0,0 +1,13 @@ +# Automata one way + +An [automaton] which reads its input [word] in one pass from left to right, by contrast to [two_way_automata] + +- [one_way_word_automaton] + - [NFA] + - [UFA] + - [DFA] +- [one_way_tree_automaton] + +Up: [word_automata] + +Aliases: one way automaton, one way automata, automaton one way diff --git a/automata_two_way b/automata_two_way @@ -1,17 +1,10 @@ # Automata two way -[Automata] that can read the input [word] in both directions - -[Automata_two_way_determinization] - -Can be converted back to [automata_one_way]. -- Elementary construction to get an [automata_nondeterministic] for the complement language in [vardi1989note] with exp(n) blowup -- Elementary construction to get an [automata_deterministic] for the language in [shepherdson1959reduction] with exp(n^2) blowup - -Generalization: [Two_way_nondeterministic_pushdown_automaton] +- [word_automaton_two_way] +- [tree_automaton_two_way] Up: [automata] See also: [2rpq] -Aliases: two-way automaton, two-way automata, 2 way automaton, 2 way automata +Aliases: two-way automaton, two-way automata, 2 way automaton, 2 way automata, two way automata, automaton two way diff --git a/automata_types b/automata_types @@ -29,5 +29,6 @@ - [vector_addition_system] - [automata_weighted] - [omega_automata] +- [automata_multitape] Up: [automata] diff --git a/automatic_relation b/automatic_relation @@ -6,6 +6,16 @@ symbol, i.e., [automaton_synchronous] - Paper about this: [barcelo2023separating] - [automatic_relation_algebra] +Special case: [recognizable_relations] + +Generalization: [deterministic_rational_relations], [rational_relations] + +The [CD_membership_problem] for C=automatic relations and D=[recognizable_relations] is [PSPACE_complete] (cf [morvan2025homomorphism] Proposition VII.1.9) + +It is an [open_problem] whether the [computational_problem] of deciding [formal_language_separation] of automatic relations by a [recognizable_relation] is a [decidable] problem + Up: [automata], [relation] -See also: [automatic_structure], [automatic_graph], [sequence_automatic] +See also: [automatic_structure], [automatic_graph], [sequence_automatic], [post_correspondence_problem] + +Aliases: automatic relations diff --git a/automaton_equivalence b/automaton_equivalence @@ -8,3 +8,5 @@ Up: [automata_problems] See also: [language_equivalence], [automaton_inclusion], [query_equivalence_problem] + +Aliases: automaton equivalence problem, automata equivalence problem diff --git a/automaton_synchronous b/automaton_synchronous @@ -0,0 +1,14 @@ +# Automaton synchronous + +An [automaton] which reads two [words] simultaneously, with pairs of characters and a padding symbol +- [word_convolution] to mean zipping two words together + +Defines an [automatic_relation] + +The semantics of such automata is only considered on [wellformed_word_convolutions], there the padding symbols correspond only at the end + +Up: [automata_types] + +Aliases: synchronous automaton, synchronous automata, automata synchronous + +See also: [automaton_multitape] diff --git a/cd_membership_problem b/cd_membership_problem @@ -0,0 +1,10 @@ +# CD membership problem + +Terminology from [morvan2025homomorphism]: for C and D two classes of inputs with D subseteq C, the [computational_problem] of: + +- input: an object in C +- output: does the object belong to D? + +Up: [computational_problem] + +See also: [Formal_language_separation] diff --git a/equivalence_problem b/equivalence_problem @@ -8,4 +8,4 @@ Up: [computational_problem], [equivalence] -See also: [equisatisfiability] +See also: [equisatisfiability], [inclusion_problem] diff --git a/formal_language_computational_problems b/formal_language_computational_problems @@ -7,6 +7,7 @@ - [finiteness_problem] - [emptiness_testing] - [cofiniteness_testing] +- [cd_membership_problem] Up: [formal_language] diff --git a/function b/function @@ -1,7 +1,5 @@ # Function -can be [function_partial] - - [linear_function] - [piecewise_linear] function @@ -18,6 +16,16 @@ Notions: - [function_evaluation] +Basic notions: + +- [function_graph] +- [injective] +- [surjective] +- [bijective] +- [function_partial] +- [function_image] +- [function_preimage] + Up: [mathematics] See also: [functional_dependency], [function_symbol] diff --git a/intersection b/intersection @@ -6,3 +6,5 @@ - [sorted_list_intersection] Up: [boolean_operator] + +Aliases: intersections diff --git a/language_emptiness b/language_emptiness @@ -8,4 +8,4 @@ Up: [computational_problem], [formal_language] See also: [universality_problem] -Aliases: emptiness testing +Aliases: emptiness testing, emptiness problem diff --git a/machine_model b/machine_model @@ -3,5 +3,9 @@ - [memory_model_external] - [ram_model] - [cell_probe_model] +- [automata] + - [transducers] Up: [theoretical_computer_science] + +Aliases: machine models diff --git a/mathematical_foundations_of_automata_theory b/mathematical_foundations_of_automata_theory @@ -4,3 +4,5 @@ https://www.irif.fr/~jep/PDF/MPRI/MPRI.pdf [course_notes] by [jean_eric_pin] Up: [course_notes] + +Aliases: mpri PDF diff --git a/morphism b/morphism @@ -2,9 +2,10 @@ On [words]: -- [non_erasing_morphism] -- [length_preserving_morphism] +[morphism_types] Up: [mathematics] See also: [homomorphism] + +Aliases: morphisms diff --git a/morphism_types b/morphism_types @@ -0,0 +1,10 @@ +# Morphism types + +cf [mpri_pdf], Chapter XIII, section 2, p225 + +- [non_erasing_morphism] +- [length_preserving_morphism]: the [function_image] of every [letter] is a [letter] +- [length_multiplying_morphism]: the [function_image] of all [letters] have the same [length] + + +Up: [morphism] diff --git a/one_way_word_automaton b/one_way_word_automaton @@ -0,0 +1,11 @@ +# One way word automaton + +A [word_automaton] which is [automata_one_way] + +- [NFA] +- [UFA] +- [DFA] + +Up: [automata_one_way], [word_automaton] + +See also: [one_way_tree_automaton] diff --git a/post_correspondence_problem b/post_correspondence_problem @@ -0,0 +1,12 @@ +# Post correspondence problem + +https://en.wikipedia.org/wiki/Post_correspondence_problem + +The [computational_problem], given a set of [word] [pairs] (u_1, v_1), ..., (u_k, v_k), of deciding whether there is a sequence of indices i_1, ..., i_n in {1, ..., k} (potentially with repetitions) so that the concatenations +u_{i_1} ... u_{i_n} and v_{i_1} ... v_{i_n} are the same [word] + +It is an [undecidable] problem + +Up: [computational_problem] + +Aliases: PCP diff --git a/rational_relation b/rational_relation @@ -0,0 +1,11 @@ +# Rational relation + +The [word_relations] defined by [multitape_automata] + +Special cases: +- [rational_relation_deterministic] +- [automatic_relation] + +Up: [word_relation] + +Aliases: rational relations diff --git a/rational_relation_deterministic b/rational_relation_deterministic @@ -0,0 +1,18 @@ +# Deterministic rational relation + +Special case: [automatic_relation] + +Generalization: [rational_relation] + +The [rational_relations] recognized by a [multitape_automaton] which is [deterministic_automaton] and where, on every state, we know precisely which set of [heads] will move. This can be called a [deterministic_multitape_automaton] + +Must also add a fresh padding symbol to the right of words + +The [emptiness_problem] on the [intersections] of two dynamic rational relations is [undecidable] by reduction from [PCP], cf [morvan2025homomorphism] p209 + +The [inclusion_problem] for [deterministic_multitape_automata] is [undecidable] but the [automaton_equivalence_problem] is [decidable], cf [morvan2025homomorphism] p209 + + +Up: [rational_relation], [determinism] + +Aliases: deterministic rational relation, deterministic rational relations diff --git a/recognizable_relation b/recognizable_relation @@ -0,0 +1,14 @@ +# Recognizable relation + +A [relation] over [words] (i.e., a subset of pairs of words -- potentially the first and second component are not over the same [alphabet]) is *recognizable* if it is a finite [union] of [Cartesian_products] of [regular_languages] (on each alphabet) + +By [Mezei's_theorem] (cf [morvan2025homomorphism] Prop VII.1.1), they are exactly the relations that are [monoid_recognized] by finite [monoids] and [morphisms] +- This theorem generalizes to a correspondence between [monoid_varieties] and [language_varieties] + +A recognizable relation must contain an infinite [clique] (cf [morvan2025homomorphism] Cor VII.1.3) + +Generalizations: [automatic_relations] + +Up: [word_relation] + +Aliases: recognizable relations diff --git a/tree_automaton b/tree_automaton @@ -4,22 +4,23 @@ Defines [regular_tree_language] ## Types -- [tree_automaton_bottom_up] -- [tree_automaton_top_down] -- [tree_automaton_deterministic] -- [tree_automaton_nondeterministic] +- [tree_automaton_one_way] + - [tree_automaton_bottom_up] + - [tree_automaton_top_down] + - [tree_automaton_deterministic] + - [tree_automaton_nondeterministic] ## Variants -Also [dag_automaton] DAG-automaton +Also [DAG_automaton] https://codeberg.org/yvomeeres/pubs/raw/branch/draft/dag-draft.pdf -and [jumping_automata_on_graphs] jumping automata on graphs +and [jumping_automata_on_graphs] - [tree_automaton_infinite] - [counter_automata_trees] Up: [automata] on [tree] -See also: [dtd], [xml] +See also: [dtd], [xml], [Tree_walking_automaton] Aliases: tree automata diff --git a/tree_automaton_one_way b/tree_automaton_one_way @@ -0,0 +1,12 @@ +# Tree automaton one way + +- [tree_automaton_bottom_up] +- [tree_automaton_top_down] +- [tree_automaton_deterministic] +- [tree_automaton_nondeterministic] + +Up: [tree_automaton], [one_way_automaton] + +Aliases: one way tree automaton, one way tree automata + +See also: [tree_automaton_two_way] diff --git a/variety b/variety @@ -2,15 +2,11 @@ ## Variety of formal language -Variety of [formal_languages] is closed under: -- [Derivative] -- [Boolean_operators] ([union], [intersection], [complementation]) - - maybe not [complementation] in which case it is a [positive_variety] -- and [inverse_morphism] +[variety_formal_language] ## Variety of [monoid] -Variety of [monoid] is closed under [direct_product], [quotient], and [submonoid] +[variety_monoid] ## Variety of [semigroup] diff --git a/word_automaton b/word_automaton @@ -1,28 +0,0 @@ -# Word automata - -- [word_automaton_unambiguous] - - [word_automaton_self_verifying] -- [automata_nondeterministic] -- [automata_bideterministic] - - [automata_reversible] -- [automata_probabilistic] -- [counter_automata] -- [automata_weighted] - -conciseness bounds between [automata_two_way] 2NFA and 1NFA, [automata_alternating] alternating or not, etc? - -[word_automata_taxonomy] - -problems: - -- [automaton_minimization] -- [language_inclusion] -- [language_equivalence] -- [universality_automata] -- [formal_language_separation] - -Up: [automata] - -See also: [word_problem] - -Aliases: word automata diff --git a/word_automaton_two_way b/word_automaton_two_way @@ -0,0 +1,11 @@ +# Word automaton two way + +[Word_automata] that can read the input [word] in both directions + +[Automata_two_way_determinization] + +Can be converted back to [automata_one_way]: [word_automaton_two_way_one_way_conversion] + +Generalization: [Two_way_nondeterministic_pushdown_automaton] + +Up: [word_automaton], [automata_two_way] diff --git a/word_automaton_two_way_one_way_conversion b/word_automaton_two_way_one_way_conversion @@ -0,0 +1,7 @@ +# Word automaton two way one way conversion + +- Elementary construction to get a [DFA] for the complement [formal_language] in [vardi1989note] with exp(n) blowup +- Elementary construction to get a [DFA] for the language in [shepherdson1959reduction] with exp(n^2) blowup +- Historical attribution in [morvan2025homomorphism] VII.1.1 p197 + +Up: [conversion_automaton] of [word_automaton_two_way] to [word_automaton_one_way] diff --git a/word_relation b/word_relation @@ -0,0 +1,21 @@ +# Word relation + +A [relation] on [words] + +- [recognizable_relation] +- [automatic_relation] +- [rational_relation] + +Cf [morvan2025homomorphism] Figure VII.1 for an [inclusion_diagram] + +[machine_models]: + +- [transducers] +- [multitape_automata] +- [synchronous_automaton]: gives [automatic_relations] +- combining [automata] on each [word] + - gives [recognizable_relations] via [Mezei's_theorem] + +Up: [relation], [word] + +Aliases: word relations