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.

  • 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 agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.