Hi Ramana,
Thanks very much! Yes, actually I was seeking HOL's operator for
building lexicographic
relations but couldn't find it...
For the cardinality of J, it will finally equal to the number of ``rec``
operators inside the input CCS term, and loosely speaking, ``CARD J``
should always smaller than ``size p``, which p is the initial first
parameter. But how can I incorporate this information into the relation?
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)
------------------------------------------------------------------------------
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
