NEWS about measure functions
Tue, 13 May 2008 09:10:56 +0200
changeset 26877 c3bb1f397811
parent 26876 d50ef6b952ba
child 26878 1aeac4d6b377
NEWS about measure functions
--- a/NEWS	Mon May 12 23:01:13 2008 +0200
+++ b/NEWS	Tue May 13 09:10:56 2008 +0200
@@ -244,6 +244,22 @@
 reconstruction_modulus, reconstruction_sorts renamed
 sledgehammer_modulus, sledgehammer_sorts.  INCOMPATIBILITY.
+* More flexible generation of measure functions for termination proofs:
+Measure functions can be declared by proving a rule of the form
+"is_measure f" and giving it the [measure_function] attribute. The
+"is_measure" predicate is logically meaningless (always true), and
+just guides the heuristic.  To find suitable measure functions, the
+termination prover sets up the goal "is_measure ?f" of the appropriate
+type and generates all solutions by prolog-style backwards proof using
+the declared rules.
+This setup also deals with rules like 
+  "is_measure f ==> is_measure (list_size f)"
+which accomodates nested datatypes that recurse through lists. Similar
+rules are predeclared for products and option types.
 *** ZF ***