Formalization of Succinctness #98

ibbem · 2025-12-13T22:57:29Z

This is the formalization of succinctness as advertised in my master thesis "On the Succinctness of
Languages for Static Variability".

Note that there are merge conflicts between thesis_bm and main. Hence, this branch already includes the merge to main and should be merged using a fast-forward merge.

This is the first definition has come to my mind. It works at least for ADT < CCC intuitively.

I expect `2CC < CCC` so `ADT < CCC` should follow using transitivity.

As ≤Size is not total, <Size is not transitive without requiring ≤Size. Moreover, ≱Size is not antisymmetric. Note that ≱Size is ¬ ≤Size with the arguments flipped and the negation moved inside.

This makes it easier to use because the artifact type doesn't need to be applied when invoking `≤Size`. Furthermore, this enables proofs of `≱Size` to fix a single artifact type, for example the natural numbers, and automatically have the inhabitants it needs. The order between the quantifier over `n` and `A` doesn't have a big impact. On the one hand, the chosen order allows `≱Size` to use different artifact types for each `n`. However, it doesn't change the relation inhabitants if they are swapped because there exists a type with enough elements (i.e., union of all `A` ranging all `n`s) that can be fixed and then only a subset of the artifacts can be used for a specific `n`. On the other hand, `≤Size` is a `Set` and, thus, can't be inspected if the order is changed. This specific order is chosen purely as it's more convenient for pattern matching (e.g., one less `with` clause in case of `≤Size`).

Previously, these where not inferred correctly, but now it works™.

This reduces duplication and allows refactoring of 𝔸.

This allows to easily add more fields.

The designed succinctness definition includes a translatable constraint that the old definition was missing. This gets rid of the unfortunate `¬Compiler→¬≤` and `¬Compiler→≤` properties. A drawback of this new definition is that it breaks transitivity. Consider some languages L1 and L3 that are complete and a language L2 that is incomplete. There is an expression e in L1 that cannot be translated to L2. If we have L1 <= L2 and L2 <= L3 we cannot conclude L1 <= L3 because we know nothing about the size of e translated to L3 because we just proved that there exists no translation to L2. Note that the order of `∀ (A : 𝔸)` and `Σ[ m ∈ ℕ ]` was changed. Due to parametricity (type parameters cannot be inspected) this does not change the actual semantics of the definitions. However, it does simplify the proofs by being friendlier to pattern matching and `with` clauses avoiding additional helper functions in many cases.

This makes the names consistent with the symbol that is used now.

This merge introduces succinctness as explored in my master thesis "On the Succinctness of Languages for Static Variability."

pmbittner

Hi @ibbem

thank you for the PR. As always, it would be great to have some documentation here and there. I leave it up to you to decide how much time you want to invest. I have some comments below but would be willing to merge in any case.

pmbittner · 2026-01-06T15:54:02Z

src/Vatras/Framework/Definitions.agda

-atoms : 𝔸 → Set
-atoms = proj₁
+record 𝔸 : Set₁ where
+  no-eta-equality


Maybe you could document here why eta equality must be forbidden?

pmbittner · 2026-01-06T15:54:37Z

src/Vatras/Framework/Definitions.agda

-  open import Data.Nat using (ℕ; _≟_)
+NAT : 𝔸
+NAT = record
+  { atoms = ℕ × ℕ


Could you document why there are two natural numbers? What is each number supposed to mean?

pmbittner · 2026-01-06T15:58:02Z

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

+  → (vs : List (Rose ∞ A))
+  → AllPairs (_≉_) vs
+  → All (_∈ ⟦ e ⟧) vs
+  → List.sum (List.map sizeRose vs) ≤ size2CC e


This seems rather counter-intuitive. A plain enumeration of trees is smaller absolute size than a single 2CC expression which potentially reduces duplication? Am I misreading this theorem? Could you add some documentation?

pmbittner · 2026-01-06T16:03:27Z

src/Vatras/Lang/FST/NoBaseArtifacts.agda

+does-not-describe-variant (e , variant⊆e , e⊆variant) | zero , e≡variant | a , e≡empty | ()
+
+FST-is-incomplete : Incomplete (Rose ∞) (FST.FSTL F)
+FST-is-incomplete complete = does-not-describe-variant (Prod.map₂ (≅-sym) (complete variantGenerator))


Maybe you could add a sentence of documentation to this module what the main insight is here. Is this the first (direct) proof of FST incompleteness?

pmbittner · 2026-01-06T16:04:50Z

src/Vatras/Lang/OC/DeadElim.agda

+open import Vatras.Lang.OC F using (OC; _-<_>-; _❲_❳; Configuration; ⟦_⟧ₒ)
+open import Vatras.Lang.OC.Util using (all-oc)
+
+data RestrictOptions {A : 𝔸} : {i : Size} → List F → OC i A → Set₁ where


What does this do? Restrict options to not be in a given environment (i.e., list of options)?

pmbittner · 2026-01-06T16:11:30Z

src/Vatras/Succinctness/Relations/2CC<ADT.agda

+  where
+  open Eq.≡-Reasoning
+
+todo5 :


Should we keep these todo... names? Looks like you wanted to give hem a name?

pmbittner · 2026-01-06T16:13:05Z

src/Vatras/Succinctness/Relations/2CC=2CC.agda

@@ -0,0 +1,153 @@
+module Vatras.Succinctness.Relations.2CC=2CC where


A short note what this module is about? The name is rather irritating :D

pmbittner · 2026-01-06T16:16:53Z

src/Vatras/Util/Big-O.agda

+open import Data.Product using (_,_; Σ-syntax)
+open import Function using (id)
+import Relation.Binary.PropositionalEquality as Eq
+open import Relation.Unary using (_∈_)


I believe this module is more than just utility isn't it? Would it make sense to move it to the Succinctness module? What do you think? In any case, we can leave it here of course to save some work.

pmbittner · 2026-01-06T16:18:30Z

src/Vatras/Util/Nat/Diagonalization.agda

@@ -0,0 +1,214 @@
+{-# OPTIONS --allow-unsolved-metas #-}


unsolved-metas still necessary?

pmbittner · 2026-01-06T16:19:11Z

src/Vatras/Util/Nat/Diagonalization.agda

+
+import Vatras.Util.List as List
+
+diagonalization : ℕ × ℕ → ℕ


Can you add some documentation of what this diagonalization module is doing?

ibbem added 30 commits July 10, 2025 20:37

Initial syntactic expressiveness experiments

1f2d641

This is the first definition has come to my mind. It works at least for ADT < CCC intuitively.

Factor out the syntactic expressiveness definitions

e7e9afc

Proof the expressiveness theorem for CCC instead of 2CC

a1215d8

I expect `2CC < CCC` so `ADT < CCC` should follow using transitivity.

Require ≤Size for <Size

bee9518

As ≤Size is not total, <Size is not transitive without requiring ≤Size. Moreover, ≱Size is not antisymmetric. Note that ≱Size is ¬ ≤Size with the arguments flipped and the negation moved inside.

Prove that =Size, ≤Size and <Size behave as expected

2286120

Rename temporary files to have proper names

751b52c

Move the size definitions into a separate file

a0658c5

Prove 2CC ≤ ADT to conclude 2CC < ADT

c6a9a0e

Prove that L₁ ≤Size L₂ and L₂ ≱Size L₁ cannot both be true

49f0193

Use more representative variable names

74ddc2d

Use shorter and more explicit notation for proofs

ae3a768

Prove CCC ≤ NCC

46d6503

Prove 2CC < CCC

d1c80b2

Remove unused imports

284df1e

Cleanup the 2CC<ADT file

1caa068

Make language arguments implicit

762fe1a

Previously, these where not inferred correctly, but now it works™.

Prove 2CC=2CC, NCC=2CC (for N=2) and conclude 2CC=CCC

2b63e25

Prove FST ≱ 2CC

4ef38a3

Investigate the relationship between ≤Size and compilers

4d9da19

Prove our FST formalization misses a base feature

3d99014

Use more specialized versions of ∷-injective

edc4000

Prove OC ≱ 2CC

0bbea43

Use the artifact example definitions where possible

4789f75

This reduces duplication and allows refactoring of 𝔸.

Redefine 𝔸 as a record

26efb57

This allows to easily add more fields.

Implement atom sizes

a70486c

Take advantage of artifact sizes

e5d7ed4

Rename e₁ to fst and e₂ to 2cc

546d663

Factor out 2CC.reflectsVariantSize

944d137

Reuse List.replicate in OC≱2CC

71fd187

ibbem added 29 commits September 7, 2025 11:28

Add the designed definition

290d6e6

Inline size comparison

5860509

Use SizedLang in the designed succinctness relation

f8db551

Split the relation definitions into separate files

96f0427

Proof that there exists a diagonalization of ℕ

9ac51ba

Prove that ≤ and ≰ are opposites

4916fbf

Prove ≤ₛ-weakening

ffb965c

Prove more general succinctness transitivity properties

5368a8a

Add missing size definitions

bdce75f

Define an OC with a propositional selection language

e16ef09

Prove that OC is a subset of PropOC

c31b2f9

Prove that PropOC is at least as succinct as OC

69a2e6f

Remove annoying module prefixes in 2CC<ADT

b3c4d3b

Generalize the coarseness of 2CC < ADT

9297133

Add some more transitivity theorems

5e053cd

Replace ≱ in names with ≰

a11219c

This makes the names consistent with the symbol that is used now.

Generalize the dimension of 2CC ≰ₛ FST

0ac88f7

Generalize the dimension of 2CC ≰ₛ OC

4e175e1

Generalize the dimension of 2CC <ₛ ADT

b47e7ab

Prove VariantList ≤ₛ ADT

3b113bb

Prove NADT ≤ₛ VariantList

d38fafb

Prove ADT ≤ₛ NADT

4a07f0d

Prove NADT ≤ₛ ADT

1cab421

Simplify the FixedArtifactLength lemma

3385ba9

Generalize the coarseness of the relationship between ≰ and ≤

ff6e993

Prove independence of size definition

0d29667

Merge branch 'thesis_bm'

44e994a

This merge introduces succinctness as explored in my master thesis "On the Succinctness of Languages for Static Variability."

Remove a lemma that is available in the standard library

b390215

pmbittner approved these changes Jan 6, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Formalization of Succinctness #98

Formalization of Succinctness #98

Uh oh!

ibbem commented Dec 13, 2025

Uh oh!

pmbittner left a comment

Uh oh!

pmbittner Jan 6, 2026

Uh oh!

pmbittner Jan 6, 2026

Uh oh!

pmbittner Jan 6, 2026

Uh oh!

pmbittner Jan 6, 2026

Uh oh!

pmbittner Jan 6, 2026

Uh oh!

pmbittner Jan 6, 2026

Uh oh!

pmbittner Jan 6, 2026

Uh oh!

pmbittner Jan 6, 2026

Uh oh!

pmbittner Jan 6, 2026

Uh oh!

pmbittner Jan 6, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

		@@ -0,0 +1,153 @@
		module Vatras.Succinctness.Relations.2CC=2CC where


		import Vatras.Util.List as List

		diagonalization : ℕ × ℕ → ℕ

Formalization of Succinctness #98

Are you sure you want to change the base?

Formalization of Succinctness #98

Uh oh!

Conversation

ibbem commented Dec 13, 2025

Uh oh!

pmbittner left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants