Types and Programming Languages book introduces a theorem about principles of induction on term (p. 31, theorem 3.3.4):

Suppose P is a predicate on terms.

Induction on depth:

If, for each term s, given P (r) for all r such that depth(r) < depth(s) we can show P(s), then P(s) holds for all s.

Proof of this theorem is left as the exercise for the reader. The solution to the exercise given in the book hints at defining a new predicate Q(n) on natural numbers such as:

∀s with depth(s) = n. P(s)

and apply the principle of complete induction on natural number (p. 19, axiom 2.4.2):

If, for each natural number n, given P(i) for all i < n we can show P(n), then P(n) holds for all n.

Since I lack experience in writing mathematical proofs, I'm struggling with applying the hint from the book and proving that theorem.

Given that:

  • n = i + 1
  • for all natural numbers i less than i + 1, the predicate Q(i) holds (from the induction axiom)

How do I prove that Q(n) (or Q(i + 1)) is true? Should I use depth function definition introduced previously for the simple arithmetic language?

  • $\begingroup$ I'm voting to close this question as off-topic because it belongs to Mathematics. $\endgroup$ – Yuval Filmus Sep 17 '19 at 21:33

While you should get in the habit of providing definitions so your question is self-contained, especially when the original text is not easily accessible, the first thing to note is that the theorem doesn't actually depend at all on what "terms" are or how "depth" is defined.

Given any set $S$ and any function $f:S\to\mathbb N$, the theorem will hold. That is, $$(\forall s\in S.(\forall r\in S.f(r) < f(s) \to P(r))\to P(s))\to \forall s\in S.P(S)$$

How useful this theorem is depends on $f$. For example, if $f$ is a constant function then this theorem simplifies to $(\forall s\in S.P(s))\to(\forall s\in S.P(s))$ which isn't very useful.

To prove this via complete induction, you should, as is always a helpful strategy, write out the definitions, in this case, of complete induction. Complete induction states: $$(\forall n\in\mathbb N.(\forall m\in\mathbb N.m < n\to Q(m))\to Q(n))\to\forall n\in\mathbb N.Q(n)$$

So the bulk of the task is choosing an appropriate $Q$ to get the result that you want. As the hint states, the fairly obvious choice is $Q(n)\equiv\forall s\in S.f(s)=n\to P(s)$. If you stick this $Q$ into the formula for complete induction, you can simplify it into the first formula. All the work comes down basically to showing that $\forall n\in\mathbb N.\forall s\in S.f(s)=n\to P(s)\iff\forall s\in S.P(s)$ which is a simple and purely logical exercise. Indeed, we don't even need the fact that $\mathbb N$ is the naturals to prove this lemma, though we do need that fact to apply complete induction for the theorem overall.

| cite | improve this answer | |
  • $\begingroup$ Thank you for pointing me out the completeness of my question. I added the citation of the axiom definition from the TAPL book. $\endgroup$ – mgryszko Sep 18 '19 at 20:20

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.