Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

enter image description here

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

enter image description here

enter image description here

enter image description here

share|cite|improve this question
up vote 1 down vote accepted

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".

share|cite|improve this answer
Thank You Very Much Henning , and yes I agree that it should be "By inspection of the typing rules" – Adel Apr 10 '12 at 16:18

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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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