Fixed-arity Boolean constraint languages

The existing CSP syntax is retained. A language supplies arity : Rel → ℕ and the existing list semantics sem : Rel → List Bool → Bool; only lists of the declared arity are used. CSP.WellFormed checks this condition on every constraint. The language, including its arities and truth tables, is fixed independently of the input instance [Che06], Definitions 3.1–3.3. Relation symbols need not be finite for these semantic definitions.

CSP.HasSchaeferPolymorphism is the six-case Boolean criterion of [Che06], Theorem 3.20. The constants are unary operations: they preserve an empty relation vacuously. Empty and nullary relations are allowed. This module defines the criterion, not its complexity dichotomy.

Main definitions

• Cslib.Logic.PL.CSP.WellFormed, Cslib.Logic.PL.CSP.validArity: exact-arity condition and guard.
• Cslib.Logic.PL.CSP.booleanRelation: a relation on its declared finite set of coordinates.
• Cslib.Logic.PL.CSP.HasPolymorphism: a common polymorphism of all relations in a language.
• Cslib.Logic.PL.CSP.HasSchaeferPolymorphism: constants, AND, OR, majority or minority.

def Cslib.Logic.PL.CSP.WellFormed {Rel : Type u_1} {V : Type u_2} (arity : Rel → ℕ) (F : CSP Rel V) : Prop

Every constraint scope has the arity declared by its relation symbol. Repeated variables are allowed and count as distinct positions in the scope.

def Cslib.Logic.PL.CSP.validArity {Rel : Type u_1} {V : Type u_2} (arity : Rel → ℕ) (F : CSP Rel V) : Bool

Executable exact-arity guard for an instance of a fixed constraint language.

@[simp]

theorem Cslib.Logic.PL.CSP.validArity_eq_true_iff {Rel : Type u_1} {V : Type u_2} (arity : Rel → ℕ) (F : CSP Rel V) : validArity arity F = true ↔ WellFormed arity F

The exact-arity guard agrees with the semantic well-formedness condition.

@[instance_reducible]

instance Cslib.Logic.PL.CSP.instDecidableWellFormed {Rel : Type u_1} {V : Type u_2} (arity : Rel → ℕ) (F : CSP Rel V) : Decidable (WellFormed arity F)

Well-formedness is decidable by the executable exact-arity guard.

def Cslib.Logic.PL.CSP.booleanRelation {Rel : Type u_1} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (R : Rel) : Set (Fin (arity R) → Bool)

The relation belonging to a symbol, evaluated only at its declared arity.

def Cslib.Logic.PL.CSP.HasPolymorphism {Rel : Type u_1} {J : Type u_3} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (f : (J → Bool) → Bool) : Prop

A common coordinatewise polymorphism of a fixed Boolean constraint language.

def Cslib.Logic.PL.CSP.HasSchaeferPolymorphism {Rel : Type u_1} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) : Prop

The six common-polymorphism cases of Boolean Schaefer: unary false, unary true, binary AND, binary OR, ternary majority and ternary parity (minority).

theorem Cslib.Logic.PL.CSP.hasPolymorphism_const_iff {Rel : Type u_1} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (b : Bool) : (HasPolymorphism arity sem fun (x : Fin 1 → Bool) => b) ↔ ∀ (R : Rel), (booleanRelation arity sem R).Nonempty → (fun (x : Fin (arity R)) => b) ∈ booleanRelation arity sem R

A unary constant preserves precisely those nonempty relations containing its constant tuple. Empty relations impose no condition, unlike preservation by a nullary constant.