Email Gateway (Aug 22 2022 at 15:23): Email Gateway (Aug 22 2022 at 15:23):From: Lars Hupel <hupel@in.tum.de>
Dear Isabelle power users,
the following is more of a "problem statement" rather than any concrete
suggestion. I've found an interesting side effect of how the function
package works in combination with the way local theories are handled in
Isabelle, and thought I should document it here and solicit opinions.
Consider the function "sum_list". It's very simple.
sum_list [] = 0
sum_list (x # xs) = x + sum_list xs
Instead of defining this with "primrec", assume it has been defined with
"fun".
"fun" will helpfully prove termination of this automatically. Before
doing so, it defines "sum_list_rel", which is a a set of pairs
(essentially, containing all tuples "(x # xs, x)"). Then, the automatic
termination proof shows that this relation is wellfounded, i.e., that
there are no infinite descending chains.
Note how "sum_list_rel" only talks about "op #", but not about "0" or
"op +". In other words, the termination condition of "sum_list" is
independent of class axioms. The most general type of "sum_list_rel"
could be more general ("'a::type") than that of "sum_list"
("'a::{plus,zero}").
The sort constraint carried by "sum_list_rel" is necessary because – as
far as I can tell – all internal constructions of the function package
happen in the same local theory, which means that you can't have both
"'a::type" and "'a::{plus,zero}".
Why is this interesting to me? During dictionary construction, I define
a new version of "sum_list" which doesn't have sort constraints. When
trying to "port" the original termination proof of "sum_list" I need to
play tricks with parametricity to get rid of the sort constraints (in
essence, I also need to define a sort-less "sum_list_rel" and prove
simulation). If "sum_list_rel" were sort-less, I wouldn't have these
problems.
The following questions are of interest to me:
To people familiar with how local theories work: Is changing the
function package to make it define the termination relation with less
sort constraints feasible? Or would that produce unwanted side effects,
e.g. when defining a function in a class instantiation?
To users of the function package: Can you give me an example of a
function that uses class axioms to prove termination? Or possibly
requires a "fundef_cong" rule with a sort constraint?
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:24):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear Lars,
Here is an example: look at function sqrt_approx_main in AFP/Sqrt_Babylonian/Sqrt_Babylonian.
It is of type “‘a :: {linordered_field,floor_ceiling} => ‘a” and uses the distance to the
sqrt as termination measure, so some argument which definitely requires reasoning about fields, etc.
Perhaps not the easiest example, but one which falls into the desired class.
Cheers,
René
Email Gateway (Aug 22 2022 at 15:24):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Hi again,
looking a bit further, I also found a fundef-cong-rule which contains
sort-constraints, namely sum.cong.
Look at AFP/Bernoulli/Bernoulli.thy, function bernoulli.
Cheers,
René
Email Gateway (Aug 22 2022 at 15:24):From: Lars Hupel <hupel@in.tum.de>
sum.cong is a great example, thanks!
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:24):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lars,
my PhD thesis contains a contrived example in §4.6.2 Definitional
eliminating of overloading
Cheers,
Florian
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC