------------------------------------------------------------------------ -- The two semantics are equivalent ------------------------------------------------------------------------ module Semantics.Equivalence where open import Syntax open import Semantics.BigStep open import Semantics.SmallStep open import Semantics.SmallStep.EvalCtxt open ⟶-Reasoning open import Infinite hiding (_⇓_; return) open import Totality open import Data.Star hiding (return) open import Data.Product open import Data.Nat open import Relation.Nullary open import Category.Monad open RawMonad ¬¬-Monad hiding (_>>_) open import Data.Function ------------------------------------------------------------------------ -- Statement of equivalence record Big⇒Small : Set where field ⇓ : ∀ {t} {e : Expr t} {i v} → e ⇓[ i ] v → e ˢ ⟶⋆[ i ] done v ⇑ : ∀ {t} {e : Expr t} {i} → e ⇑[ i ] → e ˢ ⟶∞[ i ] record Small⇒Big : Set where field ⟶⋆ : ∀ {t} {e : Exprˢ t} {i v} → e ⟶⋆[ i ] done v → e ˢ⁻¹ ⇓[ i ] v ⟶∞ : ∀ {t} (e : Exprˢ t) i → e ⟶∞[ i ] → ¬ ¬ e ˢ⁻¹ ⇑[ i ] ------------------------------------------------------------------------ -- Proof of Big⇒Small big⇒small⇓ : ∀ {t} {e : Expr t} {i v} → e ⇓[ i ] v → e ˢ ⟶⋆[ i ] done v big⇒small⇓ (Val {v = v}) = begin run ⌜ v ⌝ ⟶⟨ Red Val ⟩ done v ∎ big⇒small⇓ (Loop {x = x} {v} ⇓) = begin run (loop (x ˢ)) ⟶⟨ Red Loop ⟩ run (x ˢ >> run (loop (x ˢ))) ⟶⋆⟨ big⇒small⇓ ⇓ ⟩ done v ∎ big⇒small⇓ (Add₁ {x = x} {y} {m} {n} x⇓ y⇓) = begin run (x ˢ ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (• •⊕ y ˢ) (big⇒small⇓ x⇓) ⟩ run (done (nat m) ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (nat m ⊕• •) (big⇒small⇓ y⇓) ⟩ run (done (nat m) ⊕ done (nat n)) ⟶⟨ Red Add₁ ⟩ done (nat (m + n)) ∎ big⇒small⇓ (Add₂ {x = x} {y} x↯) = begin run (x ˢ ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (• •⊕ y ˢ) (big⇒small⇓ x↯) ⟩ run (done throw ⊕ y ˢ) ⟶⟨ Red Add₂ ⟩ done throw ∎ big⇒small⇓ (Add₃ {x = x} {y} {m} x⇓ y↯) = begin run (x ˢ ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (• •⊕ y ˢ) (big⇒small⇓ x⇓) ⟩ run (done (nat m) ⊕ y ˢ) ⟶⋆⟨ lift⟶⋆ (nat m ⊕• •) (big⇒small⇓ y↯) ⟩ run (done (nat m) ⊕ done throw) ⟶⟨ Red Add₃ ⟩ done throw ∎ big⇒small⇓ (Seqn₁ {x = x} {y} {m} {v} x⇓ y⇒) = begin run (x ˢ >> y ˢ) ⟶⋆⟨ lift⟶⋆ (• •>> y ˢ) (big⇒small⇓ x⇓) ⟩ run (done (nat m) >> y ˢ) ⟶⟨ Red Seqn₁ ⟩ y ˢ ⟶⋆⟨ big⇒small⇓ y⇒ ⟩ done v ∎ big⇒small⇓ (Seqn₂ {x = x} {y} x↯) = begin run (x ˢ >> y ˢ) ⟶⋆⟨ lift⟶⋆ (• •>> y ˢ) (big⇒small⇓ x↯) ⟩ run (done throw >> y ˢ) ⟶⟨ Red Seqn₂ ⟩ done throw ∎ big⇒small⇓ (Catch₁ {x = x} {y} {m} x⇓) = begin run (x ˢ catch y ˢ) ⟶⋆⟨ lift⟶⋆ (• •catch y ˢ) (big⇒small⇓ x⇓) ⟩ run (done (nat m) catch y ˢ) ⟶⟨ Red Catch₁ ⟩ done (nat m) ∎ big⇒small⇓ (Catch₂ {x = x} {y} {v} x↯ y⇒) = begin run (x ˢ catch y ˢ) ⟶⋆⟨ lift⟶⋆ (• •catch y ˢ) (big⇒small⇓ x↯) ⟩ run (done throw catch y ˢ) ⟶⋆⟨ lift⟶⋆ (handler• •) (big⇒small⇓ y⇒) ⟩ run (done throw catch done v) ⟶⟨ Red Catch₂ ⟩ done v ∎ big⇒small⇓ (Int {x = x}) = begin x ˢ ⟶⟨ Red (Int (x ˢ-interruptible)) ⟩ done throw ∎ big⇒small⇓ (Block {x = x} {v} x⇒) = begin run (block (x ˢ)) ⟶⋆⟨ lift⟶⋆ (block• •) (big⇒small⇓ x⇒) ⟩ run (block (done v)) ⟶⟨ Red Block ⟩ done v ∎ big⇒small⇓ (Unblock {x = x} {v} x⇒) = begin run (unblock (x ˢ)) ⟶⋆⟨ lift⟶⋆ (unblock• •) (big⇒small⇓ x⇒) ⟩ run (unblock (done v)) ⟶⟨ Red Unblock ⟩ done v ∎ -- big⇒small⇑ʳ would not pass the productivity checker if it was -- defined corecursively, so a workaround is used (see -- Infinite.Infiniteʳ). data Loops t i : Exprˢ t → Set where ⇑:_ : ∀ {e} (⇑ : e ⇑[ i ]) → Loops t i (e ˢ) lift⟶∞ʳ : ∀ {t i j x g} (E : EvalCtxt t i j) → Infiniteʳ Step (Loops t) g i x → Infiniteʳ Step (Loops t) g j (E [ x ]) lift⟶∞ʳ E = map∞ʳ (λ x → E [ x ]) (lift⟶ E) big⇒small⇑ʳ : ∀ {t g} → Stepper Step (Loops t) g big⇒small⇑ʳ (⇑: Loop ⇑) = Red Loop ◅∞ rec (⇑: ⇑) big⇒small⇑ʳ (⇑: Add₁ x⇑) = lift⟶∞ʳ (• •⊕ _) (big⇒small⇑ʳ (⇑: x⇑)) big⇒small⇑ʳ (⇑: Add₂ x↡ y⇑) = lift⟶⋆ (• •⊕ _) (big⇒small⇓ (proj₂ x↡)) ◅◅∞ʳ lift⟶∞ʳ (nat proj₁ x↡ ⊕• •) (big⇒small⇑ʳ (⇑: y⇑)) big⇒small⇑ʳ (⇑: Seqn₁ x⇑) = lift⟶∞ʳ (• •>> _) (big⇒small⇑ʳ (⇑: x⇑)) big⇒small⇑ʳ (⇑: Seqn₂ x↡ y⇑) = lift⟶⋆ (• •>> _) (big⇒small⇓ (proj₂ x↡)) ◅◅∞ʳ Red Seqn₁ ◅∞ big⇒small⇑ʳ (⇑: y⇑) big⇒small⇑ʳ (⇑: Catch₁ x⇑) = lift⟶∞ʳ (• •catch _) (big⇒small⇑ʳ (⇑: x⇑)) big⇒small⇑ʳ (⇑: Catch₂ x↯ y⇑) = lift⟶⋆ (• •catch _) (big⇒small⇓ x↯) ◅◅∞ʳ lift⟶∞ʳ (handler• •) (big⇒small⇑ʳ (⇑: y⇑)) big⇒small⇑ʳ (⇑: Block x⇑) = lift⟶∞ʳ (block• •) (big⇒small⇑ʳ (⇑: x⇑)) big⇒small⇑ʳ (⇑: Unblock x⇑) = lift⟶∞ʳ (unblock• •) (big⇒small⇑ʳ (⇑: x⇑)) big⇒small⇑ : ∀ {t} {e : Expr t} {i} → e ⇑[ i ] → e ˢ ⟶∞[ i ] big⇒small⇑ = unfold big⇒small⇑ʳ ∘ ⇑:_ -- An alternative solution to the productivity problem. Unfortunately -- Agda does not normalise the right-hand sides (with the thing -- defined kept neutral) before checking productivity, so the code is -- not accepted. (And inlining lift⟶∞′ leads to less readable code, -- especially since it appears that some hidden arguments need to be -- given in order to keep the type checker happy.) -- lift⟶∞′ : ∀ {t i j x} -- (E : EvalCtxt t i j) → -- Infinite″ (Step i) x → -- Infinite″ (Step j) (E [ x ]) -- lift⟶∞′ E = map∞′ (λ x → E [ x ]) (lift⟶ E) -- big⇒small⇑' : ∀ {t i} {e : Expr t} → -- e ⇑[ i ] → Infinite″ (Step i) (e ˢ) -- big⇒small⇑' (Loop ⇑) ~ ↓ Red Loop ◅∞ big⇒small⇑' ⇑ -- big⇒small⇑' (Add₁ x⇑) ~ lift⟶∞′ (• •⊕ _) (big⇒small⇑' x⇑) -- big⇒small⇑' (Add₂ x↡ y⇑) ~ lift⟶⋆ (• •⊕ _) (big⇒small⇓ (proj₂ x↡)) -- ◅◅∞′ -- lift⟶∞′ (nat proj₁ x↡ ⊕• •) (big⇒small⇑' y⇑) -- big⇒small⇑' (Seqn₁ x⇑) ~ lift⟶∞′ (• •>> _) (big⇒small⇑' x⇑) -- big⇒small⇑' (Seqn₂ x↡ y⇑) ~ lift⟶⋆ (• •>> _) (big⇒small⇓ (proj₂ x↡)) -- ◅◅∞′ -- (↓ Red Seqn₁ ◅∞ big⇒small⇑' y⇑) -- big⇒small⇑' (Catch₁ x⇑) ~ lift⟶∞′ (• •catch _) (big⇒small⇑' x⇑) -- big⇒small⇑' (Catch₂ x↯ y⇑) ~ lift⟶⋆ (• •catch _) (big⇒small⇓ x↯) -- ◅◅∞′ -- lift⟶∞′ (handler• •) (big⇒small⇑' y⇑) -- big⇒small⇑' (Block x⇑) ~ lift⟶∞′ (block• •) (big⇒small⇑' x⇑) -- big⇒small⇑' (Unblock x⇑) ~ lift⟶∞′ (unblock• •) (big⇒small⇑' x⇑) -- big⇒small⇑₂ : ∀ {t i} {e : Expr t} → e ⇑[ i ] → e ˢ ⟶∞[ i ] -- big⇒small⇑₂ ⇑ = ∞″→∞ (big⇒small⇑' ⇑) big⇒small : Big⇒Small big⇒small = record { ⇓ = big⇒small⇓; ⇑ = big⇒small⇑ } ------------------------------------------------------------------------ -- Proof of Small⇒Big -- First note that we can map over combinations of evaluation contexts -- and the big-step relations. map⇓ : ∀ {t} {x₁ x₂ : Exprˢ t} {i j v} (E : EvalCtxt t i j) → (∀ {v} → x₁ ˢ⁻¹ ⇓[ i ] v → x₂ ˢ⁻¹ ⇓[ i ] v) → E [ x₁ ] ˢ⁻¹ ⇓[ j ] v → E [ x₂ ] ˢ⁻¹ ⇓[ j ] v map⇓ • f ⇓ = f ⇓ map⇓ (E •⊕ y) f (Add₁ x↡ y↡) = Add₁ (map⇓ E f x↡) y↡ map⇓ (E •⊕ y) f (Add₂ x↯) = Add₂ (map⇓ E f x↯) map⇓ (E •⊕ y) f (Add₃ x↡ y↯) = Add₃ (map⇓ E f x↡) y↯ map⇓ (E •⊕ y) f Int = Int map⇓ (E •>> y) f (Seqn₁ x↡ y⇓) = Seqn₁ (map⇓ E f x↡) y⇓ map⇓ (E •>> y) f (Seqn₂ x↯) = Seqn₂ (map⇓ E f x↯) map⇓ (E •>> y) f Int = Int map⇓ (E •catch y) f (Catch₁ x↡) = Catch₁ (map⇓ E f x↡) map⇓ (E •catch y) f (Catch₂ x↯ y⇓) = Catch₂ (map⇓ E f x↯) y⇓ map⇓ (E •catch y) f Int = Int map⇓ (nat m ⊕• E) f (Add₁ x↡ y↡) = Add₁ x↡ (map⇓ E f y↡) map⇓ (nat m ⊕• E) f (Add₂ x↯) = Add₂ x↯ map⇓ (nat m ⊕• E) f (Add₃ x↡ y↯) = Add₃ x↡ (map⇓ E f y↯) map⇓ (nat m ⊕• E) f Int = Int map⇓ (handler• E) f (Catch₁ ()) map⇓ (handler• E) f (Catch₂ x↯ y⇓) = Catch₂ x↯ (map⇓ E f y⇓) map⇓ (handler• E) f Int = Int map⇓ (block• E) f (Block x⇓) = Block (map⇓ E f x⇓) map⇓ (block• E) f Int = Int map⇓ (unblock• E) f (Unblock x⇓) = Unblock (map⇓ E f x⇓) map⇓ (unblock• E) f Int = Int map⇑ : ∀ {t} {x₁ x₂ : Exprˢ t} {i j} (E : EvalCtxt t i j) → (∀ {v} → x₁ ˢ⁻¹ ⇓[ i ] v → x₂ ˢ⁻¹ ⇓[ i ] v) → (x₁ ˢ⁻¹ ⇑[ i ] → x₂ ˢ⁻¹ ⇑[ i ]) → E [ x₁ ] ˢ⁻¹ ⇑[ j ] → E [ x₂ ] ˢ⁻¹ ⇑[ j ] map⇑ • f g ⇑ = g ⇑ map⇑ (E •⊕ y) f g (Add₁ x⇑) = Add₁ (map⇑ E f g x⇑) map⇑ (E •⊕ y) f g (Add₂ (_ , x↡) y⇑) = Add₂ (_ , map⇓ E f x↡) y⇑ map⇑ (E •>> y) f g (Seqn₁ x⇑) = Seqn₁ (map⇑ E f g x⇑) map⇑ (E •>> y) f g (Seqn₂ (_ , x↡) y⇑) = Seqn₂ (_ , map⇓ E f x↡) y⇑ map⇑ (E •catch y) f g (Catch₁ x⇑) = Catch₁ (map⇑ E f g x⇑) map⇑ (E •catch y) f g (Catch₂ x↯ y⇑) = Catch₂ (map⇓ E f x↯) y⇑ map⇑ (nat m ⊕• E) f g (Add₁ ()) map⇑ (nat m ⊕• E) f g (Add₂ x↡ y⇑) = Add₂ x↡ (map⇑ E f g y⇑) map⇑ (handler• E) f g (Catch₁ ()) map⇑ (handler• E) f g (Catch₂ x↯ y⇑) = Catch₂ x↯ (map⇑ E f g y⇑) map⇑ (block• E) f g (Block x⇑) = Block (map⇑ E f g x⇑) map⇑ (unblock• E) f g (Unblock x⇑) = Unblock (map⇑ E f g x⇑) -- Then note that the reduction relation is compatible with the -- big-step relations in the following sense: small⇒big⟶ʳ⇓ : ∀ {t i} {e₁ e₂ : Exprˢ t} {v} → e₁ ⟶ʳ[ i ] e₂ → e₂ ˢ⁻¹ ⇓[ i ] v → e₁ ˢ⁻¹ ⇓[ i ] v small⇒big⟶ʳ⇓ Val ⇓ = ⇓ small⇒big⟶ʳ⇓ Loop (Seqn₁ x↡ y⇓) = y⇓ small⇒big⟶ʳ⇓ Loop (Seqn₂ x↯) = Loop (Seqn₂ x↯) small⇒big⟶ʳ⇓ Loop Int = Int small⇒big⟶ʳ⇓ Add₁ Val = Add₁ Val Val small⇒big⟶ʳ⇓ Add₁ Int = Int small⇒big⟶ʳ⇓ Add₂ Val = Add₂ Val small⇒big⟶ʳ⇓ Add₂ Int = Int small⇒big⟶ʳ⇓ Add₃ Val = Add₃ Val Val small⇒big⟶ʳ⇓ Add₃ Int = Int small⇒big⟶ʳ⇓ Seqn₁ ⇓ = Seqn₁ Val ⇓ small⇒big⟶ʳ⇓ Seqn₂ Val = Seqn₂ Val small⇒big⟶ʳ⇓ Seqn₂ Int = Int small⇒big⟶ʳ⇓ Catch₁ Val = Catch₁ Val small⇒big⟶ʳ⇓ Catch₁ Int = Int small⇒big⟶ʳ⇓ Catch₂ Val = Catch₂ Val Val small⇒big⟶ʳ⇓ Catch₂ Int = Int small⇒big⟶ʳ⇓ Block Val = Block Val small⇒big⟶ʳ⇓ Block Int = Int small⇒big⟶ʳ⇓ Unblock Val = Unblock Val small⇒big⟶ʳ⇓ Unblock Int = Int small⇒big⟶ʳ⇓ (Int int) Val = Int small⇒big⟶ʳ⇓ (Int int) Int = Int small⇒big⟶ʳ⇑ : ∀ {t} {e₁ e₂ : Exprˢ t} {i} → e₁ ⟶ʳ[ i ] e₂ → e₂ ˢ⁻¹ ⇑[ i ] → e₁ ˢ⁻¹ ⇑[ i ] small⇒big⟶ʳ⇑ Val () small⇒big⟶ʳ⇑ Loop ⇑ = Loop ⇑ small⇒big⟶ʳ⇑ Add₁ () small⇒big⟶ʳ⇑ Add₂ () small⇒big⟶ʳ⇑ Add₃ () small⇒big⟶ʳ⇑ Seqn₁ ⇑ = Seqn₂ (_ , Val) ⇑ small⇒big⟶ʳ⇑ Seqn₂ () small⇒big⟶ʳ⇑ Catch₁ () small⇒big⟶ʳ⇑ Catch₂ () small⇒big⟶ʳ⇑ Block () small⇒big⟶ʳ⇑ Unblock () small⇒big⟶ʳ⇑ (Int int) () -- It is then easy to prove the desired result in the terminating -- case. small⇒big⟶⋆ : ∀ {t} {e : Exprˢ t} {i v} → e ⟶⋆[ i ] done v → e ˢ⁻¹ ⇓[ i ] v small⇒big⟶⋆ ε = Val small⇒big⟶⋆ (⟶ ◅ ⟶⋆) with ⟶⇒⟶E ⟶ small⇒big⟶⋆ (⟶ ◅ ⟶⋆) | Red E ⟶ʳ = map⇓ E (small⇒big⟶ʳ⇓ ⟶ʳ) (small⇒big⟶⋆ ⟶⋆) -- The non-terminating case is not quite as easy, though. Note that -- the following proof is not productive. The right-hand side inspects -- the result of the recursive call before emitting the first -- constructor, so if this proof were a Haskell function its semantics -- would be ⊥. -- small⇒big⟶∞ : ∀ {t} {e : Exprˢ t} {i} → -- e ⟶∞[ i ] → e ˢ⁻¹ ⇑[ i ] -- small⇒big⟶∞ (⟶ ◅∞ ⟶∞) with ⟶⇒⟶E ⟶ -- small⇒big⟶∞ (⟶ ◅∞ ⟶∞) | Red E ⟶ʳ = -- map⇑ E (small⇒big⟶ʳ⇓ ⟶ʳ) (small⇒big⟶ʳ⇑ ⟶ʳ) (small⇒big⟶∞ ⟶∞) -- In "Coinductive big-step operational semantics" Leroy and Grall use -- excluded middle to prove this result. Here I follow them, but I use -- double-negation instead of postulating anything (as suggested by -- Thorsten Altenkirch). open import Semantics.Equivalence.Lemmas small⇒big⟶∞ : ∀ {t} (e : Exprˢ t) i → e ⟶∞[ i ] → ¬ ¬ e ˢ⁻¹ ⇑[ i ] small⇒big⟶∞ (done v) i ⟶∞ = const (done↛∞ ⟶∞) small⇒big⟶∞ (run ⌜ v ⌝) i (Red Val ◅∞ ⟶∞) = const (done↛∞ ⟶∞) small⇒big⟶∞ (run ⌜ v ⌝) .U (Red (Int int) ◅∞ ⟶∞) = const (done↛∞ ⟶∞) small⇒big⟶∞ (run (loop x)) i ⟶∞ = helper =<< excluded-middle where helper : Dec (∃ λ z → (x ⟶⋆[ i ] z) × Loop.Pred i z) → _ helper (yes (._ , x⟶⋆n , Loop.• n)) = return (loop-⇑ (n , small⇒big⟶⋆ x⟶⋆n)) helper (no x↛⋆n) = Loop <$> (Seqn₁ <$> small⇒big⟶∞ x i x⟶∞) where x⟶∞ = ⋆∞⇒∞ (Loop.lemma ⟶∞) x↛⋆n small⇒big⟶∞ (run (x ⊕ y)) i ⟶∞ = helper =<< excluded-middle where helper : Dec (∃ λ z → (x ⟶⋆[ i ] z) × Add.Pred y i z) → _ helper (yes (._ , x⟶⋆n , Add.• n y⟶∞)) = Add₂ (n , small⇒big⟶⋆ x⟶⋆n) <$> small⇒big⟶∞ y i y⟶∞ helper (no x↛⋆n) = Add₁ <$> small⇒big⟶∞ x i x⟶∞ where x⟶∞ = ⋆∞⇒∞ (Add.lemma ⟶∞) x↛⋆n small⇒big⟶∞ (run (x >> y)) i ⟶∞ = helper =<< excluded-middle where helper : Dec (∃ λ z → (x ⟶⋆[ i ] z) × Seqn.Pred y i z) → _ helper (yes (._ , x⟶⋆n , Seqn.• n y⟶∞)) = Seqn₂ (n , small⇒big⟶⋆ x⟶⋆n) <$> small⇒big⟶∞ y i y⟶∞ helper (no x↛⋆n) = Seqn₁ <$> small⇒big⟶∞ x i x⟶∞ where x⟶∞ = ⋆∞⇒∞ (Seqn.lemma ⟶∞) x↛⋆n small⇒big⟶∞ (run (x catch y)) i ⟶∞ = helper =<< excluded-middle where helper : Dec (∃ λ z → (x ⟶⋆[ i ] z) × Catch.Pred y i z) → _ helper (yes (._ , x⟶⋆↯ , Catch.• y⟶∞)) = Catch₂ (small⇒big⟶⋆ x⟶⋆↯) <$> small⇒big⟶∞ y B y⟶∞ helper (no x↛⋆↯) = Catch₁ <$> small⇒big⟶∞ x i x⟶∞ where x⟶∞ = ⋆∞⇒∞ (Catch.lemma ⟶∞) x↛⋆↯ small⇒big⟶∞ (run (block x)) i ⟶∞ = Block <$> small⇒big⟶∞ x B (Block.lemma ⟶∞) small⇒big⟶∞ (run (unblock x)) i ⟶∞ = Unblock <$> small⇒big⟶∞ x U (Unblock.lemma ⟶∞) small⇒big : Small⇒Big small⇒big = record { ⟶⋆ = small⇒big⟶⋆; ⟶∞ = small⇒big⟶∞ }