Exercise 6.6
Let $$M ≡λS : *. λP : S →*. λx : S. (P x →⊥)$$
(a) Which is the smallest system in the λ-cube in which $M$ may occur?
(b) Prove that $M$ is legal and determine its type.
(c) How could you interpret the constructor $M$, if $A →⊥$ encodes $¬A$?
(a) The arrow types and their corresponding (form) types in the judgment $M$ are as follows:
- $S \to *$ corresponds to $(*,\Box)$
- $\bot$ corresponds to $(\Box, *)$
- $Px \to \bot$ corresponds to $(*, *)$
- $(S \to *) \to (S \to *)$ corresponds to $(\Box,\Box)$ - see derivation of types below.
- $* \to (S \to *) \to (S \to *)$ corresponds to $(\Box,\Box)$ - see derivation of types below.
Therefore the smallest system in the λ-cube in which $M$ can occur is the full λC?.
(b) The following is a shorted derivation of the judgement.
Because $M$ has been derived following the derivation rules, has a type and a context (here, empty), then $M$ is legal.
As a reminder, Definition 6.3.7 updates the definition of legality as being typable or inhabited.
In the empty context, $M$ has the following type $$\Pi S:*. ( (S \to *) \to (S \to *) )$$
Note 1, alternative notation for this is $(S:*) \to ( (S \to *) \to (S \to *)$.
Note 2, the official solutions appear to have a typo, suggesting the type is $S \to ( (S \to *) \to (S \to *)$.
(c) $M$ can be interpreted as constructing the negation of a proposition $P$ supplied as an argument, where that proposition is about all elements of a set $S$.
