Example:Inductive definition of addition

From CS2800 wiki

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].