> because J is *NOT* assumed to be FINITE.
On 1 July 2017 at 16:51, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
> No ... my previous idea doesn't work. I got this goal unprovable:
>
> CARD (J DELETE a) < CARD J
> ------------------------------------
> a ∈ J
>
> because J is assumed to be FINITE.
>
> I think I still need to know how to put the cardinality bound into the
> relation for WF_REL_TAC ...
>
> Regards,
>
> Chun
>
>
> On 1 July 2017 at 16:28, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
>
>> Hi again,
>>
>> I think it's possible to change the original definition to make the
>> cardinality *decrease* instead: previous I use the set J as the set of
>> constants that have already been processed, but I can also rethink it as
>> the set of contants that *remains to be processed*:
>>
>> So now I have a definition like this:
>>
>> val FN_defn = Hol_defn "FN" `
>> (FN (nil :('a, 'b) CCS) (J: 'a set) = (EMPTY :'b Label set)) /\
>> (FN (prefix (label l) p) J = l INSERT (FN p J)) /\
>> (FN (prefix tau p) J = FN p J) /\
>> (FN (sum p q) J = (FN p J) UNION (FN q J)) /\
>> (FN (par p q) J = (FN p J) UNION (FN q J)) /\
>> (FN (restr L p) J = (FN p J) DIFF (L UNION (IMAGE COMPL_LAB L))) /\
>> (FN (relab p rf) J = IMAGE (REP_Relabeling rf) (FN p J)) /\
>> (FN (var x) J = EMPTY) /\
>> (FN (rec x p) J = if (x IN J) then
>> FN (CCS_Subst p (rec x p) x) (J DELETE x)
>> else EMPTY) `;
>>
>> and by following your way, using: WF_REL_TAC `inv_image ($< LEX $<) (\x.
>> (size (FST x), CARD (SND x)))`, and then I have the following sub-goal
>> which looks perfect: (and no need to prove the well-foundness any more)
>>
>> Current goal:
>>
>> size (CCS_Subst p (rec x p) x) < size (rec x p) ∨
>> (size (CCS_Subst p (rec x p) x) = size (rec x p)) ∧
>> CARD (J DELETE x) < CARD J
>> ------------------------------------
>> x ∈ J
>>
>> To actually use this definition, I need to set the initial J set as the
>> set of all constants in the CCS term, but that's irrelevant to the above FN
>> definition. So I would say my initial problem has completely resolved.
>>
>> Thank you again!!!
>>
>> Regards,
>>
>> Chun Tian
>>
>>
>> On 1 July 2017 at 12:55, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:
>>
>>> 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
>>>>
>>>>
>>>
>>
>>
>> --
>> Chun Tian (binghe)
>> University of Bologna (Italy)
>>
>>
>
>
> --
> Chun Tian (binghe)
> University of Bologna (Italy)
>
>
--
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
