From 6e5e1945c99404f171f90a93c18c336aaeaab546 Mon Sep 17 00:00:00 2001 From: acondolu Date: Thu, 31 May 2018 18:27:51 +0200 Subject: [PATCH] New (in-)decision procedure for termination --- ocaml/pure.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/ocaml/pure.ml b/ocaml/pure.ml index 11cb9af..3bd7ec4 100644 --- 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 -- 2.39.2