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

• $\bot$ corresponds to $(\Box, *)$.
• $(Px \to \bot)$ corresponds to $(*,*)$.
• $S \to *$ corresponds to $(*,\Box)$.
• $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.

Chapter 5 - Exercise 12

Exercise 5.12

In λP, consider the context

$Γ ≡ S : *$,

$R : S →S →*$,

$u : Πx,y : S. Rxy →Ryx$,

$v : Πx,y,z : S. Rxy →Rxz →Ryz$

(a) Show that $R$ is ‘reflexive on its domain’, by constructing an inhabitant of the type $Πx,y : S. Rxy →R xx$ in context $Γ$; give a corresponding (shortened) derivation.

(b) Show that $R$ is transitive by constructing an inhabitant of the type $Πx,y,z : S. Rxy →Ryz →Rxz$ in context $Γ$; give a corresponding (shortened) derivation.

(a) Before we develop a proper derivation, let's sketch out why $Πx,y : S. Rxy →R xx$ is true. 

• (i) $\forall_{x,y \in S}(Rxy \implies Ryx)$
• (ii) $\forall_{x,y \in S}(Rxy \implies Rxz \implies Ryz)$
• We start with the assumption that $Rxy$ is true. By (i) this means $Ryx$ is true.
• Renaming variables in $(ii)$ gives $(Ryx \implies Ryx \implies Rxx)$. We swapped $x$ for $y$, and set $z$ to $x$.
• From $Ryx$, we have $Ryx \implies Rxx$. Since we have $Ryx$, we conclude $Rxx$.
• The assumption $Rxy$ gave us $Rxx$, that is $Rxy \implies Rxx$.

The following is a shortened λP derivation.

(b) Again, before we develop a proper derivation, let's sketch out why $Πx,y,z : S. Rxy →Ryz →Rxz$ is true.

• (i) $\forall_{x,y \in S}(Rxy \implies Ryx)$
• (ii) $\forall_{x,y \in S}(Rxy \implies Rxz \implies Ryz)$
• We start with the assumption that $Rxy$ is true. By (i) this means $Ryx$ is true.
• Renaming variables in (ii) gives us $(Ryx \implies Ryz \implies Rxz)$. He we swapped $x$ for $y$ and left $z$ as is.
• From $Ryx$, we have $(Ryz \implies Rxz)$.
• The first assumption $Rxy$ gave us $Ryz \implies Rxz$, that is $ Rxy \implies Ryz \implies Rxz$.

The following is a shortened λP derivation.

Chapter 5 - Exercise 11

Exercise 5.11

Let $S$ be a set, with $Q$ and $R$ relations on $S \times S$, and let $f$ and $g$ be functions from $S$ to $S$. 

Assume that

(i) $∀_{x,y∈S}(Q(x,f(y)) ⇒ Q(g(x),y))$

(ii) $∀_{x,y∈S}(Q(x,f(y)) ⇒R(x,y))$

(iii) $∀_{x∈S}(Q(x,f(f(x))))$

Prove that $$∀_{x∈S}(R(g(g(x)),g(x)))$$ by giving a context $Γ$ and finding a term $M$ such that:

$$Γ ⊢ M : Πx : S. R (g(gx)) (gx)$$

Give the corresponding (shortened) λP-derivation.

Before we develop a proper proof it is useful to sketch out why $\forall_{x \in S}(R(g(g(x)),g(x)))$ is true. 

We first note that since $f:S \to S$ and $g:S \to S$, then $f(x) \in S$ and $g(x) \in S$ for all $x \in S$. In addition the output of any function composition of $f$ and $g$ is also in $S$.

We then note, for all $x \in S$:

• Assumption (ii) tells us $Q(g(g(x)),f(g(x))$ implies $R(g(g(x)),g(x))$.
• Assumption (i) tell us $Q(g(x),f(f(g(x))))$ implies $(Q(g(g(x)),f(g(x)))$.
• Assumption (iii) tells us $Q(g(x),f(f(g(x))))$ is true because $g(x) \in S$.

The following is a λP derivation, with a context and an inhabitant of $Πx : S. R (g(gx)) (gx)$.

So the full judgement is

$$\begin{align} S &:*, \\ Q, R &: S \to S \to *, \\ f,g &: S \to S, \\ u &: \Pi x,y:S .Qx(fy) \to Q(gx)y, \\ v &: \Pi x,y:S .Qx(fy) \to Rxy, \\ w &: \Pi x:S.Qx(f(fx)) \\ \\ & \vdash  \lambda x:S. v(g(gx))(gx)(u(gx)(f(gx))(w(gx))) \; : \; \Pi x:S. R(g(gx))(gx) \end{align}$$

Chapter 5 - Exercise 10

Exercise 5.10

Consider the following context:

$$\begin{align}Γ ≡ S &: ∗, \\ P &: S →∗, \\ f &: S →S, \\ g &: S →S, \\ u &: Πx : S. (P(fx) →P(gx)), \\ v &: Πx,y : S. ((Px →Py) →P(fx))\end{align}$$

(cf. Notation 3.4.2). 

Let $$M ≡ λx : S. v(fx)(gx)(ux)$$

(a) Make a guess at which type $N$ may satisfy $Γ ⊢ M : N$.

(b) Demonstrate that the proof object $M$ does indeed code a proof of the proposition $N$ you have guessed, by elaborating the λP-derivation corresponding to $M$.

(a) Let's rename $x$ to $z$ in the definition of $M$ to aid readability.

$$M ≡ λz : S. v \; (fz) \; (gz) \; (uz)$$

• We start by noting the type of $f$ and $g$ is $S \to S$. So if the type of $z$ is $S$, then the type of $fz$ and $gz$ is $S$.
• The function $v$ takes two arguments of type $S$, and indeed these are $fx$ and $gz$ in the definition of $M$.
• This means $v(fx)(gz)$ has type $((P(fz) →P(gz)) →P(f(fz)))$.

Let's now focus on $(uz)$:

• $u$ is a function that takes one argument of type $S$, and in the definition of $M$ it is applied to $z$ which indeed has type $S$.
• So $(uz)$ has type $(P(fz) →P(gz))$. 

Bring it together, we have

•  $v(fx)(gz)$ has type $((P(fz) →P(gz)) →P(f(fz)))$, and is applied to $uv$ which has a compatible type $(P(fz) →P(gz))$.
• This means $v(fx)(gz)(uz)$ has type $P(f(fz))$

To conclude, $$N \equiv \Pi z:S . P(f(fz))$$

(b) The following is a λP derivation of $Γ⊢M:N$.

Chapter 5 - Exercise 9

Exercise 5.9

Give proofs that the following propositions are tautologies, (first) in natural deduction and (second) by means of a shortened λP-derivation.

(a) $∀_{x∈S} (Q(x)) ⇒ ∀_{y∈S}(P(y) ⇒Q(y))$

(b) $∀_{x∈S}(P(x) ⇒Q(x)) ⇒ (∀_{y∈S} (P(y)) ⇒∀_{z∈S} (Q(z)))$

(a) The following is a natural deduction.

The corresponding λP type is

$$ \Pi a:(\Pi x:S . (Qx)) . ( \Pi y:S.(\Pi b:(Py). Qy)) $$

where the context is $S:*, Q:S \to *, P:S \to *$.

By inspection, an inhabitant is

$$ \lambda a:(\lambda x:S.ax).(\lambda y:S . (\lambda b:(Py).ay )) $$

The following is a shortened λP derivation.

(b) The following is a natural deduction.

The corresponding λP type is

$$ \Pi a: (\Pi x:S.(\Pi b:(Px).Qx)) . ( \Pi c:(\Pi y:S.Py) . (\Pi z:S.Qz)) $$

where the context is $S:*, Q:S \to *, P:S \to *$.

By inspection, an inhabitant is

$$  \lambda a: (\Pi x:S.(\Pi b:(Px).Qx)) . ( \lambda c:(\Pi y:S.Py) . ( \lambda z:S. az(cz) ))  $$

The following is a shortened λP derivation.