View source for SP18:Lecture 19 Inductive sets

We discussed how to build sets [[inductively]], and introduced [[BNF]] notation.  We also discussed [[inductively defined function]]s.

* [http://www.cs.cornell.edu/courses/cs2800/2017fa/lectures/lec20-ind-defns.html Last semester]
* Reading: [[MCS]] chapter 7
* [[File:lec19-board.pdf]]

= Inductively defined sets =

Over the next several weeks, we will be working with [[string]]s and
[[machine]]s that process [[string]]s.  We could prove things about those machines
by doing [[induction]] on the [[length]] of the strings: if <math>P(x)</math>
was a [[property]] of a [[string]] <math>x</math>, then we could prove "[[for
all]] [[string]]s x, <math>P(x)</math> by doing an [[inductive proof]]
of the statement "[[for all]] <math>n [[∈]] [[ℕ]]</math>, if <math>x</math> is a
[[string]] of [[length]] <math>n</math>, then P(x) holds".  Since every [[string]]
has a [[finite]] [[length]], this would allow us to conclude <math>P(x)</math>
[[for all]] <math>x</math>.

This approach works well enough, but there are a few rough edges:

* we haven't defined strings, or proved that every string has a length.

* using induction forces us to state everything as a property of numbers, when it is more natural to think of our claims as properties of strings


Instead, we will use this opportunity to introduce a generalization of weak
induction: structural induction.  Structural induction gives us a technique for
defining new objects by combining smaller objects, and for defining functions
and proving facts about those objects and functions.

== Inductively defined sets ==

{{:Inductively defined set}}

== Inductively defined functions ==

{{:Inductively defined function}}