Add proof of equivalence of the two languages

This commit is contained in:
Danila Fedorin 2024-09-24 18:45:46 -07:00
parent 62f59a9a4d
commit ab56a8414f

154
Language/Equivalence.agda Normal file
View File

@ -0,0 +1,154 @@
{-# OPTIONS --guardedness #-}
module Language.Equivalence where
open import Language.Nested using () renaming
( Instruction to Instructionᵃ; Program to Programᵃ; Env to Envᵃ
; pushint to pushintᵃ; pushbool to pushboolᵃ; add to addᵃ
; loop to loopᵃ; break to breakᵃ
; Triple to Tripleᵃ
; _⇒_ to _⇒ᵃ_; _⇒*_ to _⇒*ᵃ_
; pushint-eval to pushint-evalᵃ; pushbool-eval to pushbool-evalᵃ; add-eval to add-evalᵃ
; break-evalᵗ to break-evalᵗᵃ; break-evalᶠ to break-evalᶠᵃ; empty-eval to empty-evalᵃ
; loop-eval⁰ to loop-eval⁰ᵃ; loop-evalⁿ to loop-evalⁿᵃ
; doneᵉ to doneᵉᵃ; _thenᵉ_ to _thenᵉᵃ_
)
open import Language.Flat
using
(_⇒ₓ_; pushint-skip; pushbool-skip; add-skip; break-skip; loop-skip; end-skip
)
renaming
( Instruction to Instructionᵇ; Program to Programᵇ; Env to Envᵇ
; pushint to pushintᵇ; pushbool to pushboolᵇ; add to addᵇ
; loop to loopᵇ; break to breakᵇ; end to endᵇ
; Triple to Tripleᵇ
; _⇒_ to _⇒ᵇ_; _⇒*_ to _⇒*ᵇ_
; pushint-eval to pushint-evalᵇ; pushbool-eval to pushbool-evalᵇ; add-eval to add-evalᵇ
; break-evalᵗ to break-evalᵗᵇ; break-evalᶠ to break-evalᶠᵇ; end-eval to end-evalᵇ
; loop-eval⁰ to loop-eval⁰ᵇ; loop-evalⁿ to loop-evalⁿᵇ
; doneᵉ to doneᵉᵇ; _thenᵉ_ to _thenᵉᵇ_
)
open import Language.Values using
( Value; int; bool
; ValueType; tint; tbool
; ⟦_⟧ˢ; ⟦⟧ˢ-empty; ⟦⟧ˢ-int; ⟦⟧ˢ-bool
; s; s'; s''
; st; st'; st''
; b; b₁; b₂
; z; z₁; z₂
)
open import Data.List using (List; _∷_; []; length; foldr; _++_)
open import Data.List.Properties using (++-assoc)
open import Data.Product using (Σ; _×_; _,_)
open import Data.Nat using ()
open import Data.Unit using (; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
variable
n n' :
iᵃ : Instructionᵃ
isᵃ isᵃ' isᵃ'' : Programᵃ
Sᵃ Sᵃ' Sᵃ'' : Envᵃ
iᵇ : Instructionᵇ
isᵇ isᵇ' isᵇ'' : Programᵇ
Sᵇ Sᵇ' Sᵇ'' : Envᵇ
interleaved mutual
⟦_⟧ⁱ : Instructionᵃ List Instructionᵇ
⟦_⟧ⁱˢ : List Instructionᵃ List Instructionᵇ
pushintᵃ z ⟧ⁱ = pushintᵇ z []
pushboolᵃ b ⟧ⁱ = pushboolᵇ b []
addᵃ ⟧ⁱ = addᵇ []
loopᵃ n is ⟧ⁱ = loopᵇ n ( is ⟧ⁱˢ ++ endᵇ [])
breakᵃ ⟧ⁱ = breakᵇ []
[] ⟧ⁱˢ = []
i is ⟧ⁱˢ = i ⟧ⁱ ++ is ⟧ⁱˢ
-- Translation always leaves well-balanced programs
interleaved mutual
lemma₁ : isᵇ ⇒ₓ isᵇ' ( iᵃ ⟧ⁱ ++ isᵇ) ⇒ₓ isᵇ'
lemma₁' : isᵇ ⇒ₓ isᵇ' ( isᵃ ⟧ⁱˢ ++ isᵇ) ⇒ₓ isᵇ'
lemma₂ : ( isᵃ ⟧ⁱˢ ++ endᵇ isᵇ) ⇒ₓ isᵇ
lemma₁ {iᵃ = pushintᵃ z} = pushint-skip
lemma₁ {iᵃ = pushboolᵃ z} = pushbool-skip
lemma₁ {iᵃ = addᵃ} = add-skip
lemma₁ {iᵃ = breakᵃ} = break-skip
lemma₁ {isᵇ = isᵇ} {iᵃ = loopᵃ n is}
rewrite ++-assoc is ⟧ⁱˢ (endᵇ []) isᵇ =
loop-skip (lemma₂ {isᵃ = is} {isᵇ = isᵇ})
lemma₁' {isᵃ = []} isᵇ⇒ₓisᵇ' = isᵇ⇒ₓisᵇ'
lemma₁' {isᵇ = isᵇ} {isᵃ = iᵃ isᵃ} isᵇ⇒ₓisᵇ'
rewrite ++-assoc iᵃ ⟧ⁱ isᵃ ⟧ⁱˢ isᵇ =
lemma₁ {iᵃ = iᵃ} (lemma₁' {isᵃ = isᵃ} isᵇ⇒ₓisᵇ')
lemma₂ {isᵃ = isᵃ} = lemma₁' {isᵃ = isᵃ} end-skip
-- In flat semantics, we drop the top continuation and seek forward until we find
-- an 'end'. In nested semantics, we drop the current instructions and use the
-- bit of the top continuation after the 'while'. We need to be able to reconcile
-- the two.
data ⟦_⟧ᵀ=_ : Programᵃ × Envᵃ Programᵇ × Envᵇ Set where
⟦⟧ᵀ-empty : isᵃ , [] ⟧ᵀ= ( isᵃ ⟧ⁱˢ , [])
⟦⟧ᵀ-step : isᵃ'' , Sᵃ ⟧ᵀ= (isᵇ , Sᵇ)
isᵃ , ((loopᵃ n isᵃ' isᵃ'') Sᵃ) ⟧ᵀ= (( isᵃ ⟧ⁱˢ ++ endᵇ []) ++ isᵇ , ( loopᵃ n isᵃ' ⟧ⁱ ++ isᵇ) Sᵇ)
step-equivalence : (s , isᵃ , Sᵃ) ⇒ᵃ (s' , isᵃ' , Sᵃ')
isᵃ , Sᵃ ⟧ᵀ= (isᵇ , Sᵇ)
Σ (Programᵇ × Envᵇ) (λ { (isᵇ' , Sᵇ') (s , isᵇ , Sᵇ) ⇒ᵇ (s' , isᵇ' , Sᵇ') ×
isᵃ' , Sᵃ' ⟧ᵀ= (isᵇ' , Sᵇ') })
step-equivalence pushint-evalᵃ ⟦⟧ᵀ-empty = ((_ , _) , pushint-evalᵇ , ⟦⟧ᵀ-empty)
step-equivalence pushint-evalᵃ (⟦⟧ᵀ-step next) = ((_ , _) , pushint-evalᵇ , ⟦⟧ᵀ-step next)
step-equivalence pushbool-evalᵃ ⟦⟧ᵀ-empty = ((_ , _) , pushbool-evalᵇ , ⟦⟧ᵀ-empty)
step-equivalence pushbool-evalᵃ (⟦⟧ᵀ-step next) = ((_ , _) , pushbool-evalᵇ , ⟦⟧ᵀ-step next)
step-equivalence add-evalᵃ ⟦⟧ᵀ-empty = ((_ , _) , add-evalᵇ , ⟦⟧ᵀ-empty)
step-equivalence add-evalᵃ (⟦⟧ᵀ-step next) = ((_ , _) , add-evalᵇ , ⟦⟧ᵀ-step next)
step-equivalence {isᵃ = loopᵃ n isˡ isᵃ} loop-eval⁰ᵃ ⟦⟧ᵀ-empty
rewrite ++-assoc isˡ ⟧ⁱˢ (endᵇ []) isᵃ ⟧ⁱˢ
= ((_ , _) , loop-eval⁰ᵇ (lemma₁' {isᵃ = isˡ} end-skip) , ⟦⟧ᵀ-empty)
step-equivalence {isᵃ = loopᵃ n isˡ isᵃ} loop-eval⁰ᵃ (⟦⟧ᵀ-step {isᵇ = isᵇ} rec)
rewrite ++-assoc isˡ ⟧ⁱˢ (endᵇ []) isᵃ ⟧ⁱˢ
rewrite ++-assoc isˡ ⟧ⁱˢ (endᵇ isᵃ ⟧ⁱˢ) (endᵇ [])
rewrite ++-assoc isˡ ⟧ⁱˢ (endᵇ isᵃ ⟧ⁱˢ ++ endᵇ []) isᵇ
= ((_ , _) , loop-eval⁰ᵇ (lemma₁' {isᵃ = isˡ} end-skip) , (⟦⟧ᵀ-step rec))
step-equivalence {isᵃ = loopᵃ n isˡ isᵃ} loop-evalⁿᵃ ⟦⟧ᵀ-empty
= ((_ , _) , loop-evalⁿᵇ , ⟦⟧ᵀ-step ⟦⟧ᵀ-empty)
step-equivalence {isᵃ = loopᵃ n isˡ isᵃ} loop-evalⁿᵃ (⟦⟧ᵀ-step {isᵇ = isᵇ} rec)
rewrite ++-assoc ( isˡ ⟧ⁱˢ ++ endᵇ []) isᵃ ⟧ⁱˢ (endᵇ [])
rewrite ++-assoc isˡ ⟧ⁱˢ (endᵇ []) ( isᵃ ⟧ⁱˢ ++ endᵇ [])
rewrite sym (++-assoc isˡ ⟧ⁱˢ (endᵇ []) ( isᵃ ⟧ⁱˢ ++ endᵇ []))
rewrite ++-assoc ( isˡ ⟧ⁱˢ ++ endᵇ []) ( isᵃ ⟧ⁱˢ ++ endᵇ []) isᵇ
= (_ , loop-evalⁿᵇ , ⟦⟧ᵀ-step (⟦⟧ᵀ-step rec))
step-equivalence break-evalᶠᵃ (⟦⟧ᵀ-step next) = ((_ , _) , break-evalᶠᵇ , ⟦⟧ᵀ-step next)
step-equivalence {isᵃ = breakᵃ isᵃ} {Sᵃ = (loopᵃ n isˡ isᵃ') Sᵃ} break-evalᵗᵃ (⟦⟧ᵀ-step {isᵇ = isᵇ} next)
rewrite ++-assoc isᵃ ⟧ⁱˢ (endᵇ []) isᵇ
= ((_ , _) , break-evalᵗᵇ (lemma₁' {isᵃ = isᵃ} end-skip) , next)
step-equivalence empty-evalᵃ (⟦⟧ᵀ-step ⟦⟧ᵀ-empty)
= ((_ , _) , end-evalᵇ , ⟦⟧ᵀ-empty)
step-equivalence {Sᵃ = (loopᵃ n isˡ isᵃ') Sᵃ} empty-evalᵃ (⟦⟧ᵀ-step (⟦⟧ᵀ-step {isᵇ = isᵇ} next))
rewrite sym (++-assoc (loopᵇ n isˡ ⟧ⁱˢ ++ endᵇ []) ( isᵃ' ⟧ⁱˢ ++ endᵇ []) isᵇ)
rewrite sym (++-assoc ( isˡ ⟧ⁱˢ ++ endᵇ []) ( isᵃ' ⟧ⁱˢ) (endᵇ []))
= ((_ , _) , end-evalᵇ , ⟦⟧ᵀ-step next)
equivalence : (s , isᵃ , Sᵃ) ⇒*ᵃ (s' , isᵃ' , Sᵃ')
isᵃ , Sᵃ ⟧ᵀ= (isᵇ , Sᵇ)
Σ (Programᵇ × Envᵇ) (λ { (isᵇ' , Sᵇ') (s , isᵇ , Sᵇ) ⇒*ᵇ (s' , isᵇ' , Sᵇ') ×
isᵃ' , Sᵃ' ⟧ᵀ= (isᵇ' , Sᵇ') })
equivalence doneᵉᵃ trans@(⟦⟧ᵀ-empty) = (_ , (doneᵉᵇ , trans))
equivalence (isᵃ⇒isᵃ' thenᵉᵃ rest) trans =
let (_ , isᵇ⇒isᵇ' , trans') = step-equivalence isᵃ⇒isᵃ' trans in
let (_ , isᵇ'⇒*isᵇ'' , trans'') = equivalence rest trans' in
(_ , isᵇ⇒isᵇ' thenᵉᵇ isᵇ'⇒*isᵇ'' , trans'')
equivalence' : (s , isᵃ , []) ⇒*ᵃ (s' , [] , [])
(s , isᵃ ⟧ⁱˢ , []) ⇒*ᵇ (s' , [] , [])
equivalence' eval with
(_ , isᵃ⇒| , ⟦⟧ᵀ-empty) equivalence eval ⟦⟧ᵀ-empty = isᵃ⇒|