Examples.Structures.Basic

Examples of Structures

This is the Examples.Structures.Basic module of the Agda Universal Algebra Library.

Two tiny worked examples of the general structure type of the frozen Legacy.Base tree, which packages operation symbols and relation symbols in one signature pair: a purely algebraic structure and a purely relational one. The signatures come from Examples.Structures.Signatures.

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

module Examples.Structures.Basic where

open import Level                           using ( 0ℓ )
open import Data.Product                    using ( _,_ ; _×_  )
open import Relation.Unary                  using ( Pred ; _∈_ )

open import Overture                        using ( 𝟚 ; 𝟛 )
open import Legacy.Base.Structures          using ( structure )
open import Examples.Structures.Signatures  using ( S001 ; S∅ ; S0001 )

SL is a three-element meet semilattice presented as a structure with one binary operation symbol (S001) and no relation symbols (S∅). The meet of two distinct elements is 𝟎, so the induced order has bottom 𝟎 below the incomparable pair 𝟏, 𝟐.

-- An example of a (purely) algebraic structure is a 3-element meet semilattice.

SL : structure  S001   -- (one binary operation symbol)
                S∅     -- (no relation symbols)
                {ρ = 0ℓ}

SL = record { carrier = 𝟛
            ; op = λ _ x → meet (x 𝟚.𝟎) (x 𝟚.𝟏)
            ; rel = λ ()
            } where
              meet : 𝟛 → 𝟛 → 𝟛
              meet 𝟛.𝟎 𝟛.𝟎 = 𝟛.𝟎
              meet 𝟛.𝟎 𝟛.𝟏 = 𝟛.𝟎
              meet 𝟛.𝟎 𝟛.𝟐 = 𝟛.𝟎
              meet 𝟛.𝟏 𝟛.𝟎 = 𝟛.𝟎
              meet 𝟛.𝟏 𝟛.𝟏 = 𝟛.𝟏
              meet 𝟛.𝟏 𝟛.𝟐 = 𝟛.𝟎
              meet 𝟛.𝟐 𝟛.𝟎 = 𝟛.𝟎
              meet 𝟛.𝟐 𝟛.𝟏 = 𝟛.𝟎
              meet 𝟛.𝟐 𝟛.𝟐 = 𝟛.𝟐

An example of a (purely) relational structure is the 2 element structure with the ternary NAE-3-SAT relation, R = S³ - {(0,0,0), (1,1,1)} (where S = {0, 1}).

data NAE3SAT : Pred (𝟚 × 𝟚 × 𝟚) 0ℓ where
  r1 : (𝟚.𝟎 , 𝟚.𝟎 , 𝟚.𝟏) ∈ NAE3SAT
  r2 : (𝟚.𝟎 , 𝟚.𝟏 , 𝟚.𝟎) ∈ NAE3SAT
  r3 : (𝟚.𝟎 , 𝟚.𝟏 , 𝟚.𝟏) ∈ NAE3SAT
  r4 : (𝟚.𝟏 , 𝟚.𝟎 , 𝟚.𝟎) ∈ NAE3SAT
  r5 : (𝟚.𝟏 , 𝟚.𝟎 , 𝟚.𝟏) ∈ NAE3SAT
  r6 : (𝟚.𝟏 , 𝟚.𝟏 , 𝟚.𝟎) ∈ NAE3SAT

nae3sat : structure S∅    -- (no operation symbols)
                    S0001 -- (one ternary relation symbol)

nae3sat = record { carrier = 𝟚
                 ; op = λ ()
                 ; rel = λ _ x → ((x 𝟛.𝟎) , (x 𝟛.𝟏) , (x 𝟛.𝟐)) ∈ NAE3SAT
                 }