Exercise 6.3
Let $J$ be the judgement:
$$S : *, P : S →* ⊢ λx : S. (P x →⊥) : S →*$$
(a) Give a shortened λC-derivation of $J$.
(b) Determine the $(s_1,s_2)$-combinations corresponding to all $Π$s (or arrows) occurring in $J$.
(c) Which is the ‘smallest’ system in the λ-cube to which $J$ belongs?
(a) From exercise 6.1 we have $⊥≡Πα : ∗. α$ which has type $*$.
The following is a shortened λC derivation of the judgement.
(b) The following are the arrow types in $J$:
- The arrow of sub-term $\bot$ corresponds to $(\Box, *)$.
- The arrow of the sub-term $(Px \to \bot)$ corresponds to $(*,*)$.
- The arrow of the type $S \to *$ corresponds to $(*,\Box)$.
- The arrow in the context $P: S \to *$ corresponds to $(*, \Box)$
(c) Figure 6.2 summarises the combinations $(s_1, s_2)$ corresponding to the λ-cube systems.
The smallest system to which $J$ belongs is λP2.
