Hi Chun,
Your relation that works looks like a lexicographic relation, which is
something wf_rel_tac should be able to handle automatically.
Could you try providing it using the LEX combinator, e.g.,
wf_rel_tac`inv_image ($< LEX $<) (\x y. (size(FST x), CARD(SND y)))`
Actually, looking more closely, I see that you want the cardinality of J to
_increase_. This is not obviously well-founded: can you explain what the
upper limit of the cardinality of J is, and incorporate this into the
relation?
Cheers,
Ramana
On 1 July 2017 at 19:51, Konrad Slind <konrad.sl...@gmail.com> wrote:
> 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
>
>
------------------------------------------------------------------------------
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
