Recursive data types play a central role in programming, and induction is really all about them.
Recursive data types are specified by recursive definitions, which say how to construct new data elements from previous ones. Along with each recursive data type there are recursive definitions of properties or functions on the data type. Most importantly, based on a recursive definition, there is a structural induction method for proving that all data of the given type have some property.
This chapter examines a few examples of recursive data types and recursively defined functions on them:
- strings of characters,
- “balanced” strings of brackets,
- the nonnegative integers, and
- arithmetic expressions
- 6.4: Arithmetic Expressions
- Expression evaluation is a key feature of programming languages, and recognition of expressions as a recursive data type is a key to understanding how they can be processed.