Session 9: Induction II — Structural and Well-Founded Induction

Overview

Inductively defined sets given by inference rules, the induction principles they generate, and termination arguments for functions that are not structurally recursive.

Lecturer

Yara Sleem (CSE + Mathematics)

Session Information

• Date and Time: Tueday 20 October 2026 — 17:30-19:30
• Place: (to be announced)
• Online Meeting Link
• Session Recording

Core Concepts

• Inductively defined sets, given by inference rules: base constructors and step constructors
• Defining List, Tree, and ℕ inductively
• Structural recursion: defining functions by cases on constructors
• Structural induction: deriving the induction principle from the constructors
• Rule induction over an inductively defined relation
• Well-founded induction and termination: measures, decreasing arguments, and why while is harder than for
• Functions that terminate but not structurally (gcd, Ackermann)

Slides

Session 9 Slides: Download PDF

Readings

• Mathematics for Computer Science, Ch. 3.5
• Mathematics for Computer Science (2015 ed.), Ch. 6
• The Open Logic Project, Ch. 74 — inductive definitions (74.4) and structural induction (74.5)
• For culture, read about Induction and Recursion in Lean4

Exercises & Extra Steps

• Practice (not collected): define length, append and reverse by structural recursion and prove length (append xs ys) = length xs + length ys
• Practice (not collected): prove reverse (reverse xs) = xs
• Practice (not collected): give a termination measure for Euclid’s algorithm and prove it decreases
• Problem Set 3 released today — due on paper at the start of S11 (Mon 12 Oct)

Navigation

• ← Previous: S8: Induction I — Naturals and Strong Induction
• Back to Course Overview
• Next: S10: Recursion, Iteration & Data Structures I →

Questions? Reach out on the course WhatsApp!