Re: [Hol-info] proving termination on a partial recursive function.

David Sanan Mon, 31 Mar 2014 11:01:55 -0700

Konrad, thanks for the hint and for the link to your article.

Best,
David.

On 31 Mar 2014, at 22:10, "Konrad Slind" <[email protected]> wrote:

Hi David,

Adding extra constraints to the definition of listInsert is what I would suggest. The
typical thing to do is to add the constraints via if-then-else:

f(x) = if <constraints>
then <body of function>
else ARB

You will get a constrained function definition and induction theorem. How these look,

and how to use them can be found in the example on Depth-First Traversal in
the Adapting Functional Programs to Higher Order Logic Paper Scott Owens and I
wrote. Here's a link to it:

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.96.6938

Konrad.

On Mon, Mar 31, 2014 at 6:45 AM, David Sanan <[email protected]> wrote:
Hello all,
I want to prove termination of a partial recursive function that insert an element in a linked list, which is modeled using a finite mapping to represent the heap, which can contain element of type list or nodes of the list.

I use Hol_defn to define the recursive function

val listInsertRec_def = Hol_defn "listInsertRec" `
(listInsertRec h elemIndex pIndex laddr =
let nextElemIndex = (getField next (h ' pIndex)) in
if (getField index (h ' nextElemIndex)) <= (getField index (h ' elemIndex)) then
listInsertRec h elemIndex nextElemIndex laddr
else
listInsertAfter h pIndex elemIndex laddr )
`;

This generates the function definition, induction, and the following termination conditions:

0. ∀laddr elemIndex pIndex h nextElemIndex.
(nextElemIndex = getField next (h ' pIndex)) ∧
getField index (h ' nextElemIndex) ≤
getField index (h ' elemIndex) ⇒
R (h,elemIndex,nextElemIndex,laddr) (h,elemIndex,pIndex,laddr)
1. WF R:

R should be related to the length of the sublist starting at pIndex and ending at a fixed last element, so at each step the length of this sublist decreases, so I can use the measure relation. However, I am struggling to see how can I add assumptions related to the heap and to that fixed element, which belong to a global invariant.

Is this possible or should I add these constrains to the definition of listInsert in order to restrict the domain of the function?

Thanks!

Cheers,
David.

------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info

------------------------------------------------------------------------------

_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] proving termination on a partial recursive function.

Reply via email to