commit 01aa58a2536a1d0b7ddb412d0f5b2afaf34f659e parent 274803c5992608e9d70888accaa516100bc837ea Author: Antoine Amarilli <a3nm@a3nm.net> Date: Thu, 27 Mar 2025 13:58:46 +0100 commit with codex Diffstat:
32 files changed, 315 insertions(+), 3 deletions(-)
diff --git a/algebra_basic_definitions b/algebra_basic_definitions @@ -0,0 +1,8 @@ +# Algebra basic definitions + +- [commutative] +- [neutral_element] +- [annihilating_element] +- [distributivity] + +Up: [algebra] diff --git a/annihilating_element b/annihilating_element @@ -0,0 +1,9 @@ +# Annihilating element + +For S a [set] and z an [element], if you have a [operation] on S, then z is an annihilating element if for every x in S, you have xz = zx = z. + +If there is an annihilating element, then there is exactly one. + +Up: [algebra_basic_definitions] + +See also: [nilpotent] diff --git a/automaton_emptiness b/automaton_emptiness @@ -1,6 +1,6 @@ # Automaton emptiness -[nl_complete] to check [automaton] emptiness +It is [nl_complete] to check [automaton] emptiness Up: [automata_problems], [language_emptiness] diff --git a/automaton_equivalence b/automaton_equivalence @@ -7,4 +7,4 @@ Up: [automata_problems] -See also: [language_equivalence], [automaton_inclusion] +See also: [language_equivalence], [automaton_inclusion], [query_equivalence_problem] diff --git a/common_subsequence_automaton b/common_subsequence_automaton @@ -0,0 +1,9 @@ +# Common subsequence automaton + +An [automaton] that accepts the language of all [subsequences] of a [word] or of all [common_subsequences] of a set of [words] + +[crochemore2003directed] + +Up: [common_subsequence] + +See also: [subword_automaton] diff --git a/empty_language b/empty_language @@ -0,0 +1,7 @@ +# Empty language + +The [formal_language] featuring no [words] + +Up: [formal_language] + +See also: [empty_word], [empty_set] diff --git a/enumeration_complexity b/enumeration_complexity @@ -0,0 +1,16 @@ +# Enumeration complexity + +## [complexity_time] + +- [enumeration_constant_delay] + - [linear_preprocessing_constant_delay] + - [linear_preprocessing_constant_delay_constant_memory] +- [enumeration_polylog_delay] +- [enump] + +## [complexity_space] + +- may allow constant memory or more than constant memory +- distinguish memory of the structure built by the [preprocessing] vs memory used during the [enumeration] + +Up: [enumeration] diff --git a/enumeration_tasks b/enumeration_tasks @@ -0,0 +1,25 @@ +# Enumeration tasks + +- [enumeration_query_answers]: + - [enumeration_cqs] + - [enumeration_ucqs] + - [enumeration_mso] + - [enumeration_second_order]: [durand2011enumeration] +- [enumeration_strings] + - [enumeration_dag] + - [enumeration_general_purpose] + - [enumeration_distinct_factors] + - [enumeration_cfg] + - [enumeration_compressed] + - [enumeration_slp] + - [enumeration_core] + - [enumeration_rpq] +- [enumeration_spanner] +- [enumeration_graphs] + - [enumeration_paths] +- [enumeration_homomorphisms] ([christoph_berkholz]) +- [enumeration_csp] ([christoph_berkholz]) +- [enumeration_topological_sort] + - https://cstheory.stackexchange.com/questions/36334/enumerating-topological-sorts-of-a-vertex-labeled-dag + +Up: [enumeration] diff --git a/first_order_logic_width b/first_order_logic_width @@ -0,0 +1,5 @@ +# First order logic width + +The *width* of a [first_order_logic] formula is the maximal size of a [set] of [free_variables] in a [subformula] of the [formula] + +Up: [first_order_logic] diff --git a/fixed_parameter_tractable b/fixed_parameter_tractable @@ -0,0 +1,10 @@ +# Fixed parameter tractable (FPT) + +- [fpt_reduction] +- [above_guarantee] + +See also: [xp] + +Up: [parameterized_complexity] + +Aliases: FPT, FPTness diff --git a/flipper_game b/flipper_game @@ -0,0 +1,7 @@ +# Flipper game + +A [games] played between two [graphs], with two [players] flipper and connector + +introduced in [grohe2017deciding] + +Up: [flip] diff --git a/fo2 b/fo2 @@ -0,0 +1,14 @@ +# Fo2 + +[FOk] with two variables + +extensions: +- [c2] with [counting_quantifier] +- [gc2] with [guarded_fragment] quantification + +FO2 on [words] with order cannot define [successor]: you need [fo3] +- with [successor], it defines a variety of [semigroups] + +Does not enjoy [craig_interpolation], according to [cate2023craig], but enjoys [finite_model_property] + +Up: [fok] diff --git a/fok b/fok @@ -0,0 +1,23 @@ +# FOk + +[first_order_logic] with k variables, or [first_order_logic_width] k + +## Fragments + +- [fo2] + +## Extensions + +- [fok_counting] with [counting_quantifier] + +## [Computational_problems] + +- [satisfiability] of FO^2 etc., cf "kings" [gradel1997decision] + +- [first_order_model_checking_fok] + - special case: [first_order_model_checking_fo2] + - connections to [yannakakis_algorithm] + +- finding the best k: [fok_rewriting] + +Up: [first_order_logic] diff --git a/formal_language b/formal_language @@ -2,12 +2,13 @@ A [set] of [words] over an [alphabet] +- [empty_language] - [regular_language] - [weighted_language] - [visibly_pushdown_language] - [context_free_language] - [formal_language_operator] -- [slice]: subset of the [word]s of a certain length +- [slice]: [subset] of the [words] of a certain [length] - [density_function] - [language_unary] diff --git a/formula_measure b/formula_measure @@ -0,0 +1,8 @@ +# Formula measure + +- [quantifier_rank] +- [first_order_logic_width] + +Up: [logic], [formula] + +See also: [width_measure] diff --git a/guarded_fragment b/guarded_fragment @@ -0,0 +1,13 @@ +# Guarded fragment + +- [gf2] +- [gc2]: like [fo2] with [counting_quantifiers] +- [gck] + +According to [cate2023craig], enjoys [finite_model_property] but not [craig_interpolation] + +[Online_workshop]: [GF25] + +See also: [michael], [finite_model_theory], [guarded_negation], [pratt_hartmann], [frontier_guarded], [guard_atom] + +Up: [logic] diff --git a/k_ov_conjecture b/k_ov_conjecture @@ -0,0 +1,7 @@ +# k-OV conjecture + +The [computational_hypothesis] that [k_orthogonal_vectors] requires time n^{k-o(1)} + +Up: [ov_conjecture] + +Aliases: k-OV-hypothesis diff --git a/language_emptiness b/language_emptiness @@ -0,0 +1,7 @@ +# Language emptiness + +The [computational_problem] of deciding if a [formal_language] is [empty_language] + +- [automaton_emptiness] + +Up: [formal_language], [emptiness] diff --git a/language_finite b/language_finite @@ -0,0 +1,13 @@ +# Language finite + +[Formal_language] which is [finite] + +A finite language is always a [regular_language] + +A [representation] for finite languages: [variable_strings] + +Up: [regular_language_family] + +Aliases: finite language, finite languages + +See also: [automaton_finiteness] diff --git a/marcus_tardos b/marcus_tardos @@ -0,0 +1,8 @@ +# Marcus-Tardos + +[marcus2004excluded]: linear bound on the number of 1's of a 0-1 [matrix] that avoids a [permutation_matrix] as a [submatrix] +- implies the [stanley_wilf_conjecture] + +Up: [square_testing_2d] + +See also: [permutation_pattern_matching] diff --git a/ontology b/ontology @@ -0,0 +1,12 @@ +# Ontology + +- [ontology_alignment] +- [ontology_mediated_query] +- [ontology_based_data_access] +- [upper_ontology] + +[syntax] and [semantics] + +Up: [knowledge_representation] + +See also: [knowledge_base], [logic], [philosophy], [description_logics], [database_dependency], [ontology_philosophy] diff --git a/open_world_query_answering_rpqs b/open_world_query_answering_rpqs @@ -0,0 +1,9 @@ +# Open world query answering rpqs + +Studied in [ostropolskinalewaja2024sticky] + +- bounding the [cliquewidth] ensures [decidability] +- [finite_unification_set] [undecidable] +- [tgds_sticky] [decidable] + +Up: [open_world_query_answering], [regular_path_query] diff --git a/permutation b/permutation @@ -27,3 +27,5 @@ Up: [mathematics] See also: [sorting] + +Aliases: permutations diff --git a/permutation_pattern_matching b/permutation_pattern_matching @@ -0,0 +1,12 @@ +# Permutation pattern matching + +[computational_complexity] +- [np_hard]: [bose1998pattern] +- [fixed_parameter_tractable]: [guillemot2013finding] + +[stanley_wilf_conjecture] +- [conjecture] on the proportion of [permutations] which [permutation_avoid] a [permutation_pattern] + +See also: [permutation], [vincular] + +Up: [pattern_matching], [permutation_pattern] diff --git a/query_equivalence b/query_equivalence @@ -0,0 +1,11 @@ +# Query equivalence + +Two [Boolean_queries] Q and Q' are *equivalent* if they are satisfied on precisely the same [databases]. + +For non-Boolean [queries], on every [database] the [set] of returned [answers] should be the same + +[Computational_problem]: [query_equivalence_problem] + +Up: [equivalence], [query] + +Aliases: query_equivalent diff --git a/query_rewriting b/query_rewriting @@ -0,0 +1,18 @@ +# Query rewriting + +from a [query], produce a [query] which is [query_equivalent] and has some better properties, e.g., +- membership to restricted [query_language] + +## Examples + +- [first_order_rewriting] + - [fok_rewriting] +- [datalog_rewriting] + +## Distiction + +Distinguish [rewriting] (an [algorithm] that can rewrite a [query_language] into another in a [computable] way) and [expressibility] ([queries] in a given [query_language] can always be expressed as a [query_equivalent] [query] in another [query_language]) + +Up: [database_theory] + +See also: [query_evaluation] diff --git a/satisfiability b/satisfiability @@ -0,0 +1,19 @@ +# Satisfiability + +The *satisfiability problem* is a [decision_problem] in [logic]: given a [logical_theory], decide if it has a [model] + +- [first_order_logic] with two variables is decidable also with equality, cf <www.cs.rice.edu/~vardi/papers/dimacs96.ps.gz>, page 10 + - on trees with ancestor/descendant, difficult [open_problems], cf [bojanczyk2006two] + - [vector_addition_tree_automata] ([degroote2004vector]), like [vector_addition_system] +- [kontchakov2005undecidability]: [first_order_logic] with three variables is [undecidable] even without [constants] or [equality] + - [david2010satisfiability] bottom of p10: even on [data_trees] +- [satisfiability_boolean] + - [satisfiability_cnf] +- [QBF]: http://www.qbflib.org/ +- [satisfiability_weighted] + +Tools: [sat_solver] + +See also: [strong_exponential_time_hypothesis], [satisfiability_boolean], [tautology], [automaton_emptiness], [satisfiability_modulo_theory], [equisatisfiability] + +Up: [computational_problem] diff --git a/stanley_wilf_conjecture b/stanley_wilf_conjecture @@ -0,0 +1,7 @@ +# Stanley wilf conjecture + +https://en.wikipedia.org/wiki/Stanley%E2%80%93Wilf_conjecture + +Now proved: see [marcus_tardos] + +Up: [permutation_pattern_matching] diff --git a/time_hierarchy_theorem b/time_hierarchy_theorem @@ -0,0 +1,7 @@ +# Time hierarchy theorem + +https://en.wikipedia.org/wiki/Time_hierarchy_theorem + +For each c>1, there are problems solvable in O(n^c) but not O(n^{c-eps}) + +Up: [theorem], [time_complexity] diff --git a/tuple_independent_database b/tuple_independent_database @@ -0,0 +1,13 @@ +# Tuple independent database + +A [relational_database] with a function giving a [probability] to each tuple + +We assume [probabilistic_independence] across tuples + +Concise representation of a [probability_distribution] on [possible_worlds] (it is the [product_distribution]) + +Up: [probabilistic_databases] + +See also: [probabilistic_graph], [block_independent_disjoint] + +Aliases: tuple independent databases, TID, TIDs diff --git a/ucq_to_cq b/ucq_to_cq @@ -0,0 +1,10 @@ +# Ucq to cq + +techniques to replace [UCQs] by [CQs] in [hardness] [proofs] + +- e.g., + - taking a [disjunction] on [path] lengths + - increasing the [arity] with an extra [attribute] +- cf [ability_to_count] in [atserias2008digraph] + +Up: [union_of_conjunctive_queries] diff --git a/union_of_conjunctive_queries b/union_of_conjunctive_queries @@ -2,6 +2,8 @@ [disjunction] of [conjunctive_query] that all have the same [free_variables] +Also called "existential-positive queries", i.e., [FO] queries using only [existential_quantification] and [disjunction] + [ucq_to_cq]: techniques to replace UCQs by CQs in hardness proofs special case: [hk_queries]