patternMinor
Types and Programming Languages - proof for theorem about principles of induction of terms
Viewed 0 times
principleslanguagesprogrammingfortheoremtypesandabouttermsproof
Problem
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)
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?
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)
- 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?
Solution
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.
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.
Context
StackExchange Computer Science Q#114861, answer score: 2
Revisions (0)
No revisions yet.