Lecture Notes, Week 06

• Functional abstraction and instantiations
  • A concrete situation
  • First interlude
  • A concrete situation, continued (and abstracted)
  • Second interlude
  • A concrete situation, ended
  • Postlude
  • Post-postlude
  • Post-post-postlude
  • Resources
  • Version
• Generic programming with natural numbers
  • Resources
  • The big picture
  • Doubling up a natural number, revisited
  • Express interlude
  • Adding a natural number to an integer, revisited
  • Express interlude
  • Multiplying a natural number with an integer, revisited
  • Exponentiating two integers, revisited
  • Exercise 1
  • The even predicate, revisited
  • Express interlude
  • The odd predicate, revisited
  • Exercise 2
  • Resources
  • Version
• From primitive iteration to primitive recursion for natural numbers
  • Resources
  • The case of the factorial numbers
  • Exercise 3 (hard)
  • Exercise 4
  • Specifying and implementing the Sigma (a.k.a. sum) notation
  • Exercise 5
  • Exercise 6
  • Exercise 7 (hard)
  • Postlude
  • Exercise 8
  • Exercise 9
  • Resources
  • Version
• Mutual induction and recursion over natural numbers
  • Resources
  • Mutual recursion in OCaml
  • Even or odd
  • A closer look at the definitions of the even and odd predicates
  • A more faithful trace for the even and odd predicates
  • Exercise 10
  • Declaring global mutually recursive functions
  • Resources
  • Version
• The case of the Fibonacci numbers
  • Resources
  • Inductive specification
  • A unit-test function
  • Recursive implementation
  • Tracing the implementation
  • Interlude
  • Exercise 11
  • Simplifying the original definition of the Fibonacci function
  • Exercise 12
  • Resources
  • Version
• Exercises for Week 06
  • Exercise 0
  • Mandatory exercises
  • Recommended exercises
  • Version