4
$\begingroup$

Assume an evaluation-relation on terms $t \Downarrow v$. If I want to prove correctness of a function $\phi$ w.r.t. evaluation, I have to show that the following implication always holds:

$$\frac{\phi(t) \Downarrow \phi(v)}{t \Downarrow v}$$

Naturally, this is a candidate for structural induction. But on what structure? Is it sufficient to run the induction over terms, or do I have to run it over the derivation tree? Structural induction is usually only allowed for direct sub-terms, but the function could, in principle, yield completely different results.

Is it sensible to consider $\phi$ part of the promise or do I have to consider it a part of the recursive structure?

$\endgroup$
3
$\begingroup$

You probably shouldn't write $\cfrac{\phi(t)\Downarrow \phi(u)}{t\Downarrow u}$ for "For any terms $t,u$, $\phi(t)\Downarrow \phi(u)$ implies $t\Downarrow u$".


I'll take a concrete example: Terms are made using $0,S,+$. And there are six rules:

$$\cfrac{}{0 \Downarrow 0}(0)\hspace{2em}\cfrac{x\Downarrow y}{Sx \Downarrow Sy}(S)\hspace{2em}\cfrac{x\Downarrow y}{x+0 \Downarrow y}(+0)\hspace{2em}\cfrac{x\Downarrow y}{0+x \Downarrow y}(0+)\hspace{2em}\cfrac{x+y\Downarrow z}{x+Sy \Downarrow Sz}(+S)\hspace{2em}\cfrac{x+y\Downarrow z}{Sx+y \Downarrow Sz}(S+)$$

Note that $(0+)$ and $(S+)$ are superfluous (but do not break the uniqueness of the normal form).

I'll provide three examples where different proof techniques apply.


Let's take $\phi(x)=Sx$.

Suppose that for some $a$, $Sa=\phi(a)\Downarrow \phi(b)=Sb$. The only rule that allows you to prove this is the rule $(S)$ with $x=a$ and $y=b$ (because it's the only rule that can have successor on both sides of $\Downarrow$ in the conclusion), so you must have $a\Downarrow b$, which is what you want. So you can prove that "For any terms $t,u$, $\phi(t)\Downarrow \phi(u)$ implies $t\Downarrow u$".

You were able to prove it without even using induction because the definition of $\phi$ wasn't inductive.

Remark

But you can not compose rules to get $\cfrac{St\Downarrow Su}{t\Downarrow u}$ (because there are more $S$ in the conclusion than in the premise and all rules have at most as many $S$ in the conclusion as in the premise).

Your result is a meta-theorem but not a theorem (because it's not just a combination of the rules).

A theorem would, for example, be $\cfrac{}{S0\Downarrow S0}$ (that you get by composing $(0)$ and $(S)$ or $\cfrac{x\Downarrow y}{x+S0\Downarrow Sy}$ (that you get by composing $(+0)$ and $(+S)$).


Let's take another example: $\varphi(0)=0$, $\varphi(Sx)=SSx$ and $\varphi(x+y)=\varphi(x)+\varphi(y)$.

Now suppose that $\varphi(a)\Downarrow \varphi(b)$.

We'll prove $a\Downarrow b$ by induction on the size of the proof of $\varphi(a)\Downarrow \varphi(b)$.

If it's of size $1$, then it has to be just an application of $(0)$ so $\varphi(a)=0=\varphi(b)$ and so $a=0=b$ and $(0)$ gives us the proof we want.

If it's of size $>1$, the last rule is not $(0)$ so you do case analysis and apply the induction hypothesis on the premise of the rule. You'll have to do case analysis, but you should be able to prove that it works.


There should be some case where you can do induction on terms to prove the thing but I couldn't find one. It feels more natural when you have a small step transition system $\to$ and define a big step one $x\Downarrow y$ by $x\to^* y$ and for any $z$, $y\not\to z$. Then, it you manage to prove that $\phi(x)\to \phi(y)$ implies $x\to^+ y$ and that $x\to y$ implies $\phi(x)\to^+\phi(y)$, you will get that $\phi(x)\Downarrow \phi(y)$ implies $x\Downarrow y$.

The main thing you should remember is that "case analysis" < "induction on terms" < "induction on proofs" in terms of what you can proove but often, the number of cases you have to handle often grows. So you should try the proofs techniques in that order until you get one that works.

$\endgroup$
2
$\begingroup$

If your logic has a rule like $\dfrac{\phi(t) \Downarrow \phi(v)}{t \Downarrow v}$ then you can't use induction over terms to prove something. A rule like this is not syntax-directed: you can't choose which rule to apply to deduce a conclusion based on the syntax of that conclusion.

To perform induction over proofs, you need to do induction over the syntax of the proof. This is equivalent to induction over terms only when the deduction rules are syntax-directed. Syntax-directed rules are nice, but they aren't always possible.

To give a concrete example, a logic that has a transitivity rule like $\dfrac{A \preceq B \quad A \preceq C}{A \preceq C}$ isn't syntax-directed and it's often impossible to prove properties of such relations with the syntax of terms alone, because you never know when an inequality might have been obtained via transitivity rather than for structural reasons. Sometimes transitivity is a derived rule (i.e. you can prove that for any $A$, $B$ and $C$ such that $A \preceq B$ and $B \preceq C$ are derivable then there exists a derivation of $A \preceq C$. That makes the system easier to work with because (barring other, similar rules) you no longer have to consider arbitrary intermediate $B$'s when you induct over the structure of derivations.

If $\phi$ is a meta function rather than part of the syntax of the language, then it's even more obvious that you can't do induction on the structure. Consider the case when $\phi$ is the identity function...

$\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.