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)
------------------------------------------------------------------------------
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
