Chapter 6 - Exercise 10

Exercise 6.10

Given $S : *$ and $P_1,P_2 : S →*$, we define in λC the expression:

$$R ≡ λx : S. ΠQ : S →*. (Πy : S. (P_1 y →P_2 y →Qy)) →Qx$$

We claim that $R$ codes ‘the intersection of $P_1$ and $P_2$’, i.e. the predicate that holds if and only if both $P_1$ and $P_2$ hold. In order to show this, give inhabitants of the following types, plus (shortened) derivations proving this:

(a) $Πx : S. (P_1 x →P_2 x →Rx)$

(b) $Πx : S. (Rx →P_1 x)$

(c) $Πx : S. (Rx →P_2 x)$

Why do (a), (b) and (c) entail that R is this intersection?

(Hint for (b): see Exercise 5.8(a).)

(a) An inhabitant of the type is

$$ \lambda x:S.\lambda f: P_1 x. \lambda g:P_2 x. \lambda h :  \Pi y : S. (P_1 y \to P_2 y \to Qy).hxfg  $$

The following is a shortened derivation.

(b) An inhabitant of the type is 

$$ \lambda x:S . \lambda f:Rx .    ( f P_1 (\lambda y:S.(\lambda a:P_1 y . \lambda b:P_2 y.a)) ) $$

The following is a shortened derivation.

(c) An inhabitant of the type is

$$ \lambda x:S . \lambda f:Rx .    ( f P_2 (\lambda y:S.(\lambda a:P_1 y . \lambda b:P_2 y.b)) ) $$

The following is a shortened derivation.

The claim is that, for $x \in S$,

$$ P_1(x) \land P_2(x) \iff R(x) $$

"If and only if" $\iff$ has a particular meaning. $A \iff B$ means both $A \implies B$ and $B \implies A$.

In this case, it means both of the following are true:

• $ P_1(x) \land P_2(x) \implies R(x) $
• $ R(x) \implies P_1(x) \land P_2(x) $ which is equivalent to both $ R(x) \implies P_1(x) $ and $ R(x) \implies P_2(x) $.

The first is shown by (a), and the second is shown by both (b) and (c). So together, (a), (b) and (c), show that $R$ codes the intersection of $P_1$ and $P_2$.

Chapter 6 - Exercise 9

Exercise 6.9

Given $S : ∗, P : S → *$ and $f : S → S$, we define in λC the expression:

$$M ≡ λx : S. ΠQ : S →*. (Πz : S. (Qz →Q(f z))) →Qx$$

Give a term of type $Πa : S. (M a →M(f a))$ and a (shortened) derivation proving this.

The following is an inhabitant of the type $\Pi a:S . (Ma \to M(fa))$

$$\lambda b:Ma . \lambda Q:S\to *.\lambda g: (\Pi z : S. (Qz \to Q(f z))).ga(bQg)$$

The following is a shortened derivation.

Chapter 6 - Exercise 8

Exercise 6.8

(a) Let $Γ ≡ S : *, P : S → *$. Find an inhabitant of the following type $N$ in context $Γ$, and prove your answer by means of a shortened derivation:

$$N ≡ [Πα : *. ((Πx : S. (P x →α)) →α)] → [Πx : S. (P x →⊥)] →⊥$$

(b) Which is the smallest system in the λ-cube in which your derivation may be executed?

(c) The expression $Πα : ∗. ((Πx : S. (P x →α)) →α$ may be considered as an encoding of $∃_{x∈S}(P(x))$. (We shall show this in Section 7.5.) In Section 7.1 we make plausible that $A →⊥$ may be considered as an encoding of the negation $¬A$. With these things in mind, how can we interpret the content of the expression $N$? (See also Figure 5.2.)

(a) The shortened derivation below proves the inhabitant is

$$\lambda f:[\Pi \alpha : *. ((\Pi x : S. (P x \to \alpha)) \to \alpha)].\lambda g:[\Pi x : S. (P x \to \bot)]. f \bot g$$

(b) The ∏-types and their corresponding (form) types are:

• $S \to *$ corresponds to $(*, \Box)$
• $(Px \to \alpha)$ corresponds to $(*,*)$
• $\Pi x:S.(Px \to \alpha)$ corresponds to $(*,*)$
• $((\Pi x:S.(Px \to \alpha))\to \alpha)$ corresponds to $(*,*)$
• $\Pi \alpha:*.((\Pi x:S.(Px \to \alpha))\to \alpha)$ corresponds to $(\Box,*)$
• $\bot$ corresponds to $(\Box,*)$
• $(Px \to \bot)$ corresponds to $(*,*)$
• $\Pi x:S.(Px \to \bot)$ corresponds to $(*,*)$
• $[\Pi x:S.(Px \to \bot)] \to \bot$ corresponds to $(*,*)$
• $[Πα : *. ((Πx : S. (P x →α)) →α)] → [Πx : S. (P x →⊥)] →⊥$ corresponds to $(*,*)$

The minimal system is therefore λP2.

(c) The interpretation of N is 

$$\exists_{x \in S} (P(x)) \implies \neg (\forall_{x\in S}(\neg P(x) ) )$$

In words, if there exists at least one $x \in S$ for which $P(x)$ is true, that implies it is not the case that $P(x)$ is false for all $x \in S$.

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.