From 91bc16d54ec0a6e5d904673951fe091a9973d9b4 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 18 Jan 2022 22:01:46 +0000 Subject: Define the semantics of pseudocode data types. --- src/Helium/Algebra/Decidable/Bundles.agda | 108 +++++++++++++++++++++ .../Algebra/Decidable/Construct/Pointwise.agda | 93 ++++++++++++++++++ src/Helium/Algebra/Decidable/Structures.agda | 87 +++++++++++++++++ 3 files changed, 288 insertions(+) create mode 100644 src/Helium/Algebra/Decidable/Bundles.agda create mode 100644 src/Helium/Algebra/Decidable/Construct/Pointwise.agda create mode 100644 src/Helium/Algebra/Decidable/Structures.agda (limited to 'src/Helium/Algebra/Decidable') diff --git a/src/Helium/Algebra/Decidable/Bundles.agda b/src/Helium/Algebra/Decidable/Bundles.agda new file mode 100644 index 0000000..e446706 --- /dev/null +++ b/src/Helium/Algebra/Decidable/Bundles.agda @@ -0,0 +1,108 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Definitions of decidable algebraic structures like monoids and rings +-- (packed in records together with sets, operations, etc.) +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Helium.Algebra.Decidable.Bundles where + +open import Algebra.Bundles using (RawLattice) +open import Algebra.Core +open import Helium.Algebra.Decidable.Structures +open import Level using (suc; _⊔_) +open import Relation.Binary.Bundles using (DecSetoid) +open import Relation.Binary.Core using (Rel) + +record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where + infixr 7 _∧_ + infixr 6 _∨_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∨_ : Op₂ Carrier + _∧_ : Op₂ Carrier + isLattice : IsLattice _≈_ _∨_ _∧_ + + open IsLattice isLattice public + + rawLattice : RawLattice c ℓ + rawLattice = record + { _≈_ = _≈_ + ; _∧_ = _∧_ + ; _∨_ = _∨_ + } + + open RawLattice rawLattice public + using (∨-rawMagma; ∧-rawMagma) + + decSetoid : DecSetoid _ _ + decSetoid = record { isDecEquivalence = isDecEquivalence } + + open DecSetoid decSetoid public + using (_≉_; setoid) + +record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where + infixr 7 _∧_ + infixr 6 _∨_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∨_ : Op₂ Carrier + _∧_ : Op₂ Carrier + isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_ + + open IsDistributiveLattice isDistributiveLattice public + + lattice : Lattice _ _ + lattice = record { isLattice = isLattice } + + open Lattice lattice public + using (_≉_; setoid; decSetoid; ∨-rawMagma; ∧-rawMagma; rawLattice) + +record RawBooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where + infix 8 ¬_ + infixr 7 _∧_ + infixr 6 _∨_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∧_ : Op₂ Carrier + _∨_ : Op₂ Carrier + ¬_ : Op₁ Carrier + ⊤ : Carrier + ⊥ : Carrier + + rawLattice : RawLattice c ℓ + rawLattice = record { _≈_ = _≈_; _∨_ = _∨_; _∧_ = _∧_ } + + open RawLattice rawLattice public + using (_≉_; ∨-rawMagma; ∧-rawMagma) + +record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where + infix 8 ¬_ + infixr 7 _∧_ + infixr 6 _∨_ + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _∨_ : Op₂ Carrier + _∧_ : Op₂ Carrier + ¬_ : Op₁ Carrier + ⊤ : Carrier + ⊥ : Carrier + isBooleanAlgebra : IsBooleanAlgebra _≈_ _∨_ _∧_ ¬_ ⊤ ⊥ + + open IsBooleanAlgebra isBooleanAlgebra public + + distributiveLattice : DistributiveLattice _ _ + distributiveLattice = record { isDistributiveLattice = isDistributiveLattice } + + open DistributiveLattice distributiveLattice public + using (_≉_; setoid; decSetoid; ∨-rawMagma; ∧-rawMagma; rawLattice; lattice) diff --git a/src/Helium/Algebra/Decidable/Construct/Pointwise.agda b/src/Helium/Algebra/Decidable/Construct/Pointwise.agda new file mode 100644 index 0000000..9f067ba --- /dev/null +++ b/src/Helium/Algebra/Decidable/Construct/Pointwise.agda @@ -0,0 +1,93 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Construct algebras of vectors in a pointwise manner +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +module Helium.Algebra.Decidable.Construct.Pointwise where + +open import Algebra.Bundles using (RawLattice) +open import Algebra.Core +open import Data.Nat using (ℕ) +open import Data.Product using (_,_) +open import Data.Vec.Functional using (replicate; map; zipWith) +open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise) +import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as Pwₚ +open import Function using (_$_) +open import Helium.Algebra.Decidable.Bundles +open import Helium.Algebra.Decidable.Structures +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Core using (Rel) + +module _ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} where + private + _≋_ = Pointwise _≈_ + + module _ {∨ ∧ : Op₂ A} where + isLattice : IsLattice _≈_ ∨ ∧ → ∀ n → IsLattice (_≋_ {n}) (zipWith ∨) (zipWith ∧) + isLattice L n = record + { isDecEquivalence = Pwₚ.isDecEquivalence isDecEquivalence n + ; ∨-comm = λ x y i → ∨-comm (x i) (y i) + ; ∨-assoc = λ x y z i → ∨-assoc (x i) (y i) (z i) + ; ∨-cong = λ x≈y u≈v i → ∨-cong (x≈y i) (u≈v i) + ; ∧-comm = λ x y i → ∧-comm (x i) (y i) + ; ∧-assoc = λ x y z i → ∧-assoc (x i) (y i) (z i) + ; ∧-cong = λ x≈y u≈v i → ∧-cong (x≈y i) (u≈v i) + ; absorptive = (λ x y i → ∨-absorbs-∧ (x i) (y i)) + , (λ x y i → ∧-absorbs-∨ (x i) (y i)) + } + where open IsLattice L + + isDistributiveLattice : IsDistributiveLattice _≈_ ∨ ∧ → ∀ n → IsDistributiveLattice (_≋_ {n}) (zipWith ∨) (zipWith ∧) + isDistributiveLattice L n = record + { isLattice = isLattice L.isLattice n + ; ∨-distrib-∧ = (λ x y z i → L.∨-distribˡ-∧ (x i) (y i) (z i)) + , (λ x y z i → L.∨-distribʳ-∧ (x i) (y i) (z i)) + } + where module L = IsDistributiveLattice L + + module _ {∨ ∧ : Op₂ A} {¬ : Op₁ A} {⊤ ⊥ : A} where + isBooleanAlgebra : IsBooleanAlgebra _≈_ ∨ ∧ ¬ ⊤ ⊥ → ∀ n → IsBooleanAlgebra (_≋_ {n}) (zipWith ∨) (zipWith ∧) (map ¬) (replicate ⊤) (replicate ⊥) + isBooleanAlgebra B n = record + { isDistributiveLattice = isDistributiveLattice B.isDistributiveLattice n + ; ∨-complement = (λ x i → B.∨-complementˡ (x i)) + , (λ x i → B.∨-complementʳ (x i)) + ; ∧-complement = (λ x i → B.∧-complementˡ (x i)) + , (λ x i → B.∧-complementʳ (x i)) + ; ¬-cong = λ x≈y i → B.¬-cong (x≈y i) + } + where module B = IsBooleanAlgebra B + +rawLattice : ∀ {a ℓ} → RawLattice a ℓ → ℕ → RawLattice a ℓ +rawLattice L n = record + { _≈_ = Pointwise _≈_ {n} + ; _∧_ = zipWith _∧_ + ; _∨_ = zipWith _∨_ + } + where open RawLattice L + +lattice : ∀ {a ℓ} → Lattice a ℓ → ℕ → Lattice a ℓ +lattice L n = record { isLattice = isLattice (Lattice.isLattice L) n } + +distributiveLattice : ∀ {a ℓ} → DistributiveLattice a ℓ → ℕ → DistributiveLattice a ℓ +distributiveLattice L n = record + { isDistributiveLattice = + isDistributiveLattice (DistributiveLattice.isDistributiveLattice L) n + } + +rawBooleanAlgebra : ∀ {a ℓ} → RawBooleanAlgebra a ℓ → ℕ → RawBooleanAlgebra a ℓ +rawBooleanAlgebra B n = record + { _≈_ = Pointwise _≈_ {n} + ; _∧_ = zipWith _∧_ + ; _∨_ = zipWith _∨_ + ; ¬_ = map ¬_ + ; ⊤ = replicate ⊤ + ; ⊥ = replicate ⊥ + } + where open RawBooleanAlgebra B + +booleanAlgebra : ∀ {a ℓ} → BooleanAlgebra a ℓ → ℕ → BooleanAlgebra a ℓ +booleanAlgebra B n = record + { isBooleanAlgebra = isBooleanAlgebra (BooleanAlgebra.isBooleanAlgebra B) n } diff --git a/src/Helium/Algebra/Decidable/Structures.agda b/src/Helium/Algebra/Decidable/Structures.agda new file mode 100644 index 0000000..4380cc5 --- /dev/null +++ b/src/Helium/Algebra/Decidable/Structures.agda @@ -0,0 +1,87 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Some decidable algebraic structures (not packed up with sets, +-- operations, etc.) +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary.Core using (Rel) + +module Helium.Algebra.Decidable.Structures + {a ℓ} {A : Set a} -- The underlying set + (_≈_ : Rel A ℓ) -- The underlying equality relation + where + +open import Algebra.Core +open import Algebra.Definitions (_≈_) +open import Data.Product using (proj₁; proj₂) +open import Level using (_⊔_) +open import Relation.Binary.Structures using (IsDecEquivalence) + +record IsLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where + field + isDecEquivalence : IsDecEquivalence _≈_ + ∨-comm : Commutative ∨ + ∨-assoc : Associative ∨ + ∨-cong : Congruent₂ ∨ + ∧-comm : Commutative ∧ + ∧-assoc : Associative ∧ + ∧-cong : Congruent₂ ∧ + absorptive : Absorptive ∨ ∧ + + open IsDecEquivalence isDecEquivalence public + + ∨-absorbs-∧ : ∨ Absorbs ∧ + ∨-absorbs-∧ = proj₁ absorptive + + ∧-absorbs-∨ : ∧ Absorbs ∨ + ∧-absorbs-∨ = proj₂ absorptive + + ∧-congˡ : LeftCongruent ∧ + ∧-congˡ y≈z = ∧-cong refl y≈z + + ∧-congʳ : RightCongruent ∧ + ∧-congʳ y≈z = ∧-cong y≈z refl + + ∨-congˡ : LeftCongruent ∨ + ∨-congˡ y≈z = ∨-cong refl y≈z + + ∨-congʳ : RightCongruent ∨ + ∨-congʳ y≈z = ∨-cong y≈z refl + +record IsDistributiveLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where + field + isLattice : IsLattice ∨ ∧ + ∨-distrib-∧ : ∨ DistributesOver ∧ + + open IsLattice isLattice public + + ∨-distribˡ-∧ : ∨ DistributesOverˡ ∧ + ∨-distribˡ-∧ = proj₁ ∨-distrib-∧ + + ∨-distribʳ-∧ : ∨ DistributesOverʳ ∧ + ∨-distribʳ-∧ = proj₂ ∨-distrib-∧ + +record IsBooleanAlgebra + (∨ ∧ : Op₂ A) (¬ : Op₁ A) (⊤ ⊥ : A) : Set (a ⊔ ℓ) where + field + isDistributiveLattice : IsDistributiveLattice ∨ ∧ + ∨-complement : Inverse ⊤ ¬ ∨ + ∧-complement : Inverse ⊥ ¬ ∧ + ¬-cong : Congruent₁ ¬ + + open IsDistributiveLattice isDistributiveLattice public + + ∨-complementˡ : LeftInverse ⊤ ¬ ∨ + ∨-complementˡ = proj₁ ∨-complement + + ∨-complementʳ : RightInverse ⊤ ¬ ∨ + ∨-complementʳ = proj₂ ∨-complement + + ∧-complementˡ : LeftInverse ⊥ ¬ ∧ + ∧-complementˡ = proj₁ ∧-complement + + ∧-complementʳ : RightInverse ⊥ ¬ ∧ + ∧-complementʳ = proj₂ ∧-complement -- cgit v1.2.3