Email Gateway (Aug 18 2022 at 17:37): Email Gateway (Aug 18 2022 at 17:37):From: 张欢欢 <hzhang@ecust.edu.cn>
Hi, I am thinking about proving termination of function. Can anyone tell me the differences between the following two:
1)
apply(relation inv_image(finite-psubset<lex>less-than) ...)
2) apply(measure ...)
I know the definition of measure is
definition
measure
::
"('a => nat) => ('a * 'a)set"
where
"measure == inv_image less_than"
and the definition of finite-psubset is
definition
finite_psubset
::
"('a set * 'a set) set"
where
"finite_psubset == {(A,B). A < B & finite B}"
But I hope someone can explain the detail meaning of the differences between the above two.
Thanks
Email Gateway (Aug 18 2022 at 17:38):From: Alexander Krauss <krauss@in.tum.de>
Hi,
In fact, 2) should be
apply (relation "measure ...")
It is the simplest way of specifying a termination relation, by giving a
function into the natural numbers, which decreases at each recursive call.
Example 1) is a bit trickier. It may help you to look at the types of
the subexpressions (e.g. finite_psubset).
Here, "..." must be a function that maps your function arguments into
the type 'a set * nat for some 'a. These pairs are then compared with
respect to the relation (finite-psubset <lex> less-than), which means
that first the sets are compared with the strict subset relation and
then the numbers are compared.
In other words, the relation
inv_image(finite-psubset<lex>less-than) (%x. (f x, g x))
is the same as
{ (x, y). (finite (f y) & f x \<subset> f y)
| (f x = f y & g x < g y) }
While in the second version it is easier to see what is going on, the
first version can be proved well-founded automatically, since it is
built from combinators (inv_image, <lex>, finite_psubset, less_than)
that already come with the relevant lemmas.
Hope this helps...
Alex
Last updated: Apr 19 2024 at 01:05 UTC