ONT Re: Higher Order Categorical Logic
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 14
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| Historical Perspective on Part 1
|
| For the purpose of this discussion, it will suffice
| to define a 'cartesian closed category' as a category
| with an object 1 and operations (-) x (-) and (-)^(-)
| on objects satisfying conditions which assure that:
|
| 1. Hom(A, 1) ~=~ {*},
|
| 2. Hom(C, A x B) ~=~ Hom(C, A) x Hom(C, B),
|
| 3. Hom(A, C^B) ~=~ Hom(A x B, C).
|
| Here {*} is supposed a typical one-element set,
| chosen once and for all.
|
| It will be instructive to reverse the historical process
| and see how combinatory logic could have been discovered
| by rigorous application of Occam's razor.
|
| Condition 1 says that, for each object A, there is only
| one arrow A -> 1, hence we might as well forget about
| the object 1 and the arrow leading to it. However,
| the arrows 1 -> A must be preserved, let us call
| them 'entities of type A'.
|
| Condition 2 says that the arrows C -> A x B are in one-to-one
| correspondence with pairs of arrows C -> A and C -> B, hence
| we might as well forget about the arrows going into A x B.
|
| Condition 3 says that the arrows A x B -> C are in one-to-one
| correspondence with the arrows A -> C^B, hence we might as well
| forget about the arrows coming out of A x B too. Consequently,
| we might as well forget about A x B altogether.
|
| We end up with a category with a binary operation "exponentiation"
| on objects. Of course, this will have to satisfy some conditions,
| but these may be a little difficult to state. It is interesting
| to note that Eilenberg and Kelly went on a similar 'tour de force'
| and ended up with a category with exponentiation in which some
| monstrous diagrams had to commute.
|
| We may go a little further and forget about the category structure
| as well, since arrows A -> B are in one-to-one correspondence with
| entities of type B^A, which we shall write B <= A for typographical
| reasons. Composition of arrows is then represented by a single
| entity of type ((C <= A) <= (C <= B)) <= (B <= A). However, we
| do need a binary operation on entities called "application":
| given entities f of type B^A and a of type A, there is
| an entity f`a (read "f of a") of type B.
|
| We have now arrived at typed combinatory logic. But even this
| came rather late in the thinking of logicians, although type
| theory had already been introduced by Russell and Whitehead.
| Let us continue on our journey backwards in time and apply
| Occam's razor still further.
|
| An arrow A -> B in a category has a source A and a target B.
| But what if there is only one object? Such a category is called
| a monoid and, indeed, the original presentation of combinatory logic
| by Curry does describe a monoid with additional structure. (The binary
| operation of multiplication is defined in terms of the primitive operation
| of application.) Underlying untyped combinatory logic there is a tacit
| ontological assumption, namely that all entities are functions and
| that each function can be applied to any entity.
|
| To present the work of Schoenfinkel and Curry in the modern language of
| universal algebra, one should think of an algebra A = (|A|, `, I, K, S),
| where |A| is a set, (`) is a binary operation, and I, K, S are elements
| of |A|, or nullary operations. According to Schoenfinkel, these had to
| satisfy the following identities:
|
| I`a = a,
|
| (K`a)`b = a,
|
| ((S`f)`g)`c = (f`c)`(g`c),
|
| for all elements a, b, c, f, g in |A|. (Actually, he defined I in terms of
| K and S, but this is beside the point here.) The reader may think of I as the
| identity function and of K as the function which assigns to every entity a the
| function with constant value a. It is a bit more difficult to put S into words
| and we shall refrain from doing so.
|
| Schoenfinkel (1924) discovered a remarkable result, usually called
| "functional completeness". In modern terms this may be expressed
| as follows: Every polynomial !f!(x) in an indeterminate x over
| a Schoenfinkel algebra A can be written in the form f`x, where
| f is in |A|.
|
| From now on in our exposition,
| the arrow of time will point
| in its customary direction.
|
| L&S, pages 42-44.
|
| Lambek, J. & Scott, P.J.,
|'Introduction To Higher Order Categorical Logic',
| Cambridge University Press, Cambridge, UK, 1986.
|
| http://uk.cambridge.org/mathematics/catalogue/0521356539/
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤