Lecture Notes, Week 11

• Demand-driven computation
  • Names
  • Applications
  • Parameter-passing strategies
  • Call by name, demand-driven computation, and “lazy” languages
  • Eager data structures
  • Lazy data structures
  • A simple example: lazy binary trees and mirroring them
  • Limitations
  • Resources
  • Version
• Programming with streams
  • Resources
  • Streams
  • Resources
  • Version
• Curry and uncurry
  • Resources
  • Version
• Induction principles: from first-order to higher-order induction
  • Prelude
  • Resources
  • Recurrence relations
  • First-order structural induction over Peano numbers (a.k.a. mathematical induction)
  • Interlude
  • Executive summary
  • A concrete example: the recursive addition function
  • Interlude
  • Executive summary
  • Exercise 01
  • Hint about Exercise 01
  • Second-order structural induction over Peano numbers
  • Executive summary
  • Exercise 02
  • A direct application of nat_ind2: the Fibonacci function
  • Interlude
  • Another application of nat_ind2: the evenness predicate
  • Two refinements of nat_ind2
  • Exercise 03
  • Exercise 04
  • Exercise 05
  • Third-order structural induction over Peano numbers
  • Exercise 06
  • Six refinements of nat_ind3
  • Exercise 07
  • Exercise 08
  • Exercise 09
  • Hint about Exercise 09
  • Exercise 10
  • Hint about Exercise 10
  • Exercise 11
  • Exercise 12
  • Hint about Exercise 12
  • Exercise 13
  • Hint about Exercise 13
  • Exercise 14
  • Exercise 15
  • Solution for Exercise 15
  • Exercise 16
  • Postlude
  • Resources
  • Version
• Induction principles: course-of-values induction
  • Resources
  • Towards course-of-values induction
  • Course-of-values induction
  • Exercise 17
  • Solution for Exercise 17
  • Exercise 18
  • Solution for Exercise 18
  • Exercise 19
  • Exercise 20
  • Exercise 21
  • Partial solution for Exercise 21
  • Exercise 22
  • Exercise 23
  • Exercise 24
  • Resources
  • Version
• Induction principles: strong induction
  • Resources
  • Towards strong induction
  • Strong induction
  • Exercise 25
  • Exercise 26
  • Solution for Exercise 26
  • Exercise 27
  • Solution for Exercise 27
  • Exercise 28
  • Exercise 29
  • Exercise 30
  • Partial solution for Exercise 30
  • Exercise 31
  • Exercise 32
  • Exercise 33
  • Resources
  • Version
• Mutual induction and recursion
  • Resources
  • Evenness and oddness, together
  • Exercise 20
  • Pre-ternary, ternary, or post-ternary?
  • Exercise 21
  • Resources
  • Version
• Exercises for Week 11
  • Exercise 00
  • Mandatory exercises
  • Version
• Index of concepts for Week 11
  • Version