From 4466b385f35cd106699e624ad2e69379a9bb1569 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Mon, 24 Jun 2024 10:18:22 +0200 Subject: [PATCH] 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Κ³)