Unit 1-Lecture 10：Recursive Data Type

1 Recursive Data Type Definition

Definitions of recursive data types have two parts:

Base case(s) specifying that some known mathematical elements are in the data type, and

Constructor case(s) that specify how to construct new data elements from previously constructed elements or from base elements.

Specifically, to define a function, f , on a recursive data type, define the value of f for the base cases of the data type definition, then define the value of f in each constructor case in terms of the values of f on the component data items.

2 Structural Induction

Structural induction is a method for proving that all the elements of a recursively defined data type have some property:

Prove that each base case element has the property.

Prove that each constructor case element has the property, when the constructor is applied to elements that have the property.

Ordinary induction is simply the special case of structural induction on the recursive Definition

3 Induction in Computer Science

Strong induction and its special case of ordinary induction are applicable to any kind of thing with nonnegative integer sizes.

Structural induction then goes beyond number counting, and offers a simple, natural approach to proving things about recursive data types and recursive computation.

For recursively defined data types, structural induction is a simple and natural approach.This makes it a technique every computer scientist should embrace.

Reference

[1] Lehman E, Leighton F H, Meyer A R. Mathematics for Computer Science[J]. 2015.