Choices translations #16

ibbem · 2024-02-28T09:34:50Z

Translations (with preservation proofs) of different choice language variants (n-ary, 2-ary, arbitrary) into each other. All proofs are finished.
Note that the first commit is a result I stumbled upon during this work. It could be used to eliminate one half of each preservation proof and replace it by a possibly shorter proof that the config translations are inverses. However, this lemma will need extensionality most of the time. Hence, I avoided it for now.

There is potential to generalize the version I used here, if you ever see a dependent zipWith somewhere. I also noticed that the function cappedFin implements the same semantics as clamp, except it's defined recursively. Hence, it's easier to proof properties about it.

This is currently almost completely independent of the current code base. How do we want to integrate this?
There is a Lang.CCC module whose constructors I could reuse. However, there is no arbitrary choice language, only an arbitrary choice constructor.
Furthermore, all of this is currently in one file. Should we split all of this up into multiple modules, multiple files or keep it that way? If we split it up, we could shorten the names (e.g. to translate, conf and fnoc)?

pmbittner · 2024-02-28T15:01:26Z

Hi Benjamin,

awesome! Thank you so much. <3 Here is instructions for integrating your changes into the framework:

Please put/merge your language definitions with those in src/Lang. In src/Lang, there is one agda file for each language.
- This already includes BCC (2-ary choice calculus) and CCC (arbitrary choice calculus). It would be ideal if we could reuse exactly these definitions as they are already part of other proofs. In particular, there is already a translation Variantlist->CCC which we need for spreading completeness into the whole map. Note that both definitions, CCC and BCC, reuse the constructors defined in src/Construct. (In case this complicates reintegrating the proofs too much, inlining the constructor definitions here to get simpler languages could be an option, similar as I did for 2ADTs (temporarily) on the sound branch).
- For n-ary CC, you need to add a new file.
- Reusing BCC might require a (hopefully trivial) conversion from and to your alias 2AryChoice = NAryChoice (sucs zero). Maybe we could also replace the existing definition of BCC with your new alias, but the existing one is quite convenient for "users" and tests because of its nicer syntax, but we could even alias that with a syntax or pattern clause.
- Your proofs rely on a custom Variant type. The semantics of CCC and BCC are abstracted to any variants with artifacts. Do not bother to generalize your proofs to any such variant. You can fix them to Rose \inf, which is exactly your definition of variants. We can later generalize your proofs to any variants with artifacts (low priority, post deadline if at all).
Please put your compilers and preservation proofs into src/Translation/Lang. The other files here can serve as a reference for you. Also, please try to instantiate a LanguageCompiler according to the definition from src/Framework/Compiler.agda.
Please use your preservation proofs to conclude that these languages are equally expressive. You may do this within the files containing your compilers.

Using this opportunity to also simplify names sounds great to me. Currently, some names (e.g., for config translations) are very long and that makes everything harder to read.

If you have remarks or ideas on how to better structure the framework here, I am happy to discuss.

pmbittner

Here are some first general comments. I did not look into the actual choice proofs yet. I will do this next week in Emacs.

src/Util/Vec.agda

src/Util/List.agda

src/Util/Nat/AtLeast.agda

pmbittner · 2024-02-28T16:05:08Z

I just had a quick, superficial look at the choice file. I pushed some comments. Feel free to revert/drop/squash/whatever the commit.

ibbem · 2024-03-03T21:03:22Z

I have mostly integrated the translation into the current framework. The only thing which doesn't quite fit is the LanguageCompiler. It's currently not possible to define LanguageCompiler for CCC-to-FCC (twice, one more specialized version) and CCC-to-BCC. I have added one WIP commit which breaks a lot of other things but makes it possible to define a LanguageCompiler for all choice translations except the more specialized version of CCC-to-FCC. The problem this is currently facing is that I cannot really make a usable definition of ConstructFunctor. It seems like there needs to be a constraint isSubExpression e e' → conf e ≡ conf e' which makes sense to me conceptionally. However, I can't imagine a way to define isSubExpression if it's expressible in the current framework at all. You can play around with this problem in Construct.Choices line 234:

  ⟦ compile t (Standard-Semantics chc (extract i)) ⟧₂ (conf t (Standard-Semantics chc (extract i))
≡⟨ ? ⟩
  ⟦ compile t (Standard-Semantics chc (extract i)) ⟧₂ (conf t (cons Choice∈Γ₁ chc) i)

My current TODO list looks like this:

~~change the definition of LanguageCompiler to accomodate all needs~~
documentation
at least
- saturate
- ℕ≥
- ListChoiceLengthLimit
Formatting (especially long type signatures)
cleanup imports
reuse names from Framework.Definitions (𝔸, etc.)

pmbittner

Hi Benjamin. The reintegration looks fine to me. :) I added some comments. Let's discuss your changes this week. We can then also have a look at the necessary changes within the framework. If you need help or advice for resolving the remaining compiler errors, let me know.

src/Construct/Choices.agda

src/Framework/Compiler.agda

src/Lang/FCC.lagda.md

src/Lang/FCC.lagda.md.bak

src/Translation/Lang/BCC-to-BCC.agda

src/Translation/Lang/BCC-to-CCC.agda

pmbittner · 2024-03-05T10:20:13Z

src/Translation/Lang/FCC-to-FCC.agda

+preserves : {i : Size} → {D A : Set} → (n m : ℕ≥ 2) → (expr : FCC n D i A) → ⟦ translate n m expr ⟧ₙ ≅[ fnoc n m ][ conf n m ] ⟦ expr ⟧ₙ
+preserves (sucs n) (sucs m) expr = ≅[]-trans (IncreaseArity.preserves (sucs m) (DecreaseArity.translate (sucs n) expr)) (DecreaseArity.preserves (sucs n) expr)
+
+languageCompiler : {i : Size} → {D : Set} → (n m : ℕ≥ 2) → LanguageCompiler (FCCL n D Variant Artifact∈ₛVariant {i}) (FCCL m (IndexedDimension D n) Variant Artifact∈ₛVariant)


So this reduces an FCC n expression to a FCC 2 expression and then saturates it to a FCC m expression? :)

We should probably document this somewhen.

This actually is currently documented.

src/Translation/Lang/FCC-to-FCC.agda

src/Translation/Lang/CCC-to-BCC.agda

pmbittner · 2024-03-05T11:01:25Z

Answer to your previous comment:

I see the problem with a generalised LanguageCompiler to break existing proofs. Thank you for pointing out the little playground with this problem. I am not 100% sure yet whether cons Choice∈Γ₁ chc should be the expression to feed into the configuration compiler. It makes sense somehow but we need a clear understanding first on what a configuration compiler now actually is, needs, and satisfies. Your idea of a lemma for configuration compiler makes sense at first sight but I have also no idea on how to define isSubExpression either. My solution here would be: Ignore all the Framework V2 stuff for now (abstraction of constructors) and let's discuss the changes to LanguageCompiler and their meeting this week.

Your Todolist looks good. I added some comments, mostly concerned with more documentation. Thank you for all your effort. The results look really great and I am still surprised how extensive these proofs became. This clears our a big chunk from our TODO list from our paper.

One other half of a preservation proof can be constructed if given one direction of a translation preservation proof and a proof that the configuration translations are inverses to each other. However, this is only useful if the translation functions are extensionally equal to each other. Hence, in most cases, using this theorem will require function extensionally.

Before the translation was from `CCC` to `FCC (sucs zero)`

This makes it consistent with all other choice translations and prevents a lot of unsolved metas.

Unfortunately, this breaks `ConstructFunctor` and all code associated with it. However, the benefits of having `LanguageCompiler`s for more languages outweighs the benefits of `ConstructFunctor` because `ConstructFunctor` is hard to use and hasn't yet proved itself worth yet.

The ˡ suffix is superfluous and _⊕_ is already unambiguous in this code base.

A separate, named function makes the behaviour more clear than the expression `_∘ f`.

`ListChoiceLengthLimit-⊔-comm` is just a special case of `ListChoiceLengthLimit-⊔` and is actually only needed because `ListChoiceLengthLimit-⊔` isn't flexible enough.

This makes it obvious what this lemmas are about and keeps them from polluting the namespace.

Having a consistent naming convention which works in every case is very useful.

We need a symbol in the paper.

pmbittner

Great work! Some last nitpicky comments, which we can have a look at later, potentially in a revision of the entire code base at a later stage.

pmbittner · 2024-03-13T10:20:33Z

src/Construct/Choices.agda

  open import Data.Vec using (Vec; lookup; toList) renaming (map to map-vec)
  open import Data.Vec.Properties using (lookup-map)

-  record Syntax (n : ℕ) (Q : Set) (A : Set) : Set where
+  record Syntax (n : ℕ≥ 2) (Q : Set) (A : Set) : Set where


Good catch. The previous definition allowed zero which was in fact illegal. Only very indirectly via the existence of a configuration, the case Syntax zero was forbidden. Took me quite a while to find that. Good that you fixed it here and made it explicit.... although an unary choice would have been fine too. ;)

pmbittner · 2024-03-13T10:30:50Z

src/Lang/NCC.lagda.md

+
+## Module
+
+It's required that arity is at least one to have a semantic. However, we require


I do not think semantics has a singular.

pmbittner · 2024-03-13T10:32:23Z

src/Lang/NCC.lagda.md

+```agda
+data NCC : Size → 𝔼 where
+   atom : ∀ {i A} → Artifact (NCC i) A → NCC (↑ i) A
+   chc  : ∀ {i A} → VLNChoice.Syntax n Dimension (NCC i) A → NCC (↑ i) A


Maybe it would be simpler to use NChoice directly here instead of VLNChoice? VLNChoice is mostly a proof that choices can be modelled in the framework.

pmbittner · 2024-03-13T10:33:24Z

src/Lang/NCC.lagda.md

+open Data.List using (concatMap) renaming (_++_ to _++l_)
+import Data.Vec as Vec
+
+-- get all dimensions used in a binary CC expression


comment outdated

ibbem requested a review from pmbittner February 28, 2024 09:35

pmbittner reviewed Feb 28, 2024

View reviewed changes

src/Util/Vec.agda Show resolved Hide resolved

src/Util/Vec.agda Show resolved Hide resolved

src/Util/List.agda Show resolved Hide resolved

src/Util/Nat/AtLeast.agda Show resolved Hide resolved

ibbem force-pushed the choices-translations branch from d07010c to c5065f7 Compare March 3, 2024 20:44

pmbittner reviewed Mar 5, 2024

View reviewed changes

ibbem force-pushed the choices-translations branch from 513f6e4 to a6f7307 Compare March 10, 2024 23:44

pmbittner mentioned this pull request Mar 11, 2024

2ADT -> VariantList #18

Merged

3 tasks

ibbem force-pushed the choices-translations branch from a6f7307 to 1fea5fc Compare March 11, 2024 20:08

ibbem added 19 commits March 13, 2024 09:22

Translate between all different choice language variants

b80f570

Split the choices translations into multiple files

8b9044c

Shorten the choice translation names

e591c9d

Replace ArbitraryChoice by the preexisting CCC data type

b759ebe

Replace NAryChoice by an integrated Choice-Fix data type

785e4f4

Translate FCC to BCC

0bfe070

Add missing conf and fnoc aliases

fa2a6b3

Actually translate CCC to BCC

32061d6

Before the translation was from `CCC` to `FCC (sucs zero)`

Generalize the choice translations to arbitrary variants

a811988

Translate BCC to FCC

ba1456e

Make the arity parameter of FCC-to-CCC explicit

5f0872b

This makes it consistent with all other choice translations and prevents a lot of unsolved metas.

Translate BCC to CCC

5b09474

Generalize the size constraint of the choice translations

6dc7eef

Factor out IndexedDimension

50c27f9

Generalize BCC to FCC

1afabc5

Generalize CCC to FCC

38bfe62

Instantiate LanguageCompiler for choice translations

b720d26

Conclude expressiveness

4ee1074

ibbem added 19 commits March 13, 2024 09:22

Rename _⊕ˡ_ to _⊕_

072954c

The ˡ suffix is superfluous and _⊕_ is already unambiguous in this code base.

Use LanguageCompiler composition where possible

d020c6f

Cleanup choice translation imports

c5ac8c3

Simplify the BCC ≽ OC expressiveness proof

abdd27e

Factor out configuration dimension maps

0eb7a4e

A separate, named function makes the behaviour more clear than the expression `_∘ f`.

Rename Choices to 2Choice, NChoice and Choice

d2afb70

Improve formatting of the choice translations

796ad84

Generalize ListChoiceLengthLimit-⊔

24c1e21

`ListChoiceLengthLimit-⊔-comm` is just a special case of `ListChoiceLengthLimit-⊔` and is actually only needed because `ListChoiceLengthLimit-⊔` isn't flexible enough.

Reuse maximumIsLimit in maximum⁺IsLimit

cc6a073

Document the choice translations

92c50be

Create separate conf and fnoc lemma modules for NCC-to-NCC

5325579

This makes it obvious what this lemmas are about and keeps them from polluting the namespace.

Rename *ꟲ-map-dim to *-map-config

b605cdb

Use qualified names instead suffixes for ⟦_⟧

d145885

Having a consistent naming convention which works in every case is very useful.

Calculate the exact maximum number of alternatives

5f883a5

Rename maxChoiceLength to ⌈_⌉

45debd9

We need a symbol in the paper.

Rename ChoiceLenghtLimit to NumberOfAlternatives≤

5a2f85e

Use Framework.Definitions in the choice translations

791ba80

Make CCC-to-NCC a little bit more readable

c755f84

ibbem force-pushed the choices-translations branch from 1fea5fc to c755f84 Compare March 13, 2024 08:22

ibbem mentioned this pull request Mar 13, 2024

Compile 2CC into 2ADT #19

Merged

ibbem requested a review from pmbittner March 13, 2024 09:12

pmbittner approved these changes Mar 13, 2024

View reviewed changes

pmbittner merged commit 81cf3ea into develop Mar 13, 2024
1 check passed

pmbittner deleted the choices-translations branch March 13, 2024 11:57

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Choices translations #16

Choices translations #16

ibbem commented Feb 28, 2024

pmbittner commented Feb 28, 2024 •

edited

Loading

pmbittner left a comment

pmbittner commented Feb 28, 2024

ibbem commented Mar 3, 2024 •

edited

Loading

pmbittner left a comment

pmbittner Mar 5, 2024

ibbem Mar 13, 2024

pmbittner Mar 13, 2024

ibbem Mar 13, 2024

pmbittner commented Mar 5, 2024

pmbittner left a comment

pmbittner Mar 13, 2024

pmbittner Mar 13, 2024

pmbittner Mar 13, 2024

pmbittner Mar 13, 2024


		## Module

		It's required that arity is at least one to have a semantic. However, we require

Choices translations #16

Choices translations #16

Conversation

ibbem commented Feb 28, 2024

pmbittner commented Feb 28, 2024 • edited Loading

pmbittner left a comment

Choose a reason for hiding this comment

pmbittner commented Feb 28, 2024

ibbem commented Mar 3, 2024 • edited Loading

pmbittner left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pmbittner commented Mar 5, 2024

pmbittner left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pmbittner commented Feb 28, 2024 •

edited

Loading

ibbem commented Mar 3, 2024 •

edited

Loading