↑ Top


Graph Structures (again)

This is the Structures.Graphs0 module of the Agda Universal Algebra Library.

N.B. This module differs from Graphs.lagda in that here we assume some universes are level zero (i.e., β„“β‚€). This simplifies some things; e.g., we avoid having to use lift and lower (cf. Graphs.lagda)

Definition [Graph of a structure]. Let 𝑨 be an (𝑅,𝐹)-structure (relations from 𝑅 and operations from 𝐹). The graph of 𝑨 is the structure Gr 𝑨 with the same domain as 𝑨 with relations from 𝑅 and together with a (k+1)-ary relation symbol G 𝑓 for each 𝑓 ∈ 𝐹 of arity k, which is interpreted in Gr 𝑨 as all tuples (t , y) ∈ Aᡏ⁺¹ such that 𝑓 t ≑ y. (See also Definition 2 of https://arxiv.org/pdf/2010.04958v2.pdf)

{-# OPTIONS --without-K --exact-split --safe #-}

module Structures.Graphs0 where

-- Imports from Agda and the Agda Standard Library -------------------------------------------
open import Agda.Primitive using ( _βŠ”_ ; Level ) renaming ( Set to Type ; lzero to β„“β‚€ )
open import Data.Product   using ( _,_ ; _Γ—_ ; Ξ£-syntax )
open import Data.Sum.Base  using ( _⊎_ ) renaming ( inj₁ to inl ; injβ‚‚ to inr )
open import Data.Fin.Base  using ( Fin )
open import Data.Nat       using ( β„• )
open import Data.Unit.Base using ( ⊀ ; tt )
open import Function.Base  using ( _∘_ )
open import Relation.Unary using ( Pred ; _∈_ )
open import Relation.Binary.PropositionalEquality
                           using ( _≑_ ; module ≑-Reasoning ; cong ; sym ; refl )

-- Imports from the Agda Universal Algebra Library ---------------------------------------------
open import Overture.Preliminaries         using ( ∣_∣ ; βˆ₯_βˆ₯ )
open import Relations.Continuous           using ( Rel )
open import Structures.Basic               using ( signature ; structure )
open import Examples.Structures.Signatures using ( Sβˆ… )
open import Structures.Homs                using ( hom ; is-hom-rel ; is-hom-op )


open signature
open structure
open _⊎_

Gr-sig : signature β„“β‚€ β„“β‚€ β†’ signature β„“β‚€ β„“β‚€ β†’ signature β„“β‚€ β„“β‚€

Gr-sig 𝐹 𝑅 = record { symbol = symbol 𝑅 ⊎ symbol 𝐹
                    ; arity  = ar }
 where
 ar : symbol 𝑅 ⊎ symbol 𝐹 β†’ Type β„“β‚€
 ar (inl π‘Ÿ) = (arity 𝑅) π‘Ÿ
 ar (inr 𝑓) = (arity 𝐹) 𝑓 ⊎ ⊀


private variable
 𝐹 𝑅 : signature β„“β‚€ β„“β‚€

Gr : structure 𝐹 𝑅 {β„“β‚€} {β„“β‚€} β†’ structure Sβˆ… (Gr-sig 𝐹 𝑅) {β„“β‚€} {β„“β‚€}
Gr {𝐹}{𝑅} 𝑨 = record { carrier = carrier 𝑨 ; op = Ξ» () ; rel = split }
  where
  split : (s : symbol 𝑅 ⊎ symbol 𝐹) β†’ Rel (carrier 𝑨) (arity (Gr-sig 𝐹 𝑅) s) {β„“β‚€}
  split (inl π‘Ÿ) arg = rel 𝑨 π‘Ÿ arg
  split (inr 𝑓) args = op 𝑨 𝑓 (args ∘ inl) ≑ args (inr tt)


open ≑-Reasoning

module _ {𝑨 𝑩 : structure 𝐹 𝑅 {β„“β‚€}{β„“β‚€}} where

 homβ†’Grhom : hom 𝑨 𝑩 β†’ hom (Gr 𝑨) (Gr 𝑩)
 hom→Grhom (h , hhom) = h , (i , ii)
  where
  i : is-hom-rel (Gr 𝑨) (Gr 𝑩) h
  i (inl π‘Ÿ) a x = ∣ hhom ∣ π‘Ÿ a x
  i (inr 𝑓) a x = goal
   where
   homop : h (op 𝑨 𝑓 (a ∘ inl)) ≑ op 𝑩 𝑓 (h ∘ (a ∘ inl))
   homop = βˆ₯ hhom βˆ₯ 𝑓 (a ∘ inl)

   goal : op 𝑩 𝑓 (h ∘ (a ∘ inl)) ≑ h (a (inr tt))
   goal = op 𝑩 𝑓 (h ∘ (a ∘ inl)) β‰‘βŸ¨ sym homop ⟩
          h (op 𝑨 𝑓 (a ∘ inl))   β‰‘βŸ¨ cong h x ⟩
          h (a (inr tt))         ∎

  ii : is-hom-op (Gr 𝑨) (Gr 𝑩) h
  ii = Ξ» ()


 Grhomβ†’hom : hom (Gr 𝑨) (Gr 𝑩) β†’ hom 𝑨 𝑩
 Grhom→hom (h , hhom) = h , (i , ii)
  where
  i : is-hom-rel 𝑨 𝑩 h
  i R a x = ∣ hhom ∣ (inl R) a x
  ii : is-hom-op 𝑨 𝑩 h
  ii f a = goal
   where
   split : arity 𝐹 f ⊎ ⊀ β†’ carrier 𝑨
   split (inl x) = a x
   split (inr y) = op 𝑨 f a
   goal : h (op 𝑨 f a) ≑ op 𝑩 f (Ξ» x β†’ h (a x))
   goal = sym (∣ hhom ∣ (inr f) split refl)

Lemma III.1. Let 𝑆 be a signature and 𝑨 be an 𝑆-structure. Let β„° be a finite set of identities such that 𝑨 ⊧ β„°. For every instance 𝑿 of CSP(𝑨), one can compute in polynomial time an instance 𝒀 of CSP(𝑨) such that 𝒀 ⊧ β„° and | hom 𝑿 𝑨 | = | hom 𝒀 𝑨 |.

Proof. βˆ€ s β‰ˆ t in β„° and each tuple b such that 𝑩 ⟦ s ⟧ b β‰’ 𝑩 ⟦ t ⟧ b, one can compute the congruence ΞΈ = Cg (𝑩 ⟦ s ⟧ b , 𝑩 ⟦ t ⟧ b) generated by 𝑩 ⟦ s ⟧ b and 𝑩 ⟦ t ⟧ b. Let 𝑩₁ := 𝑩 / ΞΈ, and note that | 𝑩₁ | < | 𝑩 |.

We show there exists a bijection from hom 𝑩 𝑨 to hom 𝑩₁ 𝑨. Fix an h : hom 𝑩 𝑨. For all s β‰ˆ t in β„°, we have

h (𝑩 ⟦ s ⟧ b) = 𝑨 ⟦ s ⟧ (h b) = 𝑨 ⟦ t ⟧ (h b) = h (𝑩 ⟦ t ⟧ b).

Therefore, ΞΈ βŠ† ker h, so h factors uniquely as h = h' ∘ Ο€ : 𝑩 β†’ (𝑩 / ΞΈ) β†’ 𝑨, where Ο€ is the canonical projection onto 𝑩 / ΞΈ.

Thus the mapping Ο† : hom 𝑩 𝑨 β†’ hom 𝑩₁ 𝑨 that takes each h to h' such that h = h' ∘ Ο€ is injective. It is also surjective since each g' : 𝑩 / ΞΈ β†’ 𝑨 is mapped back to a g : 𝑩 β†’ 𝑨 such that g = g' ∘ Ο€. Iterating over all identities in β„°, possibly several times, at the final step we obtain a structure 𝑩ₙ that satisfies β„° and is such that ∣ hom 𝑩 𝑨 ∣ = ∣ hom 𝑩ₙ 𝑨 ∣. Moreover, since the number of elements in the intermediate structures decreases at each step, | π‘©α΅’β‚Šβ‚ | < | 𝑩ᡒ |, the process finishes in time that is bounded by a polynomial in the size of 𝑩.

record _⇛_β‡š_ (𝑩 𝑨 π‘ͺ : structure 𝐹 𝑅) : Type β„“β‚€ where
 field
  to   : hom 𝑩 𝑨 β†’ hom π‘ͺ 𝑨
  from : hom π‘ͺ 𝑨 β†’ hom 𝑩 𝑨
  to∼from : βˆ€ h β†’ (to ∘ from) h ≑ h
  from∼to : βˆ€ h β†’ (from ∘ to) h ≑ h

 -- TODO: formalize Lemma III.1
 -- module _ {Ο‡ : Level}{X : Type Ο‡}
 --          {𝑨 : structure 𝐹 𝑅 {β„“β‚€} {β„“β‚€}} where
 -- LEMMAIII1 : {n : β„•}(β„° : Fin n β†’ (Term X Γ— Term X))(𝑨 ∈ fMod β„°)
 --  β†’          βˆ€(𝑩 : structure 𝐹 𝑅) β†’ Ξ£[ π‘ͺ ∈ structure 𝐹 𝑅 ] (π‘ͺ ∈ fMod β„° Γ— (𝑩 ⇛ 𝑨 β‡š π‘ͺ))
 -- LEMMAIII1 β„° π‘¨βŠ§β„° 𝑩 = {!!} , {!!}

← Structures.Graphs Structures.Products β†’