Polymorphisms of relations

An operation preserves a relation when its coordinatewise application to tuples in that relation again belongs to the relation. Relations are ordinary sets of functions, so the coordinate and operation index types need not be finite. Empty index types include nullary relations and operations. For finite nonempty index types this is [Che06], Definition 3.10; allowing arbitrary index types also includes infinitary and nullary operations and relations.

Preservation passes to conjunctions, variable substitutions and existential projections. These are the elementary preservation rules underlying primitive-positive definitions; no converse definability or complexity theorem is asserted here.

Main definitions

• Cslib.Logic.IsPolymorphism: coordinatewise preservation of a relation by an operation.

Main results

• Cslib.Logic.IsPolymorphism.iInter: preservation of conjunctions.
• Cslib.Logic.IsPolymorphism.substitute: preservation after variable substitution.
• Cslib.Logic.IsPolymorphism.project: preservation after existential projection.

References

• H. Chen, A Rendezvous of Logic, Complexity, and Algebra, Definition 3.10 and the preservation direction of Theorem 3.13 (arXiv version 1, pp. 8–10).

def Cslib.Logic.IsPolymorphism {D : Type u_1} {I : Type u_2} {J : Type u_3} (f : (J → D) → D) (R : Set (I → D)) : Prop

An operation f is a polymorphism of R when it preserves membership in R under coordinatewise application. The index type J may be empty (a nullary operation).

theorem Cslib.Logic.isPolymorphism_projection {D : Type u_1} {I : Type u_2} {J : Type u_3} (j : J) (R : Set (I → D)) : IsPolymorphism (fun (a : J → D) => a j) R

Every projection operation preserves every relation.

theorem Cslib.Logic.IsPolymorphism.comp {D : Type u_1} {I : Type u_2} {J : Type u_3} {K : Type u_4} {f : (K → D) → D} {g : K → (J → D) → D} {R : Set (I → D)} (hf : IsPolymorphism f R) (hg : ∀ (k : K), IsPolymorphism (g k) R) : IsPolymorphism (fun (a : J → D) => f fun (k : K) => g k a) R

Composing polymorphisms yields another polymorphism of the same relation.

theorem Cslib.Logic.IsPolymorphism.iInter {D : Type u_1} {I : Type u_2} {J : Type u_3} {K : Type u_4} {f : (J → D) → D} {R : K → Set (I → D)} (h : ∀ (k : K), IsPolymorphism f (R k)) : IsPolymorphism f (⋂ (k : K), R k)

An operation preserves a conjunction of relations if it preserves every conjunct.

theorem Cslib.Logic.IsPolymorphism.substitute {D : Type u_1} {I : Type u_2} {J : Type u_3} {K : Type u_4} {f : (J → D) → D} {R : Set (I → D)} (h : IsPolymorphism f R) (p : I → K) : IsPolymorphism f {a : K → D | a ∘ p ∈ R}

Substituting variables, including repeated variables, preserves polymorphisms.

theorem Cslib.Logic.IsPolymorphism.project {D : Type u_1} {I : Type u_2} {J : Type u_3} {K : Type u_4} {f : (J → D) → D} {R : Set (I → D)} (h : IsPolymorphism f R) (p : K → I) : IsPolymorphism f {a : K → D | ∃ b ∈ R, b ∘ p = a}

Existentially projecting coordinates preserves polymorphisms. The map p may also repeat coordinates; equality constraints are thereby included.

theorem Cslib.Logic.isPolymorphism_const_iff {D : Type u_1} {I : Type u_2} (b : D) (R : Set (I → D)) : IsPolymorphism (fun (x : Empty → D) => b) R ↔ (fun (x : I) => b) ∈ R

A nullary constant operation preserves exactly the relations containing its constant tuple. In particular an empty relation is not preserved by a nullary operation.