Hi Chun Tian,
I'd have to look more closely at your desired function to be able to help.
But, it's late and my eyes are giving out.
If all you are after is to compute free names, maybe there is a better way.
The following is what I would do for defining an operation calculating the
free variables
in the lambda calculus, and the same idea should I hope also work for CCS.
The main benefit is that
you don't have a call to another function (substitution) in the recursive
call. And termination
is trivial.
---------------------------------------------------------------------------------------------------
load "stringLib";
Datatype `term = Var string | App term term | Abs string term`;
val FV_def =
Define
`(FV (Var s) scope = if s IN scope then {} else {s}) /\
(FV (App t1 t2) scope = FV t1 scope UNION FV t2 scope) /\
(FV (Abs v t) scope = FV t (v INSERT scope))`;
On Sat, Jul 1, 2017 at 4:14 AM, Chun Tian (binghe) <binghe.l...@gmail.com>
wrote:
> 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
>
>
------------------------------------------------------------------------------
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
