[Added a small-step semantics, equivalent to the big-step one. Nils Anders Danielsson **20080520194255] hunk ./Everything.agda 8 +import SmallStep hunk ./Language.agda 44 + +⌜_⌝ : Value -> Expr +⌜ val n ⌝ = val n +⌜ throw ⌝ = throw addfile ./SmallStep.agda hunk ./SmallStep.agda 1 +------------------------------------------------------------------------ +-- A small-step semantics for the language +------------------------------------------------------------------------ + +module SmallStep where + +open import Language +open import Data.Nat +open import Relation.Binary.PropositionalEquality + +------------------------------------------------------------------------ +-- Reduction relation + +infix 3 _⟶ʳ[_]_ + +data _⟶ʳ[_]_ : Expr -> Status -> Expr -> Set where + Add₁ : forall {i m n} -> val m ⊕ val n ⟶ʳ[ i ] val (m + n) + Add₂ : forall {i y} -> throw ⊕ y ⟶ʳ[ i ] throw + Add₃ : forall {i m} -> val m ⊕ throw ⟶ʳ[ i ] throw + Seqn₁ : forall {i m y} -> val m >> y ⟶ʳ[ i ] y + Seqn₂ : forall {i y} -> throw >> y ⟶ʳ[ i ] throw + Catch₁ : forall {i m y} -> val m catch y ⟶ʳ[ i ] val m + Catch₂ : forall {i y} -> throw catch y ⟶ʳ[ i ] y + Int : forall {x} -> x ⟶ʳ[ U ] throw + Block : forall {i v} -> block ⌜ v ⌝ ⟶ʳ[ i ] ⌜ v ⌝ + Unblock : forall {i v} -> unblock ⌜ v ⌝ ⟶ʳ[ i ] ⌜ v ⌝ + +------------------------------------------------------------------------ +-- Evaluation contexts + +infix 8 _•[_]_ _[_]•_ _⟨_⟩_ + +-- "Higher-order" representation of binary operators. + +data Op : Set where + ⊕′ : Op + >>′ : Op + catch′ : Op + +-- Application. + +_⟨_⟩_ : Expr -> Op -> Expr -> Expr +x ⟨ ⊕′ ⟩ y = x ⊕ y +x ⟨ >>′ ⟩ y = x >> y +x ⟨ catch′ ⟩ y = x catch y + +-- Evaluation contexts. Indexed on the Status of the hole and the +-- Status of the expression as a whole. + +data EvalCtxt : Status -> Status -> Set where + • : forall {i} -> EvalCtxt i i + _•[_]_ : forall {i j} -> EvalCtxt i j -> Op -> Expr -> EvalCtxt i j + _[_]•_ : forall {i j} -> Value -> Op -> EvalCtxt i j -> EvalCtxt i j + block• : forall {i j} -> EvalCtxt i B -> EvalCtxt i j + unblock• : forall {i j} -> EvalCtxt i U -> EvalCtxt i j + +-- Filling holes. + +infix 9 _[_] + +_[_] : forall {i j} -> EvalCtxt i j -> Expr -> Expr +• [ y ] = y +(E •[ op ] x) [ y ] = E [ y ] ⟨ op ⟩ x +(v [ op ]• E) [ y ] = ⌜ v ⌝ ⟨ op ⟩ E [ y ] +(block• E) [ y ] = block (E [ y ]) +(unblock• E) [ y ] = unblock (E [ y ]) + +------------------------------------------------------------------------ +-- Single-step evaluation + +infix 3 _⟶[_]_ + +data _⟶[_]_ : Expr -> Status -> Expr -> Set where + reduction : forall {i j x y} (E : EvalCtxt i j) -> + x ⟶ʳ[ i ] y -> E [ x ] ⟶[ j ] E [ y ] + +------------------------------------------------------------------------ +-- Small-step semantics + +-- Reflexive transitive closure. + +open import Data.Star + +infix 3 _⟶⋆[_]_ + +_⟶⋆[_]_ : Expr -> Status -> Expr -> Set +x ⟶⋆[ i ] y = Star (\x y -> _⟶[_]_ x i y) x y + +module ⟶-Reasoning {i : Status} = StarReasoning (\x y -> _⟶[_]_ x i y) +open ⟶-Reasoning + +------------------------------------------------------------------------ +-- Equivalence to the big-step semantics + +-- Composition of evaluation contexts. + +infix 10 _∘_ + +_∘_ : forall {i j k} -> EvalCtxt j k -> EvalCtxt i j -> EvalCtxt i k +• ∘ E₂ = E₂ +(E₁ •[ op ] y) ∘ E₂ = E₁ ∘ E₂ •[ op ] y +(v [ op ]• E₁) ∘ E₂ = v [ op ]• E₁ ∘ E₂ +block• E₁ ∘ E₂ = block• (E₁ ∘ E₂) +unblock• E₁ ∘ E₂ = unblock• (E₁ ∘ E₂) + +∘-lemma : forall {i j k} (E₁ : EvalCtxt j k) (E₂ : EvalCtxt i j) {x} -> + E₁ ∘ E₂ [ x ] ≡ E₁ [ E₂ [ x ] ] +∘-lemma • E₂ = ≡-refl +∘-lemma (E₁ •[ op ] y) E₂ = ≡-cong (\x -> x ⟨ op ⟩ y) (∘-lemma E₁ E₂) +∘-lemma (v [ op ]• E₁) E₂ = ≡-cong (_⟨_⟩_ ⌜ v ⌝ op) (∘-lemma E₁ E₂) +∘-lemma (block• E₁) E₂ = ≡-cong block (∘-lemma E₁ E₂) +∘-lemma (unblock• E₁) E₂ = ≡-cong unblock (∘-lemma E₁ E₂) + +-- Lifting of reductions. + +lift⟶ : forall {i j x y} (E : EvalCtxt i j) -> + x ⟶[ i ] y -> E [ x ] ⟶[ j ] E [ y ] +lift⟶ {j = k} E₁ (reduction {x = x} {y = y} E₂ r) = + ≡-subst (\y' -> E₁ [ E₂ [ x ] ] ⟶[ k ] y') (∘-lemma E₁ E₂) + (≡-subst (\x' -> x' ⟶[ k ] E₁ ∘ E₂ [ y ]) (∘-lemma E₁ E₂) + (reduction (E₁ ∘ E₂) r)) + +-- Lifting of reduction sequences. + +lift : forall {x i j y} (E : EvalCtxt i j) -> + x ⟶⋆[ i ] y -> E [ x ] ⟶⋆[ j ] E [ y ] +lift E r = gmap (\x -> E [ x ]) (lift⟶ E) r + +-- Completeness. + +complete : forall {e i v} -> e ⇓[ i ] v -> e ⟶⋆[ i ] ⌜ v ⌝ +complete (Val {n}) = begin val n ∎ +complete Throw = begin throw ∎ +complete (Add₁ {x} {y} {m} {n} x⇓ y⇓) = begin + x ⊕ y + ⟶⋆⟨ lift (• •[ ⊕′ ] y) (complete x⇓) ⟩ + val m ⊕ y + ⟶⋆⟨ lift (val m [ ⊕′ ]• •) (complete y⇓) ⟩ + val m ⊕ val n + ⟶⟨ reduction • Add₁ ⟩ + val (m + n) + ∎ +complete (Add₂ {x} {y} x↯) = begin + x ⊕ y + ⟶⋆⟨ lift (• •[ ⊕′ ] y) (complete x↯) ⟩ + throw ⊕ y + ⟶⟨ reduction • Add₂ ⟩ + throw + ∎ +complete (Add₃ {x} {y} {m} x⇓ y↯) = begin + x ⊕ y + ⟶⋆⟨ lift (• •[ ⊕′ ] y) (complete x⇓) ⟩ + val m ⊕ y + ⟶⋆⟨ lift (val m [ ⊕′ ]• •) (complete y↯) ⟩ + val m ⊕ throw + ⟶⟨ reduction • Add₃ ⟩ + throw + ∎ +complete (Seqn₁ {x} {y} {m} {v} x⇓ y⇒) = begin + x >> y + ⟶⋆⟨ lift (• •[ >>′ ] y) (complete x⇓) ⟩ + val m >> y + ⟶⟨ reduction • Seqn₁ ⟩ + y + ⟶⋆⟨ complete y⇒ ⟩ + ⌜ v ⌝ + ∎ +complete (Seqn₂ {x} {y} x↯) = begin + x >> y + ⟶⋆⟨ lift (• •[ >>′ ] y) (complete x↯) ⟩ + throw >> y + ⟶⟨ reduction • Seqn₂ ⟩ + throw + ∎ +complete (Catch₁ {x} {y} {m} x⇓) = begin + x catch y + ⟶⋆⟨ lift (• •[ catch′ ] y) (complete x⇓) ⟩ + val m catch y + ⟶⟨ reduction • Catch₁ ⟩ + val m + ∎ +complete (Catch₂ {x} {y} {v} x↯ y⇒) = begin + x catch y + ⟶⋆⟨ lift (• •[ catch′ ] y) (complete x↯) ⟩ + throw catch y + ⟶⟨ reduction • Catch₂ ⟩ + y + ⟶⋆⟨ complete y⇒ ⟩ + ⌜ v ⌝ + ∎ +complete (Int {x}) = begin + x + ⟶⟨ reduction • Int ⟩ + throw + ∎ +complete (Block {x} {v} x⇒) = begin + block x + ⟶⋆⟨ lift (block• •) (complete x⇒) ⟩ + block ⌜ v ⌝ + ⟶⟨ reduction • Block ⟩ + ⌜ v ⌝ + ∎ +complete (Unblock {x} {v} x⇒) = begin + unblock x + ⟶⋆⟨ lift (unblock• •) (complete x⇒) ⟩ + unblock ⌜ v ⌝ + ⟶⟨ reduction • Unblock ⟩ + ⌜ v ⌝ + ∎ + +-- Soundness. + +sound⟶ʳ : forall {e₁ e₂ i v} -> + e₁ ⟶ʳ[ i ] e₂ -> e₂ ⇓[ i ] v -> e₁ ⇓[ i ] v +sound⟶ʳ Add₁ Val = Add₁ Val Val +sound⟶ʳ Add₁ Int = Int +sound⟶ʳ Add₂ Throw = Add₂ Throw +sound⟶ʳ Add₂ Int = Int +sound⟶ʳ Add₃ Throw = Add₃ Val Throw +sound⟶ʳ Add₃ Int = Int +sound⟶ʳ Seqn₁ ⇓ = Seqn₁ Val ⇓ +sound⟶ʳ Seqn₂ Throw = Seqn₂ Throw +sound⟶ʳ Seqn₂ Int = Int +sound⟶ʳ Catch₁ Val = Catch₁ Val +sound⟶ʳ Catch₁ Int = Int +sound⟶ʳ Catch₂ ⇓ = Catch₂ Throw ⇓ +sound⟶ʳ Int Throw = Int +sound⟶ʳ Int Int = Int +sound⟶ʳ (Block {i} {val n}) Val = Block Val +sound⟶ʳ (Block .{U} {val n}) Int = Int +sound⟶ʳ (Block {i} {throw}) Throw = Block Throw +sound⟶ʳ (Block .{U} {throw}) Int = Int +sound⟶ʳ (Unblock {i} {val n}) Val = Unblock Val +sound⟶ʳ (Unblock .{U} {val n}) Int = Int +sound⟶ʳ (Unblock {i} {throw}) Throw = Unblock Throw +sound⟶ʳ (Unblock .{U} {throw}) Int = Int + +sound⟶ : forall {i j} (E : EvalCtxt i j) {e₁ e₂ v} -> + e₁ ⟶ʳ[ i ] e₂ -> E [ e₂ ] ⇓[ j ] v -> E [ e₁ ] ⇓[ j ] v +sound⟶ • r ⇒ = sound⟶ʳ r ⇒ +sound⟶ (E •[ ⊕′ ] y) r (Add₁ ⇓₁ ⇓₂) = Add₁ (sound⟶ E r ⇓₁) ⇓₂ +sound⟶ (E •[ ⊕′ ] y) r (Add₂ ↯₁) = Add₂ (sound⟶ E r ↯₁) +sound⟶ (E •[ ⊕′ ] y) r (Add₃ ⇓₁ ↯₂) = Add₃ (sound⟶ E r ⇓₁) ↯₂ +sound⟶ (E •[ ⊕′ ] y) r Int = Int +sound⟶ (E •[ >>′ ] y) r (Seqn₁ ⇓₁ ⇒₂) = Seqn₁ (sound⟶ E r ⇓₁) ⇒₂ +sound⟶ (E •[ >>′ ] y) r (Seqn₂ ↯₁) = Seqn₂ (sound⟶ E r ↯₁) +sound⟶ (E •[ >>′ ] y) r Int = Int +sound⟶ (E •[ catch′ ] y) r (Catch₁ ⇓₁) = Catch₁ (sound⟶ E r ⇓₁) +sound⟶ (E •[ catch′ ] y) r (Catch₂ ↯₁ ⇒₂) = Catch₂ (sound⟶ E r ↯₁) ⇒₂ +sound⟶ (E •[ catch′ ] y) r Int = Int +sound⟶ (v [ ⊕′ ]• E) r (Add₁ ⇓₁ ⇓₂) = Add₁ ⇓₁ (sound⟶ E r ⇓₂) +sound⟶ (v [ ⊕′ ]• E) r (Add₂ ↯₁) = Add₂ ↯₁ +sound⟶ (v [ ⊕′ ]• E) r (Add₃ ⇓₁ ↯₂) = Add₃ ⇓₁ (sound⟶ E r ↯₂) +sound⟶ (v [ ⊕′ ]• E) r Int = Int +sound⟶ (v [ >>′ ]• E) r (Seqn₁ ⇓₁ ⇒₂) = Seqn₁ ⇓₁ (sound⟶ E r ⇒₂) +sound⟶ (v [ >>′ ]• E) r (Seqn₂ ↯₁) = Seqn₂ ↯₁ +sound⟶ (v [ >>′ ]• E) r Int = Int +sound⟶ (v [ catch′ ]• E) r (Catch₁ ⇓₁) = Catch₁ ⇓₁ +sound⟶ (v [ catch′ ]• E) r (Catch₂ ↯₁ ⇒₂) = Catch₂ ↯₁ (sound⟶ E r ⇒₂) +sound⟶ (v [ catch′ ]• E) r Int = Int +sound⟶ (block• E) r Int = Int +sound⟶ (block• E) r (Block ⇒) = Block (sound⟶ E r ⇒) +sound⟶ (unblock• E) r Int = Int +sound⟶ (unblock• E) r (Unblock ⇒) = Unblock (sound⟶ E r ⇒) + +sound : forall e i v -> e ⟶⋆[ i ] ⌜ v ⌝ -> e ⇓[ i ] v +sound .(⌜ val n ⌝) i (val n) ε = Val +sound .(⌜ throw ⌝) i throw ε = Throw +sound .(E [ x ]) i v (reduction {x = x} {y} E r ◅ rs) = + sound⟶ E r (sound (E [ y ]) i v rs)