Dear All,
I'm interested in proving termination of nested functions and I
have some questions:
1- First I noticed that HOL is able to prove the termination of
this definition automatically:
Define `(ack 0 y = 1 + y)
/\ (ack (SUC u) 0 = ack u (SUC 0))
/\ (ack (SUC u) (SUC v) = ack u (ack (SUC u) v))`;
I want to know how, because I'm tried to prove it manually using
Hol_defn and I couldn't.
2 - Although the function above can be proved automatically the
following can't:
Define `ack x y = if (x = 0 ) then (1 + y ) else (if (y = 0 )
then (ack (x - 1 ) 1) else (ack (x - 1 ) (ack x (y - 1 ))))`;
I wanted to know why, and again if it is possible to prove it
manually.
3 - I want to know if it is possible to prove termination of a
function like this:
Hol_defn "nest" `nest x = if x = 0 then 0 else nest (nest x-1)`
Thank you for the time and help.
Cheers,
Augusto Silva
-------------------------------------------------------------------------
This SF.net email is sponsored by the 2008 JavaOne(SM) Conference
Don't miss this year's exciting event. There's still time to save $100.
Use priority code J8TL2D2.
http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
