6
$\begingroup$

This is one of the example lemma that has been proved in TAPL book which I'm unable to grasp.

The objective is to prove |Consts(t)| <= size(t) where t is a term.

Now, Consts is a function defined like this:

Consts(true) = {true}
Consts(false) = {false}
... and so on

Similarly

size(true) = 1
size(false) = 1
... and so on

Now the proof in the book starts with something like "By induction on the depth of t" and then goes to prove the lemma. But I think I'm missing something here. Induction can be applied when we have to prove something over natural number. But there is no natural number involved in the above lemma. How come then the induction is applied ?

$\endgroup$
  • $\begingroup$ "induction on the depth of t" means the depth of t is the natural number. So you prove it for all terms with depth 0 (or 1; I'm not familiar with type theory), and then you prove that if it holds for all terms with depth n, then it holds for all terms with depth n+1. $\endgroup$ – user253751 Feb 21 '17 at 3:44
3
$\begingroup$

A term is defined recursively. You can do induction on recursive types, using structural induction.

For instance, suppose we say that a term is something of the form

  • $c$ (a constant), or

  • $t_1+t_2$, where $t_1,t_2$ are terms.

Then structural induction is (loosely) similar to doing a proof by (strong) induction on the size of the tree. You prove that the property holds if the term has the form $c$ (that's the base case). Then, you prove that if the property holds for terms $t_1$ and $t_2$, then the property holds for the term $t_1+t_2$. You can probably see how to generalize this to terms whose syntax has a more complicated definition.

$\endgroup$
  • $\begingroup$ Thanks, but that proof proceeds by strong induction method actually. After thinking more, I think they are trying to prove via this manner: $\forall n \in N(|Consts(a term with depth n)| <= size(a term with depth n)$. Is my reasoning correct ? $\endgroup$ – Sibi Feb 22 '17 at 0:50
  • $\begingroup$ @Sibi, sorry, I can't understand what you are asking or what that notation means, so I don't know how to answer. About strong induction: Strong induction is induction; it's a form of induction. Anything you can prove by strong induction, you can prove by ordinary (non-strong) induction by strengthening the inductive predicate appropriately. So, mathematicians tend not to make much of a distinction between the two, since they are equivalent in power. $\endgroup$ – D.W. Feb 22 '17 at 0:53
  • $\begingroup$ Sorry, about the formatting. The content inside the bracket is: "a term with depth n". This is the entire proof outline: texpaste.com/n/yzj1cgim . I'm asking if they are actually applying strong induction in that proof... $\endgroup$ – Sibi Feb 22 '17 at 1:05
1
$\begingroup$

This type of induction is called structural induction on a term, or usual mathematical induction on the depth of a term (this is a natural number!).

More generally, well-founded induction is known. Both structural induction and mathematical induction are particular cases of well-founded induction.

$\endgroup$
1
$\begingroup$

Induction can be applied when we have to prove something over natural number.

No. There are many forms of induction. In some areas of TCS, like programming languages theory, it is common to define sets/predicates/relations recursively (inductively), and then derive an associated induction principle from its definition. In some type theories, like CiC (the calculus of inductive constructions) this is also done inside the language itself!

For example, let $X$ be the smallest set satisfying the following inference rules:

  1. a given constant $c$ belongs to $X$.
  2. if $x,y \in X$, then $f(x,y)\in X$.
  3. if $x \in X$, then $g(x)\in X$.

(The Knaster-Tarski theorem ensures there really is a smallest set satisfying $1,2,3$.)

Now, how to deduce an associated induction principle? Well, suppose $Y$ is another set satisfying $1,2,3$. Since $X$ is the smallest, we must have $X \subseteq Y$. That's the induction principle!

Let's rephrase the principle of induction over $X$. In order to prove that any $x \in X$ satisfies $x \in Y$, it suffices to prove the following:

  1. $c \in Y$.
  2. if $x,y \in Y$ (induction hypothesis), then $f(x,y)\in Y$.
  3. if $x \in Y$ (induction hypothesis), then $g(x)\in Y$.

In other words, it suffices to prove that $x \in Y$ is a property "preserved by every rule".

As another example, if we define $\mathbb{N}$ as the smallest set such that

  1. $0 \in \mathbb{N}$.
  2. if $n \in \mathbb{N}$ then $n+1 \in \mathbb{N}$.

we get the usual induction principle on natural numbers.

On syntactic terms, we proceed similarly. The set of terms is the smallest set $T$ such that

  1. constants/variables belong to $T$
  2. if $t_1,\ldots \in T$ then the expression $f(t_1,\ldots)\in T$
  3. etc.

(actual rules depend on the language you are defining)

Hence, to prove $p(t)$ holds for every term $t\in T$, by induction on $t$, all we have to do is to prove that $p$ holds for every constant/variable, that whenever $p(t_1),p(t_2),\ldots$ hold (induction hypothesis) we also have $p(f(t_1,t_2,\ldots))$, etc.

Inducing on the syntax of a term in this way is sometimes called structural induction.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.