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.

Chapter 6 - Exercise 3

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.

Chapter 6 - Exercise 2

Exercise 6.2

Let $Γ ≡S : ∗, P : S →∗, A : ∗$.

Prove by means of a flag derivation that the following expression is inhabited in λC with respect to Γ:

$$(Πx : S. (A →P x)) →A →Πy : S. P y$$

(You may shorten the derivation, as explained in Section 4.5.)

By inspection, the following should be an inhabitant of the given type.

$$\lambda f:(\Pi x:S.(A \to P x)) . \lambda a:A . \lambda y:S . fya$$

The following is a shortened flag derivation using λC rules.

Chapter 6 - Exercise 1

Exercise 6.1

(a) Give a complete derivation in tree format showing that $⊥≡Πα : ∗. α$ is legal in λC (cf. Exercise 3.5).

(b) The same for $⊥→⊥$.

(c) To which systems of the λ-cube does $⊥$ belong? And $⊥→⊥$?

(a) The following is a tree derivation of $⊥≡Πα : ∗. α$. 

$$(1) \quad \emptyset \vdash * \; : \; \Box \quad (sort)$$

$$\frac{(1) \quad \emptyset \vdash * \; : \; \Box}{(2) \quad \alpha:* \vdash \alpha  \; : \; *} \quad (var)$$

$$\frac{(1) \quad \emptyset \vdash * \; : \; \Box \quad \quad (2) \quad \alpha:* \vdash \alpha \; : \; *}{(3) \quad \emptyset \vdash \Pi \alpha:*.\alpha \; : \; *} \quad (form)$$

So $\bot \equiv \Pi \alpha:*.\alpha$ is legal in λC since in the empty context $\bot$ has type $*$. 

(b) We continue from above.

$$\frac{(3) \quad \emptyset \vdash \bot \; : \; *}{(4) \quad x:\bot \vdash x \; : \; \bot} \quad (var)$$

$$\frac{(3) \; \emptyset \vdash \bot \; : \: * \quad \quad (4) \quad x:\bot \vdash \bot \; : \; *}{(5) \quad \emptyset \vdash \bot \to  \bot \; : \; *} \quad (form)$$

So $\bot \to \bot$ is legal in λC since in the empty context $\bot \to \bot$ has type $*$. 

(c) Let's remind ourselves of the 8 systems of the λ-cube.

Let's first consider $\bot$. From the above tree derivation we can it is the result of the (form) rule with $s_1 = \Box$ and $s_2 = *$. The combination is $(\Box, *)$. That means $\bot$ belongs only in λ2, λω, λP2, and λC.

Now let's consider $\bot \to \bot$. From the tree derivation we can see it is the result of the (form) rule with $s_1=*$ and $s_2=*$. The combination is $(*,*)$. This suggests $\bot \to \bot$ belongs to all 8 systems of the λ-cube. However, since the sub-term $\bot$ can only be derived in λ2, λω, λP2, and λC, then $\bot \to \bot$ belongs only to those same systems.