2
$\begingroup$

I have a few small questions about section 2.4 ("Rule induction") in Practical Foundations for Programming Languages (p. 19).

(1) In the rule induction principles for nat,

To show P(a nat) whenever a nat, it is enough to show: (1) P(zero nat). (2) for every a, if (a nat and) P(a nat), then P(succ(a) nat).

why is the bracketed "(a nat and)" clause necessary (and similarly for tree)? This seems "natural" - we shouldn't need to prove things about syntactic entities that don't define nats - but doesn't appear in the definition given of property P "respecting the rules" defining nat/tree (also on p. 19), which is how the rule induction principle is defined. In the proof of Lemma 2.1, the extra "a nat and" part has become part of the definition of the property P - what's going on here?

(2) I don't understand the induction step of Lemma 2.1 (succ(a) nat implies a nat). If I were doing this proof, I'd just invert the rules for nat right away, or, using Harper's property P, say: If succ(a) is of form succ(b), then by injectivity, a equals b, hence b nat as a nat, but injectivity hasn't been proven yet. It seems instead that Harper applies the induction hypothesis about a directly to succ(a) - I must be missing something.

(3) In a more naive framework, Lemma 2.3 would just follow from sufficiency of the = nat relation rules ("inversion"), but I don't know how to write down a proof in this style. Why is induction even needed?

I'm sorry if these questions seem like nitpicking, but Martin-Löf/LF feels very foreign to me. If I squint and pretend I'm doing everything in a more "traditional" operational semantics, I can read other parts of the book (with slightly different proofs), but I feel I'm missing the point in doing so.

If these questions are too tedious to answer individually, are there other references on doing semantics in this style?

Improve this question
$\endgroup$
3
  • $\begingroup$ It's actually on page 17. $\endgroup$
    – Dave Clarke
    Mar 17, 2014 at 17:24
  • $\begingroup$ The page number above refers to the current online version (v1.41) - it's different in the print edition. $\endgroup$
    – Fixnum
    Mar 17, 2014 at 17:32
  • $\begingroup$ I was referring to the online version, the page number indicated on the page, not the pdf page number. $\endgroup$
    – Dave Clarke
    Mar 17, 2014 at 18:10

2 Answers 2

Reset to default
2
$\begingroup$

At the beginning of Section 2.4 the book explains that $\mathcal{P}(J)$ stands for a property of a judgment $J$. That is, the $\mathcal{P}$ in $\mathcal{P}(a\ \mathtt{nat})$ does not stand for a property of numbers, but a property of the judgment $a\ \mathtt{nat}$, which is the judgment that "$a$ is a number".

It just so happens that the inference rules for $a\ \mathtt{nat}$ precisely match those for numbers. Namely, the two rules defining the judgment $a\ \mathtt{nat}$ are $$\frac{ }{\mathtt{zero}\ \mathtt{nat}}$$ and $$\frac{a\ \mathtt{nat}}{\mathtt{succ}(a)\ \mathtt{nat}}.$$ Therefore, if we want to show that the judgment $a\ \mathtt{nat}$ has some property $\mathcal{P}$, then we need to show that the base case $\mathtt{zero}\ \mathtt{nat}$ has the property $\mathcal{P}$, and that whenever $\mathcal{P}(a\ \mathtt{nat})$ holds then $\mathcal{P}(\mathtt{succ}(a)\ \mathtt{nat})$ holds as well.

Or to put it the other way, the strange looking "$\mathtt{nat}$" is there because we are not talking about numbers, but about the judgments "expression $a$ satisfies the judgment $\mathtt{nat}$".

Improve this answer
$\endgroup$
2
  • $\begingroup$ Wow, thanks for taking the time to answer my question! Unfortunately, I think this is the part I already understand. But even here you disagree slightly with the the book, which also assumes $a\ \mathtt{nat}$ in addition to $\mathcal{P}(\mathtt{succ}(a)\ \mathtt{nat})$ in the induction step ... why? And is the induction step in Lemma 2.1 obvious (how is $b\ \mathtt{nat}$ concluded?)? Sorry for being (temporarily) so pedantic! $\endgroup$
    – Fixnum
    Mar 21, 2014 at 16:43
  • $\begingroup$ I think the whole point of this is to be super pedantic. Speaking off the top of my head, you might get into trouble without $a\ \mathtt{nat}$ if you use a weird $a$. I'll try to cook up a concrete example (but will also be away over the weekend, so don't hold your breath). $\endgroup$
    – Andrej Bauer
    Mar 21, 2014 at 17:31
1
$\begingroup$

Question 1

The range of acceptable inputs for the property P is natural numbers, and therefore if a is not a natural number P(a) cannot be valid. Looking at it a different way, P(J) is true if and only if P(J1),P(J2),...,P(Jn) are all true. If J1 isn't true (a isn't a natural number) then P(J1) cannot be true, and P(J) cannot be true either.

Question 2

The presentation of the proof is a little confusing. Our goal is to show that if succ(a) is true, then a nat is true as well. In order to prove this, the book defines a property P(a nat) so that if a nat is true and we can describe a = succ(b), then b nat must be true as well. If we can prove this property, then P(a nat) is closed. Because we are now proving P(a nat), we can proceed on the assumptions a nat and a = succ(b).

Skipping the trivial case a = 0, if succ(a) nat and a = succ(b), then succ(succ(b)) nat, which implies succ(b) nat which in turn implies b nat. Thus our property P(a nat) holds for each of the conditions, and is therefore closed.

Question 3

Suppose succ(a1) = succ(a2) nat. By Lemma 2.1, we know a1 nat and a2 nat, leading to a1 = a2 nat.

Improve this answer
$\endgroup$
2
  • $\begingroup$ I think you're right regarding Q1, although this wasn't clear to me from the book. Regarding Q2, the second assumption in the induction step is that succ(a) (not a) has form succ(b), so the prove doesn't go through. For Q3, you've used an inversion principle? (I think you also assume the easy lemma that a = b nat implies a nat and b nat, since = and = nat are, a priori, unrelated). But (a) can a direct inductive proof to through? (b) Harper proves his inversion principles by an appeal to induction, so my question is: is this a valid form of reasoning in this framework? $\endgroup$
    – Fixnum
    Mar 20, 2014 at 3:56
  • $\begingroup$ Also, (regarding your proof in Q3,) we have no proof that a = b nat implies that a is syntactically equal to (and can be substituted for) b ... $\endgroup$
    – Fixnum
    Mar 20, 2014 at 3:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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