General Recursion

Scripts from the book

Exercises

Bounded recursion

Exercise 15.1 page 410 Division by bounded recursion
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

Well founded recursion

Exercise 15.5 page 413 Well-founded subterm relation on trees
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)

Nested recursion


Exercise 15.13 page 420 On nested recursion
Exercise 15.14 page 420 On nested recursion : a strange function

Recursion by iteration


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

Recursion with an ad hoc predicate

Exercise 15.19 page 431 A well-specified log with recursion on an ad-hoc predicate
Exercise 15.20 page 431 Semantics of for loops

Errata

  1. 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 }

Yves Bertot
Last modified: Sun May 3 13:53:45 CEST 2015