Finite ordered relation constructions

RelationMinor.Construction is a finite syntax tree of the ordered operations needed in [DK15], Lemmas 2–3, printed pp. 437–438. Its leaves are the existing language relations. A pin, disequality merge or flip carries the construction enabling that operation; thus none is silently adjoined to the language. The only conjunction constructor is binary intersection, the specific two-digon construction of Lemma 3. There is no arbitrary all-port conjunction or identification.

The syntax records operations on the existing relations, with exact intermediate semantics. An interpreter must justify its individual operations in the intended geometric model. In particular this module proves no geometric planarity or runtime theorem.

Main definitions

• Cslib.Logic.PL.CSP.RelationMinor.Construction: finite ordered construction trees.
• Cslib.Logic.PL.CSP.RelationMinor.Trace.construction: interpret a trace using enabling trees.

inductive Cslib.Logic.PL.CSP.RelationMinor.Construction {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) {n : ℕ} : Set (Fin n → Bool) → Type

Finite ordered derivations from language symbols, recording the enabling pin or disequality construction at every step where one is needed.

• atom {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} (r : Rel) : Construction arity sem (booleanRelation arity sem r)

  One original language constraint, with its original port order.

• project {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin (n + 1) → Bool)} (c : Construction arity sem R) (j : Fin (n + 1)) : Construction arity sem (RelationMinor.project R j)

  Delete one port existentially.

• equalDrop {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin (n + 2) → Bool)} (c : Construction arity sem R) : Construction arity sem (adjacent R false)

  Restrict the first adjacent pair to equality and immediately delete the first port.

• differentDrop {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin (n + 2) → Bool)} (c : Construction arity sem R) (d : Construction arity sem disequality) : Construction arity sem (adjacent R true)

  Restrict the first adjacent pair to disequality, then delete its first port.

• cofactor {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin (n + 1) → Bool)} (c : Construction arity sem R) (j : Fin (n + 1)) (b : Bool) (p : Construction arity sem (pin b)) : Construction arity sem (RelationMinor.cofactor R j b)

  Pin one port using an already constructed unary relation, then delete it.

• flip {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin n → Bool)} (c : Construction arity sem R) (j : Fin n) (d : Construction arity sem disequality) : Construction arity sem (twist R (Pi.single j true))

  Twist one coordinate using an already constructed disequality relation.

• rotate {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin (n + 1) → Bool)} (c : Construction arity sem R) : Construction arity sem (RelationMinor.rotate R)

  Rotate the port list cyclically by one position.

• binaryMeet {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {R S : Set (Fin 2 → Bool)} (c : Construction arity sem R) (d : Construction arity sem S) : Construction arity sem (R ∩ S)

  The binary intersection on the two bounded digons of three parallel edges.

@[reducible, inline]

abbrev Cslib.Logic.PL.CSP.RelationMinor.Available {Rel : Type} {n : ℕ} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (R : Set (Fin n → Bool)) : Prop

Availability means that a finite construction tree exists. This is a semantic existence statement, without a uniform algorithm or a runtime bound.

def Cslib.Logic.PL.CSP.RelationMinor.Trace.construction {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {m n : ℕ} {R : Set (Fin m → Bool)} {S : Set (Fin n → Bool)} (trace : Trace R S) (c : Construction arity sem R) (d : Construction arity sem disequality) (p : (b : Bool) → Construction arity sem (pin b)) : Construction arity sem S

Interpret an actual minor trace using actual constructions of its starting relation, disequality and the two pins. Each cofactor or flip records its enabling construction.