[Added a characterisation of infinite reduction sequences.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080617145207] adddir ./Semantics/SmallStep
hunk ./Everything.agda 23
+import Semantics.SmallStep.StepGroups  -- Currently unused.
addfile ./Semantics/SmallStep/StepGroups.agda
hunk ./Semantics/SmallStep/StepGroups.agda 1
+------------------------------------------------------------------------
+-- A characterisation of infinite reduction sequences
+------------------------------------------------------------------------
+
+module Semantics.SmallStep.StepGroups where
+
+open import Syntax
+open import Infinite
+open import Semantics.SmallStep
+
+open import Data.Nat
+open import Data.Nat.Properties
+open import Data.Bool
+open import Data.Product
+open import Data.Star
+open import Data.Star.Decoration
+open import Data.Unit
+open import Relation.Nullary
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+open import Induction.Nat
+
+-- The size of an annotated expression (the number of run
+-- constructors).
+
+mutual
+
+  size : forall {t} -> Exprˢ t -> ℕ
+  size (run  x) = 1 + size' x
+  size (done v) = 0
+
+  size' : forall {t} -> Exprˢ' t -> ℕ
+  size' (val n)     = 0
+  size' throw       = 0
+  size' loop        = 0
+  size' (x ⊕ y)     = size x + size y
+  size' (x >> y)    = size x + size y
+  size' (x catch y) = size x + size y
+  size' (block x)   = size x
+  size' (unblock x) = size x
+
+size-lemma : forall {t i j x y} (E : EvalCtxt t i j) ->
+             size x > size y -> size (E [ x ]) > size (E [ y ])
+size-lemma •                  gt = gt
+size-lemma (E •< |⊕| >     y) gt = s≤s (size-lemma E gt +-mono Poset.refl ℕ-poset)
+size-lemma (E •< |>>| >    y) gt = s≤s (size-lemma E gt +-mono Poset.refl ℕ-poset)
+size-lemma (E •< |catch| > y) gt = s≤s (size-lemma E gt +-mono Poset.refl ℕ-poset)
+size-lemma (val m ⊕• E)       gt = s≤s (size-lemma E gt)
+size-lemma (handler• E)       gt = s≤s (size-lemma E gt)
+size-lemma (block• E)         gt = s≤s (size-lemma E gt)
+size-lemma (unblock• E)       gt = s≤s (size-lemma E gt)
+
+-- A reduction step is "safe" if it does not involve unfolding loops,
+-- fixpoints or other potentially non-terminating computations.
+
+safeʳ : forall {t} {x y : Exprˢ t} {i} -> x ⟶ʳ[ i ] y -> Bool
+safeʳ Loop = false
+safeʳ _    = true
+
+Safeʳ : forall {t} {x y : Exprˢ t} {i} -> x ⟶ʳ[ i ] y -> Set
+Safeʳ r = T (safeʳ r)
+
+Safe : forall {t} {x y : Exprˢ t} {i} -> x ⟶[ i ] y -> Set
+Safe (Red E r) = Safeʳ r
+
+-- Safety is a decidable proprty.
+
+safeʳ? : forall {t} {x y : Exprˢ t} {i}
+         (r : x ⟶ʳ[ i ] y) -> Dec (Safeʳ r)
+safeʳ? r with inspect (safeʳ r)
+... | true  with-≡ eq = yes (≡-subst T eq tt)
+... | false with-≡ eq = no  (≡-subst T (≡-sym eq))
+
+safe? : forall {t} {x y : Exprˢ t} {i} (r : x ⟶[ i ] y) -> Dec (Safe r)
+safe? (Red E r) = safeʳ? r
+
+-- In a safe step the size decreases.
+
+size-decreasesʳ : forall {t} {x y : Exprˢ t} {i}
+                  (r : x ⟶ʳ[ i ] y) -> Safeʳ r -> size x > size y
+size-decreasesʳ Val       _  = s≤s z≤n
+size-decreasesʳ Throw     _  = s≤s z≤n
+size-decreasesʳ Loop      ()
+size-decreasesʳ Add₁      _  = s≤s z≤n
+size-decreasesʳ Add₂      _  = s≤s z≤n
+size-decreasesʳ Add₃      _  = s≤s z≤n
+size-decreasesʳ Seqn₁     _  = Poset.refl ℕ-poset
+size-decreasesʳ Seqn₂     _  = s≤s z≤n
+size-decreasesʳ Catch₁    _  = s≤s z≤n
+size-decreasesʳ Catch₂    _  = s≤s z≤n
+size-decreasesʳ Block     _  = s≤s z≤n
+size-decreasesʳ Unblock   _  = s≤s z≤n
+size-decreasesʳ (Int int) _  = s≤s z≤n
+
+size-decreases : forall {t} {x y : Exprˢ t} {i}
+                 (r : x ⟶[ i ] y) -> Safe r -> size x > size y
+size-decreases (Red E r) safe = size-lemma E (size-decreasesʳ r safe)
+
+-- Hence any infinite reduction sequence has to contain an infinite
+-- number of unsafe steps, with only a finite number of safe steps
+-- between any two unsafe ones:
+
+data StepGroup {t} (i : Status) (x z : Exprˢ t) : Set where
+  group : forall {y}
+          (x⟶⋆y : x ⟶⋆[ i ] y) (all-safe : All Safe x⟶⋆y)
+          (y⟶z : y ⟶[ i ] z)   (unsafe : ¬ Safe y⟶z) ->
+          StepGroup i x z
+
+_⟶∞[_]' : forall {t} (x : Exprˢ t) (i : Status) -> Set
+x ⟶∞[ i ]' = Infinite (StepGroup i) x
+
+-- Extracts the initial step group from an infinite reduction
+-- sequence.
+
+initial-group : forall {t} {x : Exprˢ t} {i} ->
+                x ⟶∞[ i ] -> ∃ \y -> StepGroup i x y × y ⟶∞[ i ]
+initial-group {x = x} = <-rec Pred step (size x) ≡-refl
+  where
+  Pred = \n -> forall {t} {x : Exprˢ t} {i} ->
+               size x ≡ n ->
+               x ⟶∞[ i ] ->
+               ∃ \y -> StepGroup i x y × y ⟶∞[ i ]
+
+  step : (n : ℕ) -> <-Rec Pred n -> Pred n
+  step .(size x) rec {x = x} ≡-refl (_◅∞_ {y = y} r rs) with safe? r
+  step .(size x) rec {x = x} ≡-refl (_◅∞_ {y = y} r rs) | no ¬s = (y , group ε ε r ¬s , rs)
+  step .(size x) rec {x = x} ≡-refl (_◅∞_ {y = y} r rs) | yes s
+    with rec (size y) (≤⇒≤′ (size-decreases r s)) ≡-refl rs
+  step .(size x) rec {x = x} ≡-refl (_◅∞_ {y = y} r rs) | yes s
+    | (z , group rs' ss last ¬s , rest) = (z , group (r ◅ rs') (↦ s ◅ ss) last ¬s , rest)
+
+-- Constructs all step groups corresponding to an infinite reduction
+-- sequence.
+
+all-groups : forall {t} {x : Exprˢ t} {i} ->
+             x ⟶∞[ i ] -> x ⟶∞[ i ]'
+all-groups x⟶∞ with initial-group x⟶∞
+all-groups x⟶∞ | (_ , g , rest) ~ g ◅∞ all-groups rest
+
+-- Flattens the groups. (The definition of append has been inlined
+-- here in order to please the productivity checker...)
+
+flatten : forall {t} {x : Exprˢ t} {i} ->
+          x ⟶∞[ i ]' -> x ⟶∞[ i ]
+flatten (group ε            _          x⟶y _  ◅∞ y⟶∞) ~ x⟶y ◅∞ flatten y⟶∞
+flatten (group (x⟶y ◅ y⟶⋆z) (↦ s ◅ ss) z⟶u ¬s ◅∞ u⟶∞) ~
+  x⟶y ◅∞ flatten (group y⟶⋆z ss z⟶u ¬s ◅∞ u⟶∞)