Complexity and csp definitions (and theorems... soon)

UniversalAlgebra/Complexity.lagda

@@ -0,0 +1,25 @@
+---
+layout: default
+title : Complexity module (The Agda Universal Algebra Library)
+date : 2021-07-13
+author: [agda-algebras development team][]
+---
+
+## Complexity Theory
+
+\begin{code}
+
+{-# OPTIONS --without-K --exact-split --safe #-}
+
+module Complexity where
+
+open import Complexity.Basic
+open import Complexity.CSP
+open import Complexity.FiniteCSP
+
+\end{code}
+
+
+--------------------------------
+
+[agda-algebras development team]: https://github.com/ualib/agda-algebras#the-agda-algebras-development-team

UniversalAlgebra/Complexity/CSP.lagda

@@ -1,7 +1,7 @@
 ---
 layout: default
 title : Complexity.CSP module (The Agda Universal Algebra Library)
-date : 2021-07-13
+date : 2021-07-14
 author: [agda-algebras development team][]
 ---
 
@@ -15,67 +15,83 @@ module Complexity.CSP where
 
 open import Agda.Primitive         using    ( _⊔_ ; lsuc ; Level)
                                    renaming ( Set to Type )
-open import Data.Nat.Base          using    ( ℕ )
-open import Data.Fin.Base          using    ( Fin )
+open import Function.Base          using    ( _∘_ )
 open import Relation.Unary         using    ( _∈_; Pred   )
 
 open import Relations.Continuous   using    ( Rel )
 
 \end{code}
 
-#### Finite CSP
+#### Constraints
 
-An instance of a (finite) constraint satisfaction problem is a triple 𝑃 = (𝑉, 𝐷, 𝐶) where
+A constraint c consists of
 
-* 𝑉 is a finite set of variables,
-* 𝐷 is a finite domain,
-* 𝐶 is a finite list of constraints, where
-  each constraint is a pair 𝐶 = (𝑥, 𝑅) in which
-  * 𝑥 is a tuple of variables of length 𝑛, called the scope of 𝐶, and
-  * 𝑅 is an 𝑛-ary relation on 𝐷, called the constraint relation of 𝐶.
+ 1. a scope function,  s : I → var, and
 
-\begin{code}
+ 2. a constraint relation, i.e., a predicate over the function type I → D
+
+        I ···> var
+         .     .
+          .   .
+           ⌟ ⌞
+            D
 
-private variable χ ρ : Level
 
-record Constraint (∣V∣ ∣D∣ : ℕ) : Type (lsuc (χ ⊔ ρ)) where
- field
-  scope : Fin ∣V∣ → Type χ -- a subset of Fin ∣V∣
+The *scope* of a constraint is an indexed subset of the set of variable symbols.
+We could define a type for this, e.g.,
 
-  relation : ((v : Fin ∣V∣ ) → v ∈ scope → Fin ∣D∣) → Type ρ
-  -- a subset of "tuples" (i.e., functions 𝑓 : scope → Fin ∣D∣)
+```
+ Scope : Type ν → Type ι → _
+ Scope V I = I → V
+```
 
- -- An assignment 𝑓 : 𝑉 → 𝐷 of values in the domain to variables in 𝑉
- -- *satisfies* the constraint 𝐶 = (𝑥, 𝑅) if 𝑓 ↾ 𝑥 ∈ 𝑅.
- satisfies : (Fin ∣V∣ → Fin ∣D∣) → Type ρ
- satisfies f = (λ v _ → f v) ∈ relation
+but we omit this definition because it's so simple; to reiterate,
+a scope of "arity" I on "variables" V is simply a map from I to V,
+where,
 
+* I denotes the "number" of variables involved in the scope
+* V denotes a collection (type) of "variable symbols"
+
+\begin{code}
 
-open Constraint
+module _ -- levels for...
+         {ι : Level} -- ...arity (or argument index) types
+         {ν : Level} -- ...variable symbol types
+         {δ : Level} -- ... domain types
+         -- {ρ : Level} -- ... relation types
+         where
 
-record CSP : Type (lsuc (χ ⊔ ρ)) where
- field
-  ∣V∣ -- # of variables,
-   ∣D∣ -- # of elements in the domain,
-    ∣C∣ -- # of constraints (resp.)
-       : ℕ
-  𝐶    : Fin ∣C∣ → Constraint{χ} ∣V∣ ∣D∣
+ record Constraint (var : Type ν)(dom : Type δ){ρ : Level} : Type (ν ⊔ δ ⊔ lsuc (ι ⊔ ρ)) where
+  field
+   arity  : Type ι               -- The "number" of variables involved in the constraint.
+   scope  : arity → var          -- Which variables are involved in the constraint.
+   rel    : Rel dom arity {ρ}    -- The constraint relation.
 
- -- An assignment 𝑓 *solves* the instance 𝑃 if it satisfies all the constraints.
- isSolution : (Fin ∣V∣ → Fin ∣D∣) → Type ρ
- isSolution f = ∀ i → (satisfies (𝐶 i)) f
+  satisfies : (var → dom) → Type ρ  -- An assignment 𝑓 : var → dom of values to variables
+  satisfies f = f ∘ scope ∈ rel     -- *satisfies* the constraint 𝐶 = (σ , 𝑅) provided
+                                    -- 𝑓 ∘ σ ∈ 𝑅, where σ is the scope of the constraint.
 
 \end{code}
 
+#### CSP Instances
 
+An instance of a constraint satisfaction problem is a triple 𝑃 = (𝑉, 𝐷, 𝐶) where
 
-#### References
+* 𝑉 denotes a set of "variables"
+* 𝐷 denotes a "domain",
+* 𝐶 denotes an indexed collection of constraints.
 
-Some of the informal (i.e., non-agda) material in this module is similar to that presented in
+\begin{code}
+
+ record CSPInstance  (var : Type ν)(dom : Type δ){ρ : Level} : Type (ν ⊔ δ ⊔ lsuc (ι ⊔ ρ)) where
+  field
+   arity : Type ι                         -- The "number" of constraints of the instance.
+   cs    : arity → Constraint var dom {ρ} -- The constraints of the instance.
 
-* Ross Willard's slides: [Constraint Satisfaction Problems: a Survey](http://www.math.uwaterloo.ca/~rdwillar/documents/Slides/willard-boulder2016-rev2.pdf)
+  isSolution : (var → dom) → Type (ι ⊔ ρ)               -- An assignment *solves* the instance
+  isSolution f = ∀ i → (Constraint.satisfies (cs i)) f  -- if it satisfies all the constraints.
 
-* [Polymorphisms, and How to Use Them](https://drops.dagstuhl.de/opus/volltexte/2017/6959/pdf/DFU-Vol7-15301-1.pdf
+\end{code}
 
 
 

UniversalAlgebra/Complexity/FiniteCSP.lagda

@@ -0,0 +1,90 @@
+---
+layout: default
+title : Complexity.FiniteCSP module (The Agda Universal Algebra Library)
+date : 2021-07-14
+author: [agda-algebras development team][]
+---
+
+### Constraint Satisfaction Problems
+
+\begin{code}
+
+{-# OPTIONS --without-K --exact-split --safe #-}
+
+module Complexity.FiniteCSP where
+
+open import Agda.Primitive         using    ( _⊔_ ; lsuc ; Level)
+                                   renaming ( Set to Type )
+open import Data.Product           using    ( _,_ ; Σ ; Σ-syntax )
+open import Data.Nat.Base          using    ( ℕ )
+open import Data.Fin.Base          using    ( Fin )
+open import Function.Base          using    ( _∘_ )
+open import Relation.Unary         using    ( _∈_; Pred   )
+
+open import Relations.Continuous   using    ( Rel )
+open import Algebras.Basic         using    ( Signature )
+
+\end{code}
+
+
+#### Finite CSP
+
+An instance of a (finite) constraint satisfaction problem is a triple 𝑃 = (𝑉, 𝐷, 𝐶) where
+
+* 𝑉 is a finite set of variables,
+* 𝐷 is a finite domain,
+* 𝐶 is a finite list of constraints, where
+  each constraint is a pair 𝐶 = (𝑥, 𝑅) in which
+  * 𝑥 is a tuple of variables of length 𝑛, called the scope of 𝐶, and
+  * 𝑅 is an 𝑛-ary relation on 𝐷, called the constraint relation of 𝐶.
+
+\begin{code}
+
+private variable χ ρ : Level
+
+record Constraint (∣V∣ ∣D∣ : ℕ) : Type (lsuc (χ ⊔ ρ)) where
+ field
+  scope : Fin ∣V∣ → Type χ -- a subset of Fin ∣V∣
+
+  relation : ((v : Fin ∣V∣ ) → v ∈ scope → Fin ∣D∣) → Type ρ
+  -- a subset of "tuples" (i.e., functions 𝑓 : scope → Fin ∣D∣)
+
+ -- An assignment 𝑓 : 𝑉 → 𝐷 of values in the domain to variables in 𝑉
+ -- *satisfies* the constraint 𝐶 = (𝑥, 𝑅) if 𝑓 ↾ 𝑥 ∈ 𝑅.
+ satisfies : (Fin ∣V∣ → Fin ∣D∣) → Type ρ
+ satisfies f = (λ v _ → f v) ∈ relation
+
+
+open Constraint
+
+record CSPInstance : Type (lsuc (χ ⊔ ρ)) where
+ field
+  ∣V∣ -- # of variables,
+   ∣D∣ -- # of elements in the domain,
+    ∣C∣ -- # of constraints (resp.)
+       : ℕ
+  𝐶    : Fin ∣C∣ → Constraint{χ} ∣V∣ ∣D∣
+
+ -- An assignment 𝑓 *solves* the instance 𝑃 if it satisfies all the constraints.
+ isSolution : (Fin ∣V∣ → Fin ∣D∣) → Type ρ
+ isSolution f = ∀ i → (satisfies (𝐶 i)) f
+
+\end{code}
+
+
+
+#### References
+
+Some of the informal (i.e., non-agda) material in this module is similar to that presented in
+
+* Ross Willard's slides: [Constraint Satisfaction Problems: a Survey](http://www.math.uwaterloo.ca/~rdwillar/documents/Slides/willard-boulder2016-rev2.pdf)
+
+* [Polymorphisms, and How to Use Them](https://drops.dagstuhl.de/opus/volltexte/2017/6959/pdf/DFU-Vol7-15301-1.pdf
+
+
+
+--------------------------------------
+
+[agda-algebras development team]: https://github.com/ualib/agda-algebras#the-agda-algebras-development-team
+
+

UniversalAlgebra/agda-algebras-everything.lagda

@@ -69,6 +69,12 @@ open import ClosureSystems.Basic            using    ( ∅ ; 𝒞𝓁 ; ClOp )
 open import ClosureSystems.Properties       using    ( clop→law⇒ ; clop→law⇐ ; clop←law )
 
 
+-- Complexity ----------------------------------------------------------------------------------------
+
+open import Complexity.CSP                  using    ( Constraint ; CSPInstance )
+
+open import Complexity.FiniteCSP            using    ( Constraint ; CSPInstance )
+
 -- ALGEBRAS ------------------------------------------------------------------------------------------
 
 open import Algebras.Basic                  using    ( Signature ; signature ; monoid-op ; monoid-sig