TERMINATION METHODS

Course Data

Location: Ornstein 103
Time: Thursday, 10-13
Instructor: Nachum Dershowitz
Office: 218 Schreiber
Phone: 03/640-5356
E-mail: nachumd@tau.ac.il

PURPOSE

The purpose of the course is to learn various interesting methods of proving the termination (halting) of programs. Topics include:

Structural Induction and Intermittent Decreases
Commutations and Transformations
Ramsey's Theorem and Ordering Decomposition
Lexicographic and Bag Orderings, Konig's Lemma
Well-founded Orderings, Ordinals, The Hydra
Higman's Lemma, Kruskal's Theorem, Simplification Orderings
Well-quasi Orderings, Recursive Path Orderings
Knuth-Bendix Orderings, General Path Ordering
Linear Termination Functions, Farkas's Lemma, Polyhedral Constraints

REQUIREMENTS

The course is open to undergraduate students and to graduate students. Only basic programming (including recursion) and basic discrete math (including induction) are required.

Lectures & Readings

Introduction (28 Feb. 2013)

Strachey on the Halting Problem

Turing's landmark paper
A Two-Minute Proof of the Second Most Important Theorem of the Second Millennium (Doron Zeilberger)

An Early Program Proof by Alan Turing

Turing's original report

A Closer Look at Termination (Shmuel Katz & Zohar Manna)

Games (7 Mar. 2013)[Gal]

Bigger and Bigger (14 Mar. 2013) [Jonathan]

Some Ordinals
Ackermann's Function is Not Primitive Recursive (Chi Woo, Planet Math)
Accessible Independence Results for Peano Arithmetic (Laurie Kirby & Jeff Paris)
The Hydra Battle Revisited (Sections 2, 4, 9)

Well-Founded Orderings (11 Apr. 2013) [Yevgeny]

Presentation: Termination Analysis of Loops (Zohar Manna & Aaron Bradley)
Proving Program Termination (Byron Cook)
Jumping and Escaping [Eitan]

Well-Quasi Orderings (18 Apr. 2013)

On Well-quasi-ordering Finite Trees (C. St. J. A. Nash-Williams)

Well-quasi Ordering, the Tree Theorem, and Vazsonyi's Conjecture (Joe Kruskal)
Michael Rabin's Paper
The Theory of Well-quasi Ordering: A Frequently Discovered Concept (Joe Kruskal)

Tree Orderings (25 Apr. 2013)

Rewriting (2 May 2013) [Gleb]

Termination of Rewriting

Semantic Path Ordering (9 May 2013) [Ori Handout]

Attempts for Generalizing the Recursive Path Orderings (Sam Kamin & Jean-Jacques Lévy)
An Improved General Path Order (Alfons Geser)

Dependency Pairs (16 May 2013)

Homework
Presentation: Automated Termination Analysis (Jürgen Giesl)
Termination of Term Rewriting using Dependency Pairs (Thomas Arts and Jürgen Giesl)

Dependency Pairs Revisited (Nao Hirokawa & Aart Middeldorp)
A Collection of Examples (Thomas Arts and Jürgen Giesl)

Recursion and Induction (23 May 2013)

Inductive Methods for Proving Properties of Programs (Zohar Manna, Steve Ness & Jean Vuillemin) (Sections I and III)

Iteration and Induction (30 May 2013) [Gitit]

Size Change Termination (Amir Ben-Amram)
Is "Sometime" Sometimes Better than "Always" (Zohar Manna & Richard Waldinger)

Is Sometime Ever Better than Alway (David Gries)

Typed Lambda Calculus (6 June 2013)

Presentation: Frédéric Blanqui's Presentation

Higher Order Orderings (13 June 2013) [Liron]

The Higher-Order Computability Path Ordering: The End of a Quest (Frédéric Blanqui, Jean-Pierre Jouannaud & Albert Rubio)

Frédéric Blanqui's Habilitation

Terminate (or Epsilon_0, Gamma_0, and Other Ordinals) (20 June 2013) [Nissan Extra]

What's so Special about Kruskal's Theorem and the Ordinal Γ₀ (Jean Gallier)

Lecture Notes (pdf) (ppt) (key)

Examples

Turing's Factorial Program
Greatest Common Divisor
McCarthy's 91 Function
Ackermann's Function
Ackermann's Function via a Stack
Dutch National Flag with Marbles
Growing Railroad Trains
Goodstein's Sequence
Battle of Hercules and Hydra
Amoeba Colonies
Grid Game
Gremlins
Differentiation
Disjunctive Normal Form Examples
Dependency Pair Examples
Unification Algorithm
Recursion Examples
Counting Leaves