↑ Top


Examples of Structures

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

module Examples.Structures.Basic where

open import Agda.Primitive                  using ( Level ) renaming ( Set to Type ; lzero to ℓ₀ )
open import Data.Product                    using ( _,_ ; _×_  )
open import Relation.Unary                  using ( Pred ; _∈_ )

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

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

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

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 (𝟚 × 𝟚 × 𝟚) ℓ₀ 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
                 }