An example of how to lengthen formal proofs

An example of how to lengthen formal proofs

for invertible $t$ of the proper type

$$ [ (\underline {{A}} x:: f. x) \equiv (\underline {{A}} x:: f. (4. x)) ] $$

The proof is by proving first (0), and then (1), with

$\left\lbrack {\left( {\underline{A} \times :}{f}{1} \times }\right) \Rightarrow \left( {\underline{A} \times :}{f}{1}\left( {+,x}\right) }\right) }\right\rbrack$ $\left\lbrack {\left( {\underline{A} \times :}{f}{1} \times }\right) \Leftarrow \left( {\underline{A} \times :{f}{1}\left( {t \cdot x}\right) }\right) }\right\rbrack$

The proof of (0) is

(0)

$$ \begin{array}{l} = {Q \Rightarrow d i s t r i b u t e s o v e r A } \ [ (\underline {{A}} x:: (\underline {{A}} x:: f. x) \Rightarrow f. (f. x)) ] \ = {\text {i n s t a n t i a t i o n}: x := t, x } \ [ (A x::: t r u e ] \ = {\mathrm {p r e d . c a l c .} } \ \mathrm {t r u e} \ \end{array} $$

a proof with which I have no quarrel. Its independ- dence of t's invertibility justifies a proof by mutual implication.

To prove now (1), one can proceed as follows

$$ \begin{array}{l} (\underline {{A}} x: f. (+, x)) \ = {\mathrm {d e f i n i t i o n o f f u n c t i o n a l c o m p o s i t i o n} } \ (\exists x: \cdot : (f o t). x) \ \Rightarrow {0) w i t h f, + := (p o t), t ^ {- 1} } \ (\underline {{A}} x: \quad (f o t). (t ^ {- 1}: x)) \ \end{array} $$

$$ \begin{array}{l} = {\mathrm {d e f i n i t i o n o f f u n c t i o n a l c o m p o s i t i o n} } \ (\underline {{A}} x: ((f o t) \circ f ^ {- 1}). x) \ = {\circ \mathrm {i s a s s o c i a t i v e} } \ \underline {{A}} x: \left(f _ {0} (t o t ^ {- 1})\right). x) \ = {\mathrm {t o t} ^ {- 1} \mathrm {i s t h e i d e n t i l y f u n c t i o n} } \ (\underline {{A}} x: f. x) \ \end{array} $$

The above is an exaggeration of a proof. Carel S. Scholten and I included in our book. What about

$$ \begin{array}{l} (\underline {{A}} x: f. (+, \times)) \ \Rightarrow \quad {(0) \mathrm {w i t h} + := t ^ {- 1} } \ (\underline {{A}} x: f. (f. (f ^ {- 1} x))) \ = {+ (t ^ {- 1} x) = x } \ (\underline {{A}} x:: f. x) \quad ? \ \end{array} $$

The first proof introduces tot as the identity element of functional composition, whereas in the last hint of the second proof -which is equivalent with ${\left( \operatorname{tot}{}^{-1}\right) }{\cdot }\mathrm{x} = \mathrm{x} - {\operatorname{tot}}^{-1}$ is not functionally composed but applied. Why did functional composition enter the first proof in the first place? Obviously, to be able to indicate ex- plicitly in the instantiation of (o) ${f}{ : } = \left( {f}{0t}\right)$ . If we so desired, this could also be achieved by ${f}{ : } = \left( {\lambda x : f\left( {t.x}\right) }\right)$ ,but this,too,now strikes me as unnecessarily pompous. You see, I am also willing to read (o) as: "A universal quan- tification is not strengthened by replacing in the

term the dummy by a function of it." In apply- in this to $(\underline{\underline{A}} x::f(t.x))$ the dummy is well- identified -viz. $x-$ , and so is the term -viz. $f(t.x)$ . In order to perform the nonstrengthening transformation without look-ahead and pattern matching, we only need to know which function to apply to the dummy, and that is precisely the information the hint $t:=t^{-1}$ supplies. So I think that the first hint of the last proof suffices.

We could have continued our second proof with

$$ \begin{array}{l} (\underline {{\underline {{\mathrm {日}}}}} x: \mathcal {P} (t, (t ^ {- 1} x))) \ = {\mathrm {d e f . o p f u n c t i o n a l c o m p o s i t i o n} } \ (\underline {{A}} x: \because f. ((t o t ^ {- 1}). x)) \ = {\mathrm {t o t} ^ {- 1} i s \mathrm {t h e i d e n t i h y f u n c t i o n} } \ \end{array} $$

$$ (\underline {{A}} \times : f. \times) $$

but, again, the explicit introduction of functional composition is no improvement.

Austin, 8 October 1989

prof. dr. Edsger W. Dgksta Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188

USA