Overview

We define sets (describe data) with the following methods:

1. Inductive Specification: Top-Down, Bottom-Up, Rules of Inference.
2. Grammar Specification

Having described sets inductively, we can use the inductive definitions in two ways: to prove theorems about members of the set and to write pro- grams that manipulate them:

1. Mathematical Induction
2. Deriving Recursive Programs
3. Auxiliary Procedures and Context Arguments

Top-Down (Recursive Definition)

Properties

• This strategy represents a process of decomposition.
• Begin with a general case and and break it down to its constituent pars.
• The recursive breakdown allows to write a procedural representation of the definition.

Example Definition

Definition (top-down): A natural number n is in S iff either n = 0, or (n - 3) is in S.

Example Procedure

;; in-S? : Int -> Bool
(define in-S? 
	(lambda (n)
		(if (zero? n) #t
			(if (>= (- n 3) 0)
				(in-S? (- n 3))
				#f))))

Bottom-Up (Mathematical Induction)

Properties

• This strategy represents a process of composition.