Skip to content

Commit

Permalink
SCP-1960 properties of ECs, EC style reduction and CC machine (Inters…
Browse files Browse the repository at this point in the history 
…ectMBO#2756)

* stacks, frames, experimenting with properties

* inductive representation of closing/factoring a evaluation context

* notboth for inductive eval ctx closure/factoring

* determinism of inductive evalctx style reduction

* change of direction lemma for CK

* some lemmas for stack style reduction and values

* possible high level structure of reduction -> CC, alt. version of `E [ E' ]`

* monoid and functor laws for eval ctx, fusion with frames

* E [ E' ] is the same whether by recursion on E or E'

* dissecting an extension gives you back the pieces and (E , E'[A]) -CC-> (E[E'],A)

* tidying/reorganising lemmas

* recursive closing of eval ctxs in reduction, progress, notboth

* a sketch of determinism of reduction for functional/recursive EC closure
  • Loading branch information
@jmchapman
jmchapman authored Mar 1, 2021
1 parent 7bc3c68 commit b389d71
Show file tree
Hide file tree
Showing 5 changed files with 1,298 additions and 43 deletions.
185 changes: 163 additions & 22 deletions plutus-metatheory/src/Type/CC.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,8 @@ open import Data.Product
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Data.Sum
-- expose the bottom inner layer of the evalctx
dissect : (E : EvalCtx K J) → K ≡ J ⊎ Σ Kind λ I → EvalCtx K I × Frame I J
dissect [] = inj₁ refl
Expand All @@ -43,18 +45,23 @@ dissect (μl E B) with dissect E
... | inj₁ refl = inj₂ (-, [] , μ- B)
... | inj₂ (_ , E' , f) = inj₂ (-, μl E' B , f)
lemma : (E : EvalCtx K J)(F : Frame J I)
→ dissect (extendEvalCtx E F) ≡ inj₂ (-, E , F)
lemma [] (-· x) = refl
lemma [] (x ·-) = refl
lemma [] (-⇒ x) = refl
lemma [] (x ⇒-) = refl
lemma [] (μ- B) = refl
lemma [] μ x - = refl
lemma (x ·r E) F rewrite lemma E F = refl
lemma (E l· x) F rewrite lemma E F = refl
lemma (x ⇒r E) F rewrite lemma E F = refl
lemma (E l⇒ x) F rewrite lemma E F = refl
lemma (μr x E) F rewrite lemma E F = refl
lemma (μl E B) F rewrite lemma E F = refl
-- this reaches down inside the evaluation context and changes the
-- scope of the hole
--
-- it could also take a frame instead of an evalctx as it's second arg
focusEvalCtx : EvalCtx K J → EvalCtx J I → EvalCtx K I
focusEvalCtx [] E' = E'
focusEvalCtx (V ·r E) E' = V ·r focusEvalCtx E E'
focusEvalCtx (E l· B) E' = focusEvalCtx E E' l· B
focusEvalCtx (V ⇒r E) E' = V ⇒r focusEvalCtx E E'
focusEvalCtx (E l⇒ B) E' = focusEvalCtx E E' l⇒ B
focusEvalCtx (μr V E) E' = μr V (focusEvalCtx E E')
focusEvalCtx (μl E B) E' = μl (focusEvalCtx E E') B
```

```
Expand All @@ -80,21 +87,155 @@ outer type which is preserved. The second index `J/J'` refers to the
kind of the subtype in focus which may change.

```
helper : {A : ∅ ⊢⋆ J}(V : Value⋆ A)
→ K ≡ J ⊎ Σ Kind (λ I → EvalCtx K I × Frame I J)
→ ∃ (State K)
helper V (inj₁ refl) = -, □ V
helper V (inj₂ (_ , E' , -· B)) = -, extendEvalCtx E' (V ·-) ▻ B
helper V (inj₂ (_ , E' , (V-ƛ N ·-))) = -, E' ▻ (N [ discharge V ])
helper V (inj₂ (_ , E' , -⇒ B)) = -, extendEvalCtx E' (V ⇒-) ▻ B
helper V (inj₂ (_ , E' , W ⇒-)) = -, E' ◅ (W V-⇒ V)
helper V (inj₂ (_ , E' , μ- B)) = -, extendEvalCtx E' (μ V -) ▻ B
helper V (inj₂ (_ , E' , μ W -)) = -, E' ◅ V-μ W V
step : State K J → ∃ λ J' → State K J'
step (E ▻ Π A) = -, E ◅ V-Π A
step (E ▻ (A ⇒ B)) = -, focusEvalCtx E ([] l⇒ B) ▻ A
step (E ▻ (A ⇒ B)) = -, compEvalCtx' E ([] l⇒ B) ▻ A
step (E ▻ ƛ A) = -, E ◅ V-ƛ A
step (E ▻ (A · B)) = -, focusEvalCtx E ([] l· B) ▻ A
step (E ▻ μ A B) = -, focusEvalCtx E (μl [] B) ▻ A
step (E ▻ (A · B)) = -, compEvalCtx' E ([] l· B) ▻ A
step (E ▻ μ A B) = -, compEvalCtx' E (μl [] B) ▻ A
step (E ▻ con c) = -, E ◅ V-con c
step (□ V) = -, □ V
step (E ◅ V) with dissect E
... | inj₁ refl = -, □ V
... | inj₂ (_ , E' , -· B) = -, focusEvalCtx E' (V ·r []) ▻ B
... | inj₂ (_ , E' , (V-ƛ N ·-)) =
-, E' ▻ (N [ discharge V ])
... | inj₂ (_ , E' , -⇒ B) = -, focusEvalCtx E' (V ⇒r []) ▻ B
... | inj₂ (_ , E' , W ⇒-) = -, E' ◅ (W V-⇒ V)
... | inj₂ (_ , E' , μ- B) = -, focusEvalCtx E' (μr V []) ▻ B
... | inj₂ (_ , E' , μ W -) = -, E' ◅ V-μ W V
-- v we look at the E to decide what to do...
step (E ◅ V) = helper V (dissect E)
```

```
variable I' : Kind
data _-→s_ : State K J → State K I → Set where
base : {s : State K J}
→ s -→s s
step* : {s : State K J}{s' : State K I}{s'' : State K I'}
→ step s ≡ (I , s')
→ s' -→s s''
→ s -→s s''
step** : {s : State K J}{s' : State K I}{s'' : State K I'}
→ s -→s s'
→ s' -→s s''
→ s -→s s''
step** base q = q
step** (step* x p) q = step* x (step** p q)
variable J' : Kind
subst-step* : {s : State K J}{s' : State K J'}{s'' : State K I}
→ _≡_ {A = Σ Kind (State K)} (J , s) (J' , s')
→ s' -→s s''
→ s -→s s''
subst-step* refl q = q
variable K' : Kind
helper·-lem : ∀(E : EvalCtx K J)(E' : EvalCtx K' I) B {A' : ∅ ⊢⋆ K' ⇒ J}(V : Value⋆ A') →
helper V (dissect (extendEvalCtx E (-· B))) ≡ (K' , extendEvalCtx E (V ·-) ▻ B)
helper·-lem E E' B V rewrite lemma E (-· B) = refl
helper⇒r-lem : ∀(E : EvalCtx K *){B}(W : Value⋆ B){A'}(V : Value⋆ A') →
helper W (dissect (extendEvalCtx E (V ⇒-))) ≡ (* , E ◅ (V V-⇒ W))
helper⇒r-lem E W V rewrite lemma E (V ⇒-) = refl
helper⇒l-lem : ∀(E : EvalCtx K *) B {A'}(V : Value⋆ A') →
helper V (dissect (extendEvalCtx E (-⇒ B))) ≡ (* , extendEvalCtx E (V ⇒-) ▻ B)
helper⇒l-lem E B V rewrite lemma E (-⇒ B) = refl
helperμl-lem : ∀(E : EvalCtx K _)(B : ∅ ⊢⋆ J){A'}(V : Value⋆ A')
→ helper V (dissect (extendEvalCtx E (μ- B))) ≡ (_ , extendEvalCtx E (μ V -) ▻ B)
helperμl-lem E B V rewrite lemma E (μ- B) = refl
helperμr-lem : ∀(E : EvalCtx K _){B : ∅ ⊢⋆ J}(W : Value⋆ B){A'}(V : Value⋆ A')
→ helper W (dissect (extendEvalCtx E (μ V -))) ≡ (* , E ◅ V-μ V W)
helperμr-lem E W V rewrite lemma E (μ V -) = refl
-- some high level structure of the reduction to CC machine below
lemV : (A : ∅ ⊢⋆ J)(V : Value⋆ A)(E : EvalCtx K J) → (E ▻ A) -→s (E ◅ V)
lemV .(Π N) (V-Π N) E = step* refl base
lemV .(_ ⇒ _) (V V-⇒ W) E = step*
refl
(step** (lemV (discharge V) V (extendEvalCtx E (-⇒ discharge W)))
(step* refl
(subst-step* (helper⇒l-lem E (discharge W) V)
(step** (lemV (discharge W) W (extendEvalCtx E (V ⇒-)))
(step* refl (subst-step* ( helper⇒r-lem E W V) base))))))
lemV .(ƛ N) (V-ƛ N) E = step* refl base
lemV .(con tcn) (V-con tcn) E = step* refl base
lemV .(μ _ _) (V-μ V W) E = step*
refl
(step** (lemV _ V (extendEvalCtx E (μ- discharge W)))
(step* refl
(subst-step* (helperμl-lem E (discharge W) V)
(step** (lemV _ W (extendEvalCtx E (μ V -)))
(step* refl (subst-step* ( helperμr-lem E W V) base))))))
lem62 : (A : ∅ ⊢⋆ I)(B : ∅ ⊢⋆ J)(E : EvalCtx K J)(E' : EvalCtx J I)
→ B ~ E' ⟦ A ⟧
→ (E ▻ B) -→s (compEvalCtx' E E' ▻ A)
lem62 A .A E [] (~[] .A) = base
lem62 A .(_ · B) E (V ·r E') (~·r .A .V B .E' x) = step*
refl
(step** (lemV _ V (extendEvalCtx E (-· B)))
(step* refl
(subst-step* (helper·-lem E E' B V)
(lem62 A B (extendEvalCtx E (V ·-)) E' x))))
lem62 A .(A₁ · x₁) E (E' l· x₁) (~l· .A A₁ .x₁ .E' x) = step*
refl
(lem62 A A₁ (extendEvalCtx E (-· x₁)) E' x)
lem62 A .(_ ⇒ B) E (V ⇒r E') (~⇒r .A _ .V .E' B x) = step*
refl
(step** (lemV _ V (extendEvalCtx E (-⇒ B)))
(step* refl
(subst-step* (helper⇒l-lem E B V)
(lem62 A B (extendEvalCtx E (V ⇒-)) E' x))))
lem62 A .(A₁ ⇒ x₁) E (E' l⇒ x₁) (~l⇒ .A A₁ .x₁ .E' x) = step*
refl
(lem62 A _ (extendEvalCtx E (-⇒ x₁)) E' x)
lem62 A .(μ _ B) E (μr x₁ E') (~μr .A _ .x₁ .E' B x) = step*
refl
(step** (lemV _ x₁ (extendEvalCtx E (μ- B)))
(step* refl
(subst-step* (helperμl-lem E B x₁)
(lem62 A B (extendEvalCtx E (μ x₁ -)) E' x))))
lem62 A .(μ A₁ B₁) E (μl E' B₁) (~μl .A A₁ .B₁ .E' x) = step*
refl
(lem62 A _ (extendEvalCtx E (μ- B₁)) E' x)
{-
lem1 : (A : ∅ ⊢⋆ J)(B : ∅ ⊢⋆ K)(E : EvalCtx K J)
(A' : ∅ ⊢⋆ J)(B' : ∅ ⊢⋆ K)(E' : EvalCtx K J)
→ B ~ E ⟦ A ⟧ → B' ~ E' ⟦ A' ⟧ → B —→⋆ B' -> (E ▻ A) -→s (E' ▻ A')
lem1 A B E A' B' E' p q r = {!!}
lem1' : (A : ∅ ⊢⋆ J)(B : ∅ ⊢⋆ K)(E : EvalCtx K J)
(B' : ∅ ⊢⋆ K) → B ~ E ⟦ A ⟧ → B —→⋆ B' →
Σ (∅ ⊢⋆ J) λ A' → Σ (EvalCtx K J) λ E' → B' ~ E' ⟦ A' ⟧ ×(E ▻ A) -→s (E' ▻ A')
lem1' A B E B' p (contextRule E₁ q x x₁) = {!lem1 !}
lem1' A .(ƛ _ · _) E .(sub (sub-cons ` _) _) p (β-ƛ x) = -, -, -, {!!}
unwind : (A : ∅ ⊢⋆ J)(A' : ∅ ⊢⋆ K)(E : EvalCtx K J) → A' ~ E ⟦ A ⟧ → (V : Value⋆ A') → (E ▻ A) -→s ([] ◅ V)
unwind = {!!}
-- thm2 follows from this stronger theorem
thm1 : (A : ∅ ⊢⋆ J)(A' : ∅ ⊢⋆ K)(E : EvalCtx K J)
→ A' ~ E ⟦ A ⟧ → (B : ∅ ⊢⋆ K)(V : Value⋆ B) → A' —↠⋆ B -> (E ▻ A) -→s ([] ◅ V)
thm1 A A' E p .A' V refl—↠⋆ = unwind A A' E p V
thm1 A A' E p B V (trans—↠⋆ {B = B'} x q) =
let A' , E' , p' , p'' = lem1' A A' E B' p x in
step** p'' (thm1 A' B' E' p' _ _ q)
-- this is the result we want
thm2 : (A B : ∅ ⊢⋆ K)(V : Value⋆ B) → A —↠⋆ B -> ([] ▻ A) -→s ([] ◅ V)
thm2 A B V p = thm1 A A [] (~[] A) B V p
-}
```
22 changes: 19 additions & 3 deletions plutus-metatheory/src/Type/CK.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,7 @@ step (s ▻ μ A B) = -, (s , μ- B) ▻ A
step (s ▻ con c) = -, s ◅ V-con c
step (ε ◅ V) = -, □ V
step ((s , (-· B)) ◅ V) = -, (s , V ·-) ▻ B
step (_◅_ (s , (V-ƛ A ·-)) B) = -, s ▻ (A [ discharge B ])
step ((s , (V-ƛ A ·-)) ◅ B) = -, s ▻ (A [ discharge B ])
step ((s , (-⇒ B)) ◅ V) = -, (s , V ⇒-) ▻ B
step ((s , (V ⇒-)) ◅ W) = -, s ◅ (V V-⇒ W)
step ((s , μ- B) ◅ A) = -, (s , μ A -) ▻ B
Expand All @@ -120,10 +120,26 @@ variable
open import Relation.Binary.PropositionalEquality
data _-→s_ : State K J → State K I → Set where
base : (s : State K J)
base : {s : State K J}
→ s -→s s
step* : (s : State K J)(s' : State K I)(s'' : State K I')
step* : {s : State K J}{s' : State K I}{s'' : State K I'}
→ step s ≡ (I , s')
→ s' -→s s''
→ s -→s s''
step** : {s : State K J}{s' : State K I}{s'' : State K I'}
→ s -→s s'
→ s' -→s s''
→ s -→s s''
step** base q = q
step** (step* x p) q = step* x (step** p q)
```

```
change-dir : (s : Stack I J)(A : ∅ ⊢⋆ J) (V : Value⋆ A) → (s ▻ A) -→s (s ◅ V)
change-dir s .(Π N) (V-Π N) = step* refl base
change-dir s .(_ ⇒ _) (V V-⇒ V₁) = step* refl (step** (change-dir _ _ V) (step* refl (step** (change-dir _ _ V₁) (step* refl base))))
change-dir s .(ƛ N) (V-ƛ N) = step* refl base
change-dir s .(con tcn) (V-con tcn) = step* refl base
change-dir s .(μ _ _) (V-μ V V₁) = step* refl (step** (change-dir _ _ V) (step* refl (step** (change-dir _ _ V₁) (step* refl base))))
```
Loading

0 comments on commit b389d71

Please sign in to comment.