------------------------------------------------------------------------
-- The Agda standard library
--
-- Example of multi-sorted algebras as indexed containers
------------------------------------------------------------------------
{-# OPTIONS --safe --cubical-compatible #-}
module README.Data.Container.Indexed.MultiSortedAlgebraExample where
------------------------------------------------------------------------
-- Preliminaries
------------------------------------------------------------------------
-- We import library content for indexed containers, standard types,
-- and setoids.
open import Level
open import Data.Container.Indexed.Core using (Container; ⟦_⟧; _◃_/_)
open import Data.Container.Indexed.FreeMonad using (_⋆C_)
open import Data.W.Indexed using (W; sup)
open import Data.Product using (Σ; _×_; _,_; Σ-syntax)
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
open import Function using (_∘_)
open import Function.Bundles using (Func)
open import Relation.Binary using (Setoid; IsEquivalence)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
import Data.Container.Indexed.Relation.Binary.Equality.Setoid as ICSetoid
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
open Setoid using (Carrier; _≈_; isEquivalence)
open Func renaming (to to apply)
-- Letter ℓ denotes universe levels.
variable
ℓ ℓ' ℓˢ ℓᵒ ℓᵃ ℓᵐ ℓᵉ ℓⁱ : Level
I : Set ℓⁱ
S : Set ℓˢ
------------------------------------------------------------------------
-- The interpretation of a container (Op ◃ Ar / sort) is
--
-- ⟦ Op ◃ Ar / sort ⟧ X s = Σ[ o ∈ Op s ] ((i : Ar o) → X (sort o i))
--
-- which contains pairs consisting of an operator $o$ and its collection
-- of arguments. The least fixed point of (X ↦ ⟦ C ⟧ X) is the indexed
-- W-type given by C, and it contains closed first-order terms of the
-- multi-sorted algebra C.
-- We need to interpret indexed containers on Setoids.
-- This definition is missing from the standard library v1.7.
⟦_⟧s : (C : Container I S ℓᵒ ℓᵃ) (ξ : I → Setoid ℓᵐ ℓᵉ) → S → Setoid _ _
⟦ C ⟧s ξ = ICSetoid.setoid ξ C
------------------------------------------------------------------------
-- Multi-sorted algebras
--------------------------------------------------------------------------
-- A multi-sorted algebra is an indexed container.
--
-- * Sorts are indexes.
--
-- * Operators are commands/shapes.
--
-- * Arities/argument are responses/positions.
--
-- Closed terms (initial model) are given by the W type for a container,
-- renamed to μ here (for least fixed-point).
-- We assume a fixed signature (Sort, Ops).
module _ (Sort : Set ℓˢ) (Ops : Container Sort Sort ℓᵒ ℓᵃ) where
open Container Ops renaming
( Command to Op
; Response to Arity
; next to sort
)
-- We let letter $s$ range over sorts and $\mathit{op}$ over operators.
variable
s s' : Sort
op op' : Op s
------------------------------------------------------------------------
-- Models
-- A model is given by an interpretation (Den $s$) for each sort $s$
-- plus an interpretation (den $o$) for each operator $o$.
record SetModel ℓᵐ : Set (ℓˢ ⊔ ℓᵒ ⊔ ℓᵃ ⊔ suc ℓᵐ) where
field
Den : Sort → Set ℓᵐ
den : {s : Sort} → ⟦ Ops ⟧ Den s → Den s
-- The setoid model requires operators to respect equality.
-- The Func record packs a function (apply) with a proof (cong)
-- that the function maps equals to equals.
record SetoidModel ℓᵐ ℓᵉ : Set (ℓˢ ⊔ ℓᵒ ⊔ ℓᵃ ⊔ suc (ℓᵐ ⊔ ℓᵉ)) where
field
Den : Sort → Setoid ℓᵐ ℓᵉ
den : {s : Sort} → Func (⟦ Ops ⟧s Den s) (Den s)
------------------------------------------------------------------------
-- Terms
-- To obtain terms with free variables, we add additional nullary
-- operators, each representing a variable.
--
-- These are covered in the standard library FreeMonad module,
-- albeit with the restriction that the operator and variable sets
-- have the same size.
Cxt = Sort → Set ℓᵒ
variable
Γ Δ : Cxt
-- Terms with free variables in Var.
module _ (Var : Cxt) where
-- We keep the same sorts, but add a nullary operator for each variable.
Ops⁺ : Container Sort Sort ℓᵒ ℓᵃ
Ops⁺ = Ops ⋆C Var
-- Terms with variables are then given by the W-type for the extended container.
Tm = W Ops⁺
-- We define nice constructors for variables and operator application
-- via pattern synonyms.
-- Note that the $f$ in constructor var' is a function from the empty set,
-- so it should be uniquely determined. However, Agda's equality is
-- more intensional and will not identify all functions from the empty set.
-- Since we do not make use of the axiom of function extensionality,
-- we sometimes have to consult the extensional equality of the
-- function setoid.
pattern _∙_ op args = sup (inj₂ op , args)
pattern var' x f = sup (inj₁ x , f )
pattern var x = var' x _
-- Letter $t$ ranges over terms, and $\mathit{ts}$ over argument vectors.
variable
t t' t₁ t₂ t₃ : Tm Γ s
ts ts' : (i : Arity op) → Tm Γ (sort _ i)
------------------------------------------------------------------------
-- Parallel substitutions
-- A substitution from Δ to Γ holds a term in Γ for each variable in Δ.
Sub : (Γ Δ : Cxt) → Set _
Sub Γ Δ = ∀{s} (x : Δ s) → Tm Γ s
-- Application of a substitution.
_[_] : (t : Tm Δ s) (σ : Sub Γ Δ) → Tm Γ s
(var x ) [ σ ] = σ x
(op ∙ ts) [ σ ] = op ∙ λ i → ts i [ σ ]
-- Letter $σ$ ranges over substitutions.
variable
σ σ' : Sub Γ Δ
------------------------------------------------------------------------
-- Interpretation of terms in a model
------------------------------------------------------------------------
-- Given an algebra $M$ of set-size $ℓ^m$ and equality-size $ℓ^e$,
-- we define the interpretation of an $s$-sorted term $t$ as element
-- of $M(s)$ according to an environment $ρ$ that maps each variable
-- of sort $s'$ to an element of $M(s')$.
module _ {M : SetoidModel ℓᵐ ℓᵉ} where
open SetoidModel M
-- Equality in $M$'s interpretation of sort $s$.
_≃_ : Den s .Carrier → Den s .Carrier → Set _
_≃_ {s = s} = Den s ._≈_
-- An environment for Γ maps each variable $x : Γ(s)$ to an element of $M(s)$.
-- Equality of environments is defined pointwise.
Env : Cxt → Setoid _ _
Env Γ .Carrier = {s : Sort} (x : Γ s) → Den s .Carrier
Env Γ ._≈_ ρ ρ' = {s : Sort} (x : Γ s) → ρ x ≃ ρ' x
Env Γ .isEquivalence .IsEquivalence.refl {s = s} x = Den s .Setoid.refl
Env Γ .isEquivalence .IsEquivalence.sym h {s} x = Den s .Setoid.sym (h x)
Env Γ .isEquivalence .IsEquivalence.trans g h {s} x = Den s .Setoid.trans (g x) (h x)
-- Interpretation of terms is iteration on the W-type.
-- The standard library offers `iter' (on sets), but we need this to be a Func (on setoids).
⦅_⦆ : ∀{s} (t : Tm Γ s) → Func (Env Γ) (Den s)
⦅ var x ⦆ .apply ρ = ρ x
⦅ var x ⦆ .cong ρ=ρ' = ρ=ρ' x
⦅ op ∙ args ⦆ .apply ρ = den .apply (op , λ i → ⦅ args i ⦆ .apply ρ)
⦅ op ∙ args ⦆ .cong ρ=ρ' = den .cong (refl , λ i → ⦅ args i ⦆ .cong ρ=ρ')
-- An equality between two terms holds in a model
-- if the two terms are equal under all valuations of their free variables.
Equal : ∀ {Γ s} (t t' : Tm Γ s) → Set _
Equal {Γ} {s} t t' = ∀ (ρ : Env Γ .Carrier) → ⦅ t ⦆ .apply ρ ≃ ⦅ t' ⦆ .apply ρ
-- This notion is an equivalence relation.
isEquiv : IsEquivalence (Equal {Γ = Γ} {s = s})
isEquiv {s = s} .IsEquivalence.refl ρ = Den s .Setoid.refl
isEquiv {s = s} .IsEquivalence.sym e ρ = Den s .Setoid.sym (e ρ)
isEquiv {s = s} .IsEquivalence.trans e e' ρ = Den s .Setoid.trans (e ρ) (e' ρ)
------------------------------------------------------------------------
-- Substitution lemma
-- Evaluation of a substitution gives an environment.
⦅_⦆s : Sub Γ Δ → Env Γ .Carrier → Env Δ .Carrier
⦅ σ ⦆s ρ x = ⦅ σ x ⦆ .apply ρ
-- Substitution lemma: ⦅t[σ]⦆ρ ≃ ⦅t⦆⦅σ⦆ρ
substitution : (t : Tm Δ s) (σ : Sub Γ Δ) (ρ : Env Γ .Carrier) →
⦅ t [ σ ] ⦆ .apply ρ ≃ ⦅ t ⦆ .apply (⦅ σ ⦆s ρ)
substitution (var x) σ ρ = Den _ .Setoid.refl
substitution (op ∙ ts) σ ρ = den .cong (refl , λ i → substitution (ts i) σ ρ)
------------------------------------------------------------------------
-- Equations
-- An equation is a pair $t ≐ t'$ of terms of the same sort in the same context.
record Eq : Set (ℓˢ ⊔ suc ℓᵒ ⊔ ℓᵃ) where
constructor _≐_
field
{cxt} : Sort → Set ℓᵒ
{srt} : Sort
lhs : Tm cxt srt
rhs : Tm cxt srt
-- Equation $t ≐ t'$ holding in model $M$.
_⊧_ : (M : SetoidModel ℓᵐ ℓᵉ) (eq : Eq) → Set _
M ⊧ (t ≐ t') = Equal {M = M} t t'
-- Sets of equations are presented as collection E : I → Eq
-- for some index set I : Set ℓⁱ.
-- An entailment/consequence $E ⊃ t ≐ t'$ is valid
-- if $t ≐ t'$ holds in all models that satify equations $E$.
module _ {ℓᵐ ℓᵉ} where
_⊃_ : (E : I → Eq) (eq : Eq) → Set _
E ⊃ eq = ∀ (M : SetoidModel ℓᵐ ℓᵉ) → (∀ i → M ⊧ E i) → M ⊧ eq
-- Derivations
--------------
-- Equalitional logic allows us to prove entailments via the
-- inference rules for the judgment $E ⊢ Γ ▹ t ≡ t'$.
-- This could be coined as equational theory over a given
-- set of equations $E$.
-- Relation $E ⊢ Γ ▹ \_ ≡ \_$ is the least congruence over the equations $E$.
data _⊢_▹_≡_ {I : Set ℓⁱ}
(E : I → Eq) : (Γ : Cxt) (t t' : Tm Γ s) → Set (ℓˢ ⊔ suc ℓᵒ ⊔ ℓᵃ ⊔ ℓⁱ) where
hyp : ∀ i → let t ≐ t' = E i in
E ⊢ _ ▹ t ≡ t'
base : ∀ (x : Γ s) {f f' : (i : ⊥) → Tm _ (⊥-elim i)} →
E ⊢ Γ ▹ var' x f ≡ var' x f'
app : (∀ i → E ⊢ Γ ▹ ts i ≡ ts' i) →
E ⊢ Γ ▹ (op ∙ ts) ≡ (op ∙ ts')
sub : E ⊢ Δ ▹ t ≡ t' →
∀ (σ : Sub Γ Δ) →
E ⊢ Γ ▹ (t [ σ ]) ≡ (t' [ σ ])
refl : ∀ (t : Tm Γ s) →
E ⊢ Γ ▹ t ≡ t
sym : E ⊢ Γ ▹ t ≡ t' →
E ⊢ Γ ▹ t' ≡ t
trans : E ⊢ Γ ▹ t₁ ≡ t₂ →
E ⊢ Γ ▹ t₂ ≡ t₃ →
E ⊢ Γ ▹ t₁ ≡ t₃
------------------------------------------------------------------------
-- Soundness of the inference rules
-- We assume a model $M$ that validates all equations in $E$.
module Soundness {I : Set ℓⁱ} (E : I → Eq) (M : SetoidModel ℓᵐ ℓᵉ)
(V : ∀ i → M ⊧ E i) where
open SetoidModel M
-- In any model $M$ that satisfies the equations $E$,
-- derived equality is actual equality.
sound : E ⊢ Γ ▹ t ≡ t' → M ⊧ (t ≐ t')
sound (hyp i) = V i
sound (app {op = op} es) ρ = den .cong (refl , λ i → sound (es i) ρ)
sound (sub {t = t} {t' = t'} e σ) ρ = begin
⦅ t [ σ ] ⦆ .apply ρ ≈⟨ substitution {M = M} t σ ρ ⟩
⦅ t ⦆ .apply ρ' ≈⟨ sound e ρ' ⟩
⦅ t' ⦆ .apply ρ' ≈⟨ substitution {M = M} t' σ ρ ⟨
⦅ t' [ σ ] ⦆ .apply ρ ∎
where
open SetoidReasoning (Den _)
ρ' = ⦅ σ ⦆s ρ
sound (base x {f} {f'}) = isEquiv {M = M} .IsEquivalence.refl {var' x λ()}
sound (refl t) = isEquiv {M = M} .IsEquivalence.refl {t}
sound (sym {t = t} {t' = t'} e) = isEquiv {M = M} .IsEquivalence.sym
{x = t} {y = t'} (sound e)
sound (trans {t₁ = t₁} {t₂ = t₂}
{t₃ = t₃} e e') = isEquiv {M = M} .IsEquivalence.trans
{i = t₁} {j = t₂} {k = t₃} (sound e) (sound e')
------------------------------------------------------------------------
-- Birkhoff's completeness theorem
------------------------------------------------------------------------
-- Birkhoff proved that any equation $t ≐ t'$ is derivable from $E$
-- when it is valid in all models satisfying $E$. His proof (for
-- single-sorted algebras) is a blue print for many more
-- completeness proofs. They all proceed by constructing a
-- universal model aka term model. In our case, it is terms
-- quotiented by derivable equality $E ⊢ Γ ▹ \_ ≡ \_$. It then
-- suffices to prove that this model satisfies all equations in $E$.
------------------------------------------------------------------------
-- Universal model
-- A term model for $E$ and $Γ$ interprets sort $s$ by (Tm Γ s) quotiented by $E ⊢ Γ ▹ \_ ≡ \_$.
module TermModel {I : Set ℓⁱ} (E : I → Eq) where
open SetoidModel
-- Tm Γ s quotiented by E⊢Γ▹·≡·.
TmSetoid : Cxt → Sort → Setoid _ _
TmSetoid Γ s .Carrier = Tm Γ s
TmSetoid Γ s ._≈_ = E ⊢ Γ ▹_≡_
TmSetoid Γ s .isEquivalence .IsEquivalence.refl = refl _
TmSetoid Γ s .isEquivalence .IsEquivalence.sym = sym
TmSetoid Γ s .isEquivalence .IsEquivalence.trans = trans
-- The interpretation of an operator is simply the operator.
-- This works because $E⊢Γ▹\_≡\_$ is a congruence.
tmInterp : ∀ {Γ s} → Func (⟦ Ops ⟧s (TmSetoid Γ) s) (TmSetoid Γ s)
tmInterp .apply (op , ts) = op ∙ ts
tmInterp .cong (refl , h) = app h
-- The term model per context Γ.
M : Cxt → SetoidModel _ _
M Γ .Den = TmSetoid Γ
M Γ .den = tmInterp
-- The identity substitution σ₀ maps variables to themselves.
σ₀ : {Γ : Cxt} → Sub Γ Γ
σ₀ x = var' x λ()
-- σ₀ acts indeed as identity.
identity : (t : Tm Γ s) → E ⊢ Γ ▹ t [ σ₀ ] ≡ t
identity (var x) = base x
identity (op ∙ ts) = app λ i → identity (ts i)
-- Evaluation in the term model is substitution $E ⊢ Γ ▹ ⦅t⦆σ ≡ t[σ]$.
-- This would even hold "up to the nose" if we had function extensionality.
evaluation : (t : Tm Δ s) (σ : Sub Γ Δ) → E ⊢ Γ ▹ (⦅_⦆ {M = M Γ} t .apply σ) ≡ (t [ σ ])
evaluation (var x) σ = refl (σ x)
evaluation (op ∙ ts) σ = app (λ i → evaluation (ts i) σ)
-- The term model satisfies all the equations it started out with.
satisfies : ∀ i → M Γ ⊧ E i
satisfies i σ = begin
⦅ tₗ ⦆ .apply σ ≈⟨ evaluation tₗ σ ⟩
tₗ [ σ ] ≈⟨ sub (hyp i) σ ⟩
tᵣ [ σ ] ≈⟨ evaluation tᵣ σ ⟨
⦅ tᵣ ⦆ .apply σ ∎
where
open SetoidReasoning (TmSetoid _ _)
tₗ = E i .Eq.lhs
tᵣ = E i .Eq.rhs
------------------------------------------------------------------------
-- Completeness
-- Birkhoff's completeness theorem \citeyearpar{birkhoff:1935}:
-- Any valid consequence is derivable in the equational theory.
module Completeness {I : Set ℓⁱ} (E : I → Eq) {Γ s} {t t' : Tm Γ s} where
open TermModel E
completeness : E ⊃ (t ≐ t') → E ⊢ Γ ▹ t ≡ t'
completeness V = begin
t ≈˘⟨ identity t ⟩
t [ σ₀ ] ≈˘⟨ evaluation t σ₀ ⟩
⦅ t ⦆ .apply σ₀ ≈⟨ V (M Γ) satisfies σ₀ ⟩
⦅ t' ⦆ .apply σ₀ ≈⟨ evaluation t' σ₀ ⟩
t' [ σ₀ ] ≈⟨ identity t' ⟩
t' ∎
where open SetoidReasoning (TmSetoid Γ s)