Clarification about what is meant in this slide by “induction on the typing rules”?

Question

I'm lost on what's happening here. This is regarding MinML( "an idealized programming language" ) . More pics below: Thank You Very Much

Answer 1

The slide is misleading and confusing because there's not actually any induction going on in the arguments for the claims on it. (Here I'm assuming here that the typing rules are remotely similar to how typing rules for ML-like languages are usually formulated).

The argument for each of the claims is very simple -- for example, if $\Gamma \vdash x : t$ is true, then by definition it must be true by virtue of a typing derivation that has $\Gamma \vdash x : t$ as the conclusion. And by looking through the list of typing rules we find that the only rule that can possibly produce a conclusion with a variable letter in the expression field has $\Gamma(x)=t$ as a side condition, and therefore this must be so -- otherwise there's no way for $\Gamma \vdash x : t$ to be true.

So what's the author's deal when he speaks about induction? Two guesses:

1. He had some kind of "induction" argument in mind, but somehow confused himself into not noticing that he never actually used the induction hypothesis.

2. He actually meant to type: "By inspection of the typing rules", which makes eminent sense here -- both as a description of the argument I've just described and as a matter of word choice. It is a bit unidiomatic to speak about "induction on the typing rules"; if one really had an induction in mind one would call it "induction on the typing derivation".

Answer 2

I have no idea what the "typing rules" are, but in order for this to make sense, they must be rules that tell you how to build up something from basic parts. "Induction" would mean doing two things: (1) Proving that a statement is true of the basic parts, whatever they are; and (2) Proving that at each step in building something up from those parts, if the statement is true of the parts that get put together at that step, then it's true of the thing that results from putting them together.

If you tell us what those parts are and how they get put together, maybe we could say more.