module CESH.Bisimulation (Node : Set) where open import GeneralLemmas open import CES Node open import CES.Properties Node open import CESH Node open import CESH.Presimulation Node open import CESH.Properties Node open import CESH.Simulation Node open import Heap open import MachineCode Node open import Relation open Bisimulation _⟶CES_ _⟶CESH_ hiding (Bisimulation) bisimulation : Bisimulation _⟶CES_ _⟶CESH_ R-config bisimulation = simulation-to-bisimulation R-config simulation presimulation det where det : ∀ a b → R-config a b → _⟶CESH_ is-deterministic-at b det a b x = determinism-CESH termination-agrees : ∀ cfg₁ cfg₂ n → R-config cfg₁ cfg₂ → cfg₁ ↓CES nat n ↔ cfg₂ ↓CESH nat n termination-agrees cfg₁ cfg₂ n Rcfg₁cfg₂ = ⇒ cfg₁ cfg₂ Rcfg₁cfg₂ , ⇐ cfg₁ cfg₂ Rcfg₁cfg₂ where sim = proj₁ bisimulation sim⁻¹ = proj₂ bisimulation ⇒ : ∀ cfg₁ cfg₂ {n} → R-config cfg₁ cfg₂ → cfg₁ ↓CES nat n → cfg₂ ↓CESH nat n ⇒ (.END , [] , val (nat n) ∷ []) (.END , [] , [] , h) (refl , tt , ()) [] ⇒ (.END , [] , val (nat n) ∷ []) (.END , [] , cont x ∷ [] , h) (refl , tt , () , tt) [] ⇒ (.END , [] , val (nat n) ∷ []) (.END , [] , x ∷ y ∷ s , h) (refl , tt , _ , ()) [] ⇒ (.END , [] , val (nat n) ∷ []) (.END , x ∷ e , s , h) (refl , () , Rs) [] ⇒ (.END , [] , val (nat n) ∷ []) (.END , [] , val (clos _) ∷ [] , h) (refl , tt , () , tt) [] ⇒ (.END , [] , val (nat n) ∷ []) (.END , [] , val (nat .n) ∷ [] , h) (refl , tt , refl , tt) [] = h , [] ⇒ cfg₁ cfg₂ Rcfg₁cfg₂ (step₁ ∷ steps) = let (cfg₂' , step₁' , Rcfg₁'cfg₂') = sim cfg₁ _ cfg₂ step₁ Rcfg₁cfg₂ (h , steps') = ⇒ _ cfg₂' Rcfg₁'cfg₂' steps in h , step₁' ∷ steps' ⇐ : ∀ cfg₁ cfg₂ {n} → R-config cfg₁ cfg₂ → cfg₂ ↓CESH nat n → cfg₁ ↓CES nat n ⇐ (.END , _ ∷ _ , s) (.END , [] , val (nat n) ∷ [] , .h) (refl , () , Rs) (h , []) ⇐ (.END , [] , []) (.END , [] , val (nat n) ∷ [] , .h) (refl , tt , ()) (h , []) ⇐ (.END , [] , x ∷ y ∷ s) (.END , [] , val (nat n) ∷ [] , .h) (refl , tt , _ , ()) (h , []) ⇐ (.END , [] , cont _ ∷ []) (.END , [] , val (nat n) ∷ [] , .h) (refl , tt , () , tt) (h , []) ⇐ (.END , [] , val (clos _) ∷ []) (.END , [] , val (nat n) ∷ [] , .h) (refl , tt , () , tt) (h , []) ⇐ (.END , [] , val (nat .n) ∷ []) (.END , [] , val (nat n) ∷ [] , .h) (refl , tt , refl , tt) (h , []) = [] ⇐ cfg₁ cfg₂ Rcfg₁cfg₂ (h , step₁' ∷ steps') = let (cfg₁' , step₁ , Rcfg₁'cfg₂') = sim⁻¹ cfg₂ _ cfg₁ step₁' Rcfg₁cfg₂ steps = ⇐ cfg₁' _ Rcfg₁'cfg₂' (h , steps') in step₁ ∷ steps divergence-agrees : ∀ cfg₁ cfg₂ → R-config cfg₁ cfg₂ → cfg₁ ↑CES ↔ cfg₂ ↑CESH divergence-agrees cfg₁ cfg₂ Rcfg₁cfg₂ = divergence-bisimulation cfg₁ cfg₂ (_ , bisimulation , Rcfg₁cfg₂) initial-related : ∀ c → R-config (c , [] , []) (c , [] , [] , ∅) initial-related c = refl , tt , tt initial-termination-agrees : ∀ c n → (c , [] , []) ↓CES nat n ↔ (c , [] , [] , ∅) ↓CESH nat n initial-termination-agrees c n = termination-agrees (c , [] , []) (c , [] , [] , ∅) n (initial-related c) initial-divergence-agrees : ∀ c → (c , [] , []) ↑CES ↔ (c , [] , [] , ∅) ↑CESH initial-divergence-agrees c = divergence-agrees (c , [] , []) (c , [] , [] , ∅) (initial-related c)