1.6: B.6- Relations and Functions
- Page ID
- 121762
\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)
\( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)
\( \newcommand{\dsum}{\displaystyle\sum\limits} \)
\( \newcommand{\dint}{\displaystyle\int\limits} \)
\( \newcommand{\dlim}{\displaystyle\lim\limits} \)
\( \newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\)
( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\)
\( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\)
\( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\)
\( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\)
\( \newcommand{\Span}{\mathrm{span}}\)
\( \newcommand{\id}{\mathrm{id}}\)
\( \newcommand{\Span}{\mathrm{span}}\)
\( \newcommand{\kernel}{\mathrm{null}\,}\)
\( \newcommand{\range}{\mathrm{range}\,}\)
\( \newcommand{\RealPart}{\mathrm{Re}}\)
\( \newcommand{\ImaginaryPart}{\mathrm{Im}}\)
\( \newcommand{\Argument}{\mathrm{Arg}}\)
\( \newcommand{\norm}[1]{\| #1 \|}\)
\( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\)
\( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\AA}{\unicode[.8,0]{x212B}}\)
\( \newcommand{\vectorA}[1]{\vec{#1}} % arrow\)
\( \newcommand{\vectorAt}[1]{\vec{\text{#1}}} % arrow\)
\( \newcommand{\vectorB}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)
\( \newcommand{\vectorC}[1]{\textbf{#1}} \)
\( \newcommand{\vectorD}[1]{\overrightarrow{#1}} \)
\( \newcommand{\vectorDt}[1]{\overrightarrow{\text{#1}}} \)
\( \newcommand{\vectE}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash{\mathbf {#1}}}} \)
\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)
\(\newcommand{\longvect}{\overrightarrow}\)
\( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)
\(\newcommand{\avec}{\mathbf a}\) \(\newcommand{\bvec}{\mathbf b}\) \(\newcommand{\cvec}{\mathbf c}\) \(\newcommand{\dvec}{\mathbf d}\) \(\newcommand{\dtil}{\widetilde{\mathbf d}}\) \(\newcommand{\evec}{\mathbf e}\) \(\newcommand{\fvec}{\mathbf f}\) \(\newcommand{\nvec}{\mathbf n}\) \(\newcommand{\pvec}{\mathbf p}\) \(\newcommand{\qvec}{\mathbf q}\) \(\newcommand{\svec}{\mathbf s}\) \(\newcommand{\tvec}{\mathbf t}\) \(\newcommand{\uvec}{\mathbf u}\) \(\newcommand{\vvec}{\mathbf v}\) \(\newcommand{\wvec}{\mathbf w}\) \(\newcommand{\xvec}{\mathbf x}\) \(\newcommand{\yvec}{\mathbf y}\) \(\newcommand{\zvec}{\mathbf z}\) \(\newcommand{\rvec}{\mathbf r}\) \(\newcommand{\mvec}{\mathbf m}\) \(\newcommand{\zerovec}{\mathbf 0}\) \(\newcommand{\onevec}{\mathbf 1}\) \(\newcommand{\real}{\mathbb R}\) \(\newcommand{\twovec}[2]{\left[\begin{array}{r}#1 \\ #2 \end{array}\right]}\) \(\newcommand{\ctwovec}[2]{\left[\begin{array}{c}#1 \\ #2 \end{array}\right]}\) \(\newcommand{\threevec}[3]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \end{array}\right]}\) \(\newcommand{\cthreevec}[3]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \end{array}\right]}\) \(\newcommand{\fourvec}[4]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}\) \(\newcommand{\cfourvec}[4]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}\) \(\newcommand{\fivevec}[5]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}\) \(\newcommand{\cfivevec}[5]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}\) \(\newcommand{\mattwo}[4]{\left[\begin{array}{rr}#1 \amp #2 \\ #3 \amp #4 \\ \end{array}\right]}\) \(\newcommand{\laspan}[1]{\text{Span}\{#1\}}\) \(\newcommand{\bcal}{\cal B}\) \(\newcommand{\ccal}{\cal C}\) \(\newcommand{\scal}{\cal S}\) \(\newcommand{\wcal}{\cal W}\) \(\newcommand{\ecal}{\cal E}\) \(\newcommand{\coords}[2]{\left\{#1\right\}_{#2}}\) \(\newcommand{\gray}[1]{\color{gray}{#1}}\) \(\newcommand{\lgray}[1]{\color{lightgray}{#1}}\) \(\newcommand{\rank}{\operatorname{rank}}\) \(\newcommand{\row}{\text{Row}}\) \(\newcommand{\col}{\text{Col}}\) \(\renewcommand{\row}{\text{Row}}\) \(\newcommand{\nul}{\text{Nul}}\) \(\newcommand{\var}{\text{Var}}\) \(\newcommand{\corr}{\text{corr}}\) \(\newcommand{\len}[1]{\left|#1\right|}\) \(\newcommand{\bbar}{\overline{\bvec}}\) \(\newcommand{\bhat}{\widehat{\bvec}}\) \(\newcommand{\bperp}{\bvec^\perp}\) \(\newcommand{\xhat}{\widehat{\xvec}}\) \(\newcommand{\vhat}{\widehat{\vvec}}\) \(\newcommand{\uhat}{\widehat{\uvec}}\) \(\newcommand{\what}{\widehat{\wvec}}\) \(\newcommand{\Sighat}{\widehat{\Sigma}}\) \(\newcommand{\lt}{<}\) \(\newcommand{\gt}{>}\) \(\newcommand{\amp}{&}\) \(\definecolor{fillinmathshade}{gray}{0.9}\)When we have defined a set of objects (such as the natural numbers or the nice terms) inductively, we can also define relations on these objects by induction. For instance, consider the following idea: a nice term \(t_1\) is a subterm of a nice term \(t_2\) if it occurs as a part of it. Let’s use a symbol for it: \(t_1 \sqsubseteq t_2\). Every nice term is a subterm of itself, of course: \(t \sqsubseteq t\). We can give an inductive definition of this relation as follows:
The relation of a nice term \(t_1\) being a subterm of \(t_2\), \(t_1 \sqsubseteq t_2\), is defined by induction on \(t_2\) as follows:
- If \(t_2\) is a letter, then \(t_1 \sqsubseteq t_2\) iff \(t_1 = t_2\).
- If \(t_2\) is \([s_1 \circ s_2]\), then \(t_1 \sqsubseteq t_2\) iff \(t = t_2\), \(t_1 \sqsubseteq s_1\), or \(t_1 \sqsubseteq s_2\).
This definition, for instance, will tell us that \(\mathrm{a} \sqsubseteq [\mathrm{b} \circ \mathrm{a}]\). For (2) says that \(\mathrm{a} \sqsubseteq [\mathrm{b} \circ \mathrm{a}]\) iff \(\mathrm{a} = [\mathrm{b} \circ \mathrm{a}]\), or \(\mathrm{a} \sqsubseteq b\), or \(\mathrm{a} \sqsubseteq \mathrm{a}\). The first two are false: \(\mathrm{a}\) clearly isn’t identical to \([\mathrm{b} \circ \mathrm{a}]\), and by (1), \(\mathrm{a} \sqsubseteq \mathrm{b}\) iff \(\mathrm{a} = \mathrm{b}\), which is also false. However, also by (1), \(\mathrm{a} \sqsubseteq \mathrm{a}\) iff \(\mathrm{a} = \mathrm{a}\), which is true.
It’s important to note that the success of this definition depends on a fact that we haven’t proved yet: every nice term \(t\) is either a letter by itself, or there are uniquely determined nice terms \(s_1\) and \(s_2\) such that \(t = [s_1 \circ s_2]\). “Uniquely determined” here means that if \(t = [s_1 \circ s_2]\) it isn’t also \(= [r_1 \circ r_2]\) with \(s_1 \neq r_1\) or \(s_2 \neq r_2\). If this were the case, then clause (2) may come in conflict with itself: reading \(t_2\) as \([s_1 \circ s_2]\) we might get \(t_1 \sqsubseteq t_2\), but if we read \(t_2\) as \([r_1 \circ r_2]\) we might get not \(t_1 \sqsubseteq t_2\). Before we prove that this can’t happen, let’s look at an example where it can happen.
Define bracketless terms inductively by
- Every letter is a bracketless term.
- If \(s_1\) and \(s_2\) are bracketless terms, then \(s_1 \circ s_2\) is a bracketless term.
- Nothing else is a bracketless term.
Bracketless terms are, e.g., \(\mathrm{a}\), \(\mathrm{b} \circ \mathrm{d}\), \(\mathrm{b} \circ \mathrm{a} \circ \mathrm{b}\). Now if we defined “subterm” for bracketless terms the way we did above, the second clause would read
If \(t_2 = s_1 \circ s_2\), then \(t_1 \sqsubseteq t_2\) iff \(t_1 = t_2\), \(t_1 \sqsubseteq s_1\), or \(t_1 \sqsubseteq s_2\).
Now \(\mathrm{b} \circ \mathrm{a} \circ \mathrm{b}\) is of the form \(s_1 \circ s_2\) with
\[s_1 = \mathrm{b} \quad\text{ and }\quad s_2 = \mathrm{a} \circ \mathrm{b}.\nonumber\]
It is also of the form \(r_1 \circ r_2\) with
\[r_1 = \mathrm{b} \circ \mathrm{a} \quad\text{ and }\quad r_2 = \mathrm{b}.\nonumber\]
Now is \(\mathrm{a} \circ \mathrm{b}\) a subterm of \(\mathrm{b} \circ \mathrm{a} \circ \mathrm{b}\)? The answer is yes if we go by the first reading, and no if we go by the second.
The property that the way a nice term is built up from other nice terms is unique is called unique readability. Since inductive definitions of relations for such inductively defined objects are important, we have to prove that it holds.
Suppose \(t\) is a nice term. Then either \(t\) is a letter by itself, or there are uniquely determined nice terms \(s_1\), \(s_2\) such that \(t = [s_1 \circ s_2]\).
Proof. If \(t\) is a letter by itself, the condition is satisfied. So assume \(t\) isn’t a letter by itself. We can tell from the inductive definition that then \(t\) must be of the form \([s_1 \circ s_2]\) for some nice terms \(s_1\) and \(s_2\). It remains to show that these are uniquely determined, i.e., if \(t = [r_1 \circ r_2]\), then \(s_1 = r_1\) and \(s_2 = r_2\).
So suppose \(t = [s_1 \circ s_2]\) and also \(t = [r_1 \circ r_2]\) for nice terms \(s_1\), \(s_2\), \(r_1\), \(r_2\). We have to show that \(s_1 = r_1\) and \(s_2 = r_2\). First, \(s_1\) and \(r_1\) must be identical, for otherwise one is a proper initial segment of the other. But by Proposition B.5.2, that is impossible if \(s_1\) and \(r_1\) are both nice terms. But if \(s_1 = r_1\), then clearly also \(s_2 = r_2\). ◻
We can also define functions inductively: e.g., we can define the function \(f\) that maps any nice term to the maximum depth of nested \([\dots]\) in it as follows:
The depth of a nice term, \(f(t)\), is defined inductively as follows: \[f(t) = \begin{cases} 0 & \text{ if $t$ is a letter}\\ \max(f(s), f(s')) + 1 & \text{ if $t = [s_1 \circ s_2]$.} \end{cases}\nonumber\]
For instance \[\begin{aligned} f([\mathrm{a} \circ \mathrm{b}]) & = \max(f(\mathrm{a}),f(\mathrm{b})) + 1 = \\ &= \max(0, 0) + 1 = 1, \text{ and}\\ f([[\mathrm{a} \circ \mathrm{b}] \circ \mathrm{c}]) & = \max(f([\mathrm{a} \circ \mathrm{b}]), f(\mathrm{c})) + 1 = \\ & = \max(1,0) + 1 = 2.\end{aligned}\]
Here, of course, we assume that \(s_1\) an \(s_2\) are nice terms, and make use of the fact that every nice term is either a letter or of the form \([s_1 \circ s_2]\). It is again important that it can be of this form in only one way. To see why, consider again the bracketless terms we defined earlier. The corresponding “definition” would be:
\[g(t) = \begin{cases} 0 & \text{ if $t$ is a letter}\\ \max(g(s), g(s')) + 1 & \text{ if $t = [s_1 \circ s_2]$.} \end{cases}\nonumber\]
Now consider the bracketless term \(\mathrm{a} \circ \mathrm{b} \circ \mathrm{c} \circ \mathrm{d}\). It can be read in more than one way, e.g., as \(s_1 \circ s_2\) with
\[s_1 = \mathrm{a} \quad\text{ and }\quad s_2 = \mathrm{b} \circ \mathrm{c} \circ \mathrm{d}, \nonumber\]
or as \(r_1 \circ r_2\) with
\[r_1 = \mathrm{a} \circ b \quad\text{ and }\quad r_2 = \mathrm{c} \circ \mathrm{d}.\nonumber\]
Calculating \(g\) according to the first way of reading it would give
\[\begin{aligned} g(s_1 \circ s_2) & = \max(g(\mathrm{a}), g(\mathrm{b} \circ \mathrm{c} \circ \mathrm{d})) + 1 =\\
& = \max(0,2) + 1 = 3 \end{aligned}\]
while according to the other reading we get
\[\begin{aligned}g(r_1 \circ r_2) & = \max(g(\mathrm{a} \circ \mathrm{b}), g(\mathrm{c} \circ \mathrm{d})) + 1=\\
& = \max(1,1) + 1 = 2\end{aligned}\]
But a function must always yield a unique value; so our “definition” of \(g\) doesn’t define a function at all.
Give an inductive definition of the function \(l\), where \(l(t)\) is the number of symbols in the nice term \(t\).
Prove by structural induction on nice terms \(t\) that \(f(t) < l(t)\) (where \(l(t)\) is the number of symbols in \(t\) and \(f(t)\) is the depth of \(t\) as defined in Definition \(\PageIndex{3}\)).


