SP18:Lecture 19 Inductive sets

From CS2800 wiki

We discussed how to build sets inductively, and introduced BNF notation. We also discussed inductively defined functions.

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 [math]P(x) [/math] was a property of a string [math]x [/math], then we could prove "[[for all]] strings x, [math]P(x) [/math] by doing an inductive proof of the statement "for all [math]n \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/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

An inductively defined set is a set where the elements are constructed by a finite number of applications of a given set of rules for creating more complicated objects from simpler ones.

For example, the set of natural numbers is the set of elements defined inductively by the following rules:

  • Rule 1: [math]\href{/cs2800/wiki/index.php/Z}{Z} \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] (We think of Z as standing for "zero")
  • Rule 2: If [math]n \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] then [math]\href{/cs2800/wiki/index.php/S}{S}~n \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] (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).

Thus the elements of [math]\href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] are [math]\{\href{/cs2800/wiki/index.php/Z}{Z}, \href{/cs2800/wiki/index.php/S}{S}~\href{/cs2800/wiki/index.php/Z}{Z}, \href{/cs2800/wiki/index.php/S}{S}~(\href{/cs2800/wiki/index.php/S}{S}~\href{/cs2800/wiki/index.php/Z}{Z}), \href{/cs2800/wiki/index.php/S}{S}\href{/cs2800/wiki/index.php/S}{S}\href{/cs2800/wiki/index.php/S}{S}\href{/cs2800/wiki/index.php/Z}{Z}, \dots\} [/math]. You can then define [math]1 [/math] as [math]1 \href{/cs2800/wiki/index.php?title=%3D&action=edit&redlink=1}{=} \href{/cs2800/wiki/index.php/S}{S}~\href{/cs2800/wiki/index.php/Z}{Z} [/math], [math]2 [/math] as [math]2 \href{/cs2800/wiki/index.php?title=%3D&action=edit&redlink=1}{=} \href{/cs2800/wiki/index.php/S}{S}\href{/cs2800/wiki/index.php/S}{S}\href{/cs2800/wiki/index.php/Z}{Z} [/math], and so on.

BNF Notation

Backus-Naur form (or BNF) is a convenient syntax for writing down inductively defined sets.

BNF definitions give the name of the set being defined, and the list of rules defining the set in a compact form, separated by a vertical bar ([math]\href{/cs2800/wiki/index.php/%5Cmid}{\mid} [/math]).

A BNF definition looks like this:

[math]\begin{align*} var_1 \href{/cs2800/wiki/index.php/%E2%88%88}{∈} Set_1 &\href{/cs2800/wiki/index.php/BNF}{::=} \text{rule 1} \href{/cs2800/wiki/index.php/%5Cmid}{\mid} \text{rule 2} \href{/cs2800/wiki/index.php/%5Cmid}{\mid} \cdots \\ var_2 \href{/cs2800/wiki/index.php/%E2%88%88}{∈} Set_2 &\href{/cs2800/wiki/index.php/BNF}{::=} \text{rule 1} \href{/cs2800/wiki/index.php/%5Cmid}{\mid} \text{rule 2} \href{/cs2800/wiki/index.php/%5Cmid}{\mid} \cdots \\ & \vdots \end{align*} [/math]

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 [math]\href{/cs2800/wiki/index.php/BNF}{::=} [/math] symbol is simply used to indicate that the definition is a BNF definition.

For example, the rules defining the natural numbers say that [math]\href{/cs2800/wiki/index.php/Z}{Z} \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] and [math]\href{/cs2800/wiki/index.php/S}{S}~n \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] for any [math]n \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math]. These would be written in BNF as follows:

Definition: natural number
The set of natural numbers is given inductively by [math]n \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/BNF}{::=} \href{/cs2800/wiki/index.php/Z}{Z} \href{/cs2800/wiki/index.php/%5Cmid}{\mid} \href{/cs2800/wiki/index.php/S}{S}~n [/math]

The second rule says that you can form a new natural number by prepending an S onto an existing natural number.

Example: strings

Definition: Σ*
The set [math]\href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] of strings with characters in the alphabet [math]\href{/cs2800/wiki/index.php/%CE%A3}{Σ} [/math] is defined inductively by:


[math]\begin{align*} x &\href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} \href{/cs2800/wiki/index.php/BNF}{::=} \href{/cs2800/wiki/index.php/%CE%95}{ε} \href{/cs2800/wiki/index.php/%5Cmid}{\mid} \href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa} \\ a &\href{/cs2800/wiki/index.php/%E2%88%88}{∈} Σ \end{align*} [/math]

[math]\href{/cs2800/wiki/index.php/%CE%95}{ε} [/math] represents the empty string, while [math]\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa} [/math] represents a string with 1 or more characters, starting with the shorter string [math]x [/math] and ending in the character [math]a [/math].

For example, if [math]\href{/cs2800/wiki/index.php/%CE%A3}{Σ} = \href{/cs2800/wiki/index.php/Enumerated_set}{\{0,1\}} [/math], then [math]\href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} = \{ε, ε0, ε1, ε00, ε01, ε10, ε11, ε000, ε001, \dots\} [/math]

To add further detail, we can show that [math]ε010 \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] as follows:

  • [math]\href{/cs2800/wiki/index.php/%CE%95}{ε} \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] by rule 1
  • [math]\href{/cs2800/wiki/index.php/%CE%95}{ε}0 \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] by rule 2, since [math]\href{/cs2800/wiki/index.php/%CE%95}{ε} \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] and [math]0 \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%CE%A3}{Σ} [/math]
  • [math]\href{/cs2800/wiki/index.php/%CE%95}{ε}01 \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] by rule 2, since [math]\href{/cs2800/wiki/index.php/%CE%95}{ε}0 \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] and [math]1 \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%CE%A3}{Σ} [/math]
  • [math]\href{/cs2800/wiki/index.php/%CE%95}{ε}010 \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] by rule 2, since [math]\href{/cs2800/wiki/index.php/%CE%95}{ε}01 \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] and [math]0 \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%CE%A3}{Σ} [/math]


By convention, we leave off the leading "ε" from non-empty strings. For example, we would write "001" instead of "ε001".

Example: trees

The set [math]T [/math] of binary trees with integer nodes is defined inductively by

  • Rule 1: The empty tree is in [math]T [/math]
  • Rule 2: If [math]t_1 [/math] and [math]t_2 [/math] are trees, then the tree with value [math]a [/math], left child [math]t_1 [/math] and right child [math]t_2 [/math] is in T.


We often think of trees pictorially; in this case we might give a BNF definition of [math]T [/math] as follows:

Tree-defn.svg

However, it is also useful to write trees symbolically; in this case we might define [math]T [/math] as follows:

[math]t \href{/cs2800/wiki/index.php/%E2%88%88}{∈} T \href{/cs2800/wiki/index.php/BNF}{::=} nil \href{/cs2800/wiki/index.php/%5Cmid}{\mid} tree(a,t_1,t_2) \qquad a \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%A4}{ℤ} [/math]

Using the first definition, the following is an example tree:

Tree-example.svg

Using the second definition, we would write this as [math]tree(3,tree(0,nil,nil),tree(1,tree(0,nil,nil),nil)) [/math]

Example: expressions

Mathematical expressions of various kinds are often defined inductively. For example, one might define a set of arithmetic expressions by the rules

[math]\begin{align*} e &\href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php?title=Expr&action=edit&redlink=1}{Expr} \href{/cs2800/wiki/index.php/BNF}{::=} n \href{/cs2800/wiki/index.php/%5Cmid}{\mid} e_1 + e_2 \href{/cs2800/wiki/index.php/%5Cmid}{\mid} -e \href{/cs2800/wiki/index.php/%5Cmid}{\mid} e_1 * e_2 \\ n &\href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \end{align*} [/math]

Here, we are treating "+", "*", and "-" as uninterpreted symbols. For example, [math](3 + (4*5)) + (-2) [/math] is an expression, formed from the substructures [math](3+(4*5)) [/math] and [math](-2) [/math] using the "+" rule. Most programming languages have a similar inductive definition, allowing us to formally model programs.

Inductively defined functions

Given an inductively defined set [math]X [/math], we know that every element [math]x [/math] of [math]X [/math] is formed using one of the rules defining [math]X [/math]. Therefore, if we want to define a function with domain [math]X [/math], it suffices to describe how to evaluate it for objects formed with each rule.

Moreover, we can think of forming the value of [math]f(x) [/math] at the same time that we show that [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} X [/math]; this means that for all of the substructures [math]x' [/math] of [math]x [/math] (i.e. the "smaller" elements of [math]X [/math] that were used to construct [math]x [/math]), we can assume that [math]f(x') [/math] has already been defined, and use it in the definition of [math]f(x) [/math].

A function defined in this way is called an inductively defined function or a recursive function.

Example: length

For example, we could define a function for computing the length of a string inductively:

Definition: len
Let [math]\href{/cs2800/wiki/index.php/Len}{len} : \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} → \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] be given inductively by [math]\href{/cs2800/wiki/index.php/Len}{len}(\href{/cs2800/wiki/index.php/%CE%95}{ε}) \href{/cs2800/wiki/index.php?title=%3D&action=edit&redlink=1}{=} 0 [/math] and [math]\href{/cs2800/wiki/index.php/Len}{len}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa}) := 1 + \href{/cs2800/wiki/index.php/Len}{len}(x) [/math].

It is reasonable to use [math]\href{/cs2800/wiki/index.php/Len}{len}(x) [/math] when defining [math]\href{/cs2800/wiki/index.php/Len}{len}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa}) [/math] because [math]x [/math] is a substructure of [math]xa [/math]; we must have already proved that [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] before we prove that [math]\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa} \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math]

We can then compute

[math]\begin{align*} \href{/cs2800/wiki/index.php/Len}{len}(0110) &= 1+\href{/cs2800/wiki/index.php/Len}{len}(011) \\ &= 1 + (1 + \href{/cs2800/wiki/index.php/Len}{len}(01)) \\ &= 1 + 1 + 1 + \href{/cs2800/wiki/index.php/Len}{len}(0) \\ &= 1 + 1 + 1 + 1 + \href{/cs2800/wiki/index.php/Len}{len}(\href{/cs2800/wiki/index.php?title=%5Cepsilon&action=edit&redlink=1}{\epsilon}) \\ &= 1 + 1 + 1 + 1 + 0 = 4 \end{align*} [/math]

Example: bad inductive definition

When giving an inductive definition of a function [math]f [/math], it is important to only use [math]f(x') [/math] in the definition of [math]f(x) [/math] if [math]x' [/math] is a substructure of [math]x [/math].

For example, the "function" [math]bogus : \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} \href{/cs2800/wiki/index.php/%5Cto}{\to} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] given inductively by [math]bogus(\href{/cs2800/wiki/index.php/%CE%95}{ε}) := 0 [/math] and [math]bogus(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa}) := bogus(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa}) [/math] is not well-defined. Indeed, try computing [math]bogus("abc") [/math]; any choice of output satisfies the defining equations.

As a more insidious example, consider [math]nasty : \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} \href{/cs2800/wiki/index.php/%5Cto}{\to} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] given by [math]nasty(\href{/cs2800/wiki/index.php/%CE%95}{ε}) := \href{/cs2800/wiki/index.php/%CE%95}{ε} [/math] and [math]nasty(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa}) := nasty(nasty(x)) [/math]. Here, it is perfectly reasonable to use [math]nasty(x) [/math] in the definition of [math]nasty(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa}) [/math] because [math]x [/math] is a substructure of [math]\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa} [/math], but [math]nasty(nasty(x)) [/math] is not ok, because [math]nasty(x) [/math] is not necessarily a substructure of [math]\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa} [/math] and we can only apply [math]nasty [/math] to substructures of [math]\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa} [/math] in the definition of [math]nasty(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa}) [/math].

Example: concatenation

We often want to concatenate two strings [math]x [/math] and [math]y [/math]: put one of them at the end of another. [math]xy [/math] 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 [math]xy [/math]).

There are at least two options. We could use induction on the second argument:

Definition: concatenation
The function [math]\href{/cs2800/wiki/index.php/Cat}{cat} : \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} \href{/cs2800/wiki/index.php/%5Ctimes}{\times} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} \href{/cs2800/wiki/index.php/%E2%86%92}{→} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] is given inductively by [math]cat(x,ε) := x [/math] and [math]cat(x,ya) := cat(x,y)a [/math].

We could also define [math]\href{/cs2800/wiki/index.php/Cat}{cat} [/math] inductively on the pair of arguments:

Definition: concatenation
The function [math]\href{/cs2800/wiki/index.php/Cat}{cat} : \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} \href{/cs2800/wiki/index.php/%5Ctimes}{\times} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} \href{/cs2800/wiki/index.php/%E2%86%92}{→} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] is given inductively by [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php/%CE%95}{ε},\href{/cs2800/wiki/index.php/%CE%95}{ε}) := \href{/cs2800/wiki/index.php/%CE%95}{ε} [/math], [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php/%CE%95}{ε},\href{/cs2800/wiki/index.php?title=Yb&action=edit&redlink=1}{yb}) := \href{/cs2800/wiki/index.php?title=Yb&action=edit&redlink=1}{yb} [/math], [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},\href{/cs2800/wiki/index.php/%CE%95}{ε}) := \href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa} [/math], and [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},\href{/cs2800/wiki/index.php?title=Yb&action=edit&redlink=1}{yb}) := \href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},y)\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{b} [/math].

Here, we have used [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},y) [/math] in the definition of [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},\href{/cs2800/wiki/index.php?title=Yb&action=edit&redlink=1}{yb}) [/math]; this is ok because [math](x,\href{/cs2800/wiki/index.php?title=Yb&action=edit&redlink=1}{yb}) [/math] can be considered a substructure of [math](\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},\href{/cs2800/wiki/index.php?title=Yb&action=edit&redlink=1}{yb}) [/math].

If [math]x' [/math] and [math]y' [/math] are substructures of [math]x [/math] and [math]y [/math] respectively, then [math](x',y') [/math], [math](x,y') [/math] and [math](x',y) [/math] can all be considered substructures of [math](x,y) [/math]: they must all have been shown to be in [math]X \href{/cs2800/wiki/index.php/%5Ctimes}{\times} X [/math] before we could show that [math](x,y) \href{/cs2800/wiki/index.php/%E2%88%88}{∈} X \href{/cs2800/wiki/index.php/%5Ctimes}{\times} X [/math].

We might be tempted to use induction on the first argument, but we fail: how do we define [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},y) [/math] in terms of [math]\href{/cs2800/wiki/index.php/Cat}{cat}(x,y) [/math] and [math]a [/math]? You might propose something like [math]\href{/cs2800/wiki/index.php/Cat}{cat}(x,a)y [/math], but this is undefined for a number of reasons: [math]a \href{/cs2800/wiki/index.php/%E2%88%88}{∈} Σ [/math] (not [math]\href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math]), so [math]cat(x,a) [/math] is undefined. Moreover, if we could just stick a string at the end of another string (in this case, appending [math]y [/math] to [math]\href{/cs2800/wiki/index.php/Cat}{cat}(x,a) [/math]), we wouldn't need to define [math]\href{/cs2800/wiki/index.php/Cat}{cat} [/math]! Without first defining cat, we can only form strings using the two rules given in the inductive definition of [math]\href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math].

Example: addition

We can inductively define familiar operations like addition and multiplication.

There are several alternatives: we could induct on the second argument, on the first argument, or on both arguments:

Definition: addition
Let [math]add : \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%5Ctimes}{\times} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%5Cto}{\to} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] be given inductively by [math]add(x,Z) := x [/math] and [math]add(x,S~n) := S~add(x,n) [/math].


Definition: addition
Let [math]add : \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%5Ctimes}{\times} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%5Cto}{\to} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] be given inductively by [math]add(Z,x) := x [/math] and [math]add(S~n,x) := S~add(n,x) [/math].


Definition: addition
Let [math]add : \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%5Ctimes}{\times} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%5Cto}{\to} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] be given inductively by [math]add(Z,Z) := Z [/math], [math]add(Z,S~n) := S~n [/math], [math]add(S~n,Z) := S~n [/math], and [math]add(S~n,S~m) := S~S~add(n,m) [/math].