A much neglected mathematical object

A much neglected mathematical object

I had noticed that, for many years, about my only use of the notion of a function was via the Rule of Leibniz, viz. that we have for any $f,x,y$ of appropriately matching types

$x = y \Rightarrow {f}{1}x = {f}{1}y$

I also knew that the more formal expression of Leibniz's Latin phrase is probably

$x = y \equiv \left( {A{f}_{1} : f.x = f.y}\right)$

but did not feel that that gave me much more: $\Rightarrow$ follows from (a) and $\Leftrightarrow$ follows from the exist-

A few months ago I realized that equality of functions is usually expressed by stating that we have for any $g,h,x$ of appropriately matching types

$g = h \equiv \left( {\underline{A}x : g \cdot x = h \cdot x}\right)$

I could not help being struck by the symmetry between (1) and (2) in function and argument; it made me wonder to what extent the traditional distinction between function and argument is primarily a linguistic artefact. I was genuinely puzzled as no effort of mine at being more explicit about the appropriately matching

types succeeded in destroying the symmetry. In analogy to (o) I wrote down

$g = h \Rightarrow g.x = h.x,$

but this only underlines the symmetry: (0) and (3) present function application as equality-preserving in both respects.

Seeing how (1) follows from (0), we can deduce (2) from (3) with the aid of the so far neglected mathematical object: the identity argument i.

The introduction of the identity argument is indeed fully restores the symmetry between function and argument, but at the price mathe-maticians are traditionally unwilling to pay: the resulting theory only admits the trivial (i.e. one-point) model. The following argument is essentially due to Samson Abramsky. We have

(4) $I \cdot x = x\;f o r\;n a n y\;x$

(5) ${p}_{i} = p\;$ for any $p$ .

Define function $F$ by

(6) $F \cdot x = I$

Then we observe for any $x$

$$ = \begin{array}{l} x \ {4 } \ I. x \end{array} $$

$$ \begin{array}{l} = {(6) \mathrm {w i t h} x := i } \ (F, i), x \ = {(5) \mathrm {w i t h} f := F } \ \overline {{F}} \cdot x \ = {(6) } \ I \quad , \ \end{array} $$

hence $\left( {\underline{A}x : x = I}\right)$ and $\left( {\underline{A}x,y : x = y}\right)$ .

The $\lambda$ -calculus allows us to define -like in (4) and (6)- a function $F$ by

$$ F. x = a n e x p r i s s i o n t h a t m a y c o n t a i n x $$

(if not, as in (6), we define what is known in the Jargon as "a constant function").

The alternative is the permission to define -like in (5)- an argument $X$ by

$$ p _ {X} = a n e x p r e s s i o n t h a t m a y c o n t a i n p $$

(if not, we define what the jargon should call "a constant argument").

The combination of both freedoms is more than we care to live with.

Austin, 30 Aug. 1987

pror. dr. Edsger W. Dgksha

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712 - 1188, USA