[Tried showing that the code is terminating.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080209205756
 + The termination checker does not accept this code, though. Reason:
   Inequalities like sizeC c < suc (sizeC c) are not derived.
] hunk ./NotStructurallyRecursive.agda 1
--- The code derived by Hutton/Wright is not structurally recursive. Is
--- it terminating? Presumably it is, but I'll try to find out after
--- getting some sleep.
+-- The code derived by Hutton/Wright is not structurally recursive.
+-- However, it is terminating.
hunk ./NotStructurallyRecursive.agda 7
+open import Logic
hunk ./NotStructurallyRecursive.agda 18
+sizeE : Expr -> ℕ
+sizeE (val n)   = 1
+sizeE (e₁ ⊕ e₂) = 3 + sizeE e₁ + sizeE e₂
+
+sizeC : Cont -> ℕ
+sizeC STOP       = 0
+sizeC (EVAL e c) = 2 + sizeE e + sizeC c
+sizeC (ADD  n c) = 1 + sizeC c
+
hunk ./NotStructurallyRecursive.agda 29
-  eval : Expr -> Cont -> ℕ
-  eval (val n)   c = exec c n
-  eval (e₁ ⊕ e₂) c = eval e₁ (EVAL e₂ c)
+  eval : forall s (e : Expr) (c : Cont) ->
+         sizeE e + sizeC c ≡ s -> ℕ
+  eval .(suc (sizeC c))
+       (val n)   c ≡-refl = exec (sizeC c) c n ≡-refl
+  eval .(suc (suc (suc ((sizeE e₁ + sizeE e₂) + sizeC c))))
+       (e₁ ⊕ e₂) c ≡-refl = eval (suc (suc ((sizeE e₁ + sizeE e₂) + sizeC c)))
+                                 e₁ (EVAL e₂ c) {! !}
hunk ./NotStructurallyRecursive.agda 37
-  exec : Cont -> ℕ -> ℕ
-  exec STOP       n = n
-  exec (EVAL e c) n = eval e (ADD n c)
-  exec (ADD n c)  m = exec c (n + m)
+  exec : forall s (c : Cont) -> ℕ -> sizeC c ≡ s -> ℕ
+  exec .0
+       STOP       n ≡-refl = n
+  exec .(suc (suc (sizeE e + sizeC c)))
+       (EVAL e c) n ≡-refl = eval (suc (sizeE e + sizeC c)) e (ADD n c) {! !}
+  exec .(suc (sizeC c))
+       (ADD n c)  m ≡-refl = exec (sizeC c) c (n + m) ≡-refl
hunk ./NotStructurallyRecursive.agda 46
-run e = eval e STOP
+run e = eval (sizeE e + 0) e STOP ≡-refl