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
