Termination of Isabelle Functions via Termination of Rewriting

Introduction

The most popular instance of the generic proof assistant Isabelle is its instantiation to higher-order logic (Isabelle/HOL). The system provides a convenient functional programming layer having datatypes and recursive functions with pattern-matching. A necessary restriction for newly defined functions is that they are terminating. Otherwise a defining equation like

f x = f x + 1

would easily lead to inconsistency. There are already some built-in means to prove termination of functions automatically in some cases. However, by exploiting IsaFoR and devising suitable tactics to reduce termination of an Isabelle/HOL function to termination of a constructed term rewrite system, we are able to use external termination tools in order to prove termination of user-defined functions. In the following we demonstrate the usage of our approach by example. (A description of the internal construction is contained in a recently submitted paper.)

Note: We describe a prototype implementation and assume basic Isabelle knowledge.

Usage

If you want to use our approach in your own Isabelle/HOL theory, you have to base it on TermFun.thy (which is part of IsaFoR) as follows:

theory MyTheory imports TermFun begin

Note: Since the new commands define_trs and export_termination_problem are provided, you also have to update your keyword file when using Proof-General (an appropriate isar-keywords.el file is included in IsaFoR).

Now, the typical situation is that you define some new function that is not proved to be terminating automatically. We give two examples illustrating the usage of our approach in the following.

A First Example

The first example is a function remdups removing duplicates from a binary search tree. For quick reference, we first present remdups and its termination proof, then we explain the single steps of the proof in more detail, and finally, we give auxiliary definitions of datatypes and functions.

Proving Termination of remdups

 1  function remdups where
 2    "remdups E = E"
 3  | "remdups (N l x r) = N (remdups (del x l)) x (remdups (del x r))"
 4    by pat_completeness auto
 5  
 6  setup {* Term_Fun.register_datatypes ["Bin_Tree.tree"] *}
 7  define_trs getmax.simps
 8  define_trs delmax.simps
 9  define_trs del.simps
10  define_trs (no_sim) remdups.psimps
11  
12  termination remdups
13    apply (trs_reduce remdups)
14    apply (simp only: all_trs_defs set_list_conv)
15    export_termination_problem "remdups.xml" 
16    apply (ceta_import_proof "remdups.proof.xml")
17    apply ceta_eval
18  done

Detailed Description

Since the datatype tree is user-defined, we have to tell the system that it should provide a first-order term representation for it, which is done in line 6.

The four define_trs commands in lines 7 to 10, generate term rewrite systems (TRSs) for all involved functions. Note the attribute (no_sim) in the last command, which prevents the system from proving the simulation lemma of remdups, since this would require termination (consult the paper for more details). The result are the four TRSs (as HOL values) getmax.trs, delmax.trs, del.trs, and remdups.trs. Every TRS for a function f has the name f.trs and the definition (i.e., defining equation of f.trs) f.trs_def.

Line 13 takes care of reducing the termination proof obligation for remdups to termination of f.trs. A major part of our paper describes this process in more detail.

In line 14 the TRS is brought in a form that facilitates the XML export in the next line, that is, the set of rules is explicitly transformed into a finite list of rules. The command of line 15, creates the file remdups.xml in the current directory which contains an XML encoding (using the XML format of the termination competition) of the remdups TRS.

At this point, we can use an arbitray termination tool which supports the CPF format to proof termination of the generated TRS. (Special versions of AProVE and TTT2 that can be used to produce the necessary certificates are available for download.) We assume that the result is saved to the file remdups.proof.xml.

In line 16 the XML certificate is parsed into Isabelle/HOL and certified by CeTA's check-function in line 17. This concludes the proof.

Auxiliary Datatypes and Functions

The function remdups is based on the following user-defined datatype and auxiliary functions:

datatype tree = E | N tree nat tree

fun getmax where
  "getmax E = 0"
| "getmax (N l x E) = x"
| "getmax (N l x r) = getmax r"

fun delmax where
  "delmax E = E"
| "delmax (N l x E) = l"
| "delmax (N l x r) = N l x (delmax r)"

fun del where
  "del x E = E"
| "del x (N E y r) = 
   (if x < y then (N E y r)
    else if eq x y then del x r
    else N E y (del x r))"
| "del x (N l y r) = 
   (if x < y then N (del x l) y r
    else if x > y then N l y (del x r)
    else N (delmax (del x l)) (getmax (del x l)) (del x r))"

A Second Example

Assume you wanted to define the function

fun evenodd :: "bool => nat => bool"
where
  "evenodd True 0 = False " |
  "evenodd False x = (~ evenodd True x)" |
  "evenodd True (Suc x) = evenodd False x"

resulting in an error-message ending with something like

*** Could not find lexicographic termination order.
*** At command "fun" (line 3 of "MyTheory.thy")

Thus we tell the system that we want to switch to "expert-mode" and prove termination manually by using function instead of fun and proving the completeness of the involved patterns as follows

function evenodd :: "bool => nat => bool"
where
  "evenodd True 0 = False " |
  "evenodd False x = (~ evenodd True x)" |
  "evenodd True (Suc x) = evenodd False x"
  by (pat_completeness) auto

We now have the partial simplification rules evenodd.psimps

evenodd_dom (True, 0) ==> evenodd True 0 = False
evenodd_dom (False, ?x) ==> evenodd False ?x = (~ evenodd True ?x)
evenodd_dom (True, Suc ?x) ==> evenodd True (Suc ?x) = evenodd False ?x

whose shape indicates that termination is still missing (every equation has the precondition that evenodd is defined on the corresponding input).

The next step is to obtain a term rewrite system, representing the function evenodd. Since this function uses ~ (Isabelle/HOL's logical negation) we further need a TRS representation of negation. Both can be obtained as follows

define_trs not_True_eq_False not_False_eq_True
define_trs (no_sim) evenodd.psimps

where the no_sim suppresses the generation of so called simulation lemmas (consult the paper for further information). Internally, the following TRS was constructed (using the ASCII format of the termination competition):

(VAR x)(RULES
              Not(True) -> False
             Not(False) -> True
       evenodd(True, 0) -> False
      evenodd(False, x) -> Not(evenodd(True, x))
  evenodd(True, Suc(x)) -> evenodd(False, x)
)

which is available under the name evenodd.trs_def. Now, to prove termination of evenodd, we first reduce the termination obligation produced by Isabelle/HOL, to termination of the above TRS, using our trs_reduce method.

termination evenodd
  apply (trs_reduce evenodd)
  apply (simp only: all_trs_defs set_list_conv)

where all_trs_defs is a theorem containing all defined TRSs and set_list_conv is used to transform finite sets into lists. Afterward we export the resulting termination problem of evenodd.trs to an external XML file (using the XML format of the termination competition).

  export_termination_problem "evenodd.xml"

An arbitrary termination tool (which has to support the CPF format) can now be used to produce a termination proof in the file evenodd.proof.xml, which is parsed into Isabelle/HOL in turn.

  apply (ceta_import_proof "evenodd.proof.xml")

Finally, the proof is certified inside Isabelle/HOL and we are done.

  apply (ceta_eval)
done

All of these steps remain to be integrated in a more user-friendly interface in the future.