I am trying to define mutually recursive functions that use two
categories of variables: time and space coordinates. HOL did not
distinguish between arguments when trying to prove termination. Is it
possible to specify the set of arguments that need to be considered
for proofing termination.
In the following simple example, The time argument of the calling
function is always strictly greater than those of the called functions.
This should be enough for the functions to terminate.
To define them using HOL, we have to prove that the summation of the
arguments of each of the called functions is strictly less than the
summation of the arguments of the calling function, which is not true
here.
val defn = Hol_defn "fn1fn2"
`(fn1 t x y =
if ((t = 0) \/ (x = 0) \/ (y = 0)) then 1 else
(fn1 (t - 1) x y ) + (fn2 (t - 1) x (y+1)))
/\
(fn2 t x y =
if ((t = 0) \/ (x = 0) \/ (y = 0)) then 1 else
(fn2 (t - 1) x y) + (fn1 (t - 1) x (y+1)))
`;
- e (WF_REL_TAC `^R`);
OK..
1 subgoal:
> val it =
(!y x t. ~(t = 0) /\ ~(x = 0) /\ ~(y = 0) ==> 0 < t) /\
(!y x t.
~(t = 0) /\ ~(x = 0) /\ ~(y = 0) ==>
t - 1 + (x + (y + 1)) < t + (x + y)) /\
(!y x t. ~(t = 0) /\ ~(x = 0) /\ ~(y = 0) ==> 0 < t) /\
!y x t.
~(t = 0) /\ ~(x = 0) /\ ~(y = 0) ==>
t - 1 + (x + (y + 1)) < t + (x + y)
: goalstack
-
Walid
-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
