1(*--------------------------------------------------------------------------- 2 3 Examples (some typed in by Ken Friis Larsen) from 4 5 "The Size-Change Principle for Program Termination", 6 Lee, Jones, Ben-Amram, Proceedings of POPL 2001 7 ---------------------------------------------------------------------------*) 8 9(*--------------------------------------------------------------------------- 10 1. Reverse function, with accumulating parameter. Automatic. 11 ---------------------------------------------------------------------------*) 12 13val REV = 14 Define 15 `(REV [] A = A) /\ 16 (REV (h::t) A = REV t (h::A))`; 17 18(*--------------------------------------------------------------------------- 19 2. Program with indirect recursion. We treat this as mutual recursion. 20 Need to define a type of s-expressions for this to be well-typed. 21 Not easy for TFL currently. 22 ---------------------------------------------------------------------------*) 23 24Hol_datatype `sexp = Nil | Cons of sexp => sexp`; 25 26val indirect_def = 27 tDefine 28 "indirect" 29 `(f Nil x = x) 30 /\ (f (Cons h t) x = g t x (Cons h t)) 31 /\ (g a b c = f a (Cons b c))` 32(WF_REL_TAC `inv_image ($< LEX $<) 33 (\s. (sum_case (\(x,y). sexp_size x) (\(a,b,c). sexp_size a) s, 34 sum_case (\v.0) (\v.1) s))`); 35 36 37(*--------------------------------------------------------------------------- 38 3. Function with lexically ordered parameters. Automatic. 39 ---------------------------------------------------------------------------*) 40 41val ack_def = 42 Define 43 `(ack (0,n) = n+1) 44 /\ (ack (SUC m,0) = ack(m,1)) 45 /\ (ack (SUC m, SUC n) = ack(m,ack(SUC m,n)))`; 46 47(*--------------------------------------------------------------------------- 48 4. Program with permuted parameters. Automatic. 49 ---------------------------------------------------------------------------*) 50 51val pparam = 52 Define 53 `pparam m n r = 54 if r > 0 then pparam m (r-1) n else 55 if n > 0 then pparam r (n-1) m 56 else m`; 57 58(*--------------------------------------------------------------------------- 59 5. Program with permuted and possibly discarded parameters. 60 Not easy for TFL currently. (measure function courtesy of Joe Hurd.) 61 ---------------------------------------------------------------------------*) 62 63val perm_def = tDefine 64 "perm" 65 `(perm x [] = x) /\ 66 (perm [] (y::ys) = perm (y::ys) ys) /\ 67 (perm (h::xs) z = perm z xs)` 68 (WF_REL_TAC 69 `measure \(l1,l2). 70 if NULL l1 then 2 * LENGTH l2 else LENGTH l1 + LENGTH l2` 71 THEN RW_TAC list_ss []); 72 73 74(*--------------------------------------------------------------------------- 75 6. Program with late-starting sequence of descending parameter 76 values. Automatic. 77 78 Note: late_g and late_g are defined in the reverse order in 79 the paper. We do it that way with multiDefine as well. 80 ---------------------------------------------------------------------------*) 81 82val late_g = 83 Define 84 ` (late_g [] d = d) 85 /\ (late_g (c::cs) d = late_g cs (c :: d))`; 86 87val late_f = 88 Define 89 ` (late_f a [] = late_g a []) 90 /\ (late_f a (x::xs) = late_f (x::a) xs)`; 91 92TotalDefn.multiDefine 93 `(late_f a [] = late_g a []) /\ 94 (late_f a (x::xs) = late_f (x::a) xs) /\ 95 (late_g [] d = d) /\ 96 (late_g (c::cs) d = late_g cs (c :: d))`; 97 98