SP18:Lecture 19 Inductive sets
Inductively defined sets
Over the next several weeks, we will be working with strings and machines that process strings. We could prove things about those machines by doing induction on the length of the strings: if was a property of a string , then we could prove "[[for all]] strings x, by doing an inductive proof of the statement "for all , if is a string of length , then P(x) holds". Since every string has a finite length, this would allow us to conclude for all .
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
- Rule 1: Z as standing for "zero") (We think of
- Rule 2: If S stands for "successor"; you can think of </math>S~n</math> it as representing "1 + n", although we will define + in terms of S instead of the other way around). then (
Thus the elements of are . You can then define as , as , and so on.
A BNF definition looks like this:
The rules define the various ways of constructing objects in the set. Any uses of the variables on the left hand-side of any of the equations, should be replaced by already-constructed elements of the corresponding set.
The BNF definition.symbol is simply used to indicate that the definition is a
For example, if, then
To add further detail, we can show thatas follows:
- Rule 1: The empty tree is in
- Rule 2: If and are trees, then the tree with value , left child and right child is in T.
We often think of trees pictorially; in this case we might give a BNF definition of as follows:
However, it is also useful to write trees symbolically; in this case we might defineas follows:
Using the first definition, the following is an example tree:
Using the second definition, we would write this as
Here, we are treating "+", "*", and "-" as uninterpreted symbols. For example, substructures and using the "+" rule. Most programming languages have a similar inductive definition, allowing us to formally model programs.is an expression, formed from the
Inductively defined functions
Given an inductively defined set , we know that every element of is formed using one of the rules defining . Therefore, if we want to define a function with domain , it suffices to describe how to evaluate it for objects formed with each rule.
Moreover, we can think of forming the value of substructures of (i.e. the "smaller" elements of that were used to construct ), we can assume that has already been defined, and use it in the definition of .at the same time that we show that ; this means that for all of the
It is reasonable to use substructure of ; we must have already proved that before we prove thatwhen defining because is a
We can then compute
Example: bad inductive definition
We often want to concatenate two strings and : put one of them at the end of another. is not a string according to the inductive definition of Σ^*, but we can define a function that produces that string (which we will then abbreviate as ).
There are at least two options. We could use induction on the second argument:
Here, we have used substructure of .in the definition of ; this is ok because can be considered a
There are several alternatives: we could induct on the second argument, on the first argument, or on both arguments: