When extending the simply typed $\lambda$-calculus with products, we extend $\beta$-reduction with the rules $\pi_i \langle M_1, M_2 \rangle \to_\beta M_i$, which makes sense (cf. Sørensen, Urzyczyn, Lectures on the Curry-Howard Isomorphism, p. 87). But in some cases we also have the equation $\langle \pi_1 M, \pi_2 M \rangle = M$ which (as far as I can tell) cannot be proved in the STLC with products and the above reduction rules. For instance, when defining the category of types it seems to be necessary for product types to be categorical products (cf. Awodey, pp. 43-44). Girard calls it and $\eta$-conversion the "secondary equations" and says that they "have never been given adequate status", but he doesn't really elaborate on this (cf. Girard, Proof and Types, p. 16, pdf).

So what is the significance of and the justification for sometimes including this equation and sometimes not? Of course it is very natural (and must at least hold if product types are categories products), but then why not include it in the $\beta$-reduction? Unless it can in fact be proved and I have just been unsuccessful. But if so then why do we sometimes assume it explicitly?



Your Answer

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

Browse other questions tagged or ask your own question.