Chapter 6 - Exercise 7

Exercise 6.7

Given $Γ ≡S : ∗, Q : S →S →∗$, we define in λC the expressions:

$M_1 ≡ λx,y : S. ΠR : S →S →∗. ((Πz : S. Rzz) →Rxy)$

$M_2 ≡ λx,y : S. ΠR : S →S →∗.((Πu,v : S. (Quv →Ruv)) →Rxy)$

(a) Give an inhabitant of $Πa : S. M_1 aa$ and a shortened derivation proving your answer.

(b) Give an inhabitant of $Πa,b : S. (Qab →M_2 ab)$ and a shortened derivation proving your answer.

(a) We first establish that $Πa : S. M_1 aa$ is

$$Πa : S.  ΠR : S →S →∗. ((Πz : S. Rzz) →Raa)$$

The following derivation proves the inhabitant is

$$\lambda a:S. \lambda R:S \to S \to *.\lambda f:(\Pi z:S.Rzz). fa$$

(b) We first establish that $Πa,b : S. (Qab →M_2 ab)$ is

$$Πa,b : S. (Qab → ΠR : S →S →∗.((Πu,v : S. (Quv →Ruv)) →Rab))$$

The following derivation proves the inhabitant is

$$\lambda a,b:S. \lambda q:Qab . \lambda R:S \to S \to *.\lambda f:(\Pi u,v : S. (Quv \to Ruv)) . fabq$$

Chapter 6 - Exercise 6

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

Chapter 6 - Exercise 5

Exercise 6.5

Let $J$ be the following judgement:

$$ S : * \quad  \vdash  \quad \lambda Q : S \to S \to *. \lambda x : S. Qxx \quad  : \quad  (S \to S \to *) \to S \to * $$

(a) Give a shortened derivation of $J$ and determine the smallest subsystem to which $J$ belongs.

(b) We may consider the variable $Q$ in $J$ as expressing a relation on set $S$. How could you describe the subexpression $λx : S. Qxx$ in this setting? And what is then the interpretation of the judgement $J$?

(a) The following is a shortened derivation.

The following are the arrow sub-expressions, and the corresponding (form) types:

• $S \to *$ corresponds to $(*,\Box)$
• $S \to S \to *$ corresponds to $(*,\Box)$
• $(S \to S \to *) \to S \to *$ corresponds to $(\Box,\Box)$

This means the smallest subsystem the judgement $J$ can belong to is λPω.

(b) The subexpression $\lambda x:S.Qxx$ can be interpreted as a relation taking one argument constructed from a relation $Q$ taking two arguments, achieved by providing $Q$ with the same argument twice.

The interpretation of the judgement is therefore "the existence of a proposition about two elements of a set implies the existence of a proposition about one element of that set, and the proof is the construction of a relation taking one parameter from a relation taking two parameters by providing it with the same parameter twice ".

Chapter 6 - Exercise 4

Exercise 6.4

Let $Γ ≡S : *, Q : S →S →*$ and let $M$ be the following expression:

$$M ≡ (Πx,y : S. (Qxy → Qyx → ⊥)) → Πz : S. (Qzz → ⊥)$$

(a) Give a shortened derivation of $Γ ⊢M : *$ and determine the smallest subsystem to which this judgement belongs.

(b) Prove in λC that $M$ is inhabited in context $Γ$. You may use a shortened derivation.

(c) We may consider $Q$ to be a relation on set $S$. Moreover, it is reasonable to see $A →⊥$ as the negation $¬A$ of proposition $A$. (We shall explain this in Section 7.1.) How can $M$ then be interpreted, if we also take Figure 5.2 into account? And what is a plausible interpretation of the inhabiting term you found in (b)?

(a) The following is a shortened derivation of $Γ ⊢M : *$.

The following are the arrow sub-terms and their corresponding (form) types:

• Context $S \to *$ corresponding to $(*,\Box)$.
• Context $S \to S \to *$ corresponding to $(*, \Box)$.
• Subterm $Qyx \to \bot$ corresponding to $(*,*)$.
• Subterm $\bot$ corresponding to $(\Box, *)$.
• Subterm $Qxy \to Qyx \to \bot$ corresponding to $(*,*)$.
• Subterm $\Pi x,y:S.(Qxy \to Qyx \to \bot)$ corresponding to $(*,*)$
• Subterm $Qzz \to \bot$ corresponding to $(*,*)$.
• Subterm $Qxy \to Qyx \to \bot$ corresponding to $(*,*)$.
• Subterm $\Pi z:S.(Qzz \to \bot)$ corresponding to $(*,*)$
• Term $(\Pi x,y:S.(Qxy \to Qyx \to \bot)) \to \Pi z:S.(Qzz \to \bot)$ corresponds to $(*,*)$.

This means the smallest subsystem the judgement can belong to is λP2.

(b) By inspection the inhabitant should be

$$\lambda f:(\Pi x,y:S.(Qxy \to Qyx \to \bot)) . (\lambda z:S.(\lambda q:Qzz.fzzq))$$

The following is a derivation of this inhabitant, continuing from the derivation of the type above.

(c) The interpretation of $M$ is as follows.

$$\forall_{x,y \in S}(\;  Q(x,y) \implies \neg Q(y,x)\; ) \implies \forall_{z \in S}(\; \neg Q(z,z) \; )$$

In words, if $Q$ is asymmetric, then $Q$ is not reflexive.

The interpretation of the inhabitant is "there exists a function (here, $f$) that maps an asymmetric function to an irreflexive function", which proves the above logical statement.