Hi,
I have an inductive datatype called CCS and a recursive function FN trying
to collect all free names of any CCS term into a set:
val FN_def = Define `
(FN (nil :('a, 'b) CCS) (J: 'a set) = (EMPTY :'b Label set)) /\
...
(FN (rec x p) J = if (x IN J) then EMPTY
else FN (CCS_Subst p (rec x p) x)
(x INSERT J))`;
val free_names = new_definition ("free_names",
``free_names p = FN(p, EMPTY)``);
The only reason that HOL can’t prove the termination is because of the last
branch in above definition involving another recursive function CCS_Subst:
in some cases the term ``(CCS_Subst p (rec x p) x)`` may return ``(rec x
p)``, and as a result, the size of the first parameter of FN doesn’t
decrease!
But this is why I have the second parameter J of FN: whenever calculating
the value of ``FN (rec x p) J``, it first check if x is in the set J, and
the recursive call happens only if it’s not in, and then x is inserted into
J to prevent further recursive invocation of FN at deeper levels. So I
believe above definition is well-defined and must always terminate. In
another words, for all other branches, the size of CCS term must decrease
in recursive calls, and in the last branch, the cardinality of the set J
will increase.
I firstly tried to use WF_REL_TAC with a measure, but I could NOT find a
good measure with both parameters considered. For example, if I use “the
size of CCS term MINUS the cardinality of the set J”, which seems always
decrease in each recursive calls, i.e. WF_REL_TAC `measure (\x. (size o
FST) x - (CARD o SND) x)`, this is actually not a measure, because it may
also take negative values, thus not WF at all.
Now if I try to use Defn.tgoal to find the tacticals which helps HOL to
prove the termination, I got the following initial goal:
Initial goal:
∃R.
WF R ∧
(∀p J x.
x ∉ J ⇒ R (CCS_Subst p (rec x p) x,x INSERT J) (rec x p,J)) ∧
(∀q J p. R (p,J) (p || q,J)) ∧ (∀p J q. R (q,J) (p || q,J)) ∧
(∀q J p. R (p,J) (p + q,J)) ∧ (∀p J q. R (q,J) (p + q,J)) ∧
(∀l J p. R (p,J) (label l..p,J)) ∧
(∀rf J p. R (p,J) (relab p rf,J)) ∧ (∀J p. R (p,J) (τ..p,J)) ∧
∀L J p. R (p,J) (ν L p,J)
So the goal is nothing but to supply a relation such that, the parameter
pairs in each recursive call must be strictly “smaller”. But if I supply
such a relation:
Q.EXISTS_TAC `\x y. (size (FST x) < size (FST y)) \/
((size (FST x) = size (FST y)) /\ (CARD (SND x) > CARD (SND y)))`
which seems precisely captured my understanding on the termination
condition. But the funny thing is, I can prove all the sub-goals except for
the well-foundness (that is, WF R), which is automatically handled in the
WF_REL_TAC approach.
Can anyone suggest me some ideas or possible paths to resolve this issue?
or possible ways to prove the WF of arbitrary relations? Since all the
related defintions are long and omitted, I’m not expecting any ready-to-use
scripts.
Regards,
Chun Tian
--
Chun Tian (binghe)
University of Bologna (Italy)
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
