From f653da1a4c8da72ef4f2e37fa23f48c00a364fab Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Wed, 29 May 2024 18:55:21 +0200 Subject: [PATCH 01/10] Investigate both possible idempotency laws for feature algebras --- src/Framework/Composition/FeatureAlgebra.agda | 567 ++++++++++++++---- src/Lang/FST.agda | 2 +- 2 files changed, 439 insertions(+), 130 deletions(-) diff --git a/src/Framework/Composition/FeatureAlgebra.agda b/src/Framework/Composition/FeatureAlgebra.agda index af461b4f..ea928ee7 100644 --- a/src/Framework/Composition/FeatureAlgebra.agda +++ b/src/Framework/Composition/FeatureAlgebra.agda @@ -1,157 +1,466 @@ {- This module implements the feature algebra by Apel et al. + +We noticed that there are two variants of the distant idempotence law depending +on the order of composition. In case the same artifact is composed from the left +and the right, one of them will determine the position in the result. If the +position of the left is prioritized over the right one, we call it +`LeftAdditive` otherwise we call it `RightAdditive`. -} module Framework.Composition.FeatureAlgebra where -open import Data.Product using (proj₁; proj₂; _×_; _,_) -open import Algebra.Structures using (IsMonoid) +open import Data.Product using (proj₁; proj₂; _×_; _,_; swap) +open import Algebra.Structures using (IsMonoid; IsSemigroup; IsMagma) open import Algebra.Core using (Op₂) open import Algebra.Definitions using (Associative) +open import Function using (flip; IsInverse; Inverseˡ; Inverseʳ) open import Relation.Binary using (Rel; Reflexive; Symmetric; Transitive; IsEquivalence; IsPreorder) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) open import Level using (suc; _⊔_) -record FeatureAlgebra {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) : Set (suc c) where - open Eq.≡-Reasoning +module LeftAdditive where + record FeatureAlgebra {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) : Set (suc c) where + open Eq.≡-Reasoning - _⊕_ = sum - infixr 7 _⊕_ - - field - monoid : IsMonoid _≡_ _⊕_ 𝟘 - - -- Only the leftmost occurence of an introduction is effective in a sum, - -- because it has been introduced first. - -- This is, duplicates of i have no effect. - distant-idempotence : ∀ (i₁ i₂ : I) → i₁ ⊕ i₂ ⊕ i₁ ≡ i₁ ⊕ i₂ - - open IsMonoid monoid - - direct-idempotence : ∀ (i : I) → i ⊕ i ≡ i - direct-idempotence i = - begin - i ⊕ i - ≡⟨ Eq.cong (i ⊕_) (proj₁ identity i) ⟨ - i ⊕ 𝟘 ⊕ i - ≡⟨ distant-idempotence i 𝟘 ⟩ - i ⊕ 𝟘 - ≡⟨ proj₂ identity i ⟩ - i - ∎ + _⊕_ = sum + infixr 7 _⊕_ - -- introduction inclusion - infix 6 _≤_ - _≤_ : Rel I c - i₂ ≤ i₁ = i₁ ⊕ i₂ ≡ i₁ - - ≤-refl : Reflexive _≤_ - ≤-refl {i} = direct-idempotence i - - ≤-trans : Transitive _≤_ - ≤-trans {i} {j} {k} i≤j j≤k = - begin - k ⊕ i - ≡⟨ Eq.cong (_⊕ i) j≤k ⟨ - (k ⊕ j) ⊕ i - ≡⟨ Eq.cong (λ x → (k ⊕ x) ⊕ i) i≤j ⟨ - (k ⊕ (j ⊕ i)) ⊕ i - ≡⟨ assoc k (j ⊕ i) i ⟩ - k ⊕ ((j ⊕ i) ⊕ i) - ≡⟨ Eq.cong (k ⊕_) (assoc j i i) ⟩ - k ⊕ (j ⊕ (i ⊕ i)) - ≡⟨ Eq.cong (k ⊕_) (Eq.cong (j ⊕_) (direct-idempotence i)) ⟩ - k ⊕ (j ⊕ i) - ≡⟨ Eq.cong (k ⊕_) i≤j ⟩ - k ⊕ j - ≡⟨ j≤k ⟩ - k - ∎ + field + monoid : IsMonoid _≡_ _⊕_ 𝟘 - ≤-IsPreorder : IsPreorder _≡_ _≤_ - ≤-IsPreorder = record - { isEquivalence = Eq.isEquivalence - ; reflexive = λ where refl → ≤-refl - ; trans = ≤-trans - } + -- Only the leftmost occurence of an introduction is effective in a sum, + -- because it has been introduced first. + -- This is, duplicates of i have no effect. + distant-idempotence : ∀ (i₁ i₂ : I) → i₁ ⊕ i₂ ⊕ i₁ ≡ i₁ ⊕ i₂ - least-element : ∀ i → 𝟘 ≤ i - least-element = proj₂ identity + open IsMonoid monoid - least-element-unique : ∀ i → i ≤ 𝟘 → i ≡ 𝟘 - least-element-unique i i≤𝟘 rewrite (proj₁ identity i) = i≤𝟘 + direct-idempotence : ∀ (i : I) → i ⊕ i ≡ i + direct-idempotence i = + begin + i ⊕ i + ≡⟨ Eq.cong (i ⊕_) (proj₁ identity i) ⟨ + i ⊕ 𝟘 ⊕ i + ≡⟨ distant-idempotence i 𝟘 ⟩ + i ⊕ 𝟘 + ≡⟨ proj₂ identity i ⟩ + i + ∎ - upper-bound-l : ∀ i₂ i₁ → i₂ ≤ i₂ ⊕ i₁ - upper-bound-l i₂ i₁ = - begin - (i₂ ⊕ i₁) ⊕ i₂ - ≡⟨ assoc i₂ i₁ i₂ ⟩ - i₂ ⊕ (i₁ ⊕ i₂) - ≡⟨ distant-idempotence i₂ i₁ ⟩ - i₂ ⊕ i₁ - ∎ + -- introduction inclusion + infix 6 _≤_ + _≤_ : Rel I c + i₂ ≤ i₁ = i₁ ⊕ i₂ ≡ i₁ - upper-bound-r : ∀ i₂ i₁ → i₁ ≤ i₂ ⊕ i₁ - upper-bound-r i₂ i₁ = - begin - (i₂ ⊕ i₁) ⊕ i₁ - ≡⟨ assoc i₂ i₁ i₁ ⟩ - i₂ ⊕ (i₁ ⊕ i₁) - ≡⟨ Eq.cong (i₂ ⊕_) (direct-idempotence i₁) ⟩ - i₂ ⊕ i₁ - ∎ + ≤-refl : Reflexive _≤_ + ≤-refl {i} = direct-idempotence i - least-upper-bound : ∀ i i₂ i₁ - → i₁ ≤ i - → i₂ ≤ i - ----------- - → i₁ ⊕ i₂ ≤ i - least-upper-bound i i₂ i₁ i₁≤i i₂≤i = - begin - i ⊕ (i₁ ⊕ i₂) - ≡⟨ assoc i i₁ i₂ ⟨ - (i ⊕ i₁) ⊕ i₂ - ≡⟨ Eq.cong (_⊕ i₂) i₁≤i ⟩ - i ⊕ i₂ - ≡⟨ i₂≤i ⟩ - i - ∎ + ≤-trans : Transitive _≤_ + ≤-trans {i} {j} {k} i≤j j≤k = + begin + k ⊕ i + ≡⟨ Eq.cong (_⊕ i) j≤k ⟨ + (k ⊕ j) ⊕ i + ≡⟨ Eq.cong (λ x → (k ⊕ x) ⊕ i) i≤j ⟨ + (k ⊕ (j ⊕ i)) ⊕ i + ≡⟨ assoc k (j ⊕ i) i ⟩ + k ⊕ ((j ⊕ i) ⊕ i) + ≡⟨ Eq.cong (k ⊕_) (assoc j i i) ⟩ + k ⊕ (j ⊕ (i ⊕ i)) + ≡⟨ Eq.cong (k ⊕_) (Eq.cong (j ⊕_) (direct-idempotence i)) ⟩ + k ⊕ (j ⊕ i) + ≡⟨ Eq.cong (k ⊕_) i≤j ⟩ + k ⊕ j + ≡⟨ j≤k ⟩ + k + ∎ + + ≤-IsPreorder : IsPreorder _≡_ _≤_ + ≤-IsPreorder = record + { isEquivalence = Eq.isEquivalence + ; reflexive = λ where refl → ≤-refl + ; trans = ≤-trans + } + + least-element : ∀ i → 𝟘 ≤ i + least-element = proj₂ identity + + least-element-unique : ∀ i → i ≤ 𝟘 → i ≡ 𝟘 + least-element-unique i i≤𝟘 rewrite (proj₁ identity i) = i≤𝟘 + + upper-bound-l : ∀ i₂ i₁ → i₂ ≤ i₂ ⊕ i₁ + upper-bound-l i₂ i₁ = + begin + (i₂ ⊕ i₁) ⊕ i₂ + ≡⟨ assoc i₂ i₁ i₂ ⟩ + i₂ ⊕ (i₁ ⊕ i₂) + ≡⟨ distant-idempotence i₂ i₁ ⟩ + i₂ ⊕ i₁ + ∎ + + upper-bound-r : ∀ i₂ i₁ → i₁ ≤ i₂ ⊕ i₁ + upper-bound-r i₂ i₁ = + begin + (i₂ ⊕ i₁) ⊕ i₁ + ≡⟨ assoc i₂ i₁ i₁ ⟩ + i₂ ⊕ (i₁ ⊕ i₁) + ≡⟨ Eq.cong (i₂ ⊕_) (direct-idempotence i₁) ⟩ + i₂ ⊕ i₁ + ∎ + + least-upper-bound : ∀ i i₂ i₁ + → i₁ ≤ i + → i₂ ≤ i + ----------- + → i₁ ⊕ i₂ ≤ i + least-upper-bound i i₂ i₁ i₁≤i i₂≤i = + begin + i ⊕ (i₁ ⊕ i₂) + ≡⟨ assoc i i₁ i₂ ⟨ + (i ⊕ i₁) ⊕ i₂ + ≡⟨ Eq.cong (_⊕ i₂) i₁≤i ⟩ + i ⊕ i₂ + ≡⟨ i₂≤i ⟩ + i + ∎ + + -- introduction equivalence + infix 6 _~_ + _~_ : Rel I c + i₂ ~ i₁ = i₂ ≤ i₁ × i₁ ≤ i₂ + + ~-refl : Reflexive _~_ + ~-refl = ≤-refl , ≤-refl + + ~-sym : Symmetric _~_ + ~-sym (fst , snd) = snd , fst + + ~-trans : Transitive _~_ + ~-trans (i≤j , j≤i) (j≤k , k≤j) = ≤-trans i≤j j≤k , ≤-trans k≤j j≤i + + ~-IsEquivalence : IsEquivalence _~_ + ~-IsEquivalence = record + { refl = ~-refl + ; sym = ~-sym + ; trans = ~-trans + } + + quasi-smaller : ∀ i₂ i₁ → i₂ ⊕ i₁ ≤ i₁ ⊕ i₂ + quasi-smaller i₂ i₁ = + begin + (i₁ ⊕ i₂) ⊕ (i₂ ⊕ i₁) + ≡⟨ assoc (i₁ ⊕ i₂) i₂ i₁ ⟨ + ((i₁ ⊕ i₂) ⊕ i₂) ⊕ i₁ + ≡⟨ Eq.cong (_⊕ i₁) (assoc i₁ i₂ i₂) ⟩ + (i₁ ⊕ (i₂ ⊕ i₂)) ⊕ i₁ + ≡⟨ Eq.cong (_⊕ i₁) (Eq.cong (i₁ ⊕_) (direct-idempotence i₂)) ⟩ + (i₁ ⊕ i₂) ⊕ i₁ + ≡⟨ assoc i₁ i₂ i₁ ⟩ + i₁ ⊕ (i₂ ⊕ i₁) + ≡⟨ distant-idempotence i₁ i₂ ⟩ + i₁ ⊕ i₂ + ∎ + + quasi-commutativity : ∀ i₂ i₁ → i₂ ⊕ i₁ ~ i₁ ⊕ i₂ + quasi-commutativity i₂ i₁ = quasi-smaller i₂ i₁ , quasi-smaller i₁ i₂ + +module RightAdditive where + record FeatureAlgebra {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) : Set (suc c) where + open Eq.≡-Reasoning + + _⊕_ = sum + infixr 7 _⊕_ + + field + monoid : IsMonoid _≡_ _⊕_ 𝟘 - -- introduction equivalence - infix 6 _~_ - _~_ : Rel I c - i₂ ~ i₁ = i₂ ≤ i₁ × i₁ ≤ i₂ + -- Only the rightmost occurence of an introduction is effective in a sum, + -- because it has been introduced first. + -- This is, duplicates of i have no effect. + distant-idempotence : ∀ (i₁ i₂ : I) → i₂ ⊕ i₁ ⊕ i₂ ≡ i₁ ⊕ i₂ - ~-refl : Reflexive _~_ - ~-refl = ≤-refl , ≤-refl + open IsMonoid monoid - ~-sym : Symmetric _~_ - ~-sym (fst , snd) = snd , fst + direct-idempotence : ∀ (i : I) → i ⊕ i ≡ i + direct-idempotence i = + begin + i ⊕ i + ≡⟨ Eq.cong (i ⊕_) (proj₁ identity i) ⟨ + i ⊕ 𝟘 ⊕ i + ≡⟨ distant-idempotence 𝟘 i ⟩ + 𝟘 ⊕ i + ≡⟨ proj₁ identity i ⟩ + i + ∎ - ~-trans : Transitive _~_ - ~-trans (i≤j , j≤i) (j≤k , k≤j) = ≤-trans i≤j j≤k , ≤-trans k≤j j≤i + -- introduction inclusion + infix 6 _≤_ + _≤_ : Rel I c + i₂ ≤ i₁ = i₂ ⊕ i₁ ≡ i₁ - ~-IsEquivalence : IsEquivalence _~_ - ~-IsEquivalence = record - { refl = ~-refl - ; sym = ~-sym - ; trans = ~-trans + ≤-refl : Reflexive _≤_ + ≤-refl {i} = direct-idempotence i + + ≤-trans : Transitive _≤_ + ≤-trans {i} {j} {k} i≤j j≤k = + begin + i ⊕ k + ≡⟨ Eq.cong (i ⊕_) j≤k ⟨ + i ⊕ (j ⊕ k) + ≡⟨ Eq.cong (λ x → i ⊕ x ⊕ k) i≤j ⟨ + i ⊕ ((i ⊕ j) ⊕ k) + ≡⟨ assoc i (i ⊕ j) k ⟨ + (i ⊕ (i ⊕ j)) ⊕ k + ≡⟨ Eq.cong (_⊕ k) (assoc i i j) ⟨ + ((i ⊕ i) ⊕ j) ⊕ k + ≡⟨ Eq.cong (_⊕ k) (Eq.cong (_⊕ j) (direct-idempotence i)) ⟩ + (i ⊕ j) ⊕ k + ≡⟨ Eq.cong (_⊕ k) i≤j ⟩ + j ⊕ k + ≡⟨ j≤k ⟩ + k + ∎ + + ≤-IsPreorder : IsPreorder _≡_ _≤_ + ≤-IsPreorder = record + { isEquivalence = Eq.isEquivalence + ; reflexive = λ where refl → ≤-refl + ; trans = ≤-trans + } + + least-element : ∀ i → 𝟘 ≤ i + least-element = proj₁ identity + + least-element-unique : ∀ i → i ≤ 𝟘 → i ≡ 𝟘 + least-element-unique i i≤𝟘 rewrite (proj₂ identity i) = i≤𝟘 + + upper-bound-l : ∀ i₂ i₁ → i₂ ≤ i₂ ⊕ i₁ + upper-bound-l i₂ i₁ = + begin + i₂ ⊕ (i₂ ⊕ i₁) + ≡⟨ Eq.sym (assoc i₂ i₂ i₁) ⟩ + (i₂ ⊕ i₂) ⊕ i₁ + ≡⟨ Eq.cong (_⊕ i₁) (direct-idempotence i₂) ⟩ + i₂ ⊕ i₁ + ∎ + + upper-bound-r : ∀ i₂ i₁ → i₁ ≤ i₂ ⊕ i₁ + upper-bound-r i₂ i₁ = distant-idempotence i₂ i₁ + + least-upper-bound : ∀ i i₂ i₁ + → i₁ ≤ i + → i₂ ≤ i + ----------- + → i₁ ⊕ i₂ ≤ i + least-upper-bound i i₂ i₁ i₁≤i i₂≤i = + begin + (i₁ ⊕ i₂) ⊕ i + ≡⟨ assoc i₁ i₂ i ⟩ + i₁ ⊕ (i₂ ⊕ i) + ≡⟨ Eq.cong (i₁ ⊕_) i₂≤i ⟩ + i₁ ⊕ i + ≡⟨ i₁≤i ⟩ + i + ∎ + + -- introduction equivalence + infix 6 _~_ + _~_ : Rel I c + i₂ ~ i₁ = i₂ ≤ i₁ × i₁ ≤ i₂ + + ~-refl : Reflexive _~_ + ~-refl = ≤-refl , ≤-refl + + ~-sym : Symmetric _~_ + ~-sym (fst , snd) = snd , fst + + ~-trans : Transitive _~_ + ~-trans (i≤j , j≤i) (j≤k , k≤j) = ≤-trans i≤j j≤k , ≤-trans k≤j j≤i + + ~-IsEquivalence : IsEquivalence _~_ + ~-IsEquivalence = record + { refl = ~-refl + ; sym = ~-sym + ; trans = ~-trans + } + + quasi-smaller : ∀ i₂ i₁ → i₂ ⊕ i₁ ≤ i₁ ⊕ i₂ + quasi-smaller i₂ i₁ = + begin + (i₂ ⊕ i₁) ⊕ i₁ ⊕ i₂ + ≡⟨⟩ + (i₂ ⊕ i₁) ⊕ (i₁ ⊕ i₂) + ≡⟨ assoc (i₂ ⊕ i₁) i₁ i₂ ⟨ + ((i₂ ⊕ i₁) ⊕ i₁) ⊕ i₂ + ≡⟨ Eq.cong (_⊕ i₂) (assoc i₂ i₁ i₁) ⟩ + (i₂ ⊕ (i₁ ⊕ i₁)) ⊕ i₂ + ≡⟨ Eq.cong (_⊕ i₂) (Eq.cong (i₂ ⊕_) (direct-idempotence i₁)) ⟩ + (i₂ ⊕ i₁) ⊕ i₂ + ≡⟨ assoc i₂ i₁ i₂ ⟩ + i₂ ⊕ i₁ ⊕ i₂ + ≡⟨ distant-idempotence i₁ i₂ ⟩ + i₁ ⊕ i₂ + ∎ + + quasi-commutativity : ∀ i₂ i₁ → i₂ ⊕ i₁ ~ i₁ ⊕ i₂ + quasi-commutativity i₂ i₁ = quasi-smaller i₂ i₁ , quasi-smaller i₁ i₂ + +open LeftAdditive.FeatureAlgebra +open RightAdditive.FeatureAlgebra +open IsMonoid +open IsSemigroup +open IsMagma + +to : ∀ {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) + → LeftAdditive.FeatureAlgebra I sum 𝟘 + → RightAdditive.FeatureAlgebra I (flip sum) 𝟘 +to I sum 𝟘 faˡ = record + { monoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faˡ))) + ; ∙-cong = flip (∙-cong (isMagma (isSemigroup (monoid faˡ)))) + } + ; assoc = λ a b c → Eq.sym (assoc (isSemigroup (monoid faˡ)) c b a) + } + ; identity = swap (identity (monoid faˡ)) + } + ; distant-idempotence = λ a b → Eq.trans (assoc (isSemigroup (monoid faˡ)) b a b) (distant-idempotence faˡ b a) + } + +from : ∀ {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) + → RightAdditive.FeatureAlgebra I sum 𝟘 + → LeftAdditive.FeatureAlgebra I (flip sum) 𝟘 +from I sum 𝟘 faʳ = record + { monoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faʳ))) + ; ∙-cong = flip (∙-cong (isMagma (isSemigroup (monoid faʳ)))) + } + ; assoc = λ a b c → Eq.sym (assoc (isSemigroup (monoid faʳ)) c b a) + } + ; identity = swap (identity (monoid faʳ)) } + ; distant-idempotence = λ a b → Eq.trans (assoc (isSemigroup (monoid faʳ)) a b a) (distant-idempotence faʳ b a) + } - quasi-smaller : ∀ i₂ i₁ → i₂ ⊕ i₁ ≤ i₁ ⊕ i₂ - quasi-smaller i₂ i₁ = - begin - (i₁ ⊕ i₂) ⊕ (i₂ ⊕ i₁) - ≡⟨ assoc (i₁ ⊕ i₂) i₂ i₁ ⟨ - ((i₁ ⊕ i₂) ⊕ i₂) ⊕ i₁ - ≡⟨ Eq.cong (_⊕ i₁) (assoc i₁ i₂ i₂) ⟩ - (i₁ ⊕ (i₂ ⊕ i₂)) ⊕ i₁ - ≡⟨ Eq.cong (_⊕ i₁) (Eq.cong (i₁ ⊕_) (direct-idempotence i₂)) ⟩ - (i₁ ⊕ i₂) ⊕ i₁ - ≡⟨ assoc i₁ i₂ i₁ ⟩ - i₁ ⊕ (i₂ ⊕ i₁) - ≡⟨ distant-idempotence i₁ i₂ ⟩ - i₁ ⊕ i₂ +open import Axioms.Extensionality +open import Relation.Binary.PropositionalEquality.WithK using (≡-irrelevant) + +isInverse : ∀ {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) + → IsInverse _≡_ _≡_ (to I (flip sum) 𝟘) (from I sum 𝟘) +isInverse I sum 𝟘 = record + { isLeftInverse = record + { isCongruent = record + { cong = Eq.cong (to I (flip sum) 𝟘) + ; isEquivalence₁ = Eq.isEquivalence + ; isEquivalence₂ = Eq.isEquivalence + } + ; from-cong = Eq.cong (from I sum 𝟘) + ; inverseˡ = invˡ + } + ; inverseʳ = invʳ + } + where + open Eq.≡-Reasoning + + invˡ : Inverseˡ _≡_ _≡_ (to I (flip sum) 𝟘) (from I sum 𝟘) + invˡ {faˡ} x rewrite x = + to I (flip sum) 𝟘 (from I sum 𝟘 faˡ) + ≡⟨⟩ + record + { monoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faˡ))) + ; ∙-cong = flip (flip (∙-cong (isMagma (isSemigroup (monoid faˡ))))) + } + ; assoc = λ a b c → Eq.sym (Eq.sym (assoc (isSemigroup (monoid faˡ)) a b c)) + } + ; identity = swap (swap (identity (monoid faˡ))) + } + ; distant-idempotence = λ a b → Eq.trans (Eq.sym (assoc (isSemigroup (monoid faˡ)) b a b)) (Eq.trans (assoc (isSemigroup (monoid faˡ)) b a b) (distant-idempotence faˡ a b)) + } + ≡⟨⟩ + record + { monoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faˡ))) + ; ∙-cong = ∙-cong (isMagma (isSemigroup (monoid faˡ))) + } + ; assoc = λ a b c → Eq.sym (Eq.sym (assoc (isSemigroup (monoid faˡ)) a b c)) + } + ; identity = identity (monoid faˡ) + } + ; distant-idempotence = λ a b → Eq.trans (Eq.sym (assoc (isSemigroup (monoid faˡ)) b a b)) (Eq.trans (assoc (isSemigroup (monoid faˡ)) b a b) (distant-idempotence faˡ a b)) + } + ≡⟨ Eq.cong₂ (λ x y → + record + { monoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faˡ))) + ; ∙-cong = ∙-cong (isMagma (isSemigroup (monoid faˡ))) + } + ; assoc = x + } + ; identity = identity (monoid faˡ) + } + ; distant-idempotence = y + }) + (extensionality λ a → extensionality λ b → extensionality (λ c → ≡-irrelevant (Eq.sym (Eq.sym (assoc (isSemigroup (monoid faˡ)) a b c))) (assoc (isSemigroup (monoid faˡ)) a b c))) + (extensionality λ a → extensionality λ b → ≡-irrelevant (Eq.trans (Eq.sym (assoc (isSemigroup (monoid faˡ)) b a b)) (Eq.trans (assoc (isSemigroup (monoid faˡ)) b a b) (distant-idempotence faˡ a b))) (distant-idempotence faˡ a b)) ⟩ + faˡ ∎ - quasi-commutativity : ∀ i₂ i₁ → i₂ ⊕ i₁ ~ i₁ ⊕ i₂ - quasi-commutativity i₂ i₁ = quasi-smaller i₂ i₁ , quasi-smaller i₁ i₂ + invʳ : Inverseʳ _≡_ _≡_ (to I (flip sum) 𝟘) (from I sum 𝟘) + invʳ {faʳ} x rewrite x = + from I sum 𝟘 (to I (flip sum) 𝟘 faʳ) + ≡⟨⟩ + record + { monoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faʳ))) + ; ∙-cong = flip (flip (∙-cong (isMagma (isSemigroup (monoid faʳ))))) + } + ; assoc = λ a b c → Eq.sym (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b c)) + } + ; identity = swap (swap (identity (monoid faʳ))) + } + ; distant-idempotence = λ a b → Eq.trans (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b a)) (Eq.trans (assoc (isSemigroup (monoid faʳ)) a b a) (distant-idempotence faʳ a b)) + } + ≡⟨⟩ + record + { monoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faʳ))) + ; ∙-cong = ∙-cong (isMagma (isSemigroup (monoid faʳ))) + } + ; assoc = λ a b c → Eq.sym (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b c)) + } + ; identity = identity (monoid faʳ) + } + ; distant-idempotence = λ a b → Eq.trans (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b a)) (Eq.trans (assoc (isSemigroup (monoid faʳ)) a b a) (distant-idempotence faʳ a b)) + } + ≡⟨ Eq.cong₂ (λ x y → + record + { monoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faʳ))) + ; ∙-cong = ∙-cong (isMagma (isSemigroup (monoid faʳ))) + } + ; assoc = x + } + ; identity = identity (monoid faʳ) + } + ; distant-idempotence = y + }) + (extensionality λ a → extensionality λ b → extensionality (λ c → ≡-irrelevant (Eq.sym (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b c))) (assoc (isSemigroup (monoid faʳ)) a b c))) + (extensionality λ a → extensionality λ b → ≡-irrelevant (Eq.trans (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b a)) (Eq.trans (assoc (isSemigroup (monoid faʳ)) a b a) (distant-idempotence faʳ a b))) (distant-idempotence faʳ a b)) ⟩ + faʳ + ∎ diff --git a/src/Lang/FST.agda b/src/Lang/FST.agda index 3e58a7cf..7c678412 100644 --- a/src/Lang/FST.agda +++ b/src/Lang/FST.agda @@ -731,7 +731,7 @@ module Impose (AtomSet : 𝔸) where idem : ∀ (x y : FSF) → x ⊛ y ⊛ x ≡ x ⊛ y idem (x ⊚ x-wf) (y ⊚ y-wf) = cong-app₂ _⊚_ (⊕-idem x y x-wf y-wf) AllWellFormed-deterministic - FST-is-FeatureAlgebra : FeatureAlgebra FSF _⊛_ 𝟘 + FST-is-FeatureAlgebra : LeftAdditive.FeatureAlgebra FSF _⊛_ 𝟘 FST-is-FeatureAlgebra = record { monoid = record { isSemigroup = record From d0e8aff77e91e44e448a254aa9f9f725238dbabf Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Wed, 29 May 2024 18:57:32 +0200 Subject: [PATCH 02/10] Prove that FST only obeys one distant idempotence law --- src/Framework/Composition/FeatureAlgebra.agda | 16 +++++++++++++++- src/Lang/FST.agda | 13 ++++++++++++- 2 files changed, 27 insertions(+), 2 deletions(-) diff --git a/src/Framework/Composition/FeatureAlgebra.agda b/src/Framework/Composition/FeatureAlgebra.agda index ea928ee7..c174d2bd 100644 --- a/src/Framework/Composition/FeatureAlgebra.agda +++ b/src/Framework/Composition/FeatureAlgebra.agda @@ -12,7 +12,7 @@ module Framework.Composition.FeatureAlgebra where open import Data.Product using (proj₁; proj₂; _×_; _,_; swap) open import Algebra.Structures using (IsMonoid; IsSemigroup; IsMagma) open import Algebra.Core using (Op₂) -open import Algebra.Definitions using (Associative) +open import Algebra.Definitions using (Associative; Commutative) open import Function using (flip; IsInverse; Inverseˡ; Inverseʳ) open import Relation.Binary using (Rel; Reflexive; Symmetric; Transitive; IsEquivalence; IsPreorder) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) @@ -305,6 +305,20 @@ module RightAdditive where quasi-commutativity : ∀ i₂ i₁ → i₂ ⊕ i₁ ~ i₁ ⊕ i₂ quasi-commutativity i₂ i₁ = quasi-smaller i₂ i₁ , quasi-smaller i₁ i₂ +commutativity : ∀ {c} (I : Set c) (_⊕_ : Op₂ I) (𝟘 : I) + → LeftAdditive.FeatureAlgebra I _⊕_ 𝟘 + → RightAdditive.FeatureAlgebra I _⊕_ 𝟘 + → Commutative _≡_ _⊕_ +commutativity I _⊕_ 𝟘 faˡ faʳ a b = + a ⊕ b + ≡⟨ LeftAdditive.FeatureAlgebra.distant-idempotence faˡ a b ⟨ + a ⊕ (b ⊕ a) + ≡⟨ RightAdditive.FeatureAlgebra.distant-idempotence faʳ b a ⟩ + b ⊕ a + ∎ + where + open Eq.≡-Reasoning + open LeftAdditive.FeatureAlgebra open RightAdditive.FeatureAlgebra open IsMonoid diff --git a/src/Lang/FST.agda b/src/Lang/FST.agda index 7c678412..911559c8 100644 --- a/src/Lang/FST.agda +++ b/src/Lang/FST.agda @@ -35,7 +35,7 @@ open import Function using (_∘_) open import Level using (0ℓ) open import Size using (Size; ↑_; ∞) -open import Algebra.Definitions using (LeftIdentity; RightIdentity; Associative; Congruent₂) +open import Algebra.Definitions using (LeftIdentity; RightIdentity; Associative; Congruent₂; Commutative) open import Relation.Nullary.Negation using (¬_) open import Relation.Nullary.Decidable using (yes; no) @@ -828,3 +828,14 @@ cannotEncodeNeighbors {A} a b (e , conf , ⟦e⟧c≡neighbors) = ¬Unique : ∀ (a : atoms A) → ¬ Unique (a -< [] >- ∷ a -< [] >- ∷ []) ¬Unique a ((a≢a ∷ []) ∷ [] ∷ []) = a≢a refl + +module _ (A : 𝔸) (a₁ a₂ : atoms A) where + open Impose A + + ¬comm : ¬ Commutative _≡_ _⊛_ + ¬comm comm with comm ((a₁ -< rose-leaf a₁ ∷ [] >- ∷ []) ⊚ (([] ∷ []) , (([] ∷ [] , ([] , []) ∷ []) ∷ []))) + ((a₁ -< rose-leaf a₂ ∷ [] >- ∷ []) ⊚ (([] ∷ []) , (([] ∷ [] , ([] , []) ∷ []) ∷ []))) + ¬comm comm | () + + FST-is-not-FeatureAlgebra2 : ¬ RightAdditive.FeatureAlgebra FSF _⊛_ 𝟘 + FST-is-not-FeatureAlgebra2 faʳ = ¬comm (commutativity FSF _⊛_ 𝟘 FST-is-FeatureAlgebra faʳ) From 685cd0c876fb5c5b9d6cce2095ee9d0aece177fc Mon Sep 17 00:00:00 2001 From: pmbittner Date: Fri, 31 May 2024 14:54:15 +0200 Subject: [PATCH 03/10] docs: extend docs on feature algebra --- src/Framework/Composition/FeatureAlgebra.agda | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/Framework/Composition/FeatureAlgebra.agda b/src/Framework/Composition/FeatureAlgebra.agda index c174d2bd..3002698a 100644 --- a/src/Framework/Composition/FeatureAlgebra.agda +++ b/src/Framework/Composition/FeatureAlgebra.agda @@ -1,5 +1,7 @@ {- -This module implements the feature algebra by Apel et al. +This module implements the feature algebra by Apel et al. in +"An Algebraic Foundation for Automatic Feature-based Program Synthesis", +SCP, 2010, Elsevier. We noticed that there are two variants of the distant idempotence law depending on the order of composition. In case the same artifact is composed from the left @@ -164,6 +166,9 @@ module LeftAdditive where quasi-commutativity : ∀ i₂ i₁ → i₂ ⊕ i₁ ~ i₁ ⊕ i₂ quasi-commutativity i₂ i₁ = quasi-smaller i₂ i₁ , quasi-smaller i₁ i₂ +{-| +This is the feature algebra as introduced initially by Apel et al. +-} module RightAdditive where record FeatureAlgebra {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) : Set (suc c) where open Eq.≡-Reasoning From 91ae91c8c48714929c5b6b630572b6ac84971d03 Mon Sep 17 00:00:00 2001 From: pmbittner Date: Fri, 31 May 2024 15:58:11 +0200 Subject: [PATCH 04/10] TODO ibbem --- src/Framework/Composition/FeatureAlgebra.agda | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/src/Framework/Composition/FeatureAlgebra.agda b/src/Framework/Composition/FeatureAlgebra.agda index 3002698a..c965ef30 100644 --- a/src/Framework/Composition/FeatureAlgebra.agda +++ b/src/Framework/Composition/FeatureAlgebra.agda @@ -6,8 +6,18 @@ SCP, 2010, Elsevier. We noticed that there are two variants of the distant idempotence law depending on the order of composition. In case the same artifact is composed from the left and the right, one of them will determine the position in the result. If the +^- TODO ibbem: Who is "them". Could you sketch the terms in brackets if that helps? position of the left is prioritized over the right one, we call it `LeftAdditive` otherwise we call it `RightAdditive`. +^- TODO ibbem: I am also not yet sure about these names. + Just googling "left additive" did not really show something + expect for some advanced category theory beyond the + things we do here. + What about just referring to these modules/algebras as + "Left" and "Right" for now? + Also, see my comment below. It might help to better + understand what x should be in a name left-x / right-x. + Other name ideas: x-dominant, x-determined,, x-override. -} module Framework.Composition.FeatureAlgebra where @@ -32,7 +42,22 @@ module LeftAdditive where -- Only the leftmost occurence of an introduction is effective in a sum, -- because it has been introduced first. + -- ^- TODO ibbem: Is this really true? + -- The ⊕ operator is right-associative (infixr) + -- so the idempotence law is + -- i₁ ⊕ (i₂ ⊕ i₁) ≡ i₁ ⊕ i₂ + -- right? + -- This means the leftmost occurence determines the order of introductions + -- but i₁ is actually already part of the of the (i₂ ⊕ i₁) introduction, right? + -- This means that introducing an introduction i₁ to an introduction (i₂ ⊕ i₁) + -- it is already contained in, may still change/mutate the introduction because + -- i₂ ⊕ i₁ ≢ i₁ ⊕ i₂ + -- but + -- i₁ ⊕ (i₂ ⊕ i₁) ≡ i₁ ⊕ i₂ + -- If you like to, we could discuss this next week. + -- -- This is, duplicates of i have no effect. + -- ^- TODO ibbem: So this is wrong, right? distant-idempotence : ∀ (i₁ i₂ : I) → i₁ ⊕ i₂ ⊕ i₁ ≡ i₁ ⊕ i₂ open IsMonoid monoid @@ -364,6 +389,11 @@ from I sum 𝟘 faʳ = record ; distant-idempotence = λ a b → Eq.trans (assoc (isSemigroup (monoid faʳ)) a b a) (distant-idempotence faʳ b a) } +-- TODO ibbem: +-- - please document on the usage and necessity of this axiom. +-- - adding imports in the middle of a module seems unclean because it is not very transparent what +-- is imported and what not. Should we move the following to its own module (within this file or in +-- another file). open import Axioms.Extensionality open import Relation.Binary.PropositionalEquality.WithK using (≡-irrelevant) From e66b1ac6906829c384cb044ffeda89b0aeb15c8d Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Fri, 31 May 2024 18:40:19 +0200 Subject: [PATCH 05/10] fixup! Investigate both possible idempotency laws for feature algebras --- src/Framework/Composition/FeatureAlgebra.agda | 210 +++++++++--------- 1 file changed, 109 insertions(+), 101 deletions(-) diff --git a/src/Framework/Composition/FeatureAlgebra.agda b/src/Framework/Composition/FeatureAlgebra.agda index c965ef30..4c585622 100644 --- a/src/Framework/Composition/FeatureAlgebra.agda +++ b/src/Framework/Composition/FeatureAlgebra.agda @@ -5,9 +5,8 @@ SCP, 2010, Elsevier. We noticed that there are two variants of the distant idempotence law depending on the order of composition. In case the same artifact is composed from the left -and the right, one of them will determine the position in the result. If the -^- TODO ibbem: Who is "them". Could you sketch the terms in brackets if that helps? -position of the left is prioritized over the right one, we call it +and the right, one of these artifacts will determine the position in the result. +If the position of the left is prioritized over the right one, we call it `LeftAdditive` otherwise we call it `RightAdditive`. ^- TODO ibbem: I am also not yet sure about these names. Just googling "left additive" did not really show something @@ -355,10 +354,10 @@ open IsMonoid open IsSemigroup open IsMagma -to : ∀ {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) +left→right : ∀ {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) → LeftAdditive.FeatureAlgebra I sum 𝟘 → RightAdditive.FeatureAlgebra I (flip sum) 𝟘 -to I sum 𝟘 faˡ = record +left→right I sum 𝟘 faˡ = record { monoid = record { isSemigroup = record { isMagma = record @@ -372,10 +371,10 @@ to I sum 𝟘 faˡ = record ; distant-idempotence = λ a b → Eq.trans (assoc (isSemigroup (monoid faˡ)) b a b) (distant-idempotence faˡ b a) } -from : ∀ {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) +right→left : ∀ {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) → RightAdditive.FeatureAlgebra I sum 𝟘 → LeftAdditive.FeatureAlgebra I (flip sum) 𝟘 -from I sum 𝟘 faʳ = record +right→left I sum 𝟘 faʳ = record { monoid = record { isSemigroup = record { isMagma = record @@ -389,63 +388,58 @@ from I sum 𝟘 faʳ = record ; distant-idempotence = λ a b → Eq.trans (assoc (isSemigroup (monoid faʳ)) a b a) (distant-idempotence faʳ b a) } --- TODO ibbem: --- - please document on the usage and necessity of this axiom. --- - adding imports in the middle of a module seems unclean because it is not very transparent what --- is imported and what not. Should we move the following to its own module (within this file or in --- another file). -open import Axioms.Extensionality -open import Relation.Binary.PropositionalEquality.WithK using (≡-irrelevant) - -isInverse : ∀ {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) - → IsInverse _≡_ _≡_ (to I (flip sum) 𝟘) (from I sum 𝟘) -isInverse I sum 𝟘 = record - { isLeftInverse = record - { isCongruent = record - { cong = Eq.cong (to I (flip sum) 𝟘) - ; isEquivalence₁ = Eq.isEquivalence - ; isEquivalence₂ = Eq.isEquivalence +module _ where + {- + To prove that `left→right` and `right→left` are inverses + we need to prove that their function compositions + keep the feature algebra composition operation and + the laws unchanged. + + The feature algebra composition operation is judgementally equal. + However, the proof that the laws are unchanged requires + extensionality because many of these laws are functions and + uniqueness of identity proofs (K axiom) because the result of these functions are equalities. + + To limit the scope of these axioms, an unnamed modules is used. + -} + open import Axioms.Extensionality + open import Relation.Binary.PropositionalEquality.WithK using (≡-irrelevant) + + isInverse : ∀ {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) + → IsInverse _≡_ _≡_ (left→right I (flip sum) 𝟘) (right→left I sum 𝟘) + isInverse I sum 𝟘 = record + { isLeftInverse = record + { isCongruent = record + { cong = Eq.cong (left→right I (flip sum) 𝟘) + ; isEquivalence₁ = Eq.isEquivalence + ; isEquivalence₂ = Eq.isEquivalence + } + ; from-cong = Eq.cong (right→left I sum 𝟘) + ; inverseˡ = invˡ } - ; from-cong = Eq.cong (from I sum 𝟘) - ; inverseˡ = invˡ + ; inverseʳ = invʳ } - ; inverseʳ = invʳ - } - where - open Eq.≡-Reasoning + where + open Eq.≡-Reasoning - invˡ : Inverseˡ _≡_ _≡_ (to I (flip sum) 𝟘) (from I sum 𝟘) - invˡ {faˡ} x rewrite x = - to I (flip sum) 𝟘 (from I sum 𝟘 faˡ) - ≡⟨⟩ - record - { monoid = record - { isSemigroup = record - { isMagma = record - { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faˡ))) - ; ∙-cong = flip (flip (∙-cong (isMagma (isSemigroup (monoid faˡ))))) - } - ; assoc = λ a b c → Eq.sym (Eq.sym (assoc (isSemigroup (monoid faˡ)) a b c)) - } - ; identity = swap (swap (identity (monoid faˡ))) - } - ; distant-idempotence = λ a b → Eq.trans (Eq.sym (assoc (isSemigroup (monoid faˡ)) b a b)) (Eq.trans (assoc (isSemigroup (monoid faˡ)) b a b) (distant-idempotence faˡ a b)) - } - ≡⟨⟩ - record - { monoid = record - { isSemigroup = record - { isMagma = record - { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faˡ))) - ; ∙-cong = ∙-cong (isMagma (isSemigroup (monoid faˡ))) + invˡ : Inverseˡ _≡_ _≡_ (left→right I (flip sum) 𝟘) (right→left I sum 𝟘) + invˡ {faˡ} x rewrite x = + left→right I (flip sum) 𝟘 (right→left I sum 𝟘 faˡ) + ≡⟨⟩ + record + { monoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faˡ))) + ; ∙-cong = flip (flip (∙-cong (isMagma (isSemigroup (monoid faˡ))))) + } + ; assoc = λ a b c → Eq.sym (Eq.sym (assoc (isSemigroup (monoid faˡ)) a b c)) } - ; assoc = λ a b c → Eq.sym (Eq.sym (assoc (isSemigroup (monoid faˡ)) a b c)) + ; identity = swap (swap (identity (monoid faˡ))) } - ; identity = identity (monoid faˡ) + ; distant-idempotence = λ a b → Eq.trans (Eq.sym (assoc (isSemigroup (monoid faˡ)) b a b)) (Eq.trans (assoc (isSemigroup (monoid faˡ)) b a b) (distant-idempotence faˡ a b)) } - ; distant-idempotence = λ a b → Eq.trans (Eq.sym (assoc (isSemigroup (monoid faˡ)) b a b)) (Eq.trans (assoc (isSemigroup (monoid faˡ)) b a b) (distant-idempotence faˡ a b)) - } - ≡⟨ Eq.cong₂ (λ x y → + ≡⟨⟩ record { monoid = record { isSemigroup = record @@ -453,49 +447,49 @@ isInverse I sum 𝟘 = record { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faˡ))) ; ∙-cong = ∙-cong (isMagma (isSemigroup (monoid faˡ))) } - ; assoc = x + ; assoc = λ a b c → Eq.sym (Eq.sym (assoc (isSemigroup (monoid faˡ)) a b c)) } ; identity = identity (monoid faˡ) } - ; distant-idempotence = y - }) - (extensionality λ a → extensionality λ b → extensionality (λ c → ≡-irrelevant (Eq.sym (Eq.sym (assoc (isSemigroup (monoid faˡ)) a b c))) (assoc (isSemigroup (monoid faˡ)) a b c))) - (extensionality λ a → extensionality λ b → ≡-irrelevant (Eq.trans (Eq.sym (assoc (isSemigroup (monoid faˡ)) b a b)) (Eq.trans (assoc (isSemigroup (monoid faˡ)) b a b) (distant-idempotence faˡ a b))) (distant-idempotence faˡ a b)) ⟩ - faˡ - ∎ - - invʳ : Inverseʳ _≡_ _≡_ (to I (flip sum) 𝟘) (from I sum 𝟘) - invʳ {faʳ} x rewrite x = - from I sum 𝟘 (to I (flip sum) 𝟘 faʳ) - ≡⟨⟩ - record - { monoid = record - { isSemigroup = record - { isMagma = record - { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faʳ))) - ; ∙-cong = flip (flip (∙-cong (isMagma (isSemigroup (monoid faʳ))))) - } - ; assoc = λ a b c → Eq.sym (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b c)) - } - ; identity = swap (swap (identity (monoid faʳ))) + ; distant-idempotence = λ a b → Eq.trans (Eq.sym (assoc (isSemigroup (monoid faˡ)) b a b)) (Eq.trans (assoc (isSemigroup (monoid faˡ)) b a b) (distant-idempotence faˡ a b)) } - ; distant-idempotence = λ a b → Eq.trans (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b a)) (Eq.trans (assoc (isSemigroup (monoid faʳ)) a b a) (distant-idempotence faʳ a b)) - } - ≡⟨⟩ - record - { monoid = record - { isSemigroup = record - { isMagma = record - { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faʳ))) - ; ∙-cong = ∙-cong (isMagma (isSemigroup (monoid faʳ))) + ≡⟨ Eq.cong₂ (λ x y → + record + { monoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faˡ))) + ; ∙-cong = ∙-cong (isMagma (isSemigroup (monoid faˡ))) + } + ; assoc = x + } + ; identity = identity (monoid faˡ) } - ; assoc = λ a b c → Eq.sym (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b c)) + ; distant-idempotence = y + }) + (extensionality λ a → extensionality λ b → extensionality (λ c → ≡-irrelevant (Eq.sym (Eq.sym (assoc (isSemigroup (monoid faˡ)) a b c))) (assoc (isSemigroup (monoid faˡ)) a b c))) + (extensionality λ a → extensionality λ b → ≡-irrelevant (Eq.trans (Eq.sym (assoc (isSemigroup (monoid faˡ)) b a b)) (Eq.trans (assoc (isSemigroup (monoid faˡ)) b a b) (distant-idempotence faˡ a b))) (distant-idempotence faˡ a b)) ⟩ + faˡ + ∎ + + invʳ : Inverseʳ _≡_ _≡_ (left→right I (flip sum) 𝟘) (right→left I sum 𝟘) + invʳ {faʳ} x rewrite x = + right→left I sum 𝟘 (left→right I (flip sum) 𝟘 faʳ) + ≡⟨⟩ + record + { monoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faʳ))) + ; ∙-cong = flip (flip (∙-cong (isMagma (isSemigroup (monoid faʳ))))) + } + ; assoc = λ a b c → Eq.sym (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b c)) + } + ; identity = swap (swap (identity (monoid faʳ))) } - ; identity = identity (monoid faʳ) + ; distant-idempotence = λ a b → Eq.trans (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b a)) (Eq.trans (assoc (isSemigroup (monoid faʳ)) a b a) (distant-idempotence faʳ a b)) } - ; distant-idempotence = λ a b → Eq.trans (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b a)) (Eq.trans (assoc (isSemigroup (monoid faʳ)) a b a) (distant-idempotence faʳ a b)) - } - ≡⟨ Eq.cong₂ (λ x y → + ≡⟨⟩ record { monoid = record { isSemigroup = record @@ -503,13 +497,27 @@ isInverse I sum 𝟘 = record { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faʳ))) ; ∙-cong = ∙-cong (isMagma (isSemigroup (monoid faʳ))) } - ; assoc = x + ; assoc = λ a b c → Eq.sym (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b c)) } ; identity = identity (monoid faʳ) } - ; distant-idempotence = y - }) - (extensionality λ a → extensionality λ b → extensionality (λ c → ≡-irrelevant (Eq.sym (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b c))) (assoc (isSemigroup (monoid faʳ)) a b c))) - (extensionality λ a → extensionality λ b → ≡-irrelevant (Eq.trans (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b a)) (Eq.trans (assoc (isSemigroup (monoid faʳ)) a b a) (distant-idempotence faʳ a b))) (distant-idempotence faʳ a b)) ⟩ - faʳ - ∎ + ; distant-idempotence = λ a b → Eq.trans (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b a)) (Eq.trans (assoc (isSemigroup (monoid faʳ)) a b a) (distant-idempotence faʳ a b)) + } + ≡⟨ Eq.cong₂ (λ x y → + record + { monoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faʳ))) + ; ∙-cong = ∙-cong (isMagma (isSemigroup (monoid faʳ))) + } + ; assoc = x + } + ; identity = identity (monoid faʳ) + } + ; distant-idempotence = y + }) + (extensionality λ a → extensionality λ b → extensionality (λ c → ≡-irrelevant (Eq.sym (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b c))) (assoc (isSemigroup (monoid faʳ)) a b c))) + (extensionality λ a → extensionality λ b → ≡-irrelevant (Eq.trans (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b a)) (Eq.trans (assoc (isSemigroup (monoid faʳ)) a b a) (distant-idempotence faʳ a b))) (distant-idempotence faʳ a b)) ⟩ + faʳ + ∎ From 6024275b2d87d93976e9d57909d934b5a3c92dbf Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Fri, 31 May 2024 20:51:41 +0200 Subject: [PATCH 06/10] TODO pmbittner --- src/Framework/Composition/FeatureAlgebra.agda | 55 +++++++++++++++++++ 1 file changed, 55 insertions(+) diff --git a/src/Framework/Composition/FeatureAlgebra.agda b/src/Framework/Composition/FeatureAlgebra.agda index 4c585622..0e5d9228 100644 --- a/src/Framework/Composition/FeatureAlgebra.agda +++ b/src/Framework/Composition/FeatureAlgebra.agda @@ -17,6 +17,7 @@ If the position of the left is prioritized over the right one, we call it Also, see my comment below. It might help to better understand what x should be in a name left-x / right-x. Other name ideas: x-dominant, x-determined,, x-override. + @pmbittner: I like x-dominant the most out of the current ideas. -} module Framework.Composition.FeatureAlgebra where @@ -54,9 +55,63 @@ module LeftAdditive where -- but -- i₁ ⊕ (i₂ ⊕ i₁) ≡ i₁ ⊕ i₂ -- If you like to, we could discuss this next week. + -- @pmbittner: Regardless of the associativity, the leftmost occurence of + -- `i₁` is the same in either case. However, I agree that the + -- reasoning "has been introduced first" is wrong. + -- On that note: I think it would make sense to use left + -- associativity for LeftAdditive. It feels more intuitive in + -- this case and is also more efficient. 😄 (The intuitive + -- implementation traverses the right argument and inserts it + -- into the left argument. The other way around is harder to + -- implement.) In the end, it doesn't matter for us though, + -- because we have associativity. + -- A meeting next week sounds good to me. + -- + -- A completely different thought I just had: + -- There is actually more than one way to implement + -- LeftDominant and RightDominant (now these names really + -- start to make sense) than just the `flip` one I implemented + -- below: + -- (For simplicity, I ignore children in the following + -- examples.) + -- + -- 1. LeftDominant (FST): + -- (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) ⊕ (5 ∷ 6 ∷ 2 ∷ 1 ∷ []) ≡ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ [] + -- + -- 2. RightDominant (left→right FST): + -- (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) ⊕ (5 ∷ 6 ∷ 2 ∷ 1 ∷ []) ≡ 5 ∷ 6 ∷ 2 ∷ 1 ∷ 3 ∷ 4 ∷ [] + -- + -- 3. alternative RightDominant: + -- (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) ⊕ (5 ∷ 6 ∷ 2 ∷ 1 ∷ []) ≡ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 2 ∷ 1 ∷ [] + -- + -- 4. alternative LeftDominant (right→left of the previous one): + -- (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) ⊕ (5 ∷ 6 ∷ 2 ∷ 1 ∷ []) ≡ 5 ∷ 6 ∷ 1 ∷ 2 ∷ 3 ∷ 4 [] + -- + -- If you are unsure what the 3ʳᵈ version is doing, think of + -- the following: + -- 1. l ⊕ r = mergeDuplicatesIntoLeftmost (l ++ r) + -- 2. l ⊕ r = mergeDuplicatesIntoLeftmost (r ++ l) + -- 3. l ⊕ r = mergeDuplicatesIntoRightmost (l ++ r) + -- 4. l ⊕ r = mergeDuplicatesIntoRightmost (r ++ l) + -- + -- Thinking about it, 3 is way more intuitive than 2 (maybe + -- even "trivial" 😂). + -- + -- Currently, I can't think of a simple way to convert 1 or 2 + -- into 3 or 4 without having implementation knowledge. + -- However, for FSTs, mirroring the variant (visually, on the + -- y-axis) before and after the composition seems to work. + -- e.g. 3. l ⊕ r = mirror (mergeDuplicatesIntoRightmost (mirror (l ++ r))) + -- with + -- mirror fs = map mirror' (reverse fs) + -- mirror' (a -< cs >-) = a -< mirror cs >- + -- -- -- This is, duplicates of i have no effect. -- ^- TODO ibbem: So this is wrong, right? + -- @pmbittner: Yes, strictly speaking. I think a better explanation would + -- be "This is, additional introductions on the right have no + -- effect." distant-idempotence : ∀ (i₁ i₂ : I) → i₁ ⊕ i₂ ⊕ i₁ ≡ i₁ ⊕ i₂ open IsMonoid monoid From 093da414e214df902c473b2520062974bb345b10 Mon Sep 17 00:00:00 2001 From: pmbittner Date: Mon, 3 Jun 2024 16:03:18 +0200 Subject: [PATCH 07/10] TODO ibbem --- src/Framework/Composition/FeatureAlgebra.agda | 66 +++++++++++++++++-- 1 file changed, 62 insertions(+), 4 deletions(-) diff --git a/src/Framework/Composition/FeatureAlgebra.agda b/src/Framework/Composition/FeatureAlgebra.agda index 0e5d9228..c0899538 100644 --- a/src/Framework/Composition/FeatureAlgebra.agda +++ b/src/Framework/Composition/FeatureAlgebra.agda @@ -16,8 +16,9 @@ If the position of the left is prioritized over the right one, we call it "Left" and "Right" for now? Also, see my comment below. It might help to better understand what x should be in a name left-x / right-x. - Other name ideas: x-dominant, x-determined,, x-override. + Other name ideas: x-dominant, x-determined, x-override. @pmbittner: I like x-dominant the most out of the current ideas. + @ibbem: Me too. Then let's stick with that for now. -} module Framework.Composition.FeatureAlgebra where @@ -48,7 +49,7 @@ module LeftAdditive where -- i₁ ⊕ (i₂ ⊕ i₁) ≡ i₁ ⊕ i₂ -- right? -- This means the leftmost occurence determines the order of introductions - -- but i₁ is actually already part of the of the (i₂ ⊕ i₁) introduction, right? + -- but i₁ is actually already part of the (i₂ ⊕ i₁) introduction, right? -- This means that introducing an introduction i₁ to an introduction (i₂ ⊕ i₁) -- it is already contained in, may still change/mutate the introduction because -- i₂ ⊕ i₁ ≢ i₁ ⊕ i₂ @@ -66,8 +67,20 @@ module LeftAdditive where -- implement.) In the end, it doesn't matter for us though, -- because we have associativity. -- A meeting next week sounds good to me. - -- - -- A completely different thought I just had: + -- @ibbem: Ah true, we have associativity, so we actually have: + -- i₂ ⊕ i₁ ≢ i₁ ⊕ i₂ + -- but + -- i₁ ⊕ (i₂ ⊕ i₁) ≡ i₁ ⊕ i₂ + -- and + -- (i₁ ⊕ i₂) ⊕ i₁ ≡ i₁ ⊕ i₂ + -- which means, the rightmost occurence has no effect, right!? + -- It still is a bit counter-intuitive because without explicit + -- brackets, i₁ ⊕ (i₂ ⊕ i₁) is still the order of computation, where + -- the rightmost occurence is handled first but is only "later" found + -- to have no effect. :thinking: + + + -- @pmbittner: A completely different thought I just had: -- There is actually more than one way to implement -- LeftDominant and RightDominant (now these names really -- start to make sense) than just the `flip` one I implemented @@ -77,9 +90,11 @@ module LeftAdditive where -- -- 1. LeftDominant (FST): -- (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) ⊕ (5 ∷ 6 ∷ 2 ∷ 1 ∷ []) ≡ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ [] + -- --> @ibbem: This is what you used for the proofs, right? -- -- 2. RightDominant (left→right FST): -- (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) ⊕ (5 ∷ 6 ∷ 2 ∷ 1 ∷ []) ≡ 5 ∷ 6 ∷ 2 ∷ 1 ∷ 3 ∷ 4 ∷ [] + -- --> @ibbem: This is what I described in the paper and had formalized in Agda, right (except for the alternating-bug)? -- -- 3. alternative RightDominant: -- (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) ⊕ (5 ∷ 6 ∷ 2 ∷ 1 ∷ []) ≡ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 2 ∷ 1 ∷ [] @@ -93,25 +108,68 @@ module LeftAdditive where -- 2. l ⊕ r = mergeDuplicatesIntoLeftmost (r ++ l) -- 3. l ⊕ r = mergeDuplicatesIntoRightmost (l ++ r) -- 4. l ⊕ r = mergeDuplicatesIntoRightmost (r ++ l) + -- --> @ibbem: This formulation is brilliant! It helped a lot in understanding 3 and 4. Also, it is a great + -- explanation how and why these four alternative composition strategies exist! + -- I am yet unsure what to do with these results. + -- What we should definitely do is to characterize which of these composition schemes + -- corresponds to which implementation, as I tried above. + -- Given the extra space in the paper in case of good reviews, we can also shed some light + -- on this, and it would also be a great explanation why our implementation of FSTs and + -- algebra slightly deviates from the Apel paper + why even in the Apel paper there seem + -- to be minor inconsistencies. + -- Good job! 🤩 -- -- Thinking about it, 3 is way more intuitive than 2 (maybe -- even "trivial" 😂). + -- --> @ibbem: I guess both 1 and 3 are in a sense more intuitive because they just concatenate and + -- then eliminate duplicates by favoring either the left or right occurence. + -- I am so biased by now, thinking 2 is super intuitive but it probably is not indeed. 😅 + -- In my mind, the numbers on the left start to walk to the right one by one, starting with the leftmost number. + -- I agree though, and we should probably replace the formulation in the paper with 1 or 3. -- -- Currently, I can't think of a simple way to convert 1 or 2 -- into 3 or 4 without having implementation knowledge. + -- --> @ibbem: If this way does not exist, it would mean that there exist incompatible algebras right? + -- I mean assuming we find an abstract formulation for 3 and 4 in the first place (maybe aab=ab?). -- However, for FSTs, mirroring the variant (visually, on the -- y-axis) before and after the composition seems to work. -- e.g. 3. l ⊕ r = mirror (mergeDuplicatesIntoRightmost (mirror (l ++ r))) -- with -- mirror fs = map mirror' (reverse fs) -- mirror' (a -< cs >-) = a -< mirror cs >- + -- --> @ibbem: Interesting. This 'mirror function then embodies the flipping _after_ composition. + -- So again, we find a commuting square, which tells us that we can "toggle" dominance + -- at multiple levels: + -- + -- FST² <--- swap ---> FST² + -- | | + -- | | Algebra + -- _⊕_ <--- flip ---> _⊕_ + -- | | + -- | | ------------------ + -- V V + -- FST <-- mirror --> FST Implementation + -- + -- | + -- left-dominant | right-dominant + -- | + -- + -- So we can toggle dominance not only on the implementation but also the algebra level. + -- In the algebra, we can perform 'swap' and 'flip' but not 'mirror'. -- + -- I guess the reason for you not finding a way to toggle from 1/2 to and from 3/4 with just _⊕_ is the following: + -- As you have demonstrated above, _⊕_ performs two actions: concatenation _++_ and eliminating duplicates + -- (which besides is the reason for the unique-neighbors-axiom). + -- So maybe, the algebra needs finer granularity in assuming the existence of both of these operations, + -- splitting _⊕_ into the two sub-operations. -- -- This is, duplicates of i have no effect. -- ^- TODO ibbem: So this is wrong, right? -- @pmbittner: Yes, strictly speaking. I think a better explanation would -- be "This is, additional introductions on the right have no -- effect." + -- @ibbem : Ok, let's rephrase accordingly, once we figured out how to handle + -- the above ordering thoughts. distant-idempotence : ∀ (i₁ i₂ : I) → i₁ ⊕ i₂ ⊕ i₁ ≡ i₁ ⊕ i₂ open IsMonoid monoid From 34a684151a7d46c4f9ab91e342e439a9a0b324d3 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Sun, 16 Jun 2024 18:35:52 +0200 Subject: [PATCH 08/10] Get rid of function extensionality in `FeatureAlgebra` --- src/Framework/Composition/FeatureAlgebra.agda | 178 +++++------------- src/Lang/FST.agda | 2 + 2 files changed, 45 insertions(+), 135 deletions(-) diff --git a/src/Framework/Composition/FeatureAlgebra.agda b/src/Framework/Composition/FeatureAlgebra.agda index c0899538..507384e6 100644 --- a/src/Framework/Composition/FeatureAlgebra.agda +++ b/src/Framework/Composition/FeatureAlgebra.agda @@ -170,7 +170,18 @@ module LeftAdditive where -- effect." -- @ibbem : Ok, let's rephrase accordingly, once we figured out how to handle -- the above ordering thoughts. - distant-idempotence : ∀ (i₁ i₂ : I) → i₁ ⊕ i₂ ⊕ i₁ ≡ i₁ ⊕ i₂ + distant-idempotence : ∀ (i₁ i₂ : I) → i₁ ⊕ (i₂ ⊕ i₁) ≡ i₁ ⊕ i₂ + + -- The following laws are already stated equivalently above. However, they + -- serve as a trick to proof that translation between LeftAdditive and + -- RightAdditive is a bijection without using the funtion extensionality + -- or K axiom. + -- This trick is an adaption of a similar trick used in + -- https://github.com/agda/agda-categories + -- as explain in + -- https://www.youtube.com/live/VQiQtH47pbM?si=AJAI24-dhYypr7p9&t=650 + distant-idempotence' : ∀ (i₁ i₂ : I) → (i₁ ⊕ i₂) ⊕ i₁ ≡ i₁ ⊕ i₂ + associative' : ∀ a b c → (a ⊕ (b ⊕ c)) ≡ ((a ⊕ b) ⊕ c) open IsMonoid monoid @@ -319,7 +330,11 @@ module RightAdditive where -- Only the rightmost occurence of an introduction is effective in a sum, -- because it has been introduced first. -- This is, duplicates of i have no effect. - distant-idempotence : ∀ (i₁ i₂ : I) → i₂ ⊕ i₁ ⊕ i₂ ≡ i₁ ⊕ i₂ + distant-idempotence : ∀ (i₁ i₂ : I) → i₂ ⊕ (i₁ ⊕ i₂) ≡ i₁ ⊕ i₂ + + -- See `LeftAdditive` for documentation of the following fields. + distant-idempotence' : ∀ (i₁ i₂ : I) → (i₂ ⊕ i₁) ⊕ i₂ ≡ i₁ ⊕ i₂ + associative' : ∀ a b c → (a ⊕ (b ⊕ c)) ≡ ((a ⊕ b) ⊕ c) open IsMonoid monoid @@ -477,11 +492,13 @@ left→right I sum 𝟘 faˡ = record { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faˡ))) ; ∙-cong = flip (∙-cong (isMagma (isSemigroup (monoid faˡ)))) } - ; assoc = λ a b c → Eq.sym (assoc (isSemigroup (monoid faˡ)) c b a) + ; assoc = λ a b c → associative' faˡ c b a } ; identity = swap (identity (monoid faˡ)) } - ; distant-idempotence = λ a b → Eq.trans (assoc (isSemigroup (monoid faˡ)) b a b) (distant-idempotence faˡ b a) + ; distant-idempotence = λ a b → distant-idempotence' faˡ b a + ; distant-idempotence' = λ a b → distant-idempotence faˡ b a + ; associative' = λ a b c → assoc (isSemigroup (monoid faˡ)) c b a } right→left : ∀ {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) @@ -494,143 +511,34 @@ right→left I sum 𝟘 faʳ = record { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faʳ))) ; ∙-cong = flip (∙-cong (isMagma (isSemigroup (monoid faʳ)))) } - ; assoc = λ a b c → Eq.sym (assoc (isSemigroup (monoid faʳ)) c b a) + ; assoc = λ a b c → associative' faʳ c b a } ; identity = swap (identity (monoid faʳ)) } - ; distant-idempotence = λ a b → Eq.trans (assoc (isSemigroup (monoid faʳ)) a b a) (distant-idempotence faʳ b a) + ; distant-idempotence = λ a b → distant-idempotence' faʳ b a + ; distant-idempotence' = λ a b → distant-idempotence faʳ b a + ; associative' = λ a b c → assoc (isSemigroup (monoid faʳ)) c b a } -module _ where - {- - To prove that `left→right` and `right→left` are inverses - we need to prove that their function compositions - keep the feature algebra composition operation and - the laws unchanged. - - The feature algebra composition operation is judgementally equal. - However, the proof that the laws are unchanged requires - extensionality because many of these laws are functions and - uniqueness of identity proofs (K axiom) because the result of these functions are equalities. - - To limit the scope of these axioms, an unnamed modules is used. - -} - open import Axioms.Extensionality - open import Relation.Binary.PropositionalEquality.WithK using (≡-irrelevant) - - isInverse : ∀ {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) - → IsInverse _≡_ _≡_ (left→right I (flip sum) 𝟘) (right→left I sum 𝟘) - isInverse I sum 𝟘 = record - { isLeftInverse = record - { isCongruent = record - { cong = Eq.cong (left→right I (flip sum) 𝟘) - ; isEquivalence₁ = Eq.isEquivalence - ; isEquivalence₂ = Eq.isEquivalence - } - ; from-cong = Eq.cong (right→left I sum 𝟘) - ; inverseˡ = invˡ +isInverse : ∀ {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) + → IsInverse _≡_ _≡_ (left→right I (flip sum) 𝟘) (right→left I sum 𝟘) +isInverse I sum 𝟘 = record + { isLeftInverse = record + { isCongruent = record + { cong = Eq.cong (left→right I (flip sum) 𝟘) + ; isEquivalence₁ = Eq.isEquivalence + ; isEquivalence₂ = Eq.isEquivalence } - ; inverseʳ = invʳ + ; from-cong = Eq.cong (right→left I sum 𝟘) + ; inverseˡ = invˡ } - where - open Eq.≡-Reasoning + ; inverseʳ = invʳ + } + where + open Eq.≡-Reasoning - invˡ : Inverseˡ _≡_ _≡_ (left→right I (flip sum) 𝟘) (right→left I sum 𝟘) - invˡ {faˡ} x rewrite x = - left→right I (flip sum) 𝟘 (right→left I sum 𝟘 faˡ) - ≡⟨⟩ - record - { monoid = record - { isSemigroup = record - { isMagma = record - { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faˡ))) - ; ∙-cong = flip (flip (∙-cong (isMagma (isSemigroup (monoid faˡ))))) - } - ; assoc = λ a b c → Eq.sym (Eq.sym (assoc (isSemigroup (monoid faˡ)) a b c)) - } - ; identity = swap (swap (identity (monoid faˡ))) - } - ; distant-idempotence = λ a b → Eq.trans (Eq.sym (assoc (isSemigroup (monoid faˡ)) b a b)) (Eq.trans (assoc (isSemigroup (monoid faˡ)) b a b) (distant-idempotence faˡ a b)) - } - ≡⟨⟩ - record - { monoid = record - { isSemigroup = record - { isMagma = record - { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faˡ))) - ; ∙-cong = ∙-cong (isMagma (isSemigroup (monoid faˡ))) - } - ; assoc = λ a b c → Eq.sym (Eq.sym (assoc (isSemigroup (monoid faˡ)) a b c)) - } - ; identity = identity (monoid faˡ) - } - ; distant-idempotence = λ a b → Eq.trans (Eq.sym (assoc (isSemigroup (monoid faˡ)) b a b)) (Eq.trans (assoc (isSemigroup (monoid faˡ)) b a b) (distant-idempotence faˡ a b)) - } - ≡⟨ Eq.cong₂ (λ x y → - record - { monoid = record - { isSemigroup = record - { isMagma = record - { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faˡ))) - ; ∙-cong = ∙-cong (isMagma (isSemigroup (monoid faˡ))) - } - ; assoc = x - } - ; identity = identity (monoid faˡ) - } - ; distant-idempotence = y - }) - (extensionality λ a → extensionality λ b → extensionality (λ c → ≡-irrelevant (Eq.sym (Eq.sym (assoc (isSemigroup (monoid faˡ)) a b c))) (assoc (isSemigroup (monoid faˡ)) a b c))) - (extensionality λ a → extensionality λ b → ≡-irrelevant (Eq.trans (Eq.sym (assoc (isSemigroup (monoid faˡ)) b a b)) (Eq.trans (assoc (isSemigroup (monoid faˡ)) b a b) (distant-idempotence faˡ a b))) (distant-idempotence faˡ a b)) ⟩ - faˡ - ∎ + invˡ : Inverseˡ _≡_ _≡_ (left→right I (flip sum) 𝟘) (right→left I sum 𝟘) + invˡ {faˡ} x rewrite x = Eq.refl - invʳ : Inverseʳ _≡_ _≡_ (left→right I (flip sum) 𝟘) (right→left I sum 𝟘) - invʳ {faʳ} x rewrite x = - right→left I sum 𝟘 (left→right I (flip sum) 𝟘 faʳ) - ≡⟨⟩ - record - { monoid = record - { isSemigroup = record - { isMagma = record - { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faʳ))) - ; ∙-cong = flip (flip (∙-cong (isMagma (isSemigroup (monoid faʳ))))) - } - ; assoc = λ a b c → Eq.sym (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b c)) - } - ; identity = swap (swap (identity (monoid faʳ))) - } - ; distant-idempotence = λ a b → Eq.trans (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b a)) (Eq.trans (assoc (isSemigroup (monoid faʳ)) a b a) (distant-idempotence faʳ a b)) - } - ≡⟨⟩ - record - { monoid = record - { isSemigroup = record - { isMagma = record - { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faʳ))) - ; ∙-cong = ∙-cong (isMagma (isSemigroup (monoid faʳ))) - } - ; assoc = λ a b c → Eq.sym (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b c)) - } - ; identity = identity (monoid faʳ) - } - ; distant-idempotence = λ a b → Eq.trans (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b a)) (Eq.trans (assoc (isSemigroup (monoid faʳ)) a b a) (distant-idempotence faʳ a b)) - } - ≡⟨ Eq.cong₂ (λ x y → - record - { monoid = record - { isSemigroup = record - { isMagma = record - { isEquivalence = isEquivalence (isMagma (isSemigroup (monoid faʳ))) - ; ∙-cong = ∙-cong (isMagma (isSemigroup (monoid faʳ))) - } - ; assoc = x - } - ; identity = identity (monoid faʳ) - } - ; distant-idempotence = y - }) - (extensionality λ a → extensionality λ b → extensionality (λ c → ≡-irrelevant (Eq.sym (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b c))) (assoc (isSemigroup (monoid faʳ)) a b c))) - (extensionality λ a → extensionality λ b → ≡-irrelevant (Eq.trans (Eq.sym (assoc (isSemigroup (monoid faʳ)) a b a)) (Eq.trans (assoc (isSemigroup (monoid faʳ)) a b a) (distant-idempotence faʳ a b))) (distant-idempotence faʳ a b)) ⟩ - faʳ - ∎ + invʳ : Inverseʳ _≡_ _≡_ (left→right I (flip sum) 𝟘) (right→left I sum 𝟘) + invʳ {faʳ} x rewrite x = Eq.refl diff --git a/src/Lang/FST.agda b/src/Lang/FST.agda index 911559c8..7f0e7062 100644 --- a/src/Lang/FST.agda +++ b/src/Lang/FST.agda @@ -744,6 +744,8 @@ module Impose (AtomSet : 𝔸) where ; identity = l-id , r-id } ; distant-idempotence = idem + ; distant-idempotence' = λ a b → Eq.trans (assoc a b a) (idem a b) + ; associative' = λ a b c → Eq.sym (assoc a b c) } where open import Data.Product using (_,_) From 4466b385f35cd106699e624ad2e69379a9bb1569 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Mon, 24 Jun 2024 10:18:22 +0200 Subject: [PATCH 09/10] Rename `*Additive` feature algebras to `*Dominant` --- src/Framework/Composition/FeatureAlgebra.agda | 34 +++++++++---------- src/Lang/FST.agda | 6 ++-- 2 files changed, 20 insertions(+), 20 deletions(-) diff --git a/src/Framework/Composition/FeatureAlgebra.agda b/src/Framework/Composition/FeatureAlgebra.agda index 507384e6..91a4aeeb 100644 --- a/src/Framework/Composition/FeatureAlgebra.agda +++ b/src/Framework/Composition/FeatureAlgebra.agda @@ -7,7 +7,7 @@ We noticed that there are two variants of the distant idempotence law depending on the order of composition. In case the same artifact is composed from the left and the right, one of these artifacts will determine the position in the result. If the position of the left is prioritized over the right one, we call it -`LeftAdditive` otherwise we call it `RightAdditive`. +`LeftDominant` otherwise we call it `RightDominant`. ^- TODO ibbem: I am also not yet sure about these names. Just googling "left additive" did not really show something expect for some advanced category theory beyond the @@ -31,7 +31,7 @@ open import Relation.Binary using (Rel; Reflexive; Symmetric; Transitive; IsEqui open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) open import Level using (suc; _⊔_) -module LeftAdditive where +module LeftDominant where record FeatureAlgebra {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) : Set (suc c) where open Eq.≡-Reasoning @@ -60,7 +60,7 @@ module LeftAdditive where -- `i₁` is the same in either case. However, I agree that the -- reasoning "has been introduced first" is wrong. -- On that note: I think it would make sense to use left - -- associativity for LeftAdditive. It feels more intuitive in + -- associativity for LeftDominant. It feels more intuitive in -- this case and is also more efficient. 😄 (The intuitive -- implementation traverses the right argument and inserts it -- into the left argument. The other way around is harder to @@ -173,8 +173,8 @@ module LeftAdditive where distant-idempotence : ∀ (i₁ i₂ : I) → i₁ ⊕ (i₂ ⊕ i₁) ≡ i₁ ⊕ i₂ -- The following laws are already stated equivalently above. However, they - -- serve as a trick to proof that translation between LeftAdditive and - -- RightAdditive is a bijection without using the funtion extensionality + -- serve as a trick to proof that translation between LeftDominant and + -- RightDominant is a bijection without using the funtion extensionality -- or K axiom. -- This trick is an adaption of a similar trick used in -- https://github.com/agda/agda-categories @@ -317,7 +317,7 @@ module LeftAdditive where {-| This is the feature algebra as introduced initially by Apel et al. -} -module RightAdditive where +module RightDominant where record FeatureAlgebra {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) : Set (suc c) where open Eq.≡-Reasoning @@ -332,7 +332,7 @@ module RightAdditive where -- This is, duplicates of i have no effect. distant-idempotence : ∀ (i₁ i₂ : I) → i₂ ⊕ (i₁ ⊕ i₂) ≡ i₁ ⊕ i₂ - -- See `LeftAdditive` for documentation of the following fields. + -- See `LeftDominant` for documentation of the following fields. distant-idempotence' : ∀ (i₁ i₂ : I) → (i₂ ⊕ i₁) ⊕ i₂ ≡ i₁ ⊕ i₂ associative' : ∀ a b c → (a ⊕ (b ⊕ c)) ≡ ((a ⊕ b) ⊕ c) @@ -463,28 +463,28 @@ module RightAdditive where quasi-commutativity i₂ i₁ = quasi-smaller i₂ i₁ , quasi-smaller i₁ i₂ commutativity : ∀ {c} (I : Set c) (_⊕_ : Op₂ I) (𝟘 : I) - → LeftAdditive.FeatureAlgebra I _⊕_ 𝟘 - → RightAdditive.FeatureAlgebra I _⊕_ 𝟘 + → LeftDominant.FeatureAlgebra I _⊕_ 𝟘 + → RightDominant.FeatureAlgebra I _⊕_ 𝟘 → Commutative _≡_ _⊕_ commutativity I _⊕_ 𝟘 faˡ faʳ a b = a ⊕ b - ≡⟨ LeftAdditive.FeatureAlgebra.distant-idempotence faˡ a b ⟨ + ≡⟨ LeftDominant.FeatureAlgebra.distant-idempotence faˡ a b ⟨ a ⊕ (b ⊕ a) - ≡⟨ RightAdditive.FeatureAlgebra.distant-idempotence faʳ b a ⟩ + ≡⟨ RightDominant.FeatureAlgebra.distant-idempotence faʳ b a ⟩ b ⊕ a ∎ where open Eq.≡-Reasoning -open LeftAdditive.FeatureAlgebra -open RightAdditive.FeatureAlgebra +open LeftDominant.FeatureAlgebra +open RightDominant.FeatureAlgebra open IsMonoid open IsSemigroup open IsMagma left→right : ∀ {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) - → LeftAdditive.FeatureAlgebra I sum 𝟘 - → RightAdditive.FeatureAlgebra I (flip sum) 𝟘 + → LeftDominant.FeatureAlgebra I sum 𝟘 + → RightDominant.FeatureAlgebra I (flip sum) 𝟘 left→right I sum 𝟘 faˡ = record { monoid = record { isSemigroup = record @@ -502,8 +502,8 @@ left→right I sum 𝟘 faˡ = record } right→left : ∀ {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) - → RightAdditive.FeatureAlgebra I sum 𝟘 - → LeftAdditive.FeatureAlgebra I (flip sum) 𝟘 + → RightDominant.FeatureAlgebra I sum 𝟘 + → LeftDominant.FeatureAlgebra I (flip sum) 𝟘 right→left I sum 𝟘 faʳ = record { monoid = record { isSemigroup = record diff --git a/src/Lang/FST.agda b/src/Lang/FST.agda index 7f0e7062..9b76aebe 100644 --- a/src/Lang/FST.agda +++ b/src/Lang/FST.agda @@ -731,7 +731,7 @@ module Impose (AtomSet : 𝔸) where idem : ∀ (x y : FSF) → x ⊛ y ⊛ x ≡ x ⊛ y idem (x ⊚ x-wf) (y ⊚ y-wf) = cong-app₂ _⊚_ (⊕-idem x y x-wf y-wf) AllWellFormed-deterministic - FST-is-FeatureAlgebra : LeftAdditive.FeatureAlgebra FSF _⊛_ 𝟘 + FST-is-FeatureAlgebra : LeftDominant.FeatureAlgebra FSF _⊛_ 𝟘 FST-is-FeatureAlgebra = record { monoid = record { isSemigroup = record @@ -839,5 +839,5 @@ module _ (A : 𝔸) (a₁ a₂ : atoms A) where ((a₁ -< rose-leaf a₂ ∷ [] >- ∷ []) ⊚ (([] ∷ []) , (([] ∷ [] , ([] , []) ∷ []) ∷ []))) ¬comm comm | () - FST-is-not-FeatureAlgebra2 : ¬ RightAdditive.FeatureAlgebra FSF _⊛_ 𝟘 - FST-is-not-FeatureAlgebra2 faʳ = ¬comm (commutativity FSF _⊛_ 𝟘 FST-is-FeatureAlgebra faʳ) + FST-is-not-RightDominant : ¬ RightDominant.FeatureAlgebra FSF _⊛_ 𝟘 + FST-is-not-RightDominant faʳ = ¬comm (commutativity FSF _⊛_ 𝟘 FST-is-FeatureAlgebra faʳ) From a16665784c1526ed7e02737639573b2d284a2689 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Mon, 24 Jun 2024 11:41:21 +0200 Subject: [PATCH 10/10] TODO pmbittner --- src/Framework/Composition/FeatureAlgebra.agda | 95 +++++++++++++++---- 1 file changed, 76 insertions(+), 19 deletions(-) diff --git a/src/Framework/Composition/FeatureAlgebra.agda b/src/Framework/Composition/FeatureAlgebra.agda index 91a4aeeb..94c3cc0d 100644 --- a/src/Framework/Composition/FeatureAlgebra.agda +++ b/src/Framework/Composition/FeatureAlgebra.agda @@ -8,17 +8,6 @@ on the order of composition. In case the same artifact is composed from the left and the right, one of these artifacts will determine the position in the result. If the position of the left is prioritized over the right one, we call it `LeftDominant` otherwise we call it `RightDominant`. -^- TODO ibbem: I am also not yet sure about these names. - Just googling "left additive" did not really show something - expect for some advanced category theory beyond the - things we do here. - What about just referring to these modules/algebras as - "Left" and "Right" for now? - Also, see my comment below. It might help to better - understand what x should be in a name left-x / right-x. - Other name ideas: x-dominant, x-determined, x-override. - @pmbittner: I like x-dominant the most out of the current ideas. - @ibbem: Me too. Then let's stick with that for now. -} module Framework.Composition.FeatureAlgebra where @@ -91,10 +80,12 @@ module LeftDominant where -- 1. LeftDominant (FST): -- (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) ⊕ (5 ∷ 6 ∷ 2 ∷ 1 ∷ []) ≡ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ [] -- --> @ibbem: This is what you used for the proofs, right? + -- A: Yes. -- -- 2. RightDominant (left→right FST): -- (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) ⊕ (5 ∷ 6 ∷ 2 ∷ 1 ∷ []) ≡ 5 ∷ 6 ∷ 2 ∷ 1 ∷ 3 ∷ 4 ∷ [] -- --> @ibbem: This is what I described in the paper and had formalized in Agda, right (except for the alternating-bug)? + -- A: Yes. -- -- 3. alternative RightDominant: -- (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) ⊕ (5 ∷ 6 ∷ 2 ∷ 1 ∷ []) ≡ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 2 ∷ 1 ∷ [] @@ -133,7 +124,7 @@ module LeftDominant where -- I mean assuming we find an abstract formulation for 3 and 4 in the first place (maybe aab=ab?). -- However, for FSTs, mirroring the variant (visually, on the -- y-axis) before and after the composition seems to work. - -- e.g. 3. l ⊕ r = mirror (mergeDuplicatesIntoRightmost (mirror (l ++ r))) + -- e.g. 3. l ⊕ r = mirror (mergeDuplicatesIntoLeftmost (mirror (l ++ r))) -- with -- mirror fs = map mirror' (reverse fs) -- mirror' (a -< cs >-) = a -< mirror cs >- @@ -163,13 +154,73 @@ module LeftDominant where -- So maybe, the algebra needs finer granularity in assuming the existence of both of these operations, -- splitting _⊕_ into the two sub-operations. -- - -- This is, duplicates of i have no effect. - -- ^- TODO ibbem: So this is wrong, right? - -- @pmbittner: Yes, strictly speaking. I think a better explanation would - -- be "This is, additional introductions on the right have no - -- effect." - -- @ibbem : Ok, let's rephrase accordingly, once we figured out how to handle - -- the above ordering thoughts. + -- --> @pmbittner: I agree that there is a diagram hiding here but yours is a little weird: + -- if you mirror only the result then you destroy most properties of the FeatureAlgebra (e.g., associativity). + -- it doesn't commute + -- (mirror ∘ _⊕_ ∘ swap) (FST₁ , FST₂) ≡ mirror (FST₂ ⊕ FST₁) ≢ FST₁ ⊕ FST₂ ≡ _⊕_ (FST₁ , FST₂) + -- + -- A better one might be: + -- ⊕₁ <--- swap ---> ⊕₂ + -- ^ ^ + -- | | + -- | | + -- mirror mirror + -- | | + -- | | + -- v v + -- ⊕₃ <--- swap ---> ⊕₃ + -- + -- Furthermore, we can actually use `mirror` as follows: + -- + -- mirror (mergeDuplicatesIntoLeftmost (mirror (l ++ r))) + -- = mirror (mergeDuplicatesIntoLeftmost (mirror r ++ mirror l)) + -- + -- which gives us + -- + -- 1. l ⊕₁ r = mergeDuplicatesIntoLeftmost (l ++ r) + -- 2. l ⊕₂ r = r ⊕₁ l + -- 3. l ⊕₃ r = mirror (mirror r ⊕₁ mirror l) + -- 4. l ⊕₄ r = mirror (mirror l ⊕₁ mirror r) + -- + -- Hence, I don't think that separating `_⊕_` into two phases makes much sense. + -- In addition, there are `FeatureAlgebra`s where I can't think of a similar `mirror` function. + -- For example: Consider variants which use sets instead of lists, i.e. do not have a children order + -- (or, as implemented below, only allow one children order) + -- + -- mutual + -- data Variant (A : StrictTotalOrder) : Set where + -- artifact : Carrier A → VariantSet A → Variant A + -- + -- VariantSet : StrictTotalOrder → Set + -- VariantSet A = Σ (List (Variant A)) (Linked (Variant-< A)) + -- + -- Variant-< : (A : StrictTotalOrder) → StrictTotalOrder (Variant A) Variant-< = ... -- ignore children, only compare artifacts + -- + -- -- Here, I left out the proofs 😅 + -- _⊕_ : {A : StrictTotalOrder} → VariantSet A → VariantSet A → VariantSet A + -- [] ⊕ vs₂ = vs₂ + -- (artifact a₁ cs₁ ∷ vs₁) ⊕ [] = (artifact a₁ cs₁ ∷ vs₁) + -- (artifact a₁ cs₁ ∷ vs₁) ⊕ (artifact a₂ cs₂ ∷ vs₂) with compare _ a₁ a₂ + -- ... | tri< a₁ a₁>a₂ = artifact a₂ cs₂ ∷ ((artifact a₁ cs₁ ∷ vs₁) ⊕ vs₂) + -- + -- This is also an example of a commutative `FeatureAlgebra`. + -- Which is equivalent to the statement that `swap` has no effect. See `swap≡id⇒commutativity` + -- + -- + -- And here is an example of a `LeftDominant` feature algebra which is not commutative and has (to my knowledge) no `mirror` equivalent: + -- + -- data Variant (A : Set) : Set where + -- identity : Variant A + -- artifact : A → Variant A + -- + -- _⊕_ : {A : Set} → Variant A → Variant A → Variant A + -- identity ⊕ b = b + -- (artifact a) ⊕ b = artifact a + + + -- This is, additional introductions on the right have no effect. distant-idempotence : ∀ (i₁ i₂ : I) → i₁ ⊕ (i₂ ⊕ i₁) ≡ i₁ ⊕ i₂ -- The following laws are already stated equivalently above. However, they @@ -542,3 +593,9 @@ isInverse I sum 𝟘 = record invʳ : Inverseʳ _≡_ _≡_ (left→right I (flip sum) 𝟘) (right→left I sum 𝟘) invʳ {faʳ} x rewrite x = Eq.refl + +swap≡id⇒commutativity : ∀ {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) + → (fa : LeftDominant.FeatureAlgebra I sum 𝟘) + → flip sum ≡ sum + → Commutative _≡_ sum +swap≡id⇒commutativity I sum 𝟘 fa flip-sum≡sum = commutativity I sum 𝟘 fa (Eq.subst (λ p → RightDominant.FeatureAlgebra I p 𝟘) flip-sum≡sum (left→right I sum 𝟘 fa))