Transcript fx 1

Termination Analysis
Math Foundations of Computer
Science
Topics
 Definitional principle
 Soundness and termination
 Proving termination and measure
functions
 Well ordering and natural numbers
 Induction and termination
 Recursively defined data structures
 Undecidability of termination
Definitional Axiom
(defunc f (x1 . . . xn)
:input-contract ic
:output-contract oc
body)
If the function f is admissible
Add definitional axiom for f: ic  [(f x1 . . . xn)
= body]
Add contract theorem for f: ic  oc
Definitional Principle
(defunc f (x1 . . . xn)
:input-contract ic
:output-contract oc
body)
The function f is admissible
f is a new function (no other axioms about f)
xi’s are distinct
body is a term, possibly using f, but with no free
variables other than xi’s
f is terminating
ic  oc is a theorem
body contracts hold under assumption of ic
Soundness and Global Variables
(defunc f (x)
:input-contract t
:output-contract t
y)
The definitional axiom for f leads to
unsound logic
Substituting ((x 0) (y nil)) we get (f 0) = nil
Substituting ((x 0) (y t)) we get (f 0) = t
Which implies t = nil.
Soundness and Termination
(defunc f(x)
:input-contract (natp x)
:output-contract (natp (f x))
(+ 1 (f x)))
 The definitional axiom for f leads to unsound
logic





(natp x)  x  x+1 [property of natural numbers]
(natp (f x))  (f x)  (+ 1 (f x)) [instantiate above]
(natp x)  (f x)  (+ 1 (f x)) [from ic  oc]
(natp x)  (f x) = (+ 1 (f x)) [from def axiom]
(natp x)  nil [from p p = nil]
How do we Prove Termination
 For recursive functions show that the
“size” of the inputs get smaller and
eventually must hit a base case
 Size is defined to be a function to the
natural numbers
 Use the well ordering principle of the
natural numbers to conclude that the
number of recursive calls can not be
infinite
Well Ordering of Natural
Numbers
 Any decreasing sequence of natural
numbers is finite. I.E. it terminates
 This implies that any non-empty set of
natural numbers has a minimum element
 Induction works as long as we have
termination
sum
(defunc sum (n)
:input-contract (natp n)
:output-contract (integerp (sum n))
(if (equal n 0)
0
(+ n (sum (- n 1)))))
 The input to the recursive call (- n 1) is smaller than the
input to sum and the decreasing sequence of natural
numbers n, n-1, n-2,... must terminate (equal 0) after a
finite number of steps
 If (integerp n) this would not be guaranteed
app
(defunc app (a b)
:input-contract (and (listp a) (listp b))
:output-contract (and (listp (app a b))
(if (endp a)
b
(cons (first a) (app (rest a) b))))
 This is a terminating function. Define the size of l to be
(len l).
 (len l) is a natural number
 (len (rest l)) < (len l)
 Implies len must eventually equal zero, i.e. l = nil
Measure Functions
 Technically we measure size with a
measure function
 A measure function m for the function f
 m is an admissible function defined over the
parameters of f
 m has the same input contract as f
 The output contract for m is (natp (m … ))
 For every recursive call, m applied to the
arguments decreases, under the conditions
that led to the recursive call.
Example Measure function
(defunc app (a b)
:input-contract (and (listp a) (listp b))
:output-contract (and (listp (app a b))
(if (endp a)
b
(cons (first a) (app (rest a) b))))
(defunc m (x y)
:input-contract (and (listp x) (listp y))
:output-contract (natp (m x y))
(len x))
(< (m (rest x) y) (m x y)) since (< (len (rest x)) (len x))
Induction Depends on
Termination
 Show that the induction scheme for a nonterminating function can lead to
unsoundness even when the definitional
axiom does not
 Alternative proof for the induction
principle that shows “termination” front
and center
General Induction Scheme
(defunc foo (x1 . . . xn)
:input-contract ic
:output-contract oc
(cond (t1 c1)
(t2 c2)
...
(tm cm)
(t cm+1)))
 None of the ci’s should have ifs in them
 If ci has a recursive call to foo, it is called a recursive case
otherwise a base case.
General Induction Scheme
 Case1 = t1
 Case2 = t2  t1
…
 Casei = ti  t1    ti-1
…
 Casem+1 = t  t1    tm
 If ci is a recursive case with Ri calls to foo with the jth call,
1  j  Ri, obtained by the substitution (foo x1 . . . xn)|sij
General Induction Scheme
To prove  prove the following
ic  
[ic  Casei] 
For all ci’s that are base cases
[ic  Casei  1 i  Ri |sij]  
For all ci’s that are recursive cases
Induction Scheme for
Non-terminating Function
(defunc f (x)
:input-contract t
:output-contract t
(f x))
 The definitional axiom, i.e. (f x) = (f x) is ok
 The induction scheme for f is unsound
 (not t)    nil    t
t     t
 Using this scheme we can derive  for any 
 In particular, we can derive nil
Induction Scheme over Naturals
 Every terminating function gives rise to an
induction scheme
1. (not (natp n)) ⇒ 
2. (natp n) ∧ (equal n 0) ⇒ 
3. (natp n) ∧ (not (equal n 0)) ∧ |((n n-1)) ⇒ 
 (1) and (2) are base cases and (3) is the
induction hypothesis
 More powerful than case analysis since you
can use assume the induction hypothesis
Proof by Contradiction
 Assume the conclusion is false and show
that that leads to a contradiction.
 1    n    1    n    F
 Proof.
 A  B  C  A  C  B (show this is valid)
 Apply to (1    n)  T  
Why does Induction Work?
 Suppose we prove the three cases in the
induction scheme but  is not valid.
 Let S be the set of ACL2 objects for which  is
false. By (1) and (2), S is a set of natural
numbers not equal to 0.
 Since S is a set of natural numbers it has a
smallest element s  0 for which |((n s)).
 This implies by (3) that |((n s-1)) is false and s-1
 S which is a contradiction
Non-terminating Function
(defunc f (x)
:input-contract t
:output-contract f
(f x))
 The induction scheme associated with f leads to
unsoundness (i.e. we can derive nil)
Termination for Recursively
Defined Data Structures
 For recursively defined data structures like
lists, trees, expression trees, etc. we can
use the number of constructors for the
size
 Number of cons’s for lists
 Number of nodes for trees
 Number of +’s, -’s, *’s and /’s for expression
trees
Boolean Expressions
BExpr :=
Constant: T|F [t | nil]
Variable [symbol]
Negation:  BExpr [(not BExpr)]
And: BExpr  BExpr [(and BExpr BExpr)
Or: BExpr  Bexpr [(or BExpr BExpr)]
23
Predicate
(defunc booleanexprp (expr)
:input-contract t
:output-contract (booleanp (booleanexprp expr))
(cond
( (is-constant expr) t )
( (is-variable expr) t )
( (is-not expr) (booleanexprp (op1 expr)) )
( (is-or expr) (and (booleanexprp (op1 expr))
(booleanexprp (op2 expr))) )
( (is-and expr) (and (booleanexprp (op1 expr))
(booleanexprp (op2 expr))) )
( t nil)
)
)
Evaluation
(defunc bool-eval (expr env)
:input-contract (and (booleanexprp expr)
(environmentp env)
(all-variables-defined expr env))
:output-contract (booleanp (bool-eval expr env))
(cond
( (is-constant expr) expr )
( (is-variable expr) (lookup expr env) )
( (is-not expr) (not (bool-eval (op1 expr) env)) )
( (is-or expr) (or (bool-eval (op1 expr) env)
(bool-eval (op2 expr) env)) )
( (is-and expr) (and (bool-eval (op1 expr) env)
(bool-eval (op2 expr) env)) )
)
)
Measure Function
(defun m (expr env)
:input-contract (and (booleanexprp expr)
(environmentp env)
(all-variables-defined expr env))
:output-contract (natp (m expr env))
(cond
( (is-constant expr) 0 )
( (is-variable expr) 0 )
( (is-not expr) (+ 1 (m (op expr) env)) )
( (is-or expr) (+ 1 (m (op1 expr) env) (m (op2 expr) env)) )
( (is-and expr) (+ 1 (m (op1 expr) env) (m (op2 expr) env)) )
))
Halting Problem
 We can prove that many functions
terminate
 In general determining if an arbitrary
function will terminate is undecidable
 What about the following function?
(defun 3np1 (n)
(cond
((equal n 1) 1 )
((evenp n) (3np1 (/ n 2)) )
((oddp n) (3np1 (+ (* 3 n) 1)) )
))