Formalization of Succinctness - #98

Merged

pmbittner merged 83 commits into

merge-thesis_bm-to-main

Apr 17, 2026

Commits on Jul 10, 2025

Initial syntactic expressiveness experiments
ibbem
committed
1f2d641
Factor out the syntactic expressiveness definitions
ibbem
committed
e7e9afc
Proof the expressiveness theorem for CCC instead of 2CC
ibbem
committed
a1215d8
Require ≤Size for <Size
ibbem
committed
bee9518
Prove that =Size, ≤Size and <Size behave as expected
ibbem
committed
2286120
Rename temporary files to have proper names
ibbem
committed
751b52c
Move the size definitions into a separate file
ibbem
committed
a0658c5
Prove 2CC ≤ ADT to conclude 2CC < ADT
ibbem
committed
c6a9a0e
Prove that L₁ ≤Size L₂ and L₂ ≱Size L₁ cannot both be true
ibbem
committed
49f0193
Use more representative variable names
ibbem
committed
74ddc2d
Use shorter and more explicit notation for proofs
ibbem
committed
ae3a768
Prove CCC ≤ NCC
ibbem
committed
46d6503
Prove 2CC < CCC
ibbem
committed
d1c80b2

Commits on Jul 12, 2025

Quantify ≤Size over the artifact type
ibbem
committed
13bb256
Remove unused imports
ibbem
committed
284df1e
Cleanup the 2CC<ADT file
ibbem
committed
1caa068
Make language arguments implicit
ibbem
committed
762fe1a
Prove 2CC=2CC, NCC=2CC (for N=2) and conclude 2CC=CCC
ibbem
committed
2b63e25
Prove FST ≱ 2CC
ibbem
committed
4ef38a3
Investigate the relationship between ≤Size and compilers
ibbem
committed
4d9da19
Prove our FST formalization misses a base feature
ibbem
committed
3d99014
Use more specialized versions of ∷-injective
ibbem
committed
edc4000
Prove OC ≱ 2CC
ibbem
committed
0bbea43

Commits on Jul 13, 2025

Use the artifact example definitions where possible
ibbem
committed
4789f75
Redefine 𝔸 as a record
ibbem
committed
26efb57
Implement atom sizes
ibbem
committed
a70486c

Commits on Jul 14, 2025

Take advantage of artifact sizes
ibbem
committed
e5d7ed4
Rename `e₁` to `fst` and `e₂` to `2cc`
ibbem
committed
546d663

Commits on Jul 15, 2025

Factor out 2CC.reflectsVariantSize
ibbem
committed
944d137
Reuse List.replicate in OC≱2CC
ibbem
committed
71fd187
Make OC≱2CC easier to read
ibbem
committed
7dbfc95
Write 2CC instead of 2CC.2CC in FST≱2CC
ibbem
committed
30ae516
Inline big-artifact in FST≱2CC
ibbem
committed
85b1ae6
Use the same approach as OC≱2CC in FST≱2CC
ibbem
committed
ae7f6ab
Apply η-conversion in FST≱2CC
ibbem
committed
8194f01
Simplify FST evaluation in FST≱2CC
ibbem
committed
875fc41
FST≱2CC: Only define variants that are needed
ibbem
committed
865509d
Make FST≱2CC more readable
ibbem
committed
15aeaee

Commits on Jul 22, 2025

Commits on Sep 4, 2025

Create size definitions using reflection
ibbem
committed
762ca77

Commits on Sep 7, 2025

Create a dead option elimination transformation
ibbem
committed
90fe544
Rename SyntacticExpressiveness to Succinctness
ibbem
committed
e2db0cf
Refactor the succinctness module structure
ibbem
committed
e69781f
Add the designed definition
ibbem
committed
290d6e6
Inline size comparison
ibbem
committed
5860509
Use `SizedLang` in the designed succinctness relation
ibbem
committed
f8db551
Split the relation definitions into separate files
ibbem
committed
96f0427

Commits on Sep 9, 2025

Use the new succinctness definition
ibbem
committed
8683001
Proof that there exists a diagonalization of ℕ
ibbem
committed
9ac51ba
Prove that ≤ and ≰ are opposites
ibbem
committed
4916fbf
Prove ≤ₛ-weakening
ibbem
committed
ffb965c
Prove more general succinctness transitivity properties
ibbem
committed
5368a8a

Commits on Nov 11, 2025

Add missing size definitions
ibbem
committed
bdce75f
Define an OC with a propositional selection language
ibbem
committed
e16ef09
Prove that OC is a subset of PropOC
ibbem
committed
c31b2f9

Commits on Dec 4, 2025

Commits on Dec 9, 2025

Replace ≱ in names with ≰
ibbem
committed
a11219c
Generalize the dimension of 2CC ≰ₛ FST
ibbem
committed
0ac88f7
Generalize the dimension of 2CC ≰ₛ OC
ibbem
committed
4e175e1
Generalize the dimension of 2CC <ₛ ADT
ibbem
committed
b47e7ab
Prove VariantList ≤ₛ ADT
ibbem
committed
3b113bb
Prove NADT ≤ₛ VariantList
ibbem
committed
d38fafb
Prove ADT ≤ₛ NADT
ibbem
committed
4a07f0d
Prove NADT ≤ₛ ADT
ibbem
committed
1cab421
Simplify the FixedArtifactLength lemma
ibbem
committed
3385ba9

Commits on Dec 13, 2025

Generalize the coarseness of the relationship between ≰ and ≤
ibbem
committed
ff6e993
Prove independence of size definition
ibbem
committed
0d29667

Commits on Apr 13, 2026

Commits on Apr 16, 2026

Add some useful documentation
ibbem
committed
3b90f96
Rename NoBaseArtifacts into NoCoreFeature
ibbem
committed
c5ce2f8
Merge branch 'develop' into thesis_bm
ibbem
committed
5aec4ca
Remove a lemma that is available in the standard library
ibbem
committed
b0902d2
Add my thesis to the README
ibbem
committed
f536bb1