Email Gateway (Aug 18 2022 at 11:32): Email Gateway (Aug 18 2022 at 11:32):From: George Karabotsos <g_karab@cs.concordia.ca>
Hello all,
I am a bit confused with function termination. In particular on the
manner the sum of types for mutually recursive functions are defined.
For example consider the attached toy theory (although none of them is
mutually recursive I believe they illustrate my confusion). Can someone
show me how I can prove termination for the quartet t1,t2,t3,and t4
functions? I know it can be proven using lexicographic_order. However,
I am more interested in proving termination via a measure function in
order to additionally understand how the summation of the types is
packaged together.
TIA,
George
FunTerm.thy
Email Gateway (Aug 18 2022 at 11:32):From: Alexander Krauss <krauss@in.tum.de>
George Karabotsos wrote:
The function package builds a balanced tree for the sum types: If you
have four functions with argument types T1,... T4, then you have to
provide a relation over the nested sum type
(T1 + T2) + (T3 + T4)
but your relation is on
T1 + T2 + T3 + T4
which is synonymous for
T1 + (T2 + (T3 + T4)) .
You can check what kind of relation you have to give by writing
termination
proof
Then the "proof" command applies the rule which is also applied by the
"relation" method, but without instantiating the relation. You can then,
say, enable "show types"...
Hope this helps,
Alex
Last updated: May 03 2024 at 04:19 UTC