diff --git a/src/AOP/Divisoids.agda b/src/AOP/Divisoids.agda new file mode 100644 index 0000000..a815358 --- /dev/null +++ b/src/AOP/Divisoids.agda @@ -0,0 +1,130 @@ +open import Relation.Binary.PropositionalEquality +open import Data.Product +open import Data.Empty + +record Divisoid (X : Set) : Set₁ where + field + _↝_⊕_ : X → X → X → Set + ε : X + split-sym : ∀{x a b} → x ↝ a ⊕ b → x ↝ b ⊕ a + split-ident₁ : ∀{x y} → x ↝ ε ⊕ y → x ≡ y + split-ident₂ : ∀{x} → x ↝ ε ⊕ x + split-split : {x a b a₁ b₁ a₂ b₂ : X} → x ↝ a ⊕ b → a ↝ a₁ ⊕ a₂ → b ↝ b₁ ⊕ b₂ + → ∃[ x₁ ] ∃[ x₂ ] x ↝ x₁ ⊕ x₂ × x₁ ↝ a₁ ⊕ b₁ × x₂ ↝ a₂ ⊕ b₂ + + variable a a₁ b₁ a₂ b₂ b c d x y : X + + split-genL : (x ↝ a ⊕ b) → (a ↝ a₁ ⊕ a₂) → ∃[ q ] (x ↝ a₁ ⊕ q) × (q ↝ a₂ ⊕ b) + split-genL x-split a-split with split-split x-split a-split split-ident₂ + split-genL {x = x} x-split a-split | x₁ , x₂ , x-split' , x₁-split , x₂-split = + -- goal: a₁ = a₁ / a₂ = a₂ / b₁ = ε / b₂ = b + -- then, q will just be x₂ + let x₁≡a₁ = split-ident₁ (split-sym x₁-split) in + x₂ , subst (λ d → x ↝ d ⊕ x₂) x₁≡a₁ x-split' , x₂-split + + split-genR : x ↝ a ⊕ b → b ↝ c ⊕ d → ∃[ q ] x ↝ q ⊕ d × q ↝ a ⊕ c + split-genR x-split b-split with split-split x-split (split-sym split-ident₂) b-split + split-genR {x = x} x-split b-split | x₁ , x₂ , x-split' , x₁-split , x₂-split = + -- same thing as above + let x₂≡d = split-ident₁ x₂-split in + x₁ , subst (λ e → x ↝ x₁ ⊕ e) x₂≡d x-split' , x₁-split + +open import Data.Maybe +open import Data.Maybe.Properties + +infixl 10 _∙_ +_∙_ = trans + +record PartialCommMonoid (X : Set) : Set₁ where + field + _·_ : X → X → Maybe X + ε : X + _·′_ : Maybe X → Maybe X → Maybe X + a ·′ b = a >>= λ x → b >>= (x ·_) + field + ·-comm : ∀{a b} → a · b ≡ b · a + ·-ident : ∀{x} → ε · x ≡ just x + ·-assoc : ∀{a b c} → (a · b) ·′ just c ≡ just a ·′ (b · c) + variable a a₁ b₁ a₂ b₂ b c d x y : X + + pcm-divis : Divisoid X + pcm-divis = record + { _↝_⊕_ = λ x a b → just x ≡ a · b + ; ε = ε + ; split-sym = λ p → p ∙ ·-comm + ; split-ident₁ = split-ident₁ + ; split-ident₂ = sym ·-ident + ; split-split = split-split + } where + split-ident₁ : {x y : X} → just x ≡ (ε · y) → x ≡ y + split-ident₁ p = just-injective (p ∙ ·-ident) + + split-split : {x a b a₁ b₁ a₂ b₂ : X} → just x ≡ (a · b) → just a ≡ (a₁ · a₂) → just b ≡ (b₁ · b₂) → ∃[ x₁ ] ∃[ x₂ ] just x ≡ (x₁ · x₂) × just x₁ ≡ (a₁ · b₁) × just x₂ ≡ (a₂ · b₂) + split-split {x} {a} {b} {a₁} {b₁} {a₂} {b₂} x-split a-split b-split = x₁ , x₂ , xproof , x1w .proj₂ , x2w .proj₂ where + -- This is probably the least elegant way to do this + + open import Data.Maybe.Relation.Unary.Any renaming (just to anyjust) + open import Data.Unit + + a·b-is-just = subst Is-just x-split (anyjust tt) + a₁∙a₂-is-just = subst Is-just a-split (anyjust tt) + b₁∙b₂-is-just = subst Is-just b-split (anyjust tt) + + ·-all-just : ∀ {a b} → Is-just (a ·′ b) → Is-just a × Is-just b + ·-all-just {just x} {just y} p = (anyjust tt) , anyjust tt + + ·-assoc-just : ∀ {a b c} → Is-just (a · b) → Is-just ((a · b) ·′ just c) → Is-just (b · c) × Is-just (just a ·′ (b · c)) + ·-assoc-just {a} {b} {c} p q = + let associated = subst Is-just ·-assoc q in + let bcjust = ·-all-just {a = just a} {b = b · c} associated .proj₂ in + bcjust , associated + + force-assoc : ∀ {a b c : Maybe X} → Is-just ((a ·′ b) ·′ c) → (a ·′ b) ·′ c ≡ a ·′ (b ·′ c) × Is-just (a ·′ (b ·′ c)) + force-assoc {a} {b} {c} p = helper p (all-just-ab .proj₁) (all-just-ab .proj₂) (all-just .proj₂) where + all-just = ·-all-just {a = a ·′ b} {b = c} p + all-just-ab = ·-all-just {a = a} {b = b} (all-just .proj₁) + helper : ∀ {a b c} → Is-just ((a ·′ b) ·′ c) → Is-just a → Is-just b → Is-just c → ((a ·′ b) ·′ c) ≡ (a ·′ (b ·′ c)) × Is-just (a ·′ (b ·′ c)) + helper abcj (anyjust x) (anyjust x₁) (anyjust x₂) = ·-assoc , subst Is-just ·-assoc abcj + force-assoc-sym : ∀ {a b c : Maybe X} → Is-just (a ·′ (b ·′ c)) → a ·′ (b ·′ c) ≡ (a ·′ b) ·′ c × Is-just ((a ·′ b) ·′ c) + force-assoc-sym {a} {b} {c} p = helper p (all-just .proj₁) (all-just-bc .proj₁) (all-just-bc .proj₂) where + all-just = ·-all-just {a = a} {b = b ·′ c} p + all-just-bc = ·-all-just {a = b} {b = c} (all-just .proj₂) + helper : ∀ {a b c} → Is-just (a ·′ (b ·′ c)) → Is-just a → Is-just b → Is-just c → a ·′ (b ·′ c) ≡ (a ·′ b) ·′ c × Is-just ((a ·′ b) ·′ c) + helper abcj (anyjust x) (anyjust x₁) (anyjust x₂) = (sym ·-assoc) , (subst Is-just (sym ·-assoc) abcj) + + [a₁a₂][b₁b₂]-is-just : Is-just ((a₁ · a₂) ·′ (b₁ · b₂)) + [a₁a₂][b₁b₂]-is-just = subst Is-just (x-split ∙ cong₂ _·′_ a-split b-split) (anyjust tt) + + a₁[a₂[b₁b₂]]-is-just : Is-just (just a₁ ·′ (just a₂ ·′ (b₁ · b₂))) + a₁[a₂[b₁b₂]]-is-just = force-assoc {a = just a₁} {b = just a₂} {c = b₁ · b₂} [a₁a₂][b₁b₂]-is-just .proj₂ + + a₁[[a₂b₁]b₂]-is-just : Is-just (just a₁ ·′ ((a₂ · b₁) ·′ just b₂)) + a₁[[a₂b₁]b₂]-is-just = subst (λ x → Is-just (just a₁ ·′ x)) (sym ·-assoc) a₁[a₂[b₁b₂]]-is-just + + a₁[[b₁a₂]b₂]-is-just : Is-just (just a₁ ·′ ((b₁ · a₂) ·′ just b₂)) + a₁[[b₁a₂]b₂]-is-just = subst (λ x → Is-just (just a₁ ·′ (x ·′ just b₂))) ·-comm a₁[[a₂b₁]b₂]-is-just + + a₁[b₁[a₂b₂]]-is-just : Is-just (just a₁ ·′ (just b₁ ·′ (a₂ · b₂))) + a₁[b₁[a₂b₂]]-is-just = subst (λ x → Is-just (just a₁ ·′ x)) ·-assoc a₁[[b₁a₂]b₂]-is-just + + [a₁b₁][a₂b₂]-is-just : Is-just ((a₁ · b₁) ·′ (a₂ · b₂)) + [a₁b₁][a₂b₂]-is-just = force-assoc-sym {a = just a₁} {b = just b₁} {c = a₂ · b₂} a₁[b₁[a₂b₂]]-is-just .proj₂ + + witness2 : ∀ {m : Maybe X} → Is-just m → Σ X (λ x → just x ≡ m) + witness2 (anyjust {x = x} _) = x , refl + + xsplit : just x ≡ (a₁ · b₁) ·′ (a₂ · b₂) + xsplit = x-split ∙ cong₂ _·′_ a-split b-split + ∙ force-assoc {a = just a₁} {b = just a₂} {c = b₁ · b₂} [a₁a₂][b₁b₂]-is-just .proj₁ + ∙ cong (just a₁ ·′_) (sym ·-assoc ∙ cong (_·′ just b₂) ·-comm ∙ ·-assoc) + ∙ force-assoc-sym {a = just a₁} {b = just b₁} {c = a₂ · b₂} a₁[b₁[a₂b₂]]-is-just .proj₁ + + just-pieces = ·-all-just {a = a₁ · b₁} {b = a₂ · b₂} [a₁b₁][a₂b₂]-is-just + x1w = witness2 (just-pieces .proj₁) + x2w = witness2 (just-pieces .proj₂) + + x₁ = x1w .proj₁ + x₂ = x2w .proj₁ + + xproof : just x ≡ x₁ · x₂ + xproof = subst₂ (λ z1 z2 → just x ≡ (z1 ·′ z2)) (sym (x1w .proj₂)) (sym (x2w .proj₂)) xsplit \ No newline at end of file diff --git a/src/AOP/NBE.agda b/src/AOP/NBE.agda new file mode 100644 index 0000000..c9013fd --- /dev/null +++ b/src/AOP/NBE.agda @@ -0,0 +1,60 @@ +module NBE where + +open import Data.Nat + +-- Consider this encoding of natural numbers +data SNat : Set where + zero : SNat + one : SNat + add : SNat → SNat → SNat + +variable + x x' y y' z z' : SNat + +-- Along with a specification for when two natural numbers are equal +data _≈_ : SNat → SNat → Set where + add-zero : add zero x ≈ x + add-one : add one x ≈ add x one + add-any : add (add x y) z ≈ add x (add y z) + ≈-refl : x ≈ x + ≈-sym : x ≈ y → y ≈ x + ≈-trans : x ≈ y → y ≈ z → x ≈ z + ≈-cong : x ≈ x' → y ≈ y' → add x y ≈ add x' y' + +-- +-- Our encoding is rather sloppy because it allows +-- suboptimal representation of natural numbers. +-- + +-- observe, for e.g., it alows: +zero' : SNat +zero' = add zero (add zero zero) + +-- zero' should really just be zero! + +-- observe that the spec agrees: +_ : zero' ≈ zero +_ = ≈-trans add-zero add-zero + +-- let's write a *correct* optimizer for our sloppy encoding in three phases: +-- +-- 1. evaluation: compiling our sloppy nats into Agda's default and optimal nats +-- 2. reification: reconstructing optimal nats in our original encoding +-- 3. correctness: prove that optimisation is correct +-- + +-- phase 1: evaluation +eval : SNat → ℕ +eval x = {!!} + +-- phase 2: reification +reify : ℕ → SNat +reify n = {!!} + +-- optimisation is just composition! hurray! +optimise : SNat → SNat +optimise x = reify (eval x) + +-- phase 3: correctness +correct : ∀ x → optimise x ≈ x +correct x = {!!}