Formalization of Succinctness

README.md

@@ -130,6 +130,14 @@ Details on the features implemented in Vatras, including tutorials for integrati
 
 The PhD thesis presents a refined and extended version of our OOPSLA'24 paper in chapter 3. In the thesis, we extended the discussion on existing variability languages to better reflect and compare their assumptions on the underlying object language and their varying semantic domains. Consequently, we also extended our formal framework and case study to also study differences in semantic domains. We also refined the notation to better align with the Agda code and to avoid some minor ambiguities.
 
+### On the Succinctness of Languages for Static Variability
+
+[![Thesis](https://img.shields.io/badge/Thesis-PDF-purple)](https://doi.org/10.18725/OPARU-59127)
+
+> Benjamin Moosherr. _On the Succinctness of Languages for Static Variability_. Master Thesis, University of Ulm, November 2025. Reviewed by Matthias Tichy and Thomas Thüm. Supervised by Paul Maximilian Bittner.
+
+This master thesis extends Vatras by a succinctness relation. Succinctness expresses how the size of expressions must change when translated using a variability language compiler. Hence, succinctness allows us to differentiate between variability languages which have equal semantic expressiveness but whose translation results in combinatorial explosion.
+
 ### On the Expressive Power of Languages for Static Variability (OOPSLA'24)
 
 [![Preprint](https://img.shields.io/badge/OOPSLA'24-Preprint-purple)](https://github.com/SoftVarE-Group/Papers/raw/main/2024/2024-OOPSLA-Bittner.pdf)

src/Vatras/Data/IndexedSet.lagda.md

@@ -882,3 +882,15 @@ re-index {_≈ᵃ_ = _≈ᵃ_} rename M rename-is-surjective ≈ᵃ-refl ≈ᵇ-
   , re-indexʳ {_≈ᵃ_ = _≈ᵃ_} rename M rename-is-surjective ≈ᵃ-refl ≈ᵇ-sym M-is-congruent
 ```
 
+### Ungrouped Properties
+
+```agda
+module _ where
+  open import Data.Nat as ℕ using (ℕ)
+  open import Data.Fin as Fin using (Fin)
+  open import Data.List using (lookup; tabulate)
+
+  tabulate⁺ : ∀ {j} {J : Set j} {n : ℕ} {A : IndexedSet (Fin n)} {B : IndexedSet J} → A ⊆ B → lookup (tabulate A) ⊆ B
+  tabulate⁺ {n = ℕ.suc n} x Fin.zero = x Fin.zero
+  tabulate⁺ {n = ℕ.suc n} x (Fin.suc i) = tabulate⁺ (x ∘ Fin.suc) i
+```

src/Vatras/Framework/Definitions.agda

@@ -1,9 +1,12 @@
 module Vatras.Framework.Definitions where
 
 open import Data.Maybe using (Maybe; just)
+open import Data.Nat as ℕ using (ℕ; zero)
 open import Data.Product using (_×_; Σ; Σ-syntax; proj₁; proj₂) renaming (_,_ to _and_)
+import Data.Product.Properties as Product
+open import Data.String as String using (String)
 open import Data.Unit using (⊤; tt) public
-open import Function using (id; _∘_)
+open import Function using (id; _∘_; const)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≗_; refl)
 open import Relation.Binary using (DecidableEquality)
 open import Relation.Nullary.Negation using (¬_)
@@ -20,12 +23,14 @@ the core definitions because it is quite reasonable.
 Any actual data we can think of to plug in here (e.g., strings, tokens or
 nodes of an abstract syntax tree) can be checked for equality.
 -}
-𝔸 : Set₁
-𝔸 = Σ Set DecidableEquality
-
--- retrieve the set of atoms from an atom type 𝔸
-atoms : 𝔸 → Set
-atoms = proj₁
+record 𝔸 : Set₁ where
+  -- We do not actually need eta equality in Vatras and it does break a proof when enabled (no idea why).
+  no-eta-equality
+  field
+    atoms : Set
+    atomsEqual? : DecidableEquality atoms
+    atomSize : atoms → ℕ
+open 𝔸 public
 
 {-|
 Variant Language.
@@ -63,14 +68,39 @@ and hence expressions are parameterized in the type of this atomic data.
 𝔼 = 𝔸 → Set₁
 
 -- some default atoms
-module _ where
-  open import Data.String using (String; _≟_)
-
-  STRING : 𝔸
-  STRING = String and _≟_
+{-|
+String artifacts.
+Equality is defined character wise
+and size is measured by length (in characters not bytes).
+-}
+STRING : 𝔸
+STRING = record
+  { atoms = String
+  ; atomsEqual? = String._≟_
+  ; atomSize = String.length
+  }
 
-module _ where
-  open import Data.Nat using (ℕ; _≟_)
+{-|
+Pairs of natural numbers as artifacts.
+The first element in the pair is treated as an identifier
+whereas the second element determines the size of the artifact.
+Both elements of the pair are tested for equality.
+-}
+NAT : 𝔸
+NAT = record
+  { atoms = ℕ × ℕ
+  ; atomsEqual? = Product.≡-dec ℕ._≟_ ℕ._≟_
+  ; atomSize = proj₂
+  }
 
-  NAT : 𝔸
-  NAT = ℕ and _≟_
+{-|
+Natural number artifacts.
+Each number is treated as a separate artifact.
+The size of all artifacts is zero.
+-}
+NAT' : 𝔸
+NAT' = record
+  { atoms = ℕ
+  ; atomsEqual? = ℕ._≟_
+  ; atomSize = const zero
+  }

src/Vatras/Framework/Variants.agda

@@ -7,7 +7,7 @@ module Vatras.Framework.Variants where
 
 open import Data.List using (List; []; _∷_; map)
 open import Data.Maybe using (nothing; just)
-open import Data.Product using (_,_; proj₁; proj₂)
+open import Data.Product using (_×_; _,_; proj₁; proj₂)
 open import Data.String using (String; _++_; intersperse)
 open import Data.Unit using (⊤; tt)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≗_; refl)
@@ -16,7 +16,7 @@ open Eq.≡-Reasoning
 open import Function using (id; _∘_; flip)
 open import Size using (Size; ↑_; ∞)
 
-open import Vatras.Framework.Definitions using (𝕍; 𝔸; atoms)
+open import Vatras.Framework.Definitions using (𝕍; 𝔸; atoms; atomsEqual?)
 open import Vatras.Framework.VariabilityLanguage
 open import Vatras.Framework.Compiler using (LanguageCompiler)
 open LanguageCompiler
@@ -77,11 +77,17 @@ GrulerVL = Variant-is-VL GrulerVariant
 RoseVL : VariabilityLanguage (Rose ∞)
 RoseVL = Variant-is-VL (Rose ∞)
 
+{-|
+Lemma to conclude that the child lists of two equal rose trees must be equal as well.
+-}
+Rose-injective : ∀ {A : 𝔸} {a₁ a₂ : atoms A} {cs₁ cs₂ : List (Rose ∞ A)} → a₁ -< cs₁ >- ≡ a₂ -< cs₂ >- → (a₁ ≡ a₂) × (cs₁ ≡ cs₂)
+Rose-injective refl = refl , refl
+
 {-|
 Lemma to conclude that the child lists of two equal rose trees must be equal as well.
 -}
 children-equality : ∀ {A : 𝔸} {a₁ a₂ : atoms A} {cs₁ cs₂ : List (Rose ∞ A)} → a₁ -< cs₁ >- ≡ a₂ -< cs₂ >- → cs₁ ≡ cs₂
-children-equality refl = refl
+children-equality = proj₂ ∘ Rose-injective
 
 {-|
 Show function for rose trees.
@@ -149,6 +155,6 @@ open import Data.Bool using (Bool; true)
 open import Data.Bool.ListAction using (or)
 
 has-atom : ∀ {A i} → atoms A → Rose i A → Bool
-has-atom {A , _≟_} a (b -< cs >-) with a ≟ b
+has-atom {A} a (b -< cs >-) with atomsEqual? A a b
 ... | yes refl = true
 ... | no x = or (map (has-atom b) cs)

src/Vatras/Lang/2CC/Encode.agda

@@ -0,0 +1,58 @@
+open import Vatras.Framework.Definitions using (𝔽)
+module Vatras.Lang.2CC.Encode {Dimension : 𝔽} where
+
+open import Data.List as List using (List; []; _∷_)
+
+open import Size using (∞)
+open import Data.Bool using (false)
+open import Data.Unit using (⊤; tt)
+open import Data.List.Properties using (map-∘; map-id; map-cong)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
+
+open import Vatras.Data.EqIndexedSet using (_≅[_][_]_; irrelevant-index-≅)
+open import Vatras.Framework.Variants as V using (Rose; Variant-is-VL; VariantEncoder)
+open import Vatras.Framework.Relation.Function using (_⇔_; to; from)
+open import Vatras.Framework.VariabilityLanguage using (Semantics; Config)
+open import Vatras.Lang.2CC Dimension
+
+encode : ∀ {i} {A} → Rose i A → 2CC ∞ A
+encode (a V.-< cs >-) = a -< List.map encode cs >-
+
+confs : ⊤ ⇔ Config 2CCL
+confs = record
+  { to = λ where tt _ → false
+  ; from = λ _ → tt
+  }
+
+2cc-encode-idemp : ∀ {A} (v : Rose ∞ A) → (c : Configuration) → ⟦ encode v ⟧ c ≡ v
+2cc-encode-idemp {A} v@(a V.-< cs >-) c =
+  begin
+    ⟦ encode v ⟧ c
+  ≡⟨⟩
+    a V.-< List.map (λ x → ⟦ x ⟧ c) (List.map encode cs) >-
+  ≡⟨ Eq.cong (a V.-<_>-) (map-∘ cs) ⟨
+    a V.-< List.map (λ x → ⟦ encode x ⟧ c) cs >-
+  ≡⟨ Eq.cong (a V.-<_>-) (go cs) ⟩
+    v
+  ∎
+  where
+  open Eq.≡-Reasoning
+
+  go : (cs' : List (Rose ∞ A)) → List.map (λ c' → ⟦ encode c' ⟧ c) cs' ≡ cs'
+  go [] = refl
+  go (c' ∷ cs') = Eq.cong₂ _∷_ (2cc-encode-idemp c' c) (go cs')
+
+preserves : ∀ {A} → (v : Rose ∞ A)
+  → Semantics (Variant-is-VL (Rose ∞)) v ≅[ to confs ][ from confs ] ⟦ encode v ⟧
+preserves {A} v = irrelevant-index-≅ v
+  (λ { tt → refl })
+  (2cc-encode-idemp v)
+  (to confs)
+  (from confs)
+
+encoder : VariantEncoder (Rose ∞) 2CCL
+encoder = record
+  { compile = encode
+  ; config-compiler = λ _ → confs
+  ; preserves = preserves
+  }

src/Vatras/Lang/2CC/FixedArtifactLength.agda

@@ -0,0 +1,142 @@
+{-|
+This module shows that artifacts of choice calculus expressions have a fixed number of children.
+Afterwards, we introduce some more usable lemmas on top og this insight.
+-}
+open import Vatras.Framework.Definitions using (𝔽; 𝔸; atoms)
+module Vatras.Lang.2CC.FixedArtifactLength (Dimension : 𝔽) (A : 𝔸) where
+
+open import Data.Bool using (true; false)
+open import Data.Empty using (⊥-elim)
+open import Data.List as List using (List; []; _∷_; _++_)
+import Data.List.Properties as List
+open import Data.List.Relation.Ternary.Interleaving.Propositional using (Interleaving; []; consˡ; consʳ)
+open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
+import Data.List.Relation.Unary.All.Properties
+open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_)
+open import Data.Nat as ℕ using (ℕ; suc; _+_; _∸_; _*_; _≤_; z≤n; s≤s; _≥_)
+import Data.Nat.Properties as ℕ
+open import Data.Product using (_×_; _,_; proj₂; ∃-syntax)
+open import Function using (_∘_; const)
+open import Relation.Binary.PropositionalEquality as Eq using (refl; _≡_; _≢_)
+open import Size using (Size; ∞)
+
+import Vatras.Util.List as List
+open import Vatras.Data.EqIndexedSet using (_∈_; _⊆_)
+open import Vatras.Framework.Variants using (Rose; children-equality)
+open import Vatras.Lang.2CC Dimension using (2CC; _⟨_,_⟩; _-<_>-; ⟦_⟧)
+open import Vatras.Lang.2CC.ReflectsVariantSize using (reflectsVariantSize)
+open import Vatras.Succinctness.Sizes using (sizeRose; size2CC)
+
+_≉_ : Rose ∞ A → Rose ∞ A → Set
+(a₁ Rose.-< cs₁ >-) ≉ (a₂ Rose.-< cs₂ >-) = List.length cs₁ ≢ List.length cs₂
+
+{-|
+The key insight of this module:
+Given a choice calculus expression with an artifact at the root,
+all expressed variants must have the same number of children.
+-}
+fixedChildCount : ∀ {i}
+  → {a₁ : atoms A} {cs₁ : List (Rose ∞ A)}
+  → {a₂ : atoms A} {cs₂ : List (2CC i A)}
+  → (a₁ Rose.-< cs₁ >-) ∈ ⟦ a₂ -< cs₂ >- ⟧
+  → List.length cs₁ ≡ List.length cs₂
+fixedChildCount {cs₁ = cs₁} {cs₂ = cs₂} (c , v≡e) =
+    List.length cs₁
+  ≡⟨ Eq.cong List.length (children-equality v≡e) ⟩
+    List.length (List.map (λ e → ⟦ e ⟧ c) cs₂)
+  ≡⟨ List.length-map (λ e → ⟦ e ⟧ c) cs₂ ⟩
+    List.length cs₂
+  ∎
+  where
+  open Eq.≡-Reasoning
+
+{-|
+We can partition a list of variants
+on whether we can choose the left or right alternative of a choice
+in order to configure each variant.
+-}
+partition : ∀ {i : Size}
+  → (D : Dimension) (c₁ c₂ : 2CC i A)
+  → (vs : List (Rose ∞ A))
+  → AllPairs _≉_ vs
+  → All (_∈ ⟦ D 2CC.⟨ c₁ , c₂ ⟩ ⟧) vs
+  → ∃[ vs₁ ] ∃[ vs₂ ]
+    Interleaving vs₁ vs₂ vs
+  × All (_∈ ⟦ c₁ ⟧) vs₁
+  × All (_∈ ⟦ c₂ ⟧) vs₂
+partition D c₁ c₂ [] unique-vs vs⊆e = [] , [] , [] , [] , []
+partition D c₁ c₂ (v ∷ vs) (v∉vs ∷ unique-vs) ((c , v≡e) ∷ vs⊆e)
+  with partition D c₁ c₂ vs unique-vs vs⊆e
+... | vs₁ , vs₂ , partition , vs₁⊆e , vs₂⊆e
+  with c D
+... | true = v ∷ vs₁ , vs₂ , consˡ partition , (c , v≡e) ∷ vs₁⊆e , vs₂⊆e
+... | false = vs₁ , v ∷ vs₂ , consʳ partition , vs₁⊆e , (c , v≡e) ∷ vs₂⊆e
+
+{-|
+Gives a lower bound on the size of a choice calculus expression
+given that it expresses a number of variants with pairwise different child count.
+-}
+sum≤size2CC : ∀ {i : Size}
+  → (e : 2CC i A)
+  → (vs : List (Rose ∞ A))
+  → AllPairs (_≉_) vs
+  → All (_∈ ⟦ e ⟧) vs
+  → List.sum (List.map sizeRose vs) ≤ size2CC e
+sum≤size2CC (a -< cs >-) [] unique-vs vs⊆e = z≤n
+sum≤size2CC (a -< cs >-) (v ∷ []) unique-vs (v∈e ∷ []) =
+  begin
+    List.sum (List.map sizeRose (v ∷ []))
+  ≡⟨⟩
+    sizeRose v + 0
+  ≡⟨ ℕ.+-identityʳ (sizeRose v) ⟩
+    sizeRose v
+  ≤⟨ reflectsVariantSize v (a -< cs >-) v∈e ⟩
+    size2CC (a -< cs >-)
+  ∎
+  where
+  open ℕ.≤-Reasoning
+sum≤size2CC (a -< cs >-) ((a₁ Rose.-< cs₁ >-) ∷ (a₂ Rose.-< cs₂ >-) ∷ vs) ((v₁≢v₂ ∷ v₁∉vs) ∷ unique-vs) (v₁∈e ∷ v₂∈e ∷ vs⊆e) =
+  ⊥-elim (v₁≢v₂ (Eq.trans (fixedChildCount v₁∈e) (Eq.sym (fixedChildCount v₂∈e))))
+sum≤size2CC (D ⟨ c₁ , c₂ ⟩) vs unique-vs vs⊆e with partition D c₁ c₂ vs unique-vs vs⊆e
+... | vs₁ , vs₂ , partition , vs₁⊆c₁ , vs₂⊆c₂ =
+  begin
+    List.sum (List.map sizeRose vs)
+  ≡⟨ List.sum-Interleaving (List.map-Interleaving partition) ⟨
+    List.sum (List.map sizeRose vs₁) + List.sum (List.map sizeRose vs₂)
+  ≤⟨ ℕ.+-mono-≤ (sum≤size2CC c₁ vs₁ (List.AllPairs-resp-⊆ (List.Interleaving⇒Sublistˡ partition) unique-vs) vs₁⊆c₁) (sum≤size2CC c₂ vs₂ (List.AllPairs-resp-⊆ (List.Interleaving⇒Sublistʳ partition) unique-vs) vs₂⊆c₂) ⟩
+    size2CC c₁ + size2CC c₂
+  <⟨ ℕ.n<1+n (size2CC c₁ + size2CC c₂) ⟩
+    size2CC (D ⟨ c₁ , c₂ ⟩)
+  ∎
+  where
+  open ℕ.≤-Reasoning
+
+{-|
+Gives a lower bound on the size of a choice calculus expression
+given that it expresses a number of variants with pairwise different child count.
+In contrast to `sum≤size2CC`, this lemma is a simplified special case
+which makes use of a lower bound on the variant size.
+-}
+different-children-counts :
+  ∀ {i : Size}
+  → (n : ℕ)
+  → (e : 2CC i A)
+  → (vs : List (Rose ∞ A))
+  → All (_∈ ⟦ e ⟧) vs
+  → All (λ v → sizeRose v ≥ n) vs
+  → AllPairs _≉_ vs
+  → size2CC e ≥ List.length vs * n
+different-children-counts n e vs vs⊆e vs≥n unique-vs =
+  begin
+    List.length vs * n
+  ≡⟨ List.sum-replicate (List.length vs) n ⟨
+    List.sum (List.replicate (List.length vs) n)
+  ≡⟨ Eq.cong List.sum (List.map-const n vs) ⟨
+    List.sum (List.map (const n) vs)
+  ≤⟨ List.sum-map-≤-with∈ vs (λ v v∈vs → All.lookup vs≥n v∈vs) ⟩
+    List.sum (List.map sizeRose vs)
+  ≤⟨ sum≤size2CC e vs unique-vs (vs⊆e) ⟩
+    size2CC e
+  ∎
+  where
+  open ℕ.≤-Reasoning