proof that we cannot compile 2CC to OC

VariantSync · Mar 18, 2024 · 63cb116 · 63cb116
1 parent c92e731
commit 63cb116
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 2 deletions.
diff --git a/src/Framework/Relation/Expressiveness.lagda.md b/src/Framework/Relation/Expressiveness.lagda.md
@@ -3,8 +3,9 @@ open import Framework.Definitions
 module Framework.Relation.Expressiveness (V : 𝕍) where
 
 open import Data.EqIndexedSet using (≅[]→≅)
+open import Data.Empty using (⊥)
 open import Data.Product using (_,_; _×_; Σ-syntax; proj₁; proj₂)
-open import Relation.Nullary.Negation using (¬_)
+open import Relation.Nullary.Negation using (¬_; contraposition)
 open import Relation.Binary using (IsEquivalence; Reflexive; Symmetric; Transitive; Antisymmetric)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans)
 open import Function using (_∘_; Injective)
@@ -87,4 +88,10 @@ expressiveness-from-compiler : ∀ {L₁ L₂ : VariabilityLanguage V}
   → LanguageCompiler L₁ L₂
   → L₂ ≽ L₁
 expressiveness-from-compiler compiler = expressiveness-by-translation (LanguageCompiler.compile compiler) (λ e → ≅[]→≅ (LanguageCompiler.preserves compiler e))
+
+compiler-cannot-exist : ∀ {L₁ L₂ : VariabilityLanguage V}
+  → L₂ ⋡ L₁
+  → LanguageCompiler L₁ L₂
+  → ⊥
+compiler-cannot-exist = contraposition expressiveness-from-compiler
 ```
diff --git a/src/Translation/LanguageMap.lagda.md b/src/Translation/LanguageMap.lagda.md
@@ -16,6 +16,7 @@ module Translation.LanguageMap where
 
 ```agda
 open import Size using (∞)
+open import Relation.Nullary.Negation using (¬_)
 
 open import Framework.Variants using (Rose; Artifact∈ₛRose; Variant-is-VL)
 Variant = Rose ∞
@@ -24,7 +25,7 @@ mkArtifact = Artifact∈ₛRose
 open import Framework.Definitions using (𝕍; 𝔽)
 open import Framework.Construct
 open import Framework.Compiler
-open import Framework.Relation.Expressiveness Variant using (_⋡_)
+open import Framework.Relation.Expressiveness Variant using (_⋡_; compiler-cannot-exist)
 open import Framework.Proof.Transitive Variant using (less-expressive-from-completeness)
 
 open import Construct.Artifact as At using () renaming (Syntax to Artifact)
@@ -82,6 +83,9 @@ module _ (F : 𝔽) where
   OC-is-less-expressive-than-2CC : WFOCL ⋡ 2CCL
   OC-is-less-expressive-than-2CC = less-expressive-from-completeness {!!} OC-is-incomplete
 
+  2CC-cannot-be-compiled-to-OC : ¬ (LanguageCompiler 2CCL WFOCL)
+  2CC-cannot-be-compiled-to-OC = compiler-cannot-exist OC-is-less-expressive-than-2CC
+
 open Translation.Lang.OC-to-2CC using (
   2CC≽OC
   ) public