New (in-)decision procedure for termination

diff --git a/ocaml/pure.ml b/ocaml/pure.ml
index 11cb9af81638ca6f546cd2a7e67ed182a3f9f50c..3bd7ec491a11059bd91c9a90800f58175fb62cf6 100644 (file)
--- a/ocaml/pure.ml
+++ b/ocaml/pure.ml
@@ -90,11 +90,20 @@ in
      String.concat "," (List.map print_machine s) ^ "]"
 ;; *)
 
+  let omega = let delta = L(A(V 0, V 0)) in A(delta,delta)
+
+  let rec is_divergent =
+   function
+      t when t = omega -> true
+    | A(t,_) -> is_divergent t
+    | L(t) -> is_divergent t
+    | _ -> false
+
   let mwhd m =
    let rec aux g =
     function
     (* mmm -> print_endline (print_machine mmm); match mmm with *)
-        m when unwind m = let d = L(A(V 0, V 0)) in A(d,d) -> [], B, []
+        m when is_divergent (unwind m) -> [], B, []
      | (e,A(t1,t2),s) ->
          let t2' = aux g (e,t2,[]) in
          let (_,t,_) = t2' in