Repository navigation

Formalization of Succinctness - #98

Merged

pmbittner merged 83 commits into

developfrom

merge-thesis_bm-to-main

Apr 17, 2026

Merged

Formalization of Succinctness#98
pmbittner merged 83 commits into
developfrom
merge-thesis_bm-to-main

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
- FST≱2CC: Simplify `select-applyUpTo-feature`
  ibbem
  committed
  f93af41
- Factor out findings about fixed artifact lengths of 2CC
  ibbem
  committed
  c705abd
- Move size>0 lemmas next to the size definitions
  ibbem
  committed
  cc33f09
- Factor out the inflation constant in OC≱2CC
  ibbem
  committed
  9e5b32f
- Rename some things
  ibbem
  committed
  a8e15fb
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
- Prove that PropOC is at least as succinct as OC
  ibbem
  committed
  69a2e6f
- Remove annoying module prefixes in 2CC<ADT
  ibbem
  committed
  b3c4d3b
- Generalize the coarseness of 2CC < ADT
  ibbem
  committed
  9297133
- Add some more transitivity theorems
  ibbem
  committed
  5e053cd
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
- Remove a superfluous `--allow-unsolved-metas`
  ibbem
  committed
  348054e
- Rename some variables and lemmas in 2CC<ADT
  ibbem
  committed
  81ddeb2
- Move OC dead elimination to `Translation`
  ibbem
  committed
  4acbaf3
- Use typical option names for OC dead elimination
  ibbem
  committed
  d0585cb
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

Commits

Commits on Jul 10, 2025

Commits on Jul 12, 2025

Commits on Jul 13, 2025

Commits on Jul 14, 2025

Commits on Jul 15, 2025

Commits on Jul 22, 2025

Commits on Sep 4, 2025

Commits on Sep 7, 2025

Commits on Sep 9, 2025

Commits on Nov 11, 2025

Commits on Dec 4, 2025

Commits on Dec 9, 2025

Commits on Dec 13, 2025

Commits on Apr 13, 2026

Commits on Apr 16, 2026