Lecturer: 穆信成 Shin-Cheng Mu

Bird-Meertens style functional program derivation.

Lecture notes and slides. To be announced here.

Logic, Functional Programming.

Day 1. The Expand/Reduce Transformation(2 hours)

• Prelude: Maximum Segment Sum
• Preliminaries
  • Functions
  • Data Structures
• The Expand/Reduce Transformation
  • Example: Sum of Squares
  • Proving Properties by Induction
  • Accumulating parameters
  • Tupling

Day 2. Fold, Unfold, and Hylomorphism (2 hours)

• Folds
  • The Fold-Fusion Theorem
  • More Useful Functions as Folds
  • Finally, Solving Maximum Segment Sum!
  • Folds on Trees
• Unfolds
  • Unfold on Lists
• Folds v.s. Unfolds
• Hylomorphism
  • A Museum of Sorting Algorithms
  • Hylomorphism and Recursion
• Wrapping Up

Day 3. Procedural Program Derivation (2 hours)

• The Guarded Command Language
  • Assignments and Selection
  • Repetition
• Procedural Program Derivation
  • Taking Conjuncts as Invariants
  • Replacing Constants by Variables
  • Strengthening the Invariant
  • Tail Invariants
• Maximum Segment Sum, Procedually
• Wrapping Up

Suggested Reading:

• Richard S. Bird. Introduction to Functional Programming using Haskell.
• Richard S. Bird and Oege de Moor. Algebra of Programming. Only the functional part.
• Some papers from H. Zantema on list segment problems.
• Anne Kaldewaij. Programming: The Derivation of Algorithms (Prentice Hall, 1990).
• Roland Backhouse. Program Construction: Calculating Implementations from Specifications. John Wiley and Sons, 2003.
• Edsgar W. Dijkstra. A Discipline of Programming. Prentice Hall, 1976.
• David Gries. The Science of Programming. Springer, 1987.