commit b28d83bc9a4d786a6fb898ddaad64173d921a165
parent 9568f40f1b591fb0739defc5dfe10023229e1ed8
Author: Antoine Amarilli <a3nm@a3nm.net>
Date: Wed, 25 Jun 2025 18:36:14 +0200
commit with codex
Diffstat:
8 files changed, 38 insertions(+), 14 deletions(-)
diff --git a/alternation_hierarchy b/alternation_hierarchy
@@ -1,7 +0,0 @@
-# Alternation hierarchy
-
-Hierarchy of [first_order_logic] on [quantifier_alternation_depth]
-
-Up: [hierarchy] of [first_order_logic]
-
-See also: [automata_alternating], [alternation], [dot_depth]
diff --git a/automata_multitape b/automata_multitape
@@ -1,7 +1,7 @@
# Automata multitape
An [automaton] with multiple [tapes] to read multiple [words]
-- each tape can advance independently from the others, unlike [synchronous_automata]
+- the head on each tape can advance independently from the others, unlike [synchronous_automata]
Defines a [rational_relation]
diff --git a/automatic_relation b/automatic_relation
@@ -10,7 +10,7 @@ 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)
+[CD_membership_problem]: [testing_if_automatic_relation_is_recognizable]
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
diff --git a/first_order_interpretation b/first_order_interpretation
@@ -0,0 +1,18 @@
+# First order interpretation
+
+A *d-dimensional FO interpretation* defines:
+
+- an [FO] formula of arity d for domain elements, among d-tuples
+- an [FO] formula of arity 2d, for equality
+ - we take the [quotient] under it
+- [FO] formulas of arity dk to define [relations] of arity k
+
+This allows [formulas] on the image of the FO interpretation to be "translated back" to the source of the FO interpretation
+
+We can get rid of equality, cf [morvan2025homomorphism], Prop VII.3.2
+
+Up: [logic_interpretation], [FO]
+
+Aliases: FO interpretation, FO reduction
+
+See also: [FO_projection]
diff --git a/first_order_projection b/first_order_projection
@@ -8,4 +8,6 @@ A very limited kind of [reduction] defined via [first_order_logic]
Up: [reduction]
-See also: [first_order_logic]
+See also: [first_order_logic], [FO_interpretation], [projection]
+
+Aliases: FO projection
diff --git a/hierarchy b/hierarchy
@@ -5,6 +5,7 @@
- [alternation_hierarchy]
- [arithmetical_hierarchy]
- [time_hierarchy_theorem] / [space_hierarchy_theorem]
+- [logarithmic_time_hierarchy]
Up: [mathematics]
diff --git a/testing_if_automatic_relation_is_recognizable b/testing_if_automatic_relation_is_recognizable
@@ -0,0 +1,6 @@
+# Testing if automatic relation is recognizable
+
+The [CD_membership_problem] for C=[automatic_relations] and D=[recognizable_relations] is [PSPACE_complete]
+- cf [morvan2025homomorphism] Proposition VII.1.9
+
+Up: [CD_membership_problem], [automatic_relation], [recognizable_relation]
diff --git a/word_relation b/word_relation
@@ -2,11 +2,13 @@
A [relation] on [words]
-- [recognizable_relation]
-- [automatic_relation]
-- [rational_relation]
+From most to least expressive:
-Cf [morvan2025homomorphism] Figure VII.1 for an [inclusion_diagram]
+- [rational_relation] with [automata_multitape]
+- [automatic_relation] with [automata_synchronous]
+- [recognizable_relation] with finite [union] of [Cartesian_products] of [regular_languages]
+
+Cf [morvan2025homomorphism] Figure VII.1 for an [inclusion_diagram]. Also discussed in [barcelo2023separating]
[machine_models]:
@@ -16,6 +18,8 @@ Cf [morvan2025homomorphism] Figure VII.1 for an [inclusion_diagram]
- combining [automata] on each [word]
- gives [recognizable_relations] via [Mezei's_theorem]
+Special case: [functional_relation], which corresponds to [transducers]
+
Up: [relation], [word]
Aliases: word relations
