Skip to content

Commit f3b696e

Browse files
pmbittnerpmbittner
authored
Merge pull request #78 from VariantSync/variant-map-to-variant-generator-documentation
Rename "variant map" to "variant generator" in the documentation
2 parents 4f0a527 + ba09176 commit f3b696e

10 files changed

Lines changed: 33 additions & 33 deletions

File tree

‎README.md‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -287,8 +287,8 @@ For details about Agda's library management, please have a look at [Agda's packa
287287
Our Agda formalization exhaustively formalizes all definitions, theorems, and proofs from our paper.
288288
The following table shows where each of the definitions, theorems, and proofs from the paper are formalized in this library.
289289

290-
| statement | notation in paper | name in our Agda Library | file | notes |
291-
|-----------------|-----------------------------------|--------------------------------------------------------------------|------------------------------------------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------|
290+
| statement | notation in paper | name in our Agda Library | file | notes |
291+
|-----------------|-----------------------------------|--------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------|
292292
| Section 1 | contribution: a map of languages | | [src/Vatras/Translation/LanguageMap.lagda.md](src/Vatras/Translation/LanguageMap.lagda.md) | |
293293
| Section 2 | running example | | [src/Vatras/Test/Experiments/RoundTrip.agda](src/Vatras/Test/Experiments/RoundTrip.agda) | |
294294
| Table 1 | | | [src/Vatras/Lang/All.agda](src/Vatras/Lang/All.agda) | This file only reexports the language definitions. Use the go-to-definition functionality of your editor for easy exploration. |
@@ -305,10 +305,10 @@ The following table shows where each of the definitions, theorems, and proofs fr
305305
| | Equivalence ≅ | `_≅_`, `_≅[_][_]`_ | [src/Vatras/Data/IndexedSet.lagda.md](src/Vatras/Data/IndexedSet.lagda.md) | The difference between `_≅_` and `_≅[_][_]_` is the same as between `_⊆_` and `_⊆[_]_`. |
306306
| Corollary 4.5 | ⊑ is a partial order | `⊆-IsIndexedPartialOrder`, `⊆[]-refl`, `⊆[]-antisym`, `⊆[]-trans` | [src/Vatras/Data/IndexedSet.lagda.md](src/Vatras/Data/IndexedSet.lagda.md) | |
307307
| | ≅ is an equivalence relation | `≅-IsIndexedEquivalence`, `≅[]-refl`, `≅[]-sym`, `≅[]-trans` | [src/Vatras/Data/IndexedSet.lagda.md](src/Vatras/Data/IndexedSet.lagda.md) | |
308-
| Definition 4.6 | Finite Indexed Set | | | We actually only need finite and non-empty indexed sets and do not define finite indexed sets separately. |
308+
| Definition 4.6 | Finite Indexed Set | | | We actually only need finite and non-empty indexed sets and do not define finite indexed sets separately. |
309309
| Definition 4.8 | Non-empty Indexed Set | `empty` | [src/Vatras/Data/IndexedSet.lagda.md](src/Vatras/Data/IndexedSet.lagda.md) | The library definition is a predicate that ensures an indexed set to be non-empty. |
310-
| Definition 4.9 | Variant Generator | `VariantGenerator` | [src/Vatras/Framework/VariantGenerator.agda](src/Vatras/Framework/VariantGenerator.agda) | This is the finite and non-empty indexed set definition mentioned above. |
311-
| Definition 4.10 | Semantic Domain | `VariantGenerator` | [src/Vatras/Framework/VariantGenerator.agda](src/Vatras/Framework/VariantGenerator.agda) | In contrast to a variant map, the semantic domain is the type of variant maps instead of its elements. |
310+
| Definition 4.9 | Variant Generator | `VariantGenerator` | [src/Vatras/Framework/VariantGenerator.agda](src/Vatras/Framework/VariantGenerator.agda) | This is the finite and non-empty indexed set definition mentioned above. |
311+
| Definition 4.10 | Semantic Domain | `VariantGenerator` | [src/Vatras/Framework/VariantGenerator.agda](src/Vatras/Framework/VariantGenerator.agda) | In contrast to a variant generator, the semantic domain is the type of variant generators instead of its elements. |
312312
| Definition 4.11 | configuration language 𝐶 | `ℂ` | [src/Vatras/Framework/Definitions.agda](src/Vatras/Framework/Definitions.agda) | |
313313
| Definition 4.12 | variability language 𝐿 | `𝔼` | [src/Vatras/Framework/Definitions.agda](src/Vatras/Framework/Definitions.agda) | |
314314
| Definition 4.13 | ⟦.⟧ | `𝔼-Semantics` | [src/Vatras/Framework/VariabilityLanguage.agda](src/Vatras/Framework/VariabilityLanguage.agda) | |
@@ -320,7 +320,7 @@ The following table shows where each of the definitions, theorems, and proofs fr
320320
| | ≻ | `_≻_` | [src/Vatras/Framework/Relation/Expressiveness.lagda.md](src/Vatras/Framework/Relation/Expressiveness.lagda.md) | |
321321
| Corollary 4.18 | ⪰ is a partial order | `≽-IsPartialOrder` | [src/Vatras/Framework/Relation/Expressiveness.lagda.md](src/Vatras/Framework/Relation/Expressiveness.lagda.md) | |
322322
| | ≡ is an equivalence relation | `≋-IsEquivalence` | [src/Vatras/Framework/Relation/Expressiveness.lagda.md](src/Vatras/Framework/Relation/Expressiveness.lagda.md) | |
323-
| Definition 4.19 | 𝑀 ⇾ 𝐿 | | | We only model correct compilers. |
323+
| Definition 4.19 | 𝑀 ⇾ 𝐿 | | | We only model correct compilers. |
324324
| Definition 4.20 | 𝑀 ⇾ 𝐿 correct | `LanguageCompiler` | [src/Vatras/Framework/Compiler.agda](src/Vatras/Framework/Compiler.agda) | |
325325
| Theorem 4.21 | 𝑀 ⇾ 𝐿 ⇒ 𝐿 ⪰ 𝑀 | `expressiveness-from-compiler` | [src/Vatras/Framework/Relation/Expressiveness.lagda.md](src/Vatras/Framework/Relation/Expressiveness.lagda.md) | |
326326
| Theorem 4.22 | Complete(M) ∧ L ≽ M ⇒ Complete(L) | `completeness-by-expressiveness` | [src/Vatras/Framework/Proof/ForFree.lagda.md](src/Vatras/Framework/Proof/ForFree.lagda.md) | |

‎src/Vatras/Framework/Proof/ForFree.lagda.md‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -26,11 +26,11 @@ The intuition is that `M` can express everything `L` can express which in turn i
2626
Thus also `M` is complete.
2727
2828
**Proof Sketch:**
29-
Let V be an arbitrary variant map.
29+
Let V be an arbitrary variant generator.
3030
Since L is complete, there exists an expression l ∈ L that describes V.
3131
By assumption, M is as expressive as L.
3232
Thus, there exists an expression m ∈ M that also describes V.
33-
Since V was picked arbitrarily, M can encode any variant map.
33+
Since V was picked arbitrarily, M can encode any variant generator.
3434
Thus, M is complete.
3535
3636
Dual theorem to: soundness-by-expressiveness.
@@ -78,7 +78,7 @@ soundness-by-expressiveness L-sound M-to-L m with M-to-L m
7878
{-|
7979
A language L is unsound if it is at least as expressive as another unsound language M.
8080
The intuition is that there are expressions in M that describe something else
81-
than a variant map.
81+
than a variant generator.
8282
Since L is at least as expressive as M, L can also express these other things.
8383
Hence, L cannot be sound as well.
8484
@@ -96,8 +96,8 @@ We can conclude that any complete language is at least as expressive as any othe
9696
9797
**Proof sketch:**
9898
Given an arbitrary expression eˢ of our target language Lˢ, we have to show that there exists an expression e₊ in our complete language Lᶜ that is variant-equivalent to eˢ.
99-
By soundness of Lˢ we can compute the variant map of eˢ.
100-
By completeness of Lᶜ, we can encode any variant map as an expression eᶜ ∈ Lᶜ.
99+
By soundness of Lˢ we can compute the variant generator of eˢ.
100+
By completeness of Lᶜ, we can encode any variant generator as an expression eᶜ ∈ Lᶜ.
101101
-}
102102
expressiveness-by-completeness-and-soundness : ∀ {Lᶜ Lˢ : VariabilityLanguage V}
103103
→ Complete Lᶜ

‎src/Vatras/Framework/Properties/Completeness.lagda.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ open import Vatras.Data.EqIndexedSet
2020
## Definitions
2121

2222
A language is complete if for any element in its semantic domain, there exists an expression that denotes that element.
23-
For variability languages, this means that given a variant map `m` there must exist an expression `e` that describes all variants in `m`.
23+
For variability languages, this means that given a variant generator `m` there must exist an expression `e` that describes all variants in `m`.
2424
In particular, for every variant `v` in `m`, there exists a configuration `c` that configures `e` to `v`.
2525
```agda
2626
Complete : VariabilityLanguage V → Set₁

‎src/Vatras/Framework/Properties/Soundness.lagda.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ open import Vatras.Data.EqIndexedSet
2020
## Definitions
2121

2222
A language is sound if every expression denotes an element in the semantic domain.
23-
For variability languages, this means that for any expression `e` there must exist a variant map `m` that is semantically equivalent.
23+
For variability languages, this means that for any expression `e` there must exist a variant generator `m` that is semantically equivalent.
2424
```agda
2525
Sound : VariabilityLanguage V → Set₁
2626
Sound ⟪ E , _ , ⟦_⟧ ⟫ =

‎src/Vatras/Framework/Relation/Expression.lagda.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ L₁ , L₂ ⊢ e₁ ≤ e₂ = ⟦ e₁ ⟧₁ ⊆ ⟦ e₂ ⟧₂
7878
infix 5 _,_⊢_≤_
7979
8080
{-|
81-
Two expressions denote equivalent variant maps.
81+
Two expressions denote equivalent variant generators.
8282
-}
8383
_,_⊢_≣_ :
8484
∀ (L₁ L₂ : VariabilityLanguage V)

‎src/Vatras/Framework/Relation/Expressiveness.lagda.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ as well as a range of related relations `_≻_`, `_⋡_`, and proves relevant pr
2323
We also show that compilers for variability languages can be used as proofs
2424
of expressiveness and vice versa (because Agda uses constructive logic).
2525

26-
We say that a language `L₁` is as expressive as another language `L₂` if for any expression `e₂` in `L₂`, there exists an expression `e₁` in `L₁` that describes the same variant map.
26+
We say that a language `L₁` is as expressive as another language `L₂` if for any expression `e₂` in `L₂`, there exists an expression `e₁` in `L₁` that describes the same variant generator.
2727
```agda
2828
{-|
2929
Our central expressiveness relation.
@@ -138,7 +138,7 @@ We now prove that:
138138
```agda
139139
{-|
140140
A translation of expressions preserves semantics if
141-
the translated expression denotes the same variant map as the initial expression.
141+
the translated expression denotes the same variant generator as the initial expression.
142142
-}
143143
SemanticsPreserving : ∀ (L M : VariabilityLanguage V) → Expression L ⇒ₚ Expression M → Set₁
144144
SemanticsPreserving L M t = ∀ {A} (e : Expression L A) → L , M ⊢ e ≣ t e

‎src/Vatras/Framework/VariantGenerator.agda‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,8 @@ import Relation.Binary.PropositionalEquality as Eq
1212
open import Vatras.Data.EqIndexedSet {A = V A}
1313

1414
{-|
15-
Variant maps constitute the semantic domain of variability languages.
16-
As a representative set, we use Fin (suc n) to ensure that variant maps
15+
Variant generators constitute the semantic domain of variability languages.
16+
As a representative set, we use Fin (suc n) to ensure that variant generators
1717
are finite (Fin) and non-empty (suc n) indexed sets.
1818
Using (suc n) here is a shortcut to ensure that the index set has at
1919
least one element and hence is not empty.
@@ -22,18 +22,18 @@ VariantGenerator : ℕ → Set₁
2222
VariantGenerator n = IndexedSet (Fin (suc n))
2323

2424
{-|
25-
This function removes the first variant from a variant map.
26-
Given that we use natural numbers as an index set for variant maps,
27-
variant maps have an implicit total order.
25+
This function removes the first variant from a variant generator.
26+
Given that we use natural numbers as an index set for variant generators,
27+
variant generators have an implicit total order.
2828
Hence, we can distinguish the first element.
2929
-}
3030
remove-first : ∀ {n} → VariantGenerator (suc n) → VariantGenerator n
3131
remove-first set i = set (Data.Fin.suc i)
3232

3333
{-|
34-
This function removes the last variant from a variant map.
35-
Given that we use natural numbers as an index set for variant maps,
36-
variant maps have an implicit total order.
34+
This function removes the last variant from a variant generator.
35+
Given that we use natural numbers as an index set for variant generators,
36+
variant generators have an implicit total order.
3737
Hence, we can distinguish the last element.
3838
-}
3939
remove-last : ∀ {n} → VariantGenerator (suc n) → VariantGenerator n

‎src/Vatras/Lang/FST.lagda.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -884,7 +884,7 @@ FSTL = ⟪ Impose.SPL , Conf , FSTL-Sem ⟫
884884
We prove that FST SPLs are an incomplete variability language, when
885885
assuming rose trees as variant type.
886886
The proof works similarly as for option calculus.
887-
The idea is that feature structure trees cannot encode variant maps
887+
The idea is that feature structure trees cannot encode variant generators
888888
with exactly two disjunct variants.
889889

890890
```agda

‎src/Vatras/Lang/VariantList.lagda.md‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,7 @@ These proofs will form the basis for proving these properties for other language
8181

8282
### Completeness
8383

84-
To prove completeness, we have to show that lists of variants can express any variant map.
84+
To prove completeness, we have to show that lists of variants can express any variant generator.
8585

8686
```agda
8787
open import Vatras.Util.Nat.AtLeast using (cappedFin)
@@ -93,7 +93,7 @@ private
9393
A : 𝔸
9494
e : VariantList A
9595
96-
-- rules for translating a variant map to a list of variants
96+
-- rules for translating a variant generator to a list of variants
9797
infix 3 _⊢_⟶_
9898
data _⊢_⟶_ : ∀ (n : ℕ) → VariantGenerator A n → VariantList A → Set₁ where
9999
-- a singleton set is translated to a singleton list
@@ -185,8 +185,8 @@ VariantList-is-Complete vs =
185185
### Soundness
186186

187187
We can use a trick to prove soundness by reusing the above definitions for completeness.
188-
The trick is that `⟦ e ⟧ ∘ vl-conf` denotes a variant map because it takes a `Fin (suc n)` as input and produces a variant.
189-
We are then left to prove that this variant map exactly denotes the expression in e which is almost true by definition.
188+
The trick is that `⟦ e ⟧ ∘ vl-conf` denotes a variant generator because it takes a `Fin (suc n)` as input and produces a variant.
189+
We are then left to prove that this variant generator exactly denotes the expression in e which is almost true by definition.
190190
It just requires playing with the configuration translation functions a bit, and to prove
191191
that `vl-conf` is the (semantic) inverse of `vl-fnoc`.
192192

0 commit comments

Comments
 (0)