Equality-free primitive-positive gadgets

The canonical table-of-tuples construction in [Che06], Theorem 3.13, arXiv v1, pp. 9–10, gives a finite gadget for a nonempty Boolean relation whose coordinate columns are distinct, whenever its polymorphisms include all positive-arity polymorphisms of the language. The variables of the canonical conjunction are all Boolean columns indexed by the tuples of the target relation. Its constraints enumerate every scope that belongs pointwise to a language relation. Satisfying assignments are exactly polymorphisms.

Distinct columns are necessary here to give separate free ports without equality symbols. We do not implement the source's equality-based removal of repeated columns. Empty target relations are excluded so that only positive-arity polymorphisms are needed. Empty and nullary language relations are allowed, as are nullary target relations.

Main definitions

• Cslib.Logic.PL.CSP.PPGadget: an equality-free conjunction with free and auxiliary ports.
• Cslib.Logic.PL.CSP.SeparatesCoordinates: distinct columns in the target tuple table.

Main results

• Cslib.Logic.PL.CSP.exists_ppGadget_of_polymorphisms: the restricted finite Inv–Pol construction, using all positive finite arities.

structure Cslib.Logic.PL.CSP.PPGadget {Rel : Type} {n : ℕ} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (R : Set (Fin n → Bool)) : Type

A finite equality-free conjunction with free coordinate ports and existential auxiliaries.

• numAux : ℕ

  Number of local auxiliary variables.

• body : CSP Rel (Fin n ⊕ Fin self.numAux)

  Conjunction over separate free and auxiliary ports.

• wellFormed : WellFormed arity self.body

  Every constraint has its declared arity.

• correct (a : Fin n → Bool) : a ∈ R ↔ ∃ (b : Fin self.numAux → Bool), eval sem (Sum.elim a b) self.body = true

  The conjunction existentially defines the target relation.

def Cslib.Logic.PL.CSP.SeparatesCoordinates {n : ℕ} (R : Set (Fin n → Bool)) : Prop

A relation separates its coordinates if its tuple table has distinct columns.

theorem Cslib.Logic.PL.CSP.exists_ppGadget_of_polymorphisms {Rel : Type} {n : ℕ} [Finite Rel] (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (R : Set (Fin n → Bool)) (hne : R.Nonempty) (hsep : SeparatesCoordinates R) (hinv : ∀ (k : ℕ), 0 < k → ∀ (f : (Fin k → Bool) → Bool), HasPolymorphism arity sem f → IsPolymorphism f R) : Nonempty (PPGadget arity sem R)

Finite positive-arity invariance suffices for an equality-free gadget when the target is nonempty and has distinct columns. This is the corresponding restricted converse direction of [Che06], Theorem 3.13; no solver or pp-definability theorem is assumed.