Translate FST to VariantList and disprove translation to OC #35

ibbem · 2024-05-20T21:44:53Z

No description provided.

pmbittner

thank you for the proofs! I appreciate the documentation for the proof idea of FST -/-> OC but was left a bit confused.

pmbittner · 2024-05-21T05:38:56Z

src/Lang/OC/Subtree.agda

+data MaybeSubtree {A : 𝔸} : Maybe (Rose ∞ A) → Maybe (Rose ∞ A) → Set₁ where
+  neither : MaybeSubtree nothing nothing
+  one : {c : Rose ∞ A} → MaybeSubtree nothing (just c)
+  both : {c₁ c₂ : Rose ∞ A} → Subtree c₁ c₂ → MaybeSubtree (just c₁) (just c₂)


Please document the purpose of this predicate.

pmbittner · 2024-05-21T05:39:59Z

src/Lang/OC/Subtree.agda

+  both : {c₁ c₂ : Rose ∞ A} → Subtree c₁ c₂ → MaybeSubtree (just c₁) (just c₂)
+
+Implies : {F : 𝔽} → Configuration F → Configuration F → Set
+Implies {F} c₁ c₂ = (f : F) → c₁ f ≡ true → c₂ f ≡ true


I wonder if this theorem could be generalized to any configuration language. We have a similar relation for configurations defined for the ADT translation, based on paths. There is nothing to change here. I was just wondering.

The predicate Implies could indeed be generalized for any configuration which is a function to Bool (e.g., 2CC). However, the subtree theorem is false for any other language in our language map except FST because they can encode alternatives. Alternatives do invalidate this theorem because setting a feature to false can add new subtrees.

I have search a bit in the standard library right now but didn't find a definition which fits Implies nicely. However there is _≤_ in Data.Bool which we could reuse. Do you think this is a good idea? The new definition would be

Implies : {F : 𝔽} → Configuration F → Configuration F → Set Implies {F} c₁ c₂ = (f : F) → c₁ f ≤ c₂ f

I haven't yet investigated how the proofs would change if we adopted _≤_.

Oh interesting! Maybe it would make sense to turn what you wrote here into a comment on this predicate.

I do not see a real benefit from using the standard-library here. It does not improve readability and if we do not make use of more features from the STL, it is probably simpler to just stick to what we have currently.

pmbittner · 2024-05-21T05:42:48Z

src/Lang/OC/Subtree.agda

+  ... | .nothing | just c' | one = c' ∷ʳ subtreeₒ-recurse cs c₁ c₂ c₁-implies-c₂
+  ... | .(just _) | .(just _) | both p = p ∷ subtreeₒ-recurse cs c₁ c₂ c₁-implies-c₂
+
+subtree : ∀ {F : 𝔽} {A : 𝔸} → (e : WFOC F ∞ A) → (c₁ c₂ : Configuration F) → Implies c₁ c₂ → Subtree (⟦ e ⟧ c₁) (⟦ e ⟧ c₂)


That's a great theorem. :) Can you add a short documentation (including a short description on why this is true)?

Is it enough to add documentation to subtree or should subtreeₒ and subtreeₒ-recurse also have documentation?

I guess the more the better. It is probably hard to document subtree's workings without documenting the other two functions? 🤔

src/Translation/Lang/FST-to-OC.agda

pmbittner · 2024-05-21T06:12:48Z

src/Translation/Lang/FST-to-OC.agda

+shared-artifact (f OC.❲ e ❳) c₁ c₂ p₁ p₂ with c₁ f | c₂ f
+shared-artifact (f OC.❲ e ❳) c₁ c₂ p₁ p₂ | true | true = shared-artifact e c₁ c₂ p₁ p₂
+
+-- This is the main induction over the top most children of the OC expression.


Great! :) Can you again shortly phrase what it is that we prove with this induction? This theorem is not obvious and it is not the final result yet.

pmbittner · 2024-05-21T06:14:10Z

src/Translation/Lang/FST-to-OC.agda

+-- all true configuration.
+--
+-- If an option evaluates to an artifact for both `c₁` and `c₂` it must also
+-- evaluate to an artifact for the intersection of these configurations. The


"interesection" in terms of _∧_ right?

Maybe add a short comment for that: (in terms of _∧_).

pmbittner · 2024-05-21T06:23:22Z

src/Translation/LanguageMap.lagda.md

@@ -269,6 +270,15 @@ module Completeness {F : 𝔽} (f : F × ℕ → F) (f⁻¹ : F → F × ℕ) (f

  OC-cannot-be-compiled-to-FST : ¬ (LanguageCompiler (WFOCL F) (FSTL F))
  OC-cannot-be-compiled-to-FST = compiler-cannot-exist FST-is-less-expressive-than-OC
+
+  module _ {F' : 𝔽} (f₁ f₂ : F') (f₁≢f₂ : f₁ ≢ f₂) (_==ꟳ_ : DecidableEquality F') where


Maybe we should shortly document here what these assumptions are and why they are reasonable. String and Nat obviously satisfy them.

pmbittner · 2024-05-21T06:26:06Z

I still have to review the last commit [Translate FST to VariantList](https://github.com/pmbittner/AgdaCCnOC/pull/35/commits/0b3868b08c86cc7df01e2c066c1c3ec96630fb30) but I have to exit my train now. :D

pmbittner · 2024-05-23T08:19:59Z

Hi @ibbem ,

thanks for the beautiful translation and proof of FST -> VariantList. I figured it would be easier this time to put my comments directly into the Agda file. I added some documentation but only got through half of the file. I will continue later.

Please have a look at my commit. Is my documentation correct? Also search for @ibbem: It would be great if you could write the documentation in these places.

pmbittner · 2024-05-23T08:20:42Z

Also I am experiences build problems with nix currently. I get hundreds of these errors on this branch

/home/paul/projects/AgdaCCnOC/src/MAlonzo/Code/Util/String.hs:112:30: error: [GHC-76037]
    Not in scope:
      data constructor ‘MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32’
    NB: the module ‘MAlonzo.Code.Relation.Nullary.Decidable.Core’ does not export ‘C__because__32’.
    Suggested fix:
      Perhaps use ‘MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__34’ (imported from MAlonzo.Code.Relation.Nullary.Decidable.Core)
    |
112 |                              MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v5 v6
    |                              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

It seems there are many things in the standard library, which cannot be found.

ibbem · 2024-05-24T07:26:47Z

Also I am experiences build problems with nix currently. I get hundreds of these errors on this branch

This has nothing to do with Nix 😇. It's a cache invalidation problem of Agda. In particular, Agda generated the src/MAlonzo folder which is now out of date. Just delete it. Agda will regenerate it with the updated versions of these files.

ibbem · 2024-05-24T07:31:17Z

I figured it would be easier this time to put my comments directly into the Agda file.

Nice! I think I prefer this way. In contrast to GitHub, I can use all power of Git to look and filter comments. This is especially nice for finding where these comments actually apply because I don't need to move from the GitHub interface to my Editor when I need to address something.

The only drawback is a kind of weird Git history in case you also add change request that way.

pmbittner · 2024-05-24T07:53:06Z

Also I am experiences build problems with nix currently. I get hundreds of these errors on this branch

This has nothing to do with Nix 😇. It's a cache invalidation problem of Agda. In particular, Agda generated the src/MAlonzo folder which is now out of date. Just delete it. Agda will regenerate it with the updated versions of these files.

Ok great! I will try that. Maybe this is something for a "Troubleshooting" section for a potential future artifact submission, as well as something work putting into the makefile (make clear). I will do that.

Edit: We already have make clean :)

Edit: This solved the problem indeed.

pmbittner · 2024-05-24T07:55:08Z

I figured it would be easier this time to put my comments directly into the Agda file.

Nice! I think I prefer this way. In contrast to GitHub, I can use all power of Git to look and filter comments. This is especially nice for finding where these comments actually apply because I don't need to move from the GitHub interface to my Editor when I need to address something.

The only drawback is a kind of weird Git history in case you also add change request that way.

Ok then let's try this kind of reviews more in the future. Another drawback could be that it might be less transparent for working in parallel. For example, I would like to continue commenting on your PR but I also don't want to introduce merge conflicts. (Maybe though, this problem is less bad as it sounds though.)

ibbem · 2024-05-24T12:04:48Z

I figured it would be easier this time to put my comments directly into the Agda file.

Nice! I think I prefer this way. In contrast to GitHub, I can use all power of Git to look and filter comments. This is especially nice for finding where these comments actually apply because I don't need to move from the GitHub interface to my Editor when I need to address something.
The only drawback is a kind of weird Git history in case you also add change request that way.

Ok then let's try this kind of reviews more in the future. Another drawback could be that it might be less transparent for working in parallel. For example, I would like to continue commenting on your PR but I also don't want to introduce merge conflicts. (Maybe though, this problem is less bad as it sounds though.)

I'm fine with solving such merge conflicts. There shouldn't be too many most of the time because one reviewer will most likely (re-)review parts are new or are changed. Except of course for big changes (e.g., renaming a file, like I will do soon 😅)

Note that this commit includes some unused lemmas. I proved them while trying to prove the actual theorem but found a better approach. They might be useful in the future, so I decided to keep them for now.

pmbittner · 2024-05-27T10:21:42Z

Hi @ibbem ,

I just pushed some revisions and TODOs. Please check my additions. Please replace the TODO ibbem commits with commits that resolve the respective TODOs.

If you are done, please merge. I think the PR looks great now. :)

spell out the conf'-lemma in natural language.

This makes distinguishing the important parts of the theorem from introduced names.

ibbem force-pushed the translate-from-FST branch from a0eb03f to 0b3868b Compare May 20, 2024 21:55

pmbittner requested changes May 21, 2024

View reviewed changes

ibbem force-pushed the translate-from-FST branch from cd3512c to 530470e Compare May 24, 2024 13:18

ibbem and others added 10 commits May 24, 2024 16:56

Proof WFOCL ⋡ FSTL

0969b50

Note that this commit includes some unused lemmas. I proved them while trying to prove the actual theorem but found a better approach. They might be useful in the future, so I decided to keep them for now.

Reexport VariantList completeness and soundness in LanguageMap

d6b0990

Translate FST to VariantList

21d0b8f

doc: some documentation in FST-to-VariantList

1d8b9b8

doc: Document the OC subtree lemma

fcefa74

Use literate Agda files for FST-to-OC and Subtree

72028c7

Use integer literals if they are only used as example data

d4660e3

doc: Add a little bit more documentation to the subtree theorem

722d575

doc: Move the motivation for the module parameters to the top

a9f7c7e

doc: Copy editing of FST-to-OC documentation

1baaae9

ibbem force-pushed the translate-from-FST branch from c5dd62a to bacf830 Compare May 24, 2024 14:56

ibbem and others added 7 commits May 27, 2024 22:48

doc: Clarify a few bits in FST-to-OC

bcdf63e

doc: Add some more comments to FST-to-VariantList

5e2bf84

Simplify FST-to-VariantList.⟦⟧-cong a little bit

cf0638d

markdown and documentation improvements

60df8ae

fix some typos

1ed15be

align with

1aaba49

docs: FST-to-VariantList

9bb0960

spell out the conf'-lemma in natural language.

pmbittner and others added 4 commits May 27, 2024 22:48

style: use inference rule style for conf'-lemma

843e164

This makes distinguishing the important parts of the theorem from introduced names.

docs: observation on ⟦⟧-cong

b7e49f4

Conclude 2CC≽FST by transitivity

039fcac

doc: Clarify the precondition of the conf'-lemma

3ca7c93

ibbem force-pushed the translate-from-FST branch from 58cb9e1 to 3ca7c93 Compare May 27, 2024 21:02

ibbem merged commit 7d75889 into develop May 27, 2024
1 check passed

ibbem deleted the translate-from-FST branch May 27, 2024 21:13

ibbem mentioned this pull request May 29, 2024

Clarify what "choosing a configuration" in the FST-to-OC proof means #38

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Translate FST to VariantList and disprove translation to OC #35

Translate FST to VariantList and disprove translation to OC #35

ibbem commented May 20, 2024

pmbittner left a comment

pmbittner May 21, 2024

pmbittner May 21, 2024

ibbem May 24, 2024

pmbittner May 27, 2024

pmbittner May 21, 2024

ibbem May 24, 2024

pmbittner May 24, 2024

pmbittner May 21, 2024

pmbittner May 21, 2024

ibbem May 24, 2024

pmbittner May 27, 2024

pmbittner May 21, 2024

pmbittner commented May 21, 2024

pmbittner commented May 23, 2024

pmbittner commented May 23, 2024 •

edited

Loading

ibbem commented May 24, 2024

ibbem commented May 24, 2024 •

edited

Loading

pmbittner commented May 24, 2024 •

edited

Loading

pmbittner commented May 24, 2024

ibbem commented May 24, 2024

pmbittner commented May 27, 2024

Translate FST to VariantList and disprove translation to OC #35

Translate FST to VariantList and disprove translation to OC #35

Conversation

ibbem commented May 20, 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

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pmbittner commented May 21, 2024

pmbittner commented May 23, 2024

pmbittner commented May 23, 2024 • edited Loading

ibbem commented May 24, 2024

ibbem commented May 24, 2024 • edited Loading

pmbittner commented May 24, 2024 • edited Loading

pmbittner commented May 24, 2024

ibbem commented May 24, 2024

pmbittner commented May 27, 2024

pmbittner commented May 23, 2024 •

edited

Loading

ibbem commented May 24, 2024 •

edited

Loading

pmbittner commented May 24, 2024 •

edited

Loading