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.

Chapter 5 - Exercise 8

Exercise 5.8

(a) Let $Γ ≡ S : *, P : S → *, Q : S → *$. Find an inhabitant of $\Pi x : S. P x → Qx → Px$ with respect to $Γ$, and give a corresponding (shortened) derivation.

(b) Give a natural deduction proof of the corresponding logical expression.

(a) Given the context and variable $x:S$,

$$\begin{align} S &: * \\ P &: S \to * \\ Q &: S \to * \\ x &: S\end{align}$$

we have

$$\begin{align} Px &: * \\ Qx &: *\end{align}$$

By inspection, an inhabitant of $\Pi x : S. P x → Qx → Px$ should be

$$ \lambda x : S. \lambda p: P x. \lambda q: Qx . p $$

The following is a shortened derivation of the inhabitant and its type.

(b) The type $\Pi x : S. P x → Qx → Px$ corresponds to the following logical expression.

$$ \forall_{x \in S} ( \; P(x) \implies Q(x) \implies P(x) \; ) $$

The following is a natural deduction of this logical statement.

Chapter 5 - Exercise 7

Exercise 5.7

Prove that the following propositions are tautologies by giving shortened λP-derivations:

(a) $(A ⇒B) ⇒((B ⇒C) ⇒(A ⇒C))$

(b) $((A ⇒B) ⇒A) ⇒((A ⇒B) ⇒B)$

(c) $(A ⇒(B ⇒C)) ⇒((A ⇒B) ⇒(A ⇒C))$

(a) The type associated with $(A ⇒B) ⇒((B ⇒C) ⇒(A ⇒C))$ is

$$ \Pi x:(\Pi a:A.B).(\Pi y:(\Pi b:B.C).(\Pi a:A.C)) $$

By inspection, the inhabitant should be

$$ \lambda x:(\Pi a:A.B).(\lambda y:(\Pi b:B.C).(\lambda a:A.y(xa))) $$

The following is a shortened derivation in λP, first deriving the type, then the inhabitant.

(b) The type associated with $((A ⇒B) ⇒A) ⇒((A ⇒B) ⇒B)$ is

$$ \Pi x:(\Pi s:(\Pi a:A.B).A) . (\Pi t:(\Pi a:A.B).B) $$

By inspection, the inhabitant should be

$$ \lambda x:(\Pi s:(\Pi a:A.B).A) . (\lambda t:(\Pi a:A.B). t(xt)) $$

The following is a shortened derivation λP, first deriving the type, then the inhabitant.

(c) The type associated with $(A ⇒(B ⇒C)) ⇒((A ⇒B) ⇒(A ⇒C))$ is

$$ \Pi x:(\Pi a:A . (\Pi b:B.C)) . (\Pi y:(\Pi a:A .B).(\Pi a:A.C)) $$

By inspection, the inhabitant should be

$$ \lambda x:(\Pi a:A . (\Pi b:B.C)) . (\lambda y:(\Pi a:A .B). (\lambda a:A.xa(ya))) $$

The following is a shortened derivation in λP, first deriving the type, then the inhabitant.

Chapter 5 - Exercise 6

Exercise 5.6

Prove that $(A ⇒(A ⇒B)) ⇒(A ⇒B)$ is a tautology, (first) in natural deduction and (second) by means of a shortened λP-derivation.

Natural Deduction

The following is a natural deduction proof of the logical statement.

Full λP Derivation

Noting that the associated type for $A \implies B$ is $\Pi x:A.B$, then the type for the given logical statement is 

$$\Pi z:(\Pi y:A.(\Pi x:A.B)) . (\Pi x:A.B)$$

By inspection, a term that inhabits that type is

$$\lambda z:(\Pi y:A.(\Pi x:A.B)). (\lambda x:A. zxx)$$

The following is a full derivation, before we develop a shorted one below (click to enlarge).

Shortened λP Derivation

The following is a shortened derivation.

Chapter 5 - Exercise 5

Exercise 5.5

Prove that $A ⇒ ((A ⇒ B) ⇒ B)$ is a tautology by giving a shortened λP-derivation.

To show that $A ⇒ ((A ⇒ B) ⇒ B)$ is a tautology, we need to show that corresponding type is derivable and is also inhabited.

Full Derivation

The following is a flag notation derivation of both the type and the inhabitant. This is a full derivation before we develop a shortened derivation.

Shortened Derivation

The following is a shortened derivation.

Chapter 5 - Exercise 4

Exercise 5.4

Prove that * is the only legal kind in λP.

The set of kinds $\mathbb{K}$ is defined as

$$\mathbb{K} = * \; | \; \mathbb{K} \to \mathbb{K}$$

The textbook gives examples of kinds

$$∗, \; ∗→∗, \; ∗→∗→∗, \; (∗→∗) →∗, \; (∗→∗) →∗→∗, \; ∗→(∗→∗) →∗$$

For a kind $k$ to be legal, there must exist a context $Γ$ and type $t$ such that $Γ⊢k:t$.

All judgements are a result of the derivation rules for λP, given in Figure 5.1, so we can examine them to see how a judgement of the form $Γ⊢k:t$ can be derived.

The axiomatic (sort) rule $\emptyset \vdash *:\Box$ immediately tells us that * is a legal kind.

Using the definition of kinds, aside from *, all other kinds are arrow types of the form $\mathbb{K} \to \mathbb{K}$. All of them are derived from the simplest $* \to *$. If we can show that $* \to *$ is not derivable, then we have shown all the other kinds (except *) are not derivable.

The type $* \to *$ is only derived by the (form) rule. Note that $* \to *$ is an abbreviation of $\Pi x:*.*$.

$$(form) \quad \frac{Γ ⊢ A:* \qquad Γ, x:A ⊢ B:s}{Γ ⊢ \Pi x:A.B:s} \quad x \notin Γ$$

To form $\Pi x:*.*$, we must have $A=*$ and $B=*$. The first premise would then require $*:*$.

There is no derivation rule that results in $Γ ⊢*:*$, and so kinds aside from * are not derivable in λP.

Chapter 5 - Exercise 3

Exercise 5.3

Extend the flag derivation of Exercise 5.2(b) to a complete derivation of

$$S : *, Q : S →S →* ⊢ Πx : S. Πy : S. Qxy : *$$

The following is the flag derivation (click to enlarge).

Chapter 5 - Exercise 2

Exercise 5.2

Give a complete (i.e. unshortened) λP-derivation of

$$ S : ∗ ⊢ S →S →∗ : \Box $$

(a) in tree format,

(b) in flag format.

(a) The following shows the derivation in tree format.

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

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

$$ \frac{(1) \; \emptyset \vdash * : \Box \qquad (1) \; \emptyset \vdash * : \Box}{(3) \; S:* \vdash *:\Box} \quad (weak)$$

$$ \frac{(3) \; S:* \vdash *:\Box \qquad (2) \; S:* \vdash S:*}{(4) \; S:*, x:S \vdash *:\Box} \quad (weak)$$

$$ \frac{(2) \; S:* \vdash S:* \qquad (4) \; S:*, x:S \vdash *:\Box}{(5) \; S:* \vdash S \to *:\Box} \quad (form)$$

$$ \frac{(5) \; S:* \vdash S \to *:\Box \qquad (2) \; S:* \vdash S:*}{(6) \; S:*, x:S \vdash S \to *:\Box} \quad (weak)$$

$$ \frac{(2) \; S:* \vdash S:* \qquad (6) \; S:*, x:S \vdash S \to *:\Box}{(7) \; S:* \vdash S \to S \to *:\Box} \quad (form)$$

(b) The following shows the derivation in flag format.

Chapter 5 - Exercise 1

Exercise 5.1

Give a diagram of the tree corresponding to the complete tree derivation of line (18) of Section 5.3.

The following is a flag format derivation for easy reference.

And the following is a diagram corresponding to the tree derivation (click to enlarge).