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 <[email protected]> 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 <[email protected]> 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) <[email protected]
>> > 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
>>> [email protected]
>>> 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
>> [email protected]
>> 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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
