Practical Foundations of Mathematics

Paul Taylor

VI. Structural Recursion

INTRODUCTION

6.1    FREE ALGEBRAS FOR FREE THEORIES

• Infinitary algebraic theories without laws
• Natural numbers
• Lists
• Infinitary conjunction and disjunction
• Existence of equationally free models

6.2    WELL FORMED FORMULAE

• Recursive covers
• Variables
• Many-sorted theories
• Formation rules in type theories
• Proof theory
• Infinitary operations

6.3    THE GENERAL RECURSION THEOREM

• Well founded coalgebras
• The recursion scheme
• The general recursion theorem

6.4    TAIL RECURSION AND LOOP PROGRAMS

• Semantics
• Transitive closure
• The recursion and induction schemes
• Partial correctness
• Discussion

6.5    UNIFICATION

• Unification

6.6    FINITENESS

• Three definitions by counting
• The ability to count
• Counting is unique
• Finite subsets
• The empty set
• Finiteness and Scott-continuity

6.7    THE ORDINALS

• Transfinite recursion
• Rank
• Arithmetic
• Classical applications
• Axiomatisation

EXERCISES  VI