1
$\begingroup$

In Finding Lexicographic Orders for Termination Proofs in Isabelle/Holl the authors construct a method for proving termination of functions based on constructing a matrix that registers for each row the recursive calls in the body and for each column a measure. The matrix itself contains the information about the decrease of the measure on that specific call.

As an example of mutually recursive functions (page 46) they give:

even 0 = True
even Suc n = odd n
odd 0 = False
odd Suc n = even n

they state that they convert these functions into a single function over the sum type nat+nat. Apparently this transformation is explained in this thesis (page 117).

How would the transformed function look like?

They go on stating that this transformation give the following proof obligations:

wf ?R

$\land$n.(Inr n,Inl Suc n) $\in$?R

$\land$n.(Inl n,Inr Suc n) $\in$?R

where Inl,Inr are the injection functions for sum types. Similarly,

Do you understand why these proof obligations are derived? What are their meaning?

Finally, the step in which I am most interested. They introduce measure functions in this sum types in order to proof termination. The set of measures for $t_1 + t_2$ is:

$M(t_1+t_2) =\{case_+ m_1 m_2 | m_1 \in M(t_1),m_2 \in M(t_2)\}$

and they explain that this means that the measures are built taking all combinations for measures of $t_1$,$t_2$ and combining them with a case combinator for sum types which has signature $case_+ :: (\alpha \Rightarrow \gamma) \Rightarrow (\beta \Rightarrow \gamma) \Rightarrow (\alpha + \beta \Rightarrow \gamma)$.

Could you explain what the case combinator does?

So summarizing, I need a clarification on the construction idea, assuming no knowledge on sum types.

$\endgroup$
  • 1
    $\begingroup$ You could think of sum types as disjoint unions: a type A+B contains all elements of A and all elements of B (with a tag declaring if they come from A or from B). I do not understand how the termination checking works, but I assume you may want Nat+Nat in the transformed function if you want to "tag" whether you are in the middle of a call to "odd" or "even". $\endgroup$ – Mario Román Aug 2 '18 at 12:17

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.