Chapter 9 - Exercise 8

See Exercises 9.6 and 9.7.

(a) Let $\Delta^{′} ≡ D_1, \ldots ,D_5$. Assume that $D_6$ is correct in environment $\Delta^{′}$ and

$$\Delta^{′} ; ∅ ⊢ (a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050) : *_p$$

Derive:

$$ \Delta ; ∅ ⊢ \texttt{formalprf}_6 : a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050 $$

(b) Assume that the conditions mentioned in Exercise 9.7(a) have been satisfied. What is the fastest manner to prove

$$D_1 ; f :  \mathbb{N} → \mathbb{R}, n :  \mathbb{N} ⊢ a_1(f,n) : \mathbb{R} $$

We remind ourselves of definitions $D_1$ to $D_6$:

$$\begin{align*} D_1 \; &≡ \; f : \mathbb{N} \to \mathbb{R}, \; n : \mathbb{N} \quad \triangleright \quad a_1(f,n) := \sum ^n_{i=0}(f i) : \mathbb{R} \\ \\ D_2 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R} \quad \triangleright \quad a_2(f,d) := \forall _{n:\mathbb{N}}(f (n+1)−f n= d) : *_p \\ \\ D_3 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\ & a_3(f,d,u,n) := \texttt{formalprf}_3 : f n= f 0 + n \cdot d \\ \\ D_4 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\ & a_4(f,d,u,n) := \texttt{formalprf}_4 : a_1(f, n) = \frac{1}{2} \cdot (n+1) \cdot (f 0 + f n)  \\ \\ D_5 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\  & a_5(f,d,u,n) := \texttt{formalprf}_5 : a_1(f,n) = (n+1) \cdot f 0+ \frac{1}{2}\cdot n \cdot (n+1) \cdot d \\ \\  D_6 \; & ≡ \; \emptyset \quad \triangleright \quad a_6 := \texttt{formalprf}_6 : \sum^{100}_{ i=0} (i) = 5050 \end{align*}$$

(a) We're given $D_6$ is correct in environment $\Delta^{′}$. This means

$$\Delta^{\prime}, \emptyset \; \triangleright \; a_6 := \texttt{formalprf}_6 : \sum^{100}_{ I=0} (i) = 5050 \; ; \; \emptyset \; \vdash \; * : \Box $$

We're also given

$$\Delta^{′} ; ∅ ⊢ (a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050) : *_p$$

And we want to derive

$$  \Delta ; ∅ ⊢ \texttt{formalprf}_6 : a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050  $$

---

Let's consider the (inst) rule. The conclusion is a judgement $\Delta; \Gamma \vdash a(\bar{U}):N[\bar{x} := \bar{U}]$. Here the constant $a$ is $\texttt{formalprf}_6$ with no parameter list. The type $N$ is $\sum^{100}_{ i=0} (i) = 5050$. Noting that $\Gamma = \emptyset$, this gives us

$$ (\textit{inst}) \quad \frac{\Delta ; \emptyset \vdash *:\Box }{\Delta; \emptyset \vdash \texttt{formalprf}_6 : \sum^{100}_{ i=0} (i) = 5050} \tag{i} $$

where $\Delta = \Delta^{\prime}, D_6$. The first premise is true because we're given that $D_6$ is correct in the environment $\Delta^{\prime}$. There is no second premise as there are no parameters to the defined constant $\texttt{formalprf}_6$.

---

Next we want to show that $\sum^{100}_{ i=0} (i) = 5050$ is $βδ$-equivalent to $a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050$. 

$$ a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050  \quad  \triangleq _ \beta \quad \sum ^{100}_{i=0}(    i)  = (λx : \mathbb{N} . x)5050 \quad \triangleq _ \beta \quad \sum ^{100}_{i=0}(i)  = 5050 $$

That is,

$$ a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050  \quad \triangleq_\beta \quad \sum ^n_{i=0}(f i)  = 5050  \tag{ii} $$

---

We need the (def) rule to build the required second premise for the (conv) rule.

$$ (\textit{def}) \quad \frac{ \Delta^{\prime};\emptyset \vdash (a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050) : *_p  \quad \quad  \Delta^{\prime};\emptyset \vdash \texttt{formalprf}_6 : \sum^{100}_{ i=0} (i) = 5050 }{ \Delta ; \emptyset ⊢ (a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050) : *_p} \tag{iii}$$

where $\Delta = \Delta^{\prime}, D_6$. The second premise is intuitively true, but can be justified by another application of the (inst) rule as follows:

$$ (\textit{inst}) \quad \frac{\Delta^{\prime} ; \emptyset \vdash *:\Box }{\Delta^{\prime}; \emptyset \vdash \texttt{formalprf}_6 : \sum^{100}_{ i=0} (i) = 5050} $$

There is no second premise as there are no parameters to the defined constant $\texttt{formalprf}_6$.

---

We can now use the (conv) rule using result (ii), and result (iii) as the second premise.

$$ (\textit{conv}) \quad \frac{ \Delta; \emptyset \vdash \texttt{formalprf}_6 : \sum^{100}_{ i=0} (i) = 5050 \quad \quad  \Delta ; ∅ ⊢ (a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050) : *_p } {\Delta ; ∅ ⊢ \texttt{formalprf}_6 : a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050}$$

---

We have derived the required conclusion.

$$\Delta ; ∅ ⊢ \texttt{formalprf}_6 : a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050 \tag*{$\Box$}$$

(b) TODO

Chapter 9 - Exercise 7

We call a definition $D$ correct in environment Δ if $\Delta,D; \emptyset ⊢ *: \Box$.

Consider $D_1$ to $D_6$ as in Exercise 9.6.

(a) On what condition can you derive that $D_1$ is correct in environment $\emptyset$?

(b) How do you prove that $D_2$ is correct in environment $D_1$?

(c) The same question for $D_3$ in environment $D_1,D_2$.

We remind ourselves of the (def) rule:

$$ \frac{ \Delta ; \Gamma \; \vdash \; K:L \quad \quad  \Delta; \bar{x}:\bar{A} \; \vdash \; M:N }{ \Delta,  \bar{x}:\bar{A} \triangleright a(\bar{x}) := M:N ; \Gamma \; \vdash \; K:L} \quad \text{ if } a \notin \Delta $$

We also remind ourselves of definitions $D_1$ to $D_6$:

$$\begin{align*} D_1 \; &≡ \; f : \mathbb{N} \to \mathbb{R}, \; n : \mathbb{N} \quad \triangleright \quad a_1(f,n) := \sum ^n_{i=0}(f i) : \mathbb{R} \\ \\ D_2 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R} \quad \triangleright \quad a_2(f,d) := \forall _{n:\mathbb{N}}(f (n+1)−f n= d) : *_p \\ \\ D_3 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\ & a_3(f,d,u,n) := \texttt{formalprf}_3 : f n= f 0 + n \cdot d \\ \\ D_4 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\ & a_4(f,d,u,n) := \texttt{formalprf}_4 : a_1(f, n) = \frac{1}{2} \cdot (n+1) \cdot (f 0 + f n)  \\ \\ D_5 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\  & a_5(f,d,u,n) := \texttt{formalprf}_5 : a_1(f,n) = (n+1) \cdot f 0+ \frac{1}{2}\cdot n \cdot (n+1) \cdot d \\ \\  D_6 \; & ≡ \; \emptyset \quad \triangleright \quad a_6 := \texttt{formalprf}_6 : \sum^{100}_{ I=0} (i) = 5050 \end{align*}$$

(a) Definition $D_1$ is correct in the empty environment $\emptyset$ if $D_1; \emptyset \vdash *: \Box$.

The (def) rule tells us the premises required to derive this.

$$ \frac{ \emptyset; \emptyset \; \vdash \; *:\Box \quad \quad  \emptyset; f : \mathbb{N} \to \mathbb{R}, \; n : \mathbb{N} \; \vdash \; \sum ^n_{i=0}(f i) : \mathbb{R} }{ \emptyset,  D_1 ; \emptyset \; \vdash \; *:\Box} $$

The first premise is simply the (sort) rule. The second premise requires the definition $D_1$ be well typed, that is, the definiens and its type can be derived from the context of the definition.

So the condition is that $D_1$ is well typed in the empty environment.

(b) Definition $D_2$ is correct in environment $D_1$ if $D_1, D_2 ; \emptyset \vdash *:\Box$. 

The (def) rule tells us the premises required to derive this.

$$ \frac{ D_1; \emptyset \; \vdash \; *:\Box \quad \quad  D_1; f : \mathbb{N} \to \mathbb{R},  d : \mathbb{R} \; \vdash \; \forall _{n:\mathbb{N}}(f (n+1)−f n= d) : *_p }{ D_1,  D_2 ; \emptyset \; \vdash \; *:\Box} $$

The first premise is the requirement that $D_1$ is correct in the empty environment, from part(a) above.

The second premise is the requirement that $D_2$ is well-formed in the environment $D_1$.

(c) Definition $D_3$ is correct in environment $D_1, D_2$ if $D_1, D_2, D_3; \emptyset \vdash *:\Box$. 

The (def) rule tells us the premises required to derive this.

$$ \frac{ D_1, D_2; \emptyset \; \vdash \; *:\Box \quad \quad  D_1, D_2; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \; \vdash \; \texttt{formalprf}_3 : f n= f 0 + n \cdot d }{ D_1,  D_2, D_3 ; \emptyset \; \vdash \; *:\Box} $$

The first premise is the requirement that $D_2$ is correct in the environment $D_1$. 

The second premise is the requirement that $D_3$ is well-formed in the environment $D_1, D_2$.

Chapter 9 - Exercise 6

Consider the following environment $\Delta$ consisting of six definitions, in which we use, for the sake of convenience, some well-known formats such as the $\Sigma$ and infix-notations:

$$ \begin{align} D_1 \; &≡ \; f : \mathbb{N} → \mathbb{R}, \; n : \mathbb{N} \quad \triangleright \quad a_1(f,n) := Σ^n_{i=0}(f i) : \mathbb{R} \\ \\ D_2 \; & ≡ \; f : \mathbb{N} →\mathbb{R}, \; d : \mathbb{R} \quad \triangleright \quad a_2(f,d) := \forall _{n:\mathbb{N}}(f (n+1)−f n= d) : ∗_p \\ \\ D_3 \; & ≡ \; f : \mathbb{N} →\mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\ & a_3(f,d,u,n) := \texttt{formalprf}_3 : f n= f 0 + n \cdot d \\ \\ D_4 \; & ≡ \; f : \mathbb{N} →\mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\ & a_4(f,d,u,n) := \texttt{formalprf}_4 : a_1(f, n) = \frac{1}{2} \cdot (n+1) \cdot (f 0 + f n)  \\ \\ D_5 \; & ≡ \; f : \mathbb{N} →\mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\  & a_5(f,d,u,n) := \texttt{formalprf}_5 : a_1(f,n) = (n+1) \cdot f 0+ \frac{1}{2}\cdot n \cdot (n+1) \cdot d \\ \\  D_6 \; & ≡ \; \emptyset \quad \triangleright \quad a_6 := \texttt{formalprf}_6 : \sum^{100}_{ I=0} (i) = 5050 \end{align} $$

Assume that $\texttt{formalprf}_3$ to $\texttt{formalprf}_6$ are meta-terms, standing for real proof terms.

(a) Rewrite this environment in flag format.

(b) What is a name used for $a_2$ in the standard literature?

(c) Find the δ-normal form with respect to $\Delta$ of $a_5(λx : \mathbb{N}. 2x,2,u,100)$, where $u$ is an inhabitant of $a_2(λx : \mathbb{N}. 2x,2)$.

(a) The following is the environment in flag format.

(b) $a_2$ defines an arithmetic progression, where $d$ is the common difference.

(c) The definition $D_5$ is

$$  a_5(f,d,u,n) := \texttt{formalprf}_5 : a_1(f,n) = (n+1) \cdot f 0+ \frac{1}{2}\cdot n \cdot (n+1) \cdot d  $$

This means $a_5(λx : \mathbb{N}. 2x,2,u,100)$ is

$$  a_5(λx : \mathbb{N}. 2x,2,u,100) := \texttt{formalprf}_5 : a_1(λx : \mathbb{N}. 2x,100) = (100 + 1) \cdot (λx : \mathbb{N}. 2x) 0+ \frac{1}{2}\cdot 100 \cdot (100 + 1) \cdot 2  $$

Continuing by unfolding $a_1$,

$$  a_5(λx : \mathbb{N}. 2x,2,u,100) := \texttt{formalprf}_5 :  \sum _{i=0}^{100}((λx : \mathbb{N}. 2x)i) = (100 + 1) \cdot (λx : \mathbb{N}. 2x) 0+ \frac{1}{2}\cdot 100 \cdot (100 + 1) \cdot 2  $$

The above is the δ-normal form. 

Out of interest we can continue to simplify,

$$  a_5(λx : \mathbb{N}. 2x,2,u,100) := \texttt{formalprf}_5 : \sum _{i=0}^{100}(2i) = 10100  $$

That is,

$$ \texttt{formalprf}_5 \; : \; \sum _{i=0}^{100}(2i) = 10100 $$

Chapter 9 - Exercise 5

Check that all instantiations of the parameters of constants defined and used in Exercise 8.2 satisfy the requirements imposed by the (inst)-rule.

The following is the text used in Exercise 8.2.

The following summarises the derivation rules for $\lambda D_0$.

The (inst)-rule ensures that the substituted expressions $\bar{U}$ are derivable in the environment and context $\Delta; \Gamma$.

There are only two instantiations in Exercise 8.2, at line (7) and (8). Let's consider each in turn.

(7) In defining $p_7$, the type $\textit{bounded-from-above}(S,p_6)$ has instantiated

• $V$ as $S$
• $u$ and $p_6$

in that order.

The (inst)-rule requires that we can derive $S:*_s$ in $\Delta; \Gamma$. Indeed, line (5) of the environment establishes $S$ with type $*_s$.

Next, the (inst)-rule requires that we can derive $p_6: V \subseteq \mathbb{R}[V:=S]$ which is $p_6:S \subseteq \mathbb{R}$. Line (6) of the environment establishes $p_6$ with type $S \subseteq \mathbb{R}$. 

And so the instantiations of $\textit{bounded-from-above}(S,p_6)$ satisfy the requirements of the (inst)-rule.

(8) In defining $p_8$, the type $\text{least-upper-bound}(S, p_6, 1)$ has instantiated

• $V$ as $S$
• $u$ as $p_6$
• $s$ as 1

in that order.

The (inst)-rule requires that we can derive $S:*_s$ in $\Delta; \Gamma$. Indeed, line (5) of the environment establishes $S$ with type $*_s$.

Next, the (inst)-rule requires that we can derive $p_6: V \subseteq \mathbb{R}[V:=S]$ which is $p_6:S \subseteq \mathbb{R}$. Line (6) of the environment establishes $p_6$ with type $S \subseteq \mathbb{R}$. 

Finally, the (inst)-rule requires that we can derive $1:\mathbb{R}[V:=S, u:=p_6]$  which is simply $1:\mathbb{R}$. Determining the type of 1 as $\mathbb{R}$ requires no further work.

And so the instantiations of $\textit{least-upper-bound}(S,p_6,1)$ satisfy the requirements of the (inst)-rule.

Chapter 9 - Exercise 4

This question has been updated by the errata.

See Section 9.6. Add the following definition to $(D_1) \ldots  (D4)$:

$$ (D_5) \quad x: \mathbb{Z}, y: \mathbb{Z} \triangleright d(x,y) := (x+ y)^2 $$

Let $\Delta  ≡D_1, \ldots ,D_5$. Give the full δ-reduction diagram of $d(a(u,v),b(w,w))$.

The following diagram illustrates the δ-reduction of $d(a(u,v),b(w,w))$.

(click to enlarge)

The final result is

$$ d(a(u,v), b(w,w)) \; \triangleq \; (u^2 + v^2 + 2 w^2)^2 $$

Chapter 9 - Exercise 3

The text in Exercise 8.2 contains eight new definitions. Let $Δ$ be the corresponding environment. Rewrite the type in line (8) in such a manner that all definitions of $Δ$ have been unfolded.

Let's remind ourselves of the text in Exercise 8.2

The type in line (8) is

$$\textit{least-upper-bound}(S, p_6, 1)$$

Using (3) we have

$$\textit{upper-bound}(S, p_6, 1) \;  \land \; \forall x:\mathbb{R}. (x < 1 \implies \neg \textit{upper-bound}(S, p_6, x))$$

Using (2) we have

$$ \forall x: \mathbb{R}.(x \in S \implies x \le 1) \;  \land \; \forall x:\mathbb{R}. (x < 1 \implies \neg \forall y: \mathbb{R}.(y \in S \implies y \le x)  )$$

Note the use of $y$ to avoid clashing with $x$.

Using $(5)$ we have

$$\begin{gather*} \forall x: \mathbb{R}.(x \in  \{z:\mathbb{R} \mid \exists n : \mathbb{R}.(n \in \mathbb{N} \land z=\frac{n}{n+1} ) \}  \implies x \le 1) \\ \\  \land \\ \\ \forall x:\mathbb{R}. (x < 1 \implies \neg \forall y: \mathbb{R}.(y \in \{z:\mathbb{R} \mid \exists n : \mathbb{R}.(n \in \mathbb{N} \land z=\frac{n}{n+1} ) \}  \implies y \le x)  ) \end{gather*}$$

Chapter 9 - Exercise 2

Consider the following two definitions, $D_i$ and $D_j$:

$ \bar{x} \; : \;  \bar{A} \;  \triangleright \; a(\bar{x}) \; := \; K : L$

$ \bar{y} \; : \;   \bar{B} \; \triangleright \; b(\bar{y}) \; := \; M : N$

Let $Δ ; Γ ⊢ U : V$ and assume that $D_i$ and $D_j$ are elements of the list $Δ$, where $D_i$ precedes $D_j$.

(a) Describe exactly where the constant $a$ may occur in $D_i$ and $D_j$.

(b) Describe where the constant $b$ may occur in $Δ$.

(a) Since $D_i$ defines the constant $a$, it can only occur once in $D_i$ at the position of the definiendum. It cannot occur in the definiens, because we don't allow self-referencing definitions, which means it is not in $K$ nor in $L$. It cannot occur in $\bar{x}$ because it hasn't been defined at this point. 

Since $D_j$ occurs after $D_i$, the constant $a$ can occur anywhere in $D_j$, except as the definiendum because we can't redefine the constant $a$. So $a$ can occur in $\bar{B}$, $M$ and $N$.

(b) The constant $b$ can only occur after it has been defined. So it cannot occur anywhere in $\Delta$ before $D_j$, and that means it cannot occur in $D_i$ which occurs before $D_j$.

Chapter 9 - Exercise 1

Consider the environment $Δ ≡ D_1,D_2, D_3, D_ 4$ of Section 9.6. Describe the dependencies between the four definitions and give all possible linearisations of the corresponding partial order.

Let's remind ourselves of the environment $\Delta$.

$ (D_1) \quad x : \mathbb{Z},y : \mathbb{Z} \quad \triangleright \quad a(x,y) := x^2 +y^2 \quad : \quad \mathbb{Z} $

$ (D_2) \quad x : \mathbb{Z},y : \mathbb{Z}  \mathbb{Z} \quad \triangleright \quad b(x,y) := 2·(x·y) \quad : \quad \mathbb{Z} $

$ (D_3) \quad x : \mathbb{Z},y : \mathbb{Z}  \mathbb{Z} \quad \triangleright \quad c(x,y) := a(x,y)+b(x,y) \quad : \quad \mathbb{Z} $

$ (D_4) \quad x : \mathbb{Z},y : \mathbb{Z}  \mathbb{Z} \quad \triangleright \quad \textit{lemma}(x,y) := c(x,y) = (x+y)^2 \quad : \quad ∗_p $

Here, $D_3$ depends on $D_1$ and also $D_2$. There is no relation between $D_1$ and $D_2$. Furthermore, $D_4$ depends only on $D_3$.

There are two possible linearisation of the partial order:

$$ D_1 \leftarrow D_2  \leftarrow D_3 \leftarrow D_4 $$

$$ D_2 \leftarrow D_1  \leftarrow D_3 \leftarrow D_4 $$