Typing functions

function The space of functions from type A to type B is denoted $A \rightarrow B$. The domaindomain type type is A, the rangerange type (or co-domain) is B. The typing rule for functions is intuitively simple. We say that $\lambda(x.\ b) \in A \rightarrow B$ provided that on each input $a \in A$, $ap(\lambda(x.\ b); a) \in B$. This judgment is usually made symbolically by assuming $x \in A$ and judging by typing rules that $b \in B$. This is the form of typing judgment we adopt. So the typing rule has the form

$\bar{H} \vdash \lambda(x.\ b) \in A \rightarrow B$ by fun_type

$\bar{H}, x\!:\!A \vdash b \in B$

More generally, given an expression f we allow

$\bar{H} \vdash f \in A \rightarrow B$ by fun_type

$\bar{H}, x\!:\!A \vdash ap(f; x) \in B$

In the course of judging that an expression t has a type T, we allow replacing t by any term t' that is definitionally equal or by a term t' that t evaluates to. So if t in T and $t \downarrow t'$, then $t \in T$. In the logic over $(A \rightarrow B)$ we add the rule for function equality

$\bar{H} \vdash f=g$ in $A \rightarrow B$ by extensional_equalityR

       $\bar{H}, x\!:\!A \vdash ap(f; x) = ap(g; x)$ in B

$\bar{H}, f = g$ in $A \rightarrow B \vdash ap(f; a) = ap(g; b)$ in B by extensional_equalityL

       $\vdash a \in A$

Here is Cantor's interesting argument about functions based on the method of diagonalizationdiagonalization. It illustrates the rules for functions. (See the appendix for a Nuprl proof.)

Definition 10   Call f in $(A \rightarrow B)$ onto iff $\exists g\!:\!(B \rightarrow A)$ such that $\forall y\!:\!B.\ f(g(y)) = y$ in B.

Cantor shows that for inhabited types A with two distinct elements there is no function from A onto $(A \rightarrow A)$--essentially because $(A \rightarrow A)$ is ``too big'' to be enumerated by A. We state the condition on A using functions. We require that there is a function $di\!f\!f\ \in A \rightarrow A$ such that $di\!f\!f(x) \neq x$ for all x in A. The theorem is

$\left(\exists\ di\!f\!f:\!(A \rightarrow A).\ \forall x\!:\!A.\ di\!f\!f(x) \ne... ...ow \left(\neg \exists e\!:\!A \rightarrow(A \rightarrow A).\ e\ is\ onto\right)$

1. $\exists\ di\!f\!f:(A \rightarrow A).\ \forall x\!:\!A.\ di\!f\!f(x) \neq x$ in A

2. $\exists e\!:\!A \rightarrow(A \rightarrow A).\ e$ is onto

$\vdash \perp$
Next use $\exists L$ on 2 THEN unfold ``onto'' THEN $\exists L$

2. $e\!:\!A \rightarrow(A\rightarrow A)$

3. $g\!:\!(A\rightarrow A) \rightarrow A$

4. $\forall h\!:\!(A \rightarrow A).\ e(g(h))=h$ in $(A \rightarrow A)$

Next $\exists L$ on 1 to replace 1 by 1.1 $di\!f\!f :\!A \rightarrow A$, 1.2 $\forall x\!:\!A.\ di\!f\!f(x) \neq x$ in A

Let $h_0==\lambda(x.\ di\!f\!f(e(x)(x)))$

Now $\forall L$ on 4 with h₀

5. e(g(h₀))=h₀ in $A \rightarrow A$

Let d==g(h₀), by $extensional\_equalityL$

6. e(d)(d)=h₀(d) in A

Now evaluate h₀(d) to rewrite 6 as

6. $e(d)(d)= di\!f\!f (e(d)(d))$

Now by $\forall L$ on 1.2 with e(d)(d)

7. $di\!f\!f (e(d)(d)) \neq e(d)(d)$ (which is $(di\!f\!f(e(d)(d))=e(d)(d)) \rightarrow \perp$)

$\vdash \perp$

Finish by $\Rightarrow\!\!L$ on 7 and 6. $\qed$