Exercise 15.2 page 410 Well specified version of division

Exercise 15.3 page 410 Merging sorted lists

Exercise 15.4 page 411 Computing square roots

More about parsing More about parsing

Exercise 15.6 page 413 Inclusion preserves well-founded

Exercise 15.7 page 413 Well founded relations and infinite sequences

Exercise 15.8 page 418 An efficient way to compute the fibonacci function

Exercise 15.9 page 418 The discrete logarithm

Exercise 15.10 page 418 The factorial function on Z

Exercise 15.11 page 418 Computing square roots (with well-founded recursion)

Exercise 15.12 page 418 Computing cubic roots (with well-founded recursion)

Exercise 15.13 page 420 On nested recursion

Exercise 15.14 page 420 On nested recursion : a strange function

Exercise 15.16 page 426 A companion theorem for division specified by a fixpoint equation

Exercise 15.17 page 427 Defining a factorial function by iteration

Exercise 15.18 page 427 Defining a discrete log function by iteration

Exercise 15.20 page 431 Semantics of for loops

- page 422 (2nd paragraph of 15.3.2):

The correct specification is the following:forall n:A, {v:B | exists p:nat, forall (k:nat)(g:A->B), p < k -> iter k F g x = v }

Going home

Yves Bertot Last modified: Mon Mar 1 12:42:27 MET 2004