Lecture Notes, Week 06

• So, induction and recursion over natural numbers
  • Structural induction
  • Express interlude
  • Structural recursion
  • The doubling function
  • Interlude
  • A more structured rendition of the trace
  • The even predicate
  • The Factorial function
  • Exercise 01
  • Solution for Exercise 01
  • Exercise 02
  • Exercise 03
  • Resources
  • Version
• 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
  • Post-post-post-postlude
  • Resources
  • Version
• Generic programming with natural numbers
  • Resources
  • The big picture
  • Terminology
  • Doubling up a natural number, revisited
  • Adding a natural number to an integer, revisited
  • Express interlude
  • Multiplying a natural number with an integer, revisited
  • Express interlude
  • Exponentiating two integers, revisited
  • Exercise 04
  • The even predicate, revisited
  • The odd predicate, revisited
  • Exercise 05
  • Exercise 06
  • Postlude
  • Food for thought
  • Exercise 07
  • Resources
  • Version
• From primitive iteration to primitive recursion for natural numbers
  • Resources
  • What nat_fold_right buys us: primitive iteration at work
  • What nat_parafold_right buys us: primitive recursion at work
  • Exercise 08
  • Exercise 09
  • Solution for Exercise 09
  • Exercise 10
  • Exercise 11
  • Exercise 12
  • Exercise 13
  • Exercise 14
  • Exercise 15
  • Specifying and implementing a sum function
  • Exercise 16
  • Specifying and implementing a capital sigma function
  • Exercise 17
  • Exercise 18
  • Exercise 19
  • Specifying and implementing a product function
  • Exercise 20
  • Exercise 21
  • Specifying and implementing a capital pi function
  • Exercise 22
  • Exercise 23
  • Exercise 24
  • The case of the Factorial numbers
  • Mini-interlude
  • Exercise 25
  • Exercise 26
  • Hint about Exercise 26
  • Mini-interlude
  • Postlude
  • Exercise 27
  • Exercise 28
  • Exercise 29
  • 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 30
  • 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 31
  • Simplifying the original definition of the Fibonacci function
  • Exercise 32
  • Resources
  • Version
• Exercises for Week 06
  • Exercise 00
  • Mandatory exercises
  • Recommended exercise
  • Mandatory mini-project
  • Version
• Index of concepts for Week 06
  • Version