ONT Re: Higher Order Categorical Logic
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 15
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Notation. The Greek letters phi and lambda
are represented as !f! and lam, respectively.
| Curry (1930) rediscovered Schoenfinkel's results, but went further in his
| thinking. He discovered that a finite set of additional identities would
| assure that the element f representing the polynomial !f!(x) was uniquely
| determined. We shall not reproduce these identities here, but reserve the
| name "Curry algebra" for a Schoenfinkel algebra which satisfies them.
|
| Using the terminology of Church (1941), one writes f as lam_x !f!(x),
| which must then satisfy two equations:
|
| beta. (lam_x !f!(x))`a = !f!(a),
|
| eta. lam_x (f`x) = f.
|
| (Many mathematicians write x ~> !f!(x) in place of lam_x !f!(x).)
|
| A lambda calculus is a formal language built up from variables x, y, z, ...
| by means of term forming operations (-)`(-) and lam_x (-), the latter
| being assumed to bind all free occurrences of the variable x occurring
| in (-), such that the two given identities hold. The basic entities
| I, K, S may then be defined formally by:
|
| I = lam_x x,
|
| K = lam_x lam_y x,
|
| S = lam_u lam_v lam_z ((u`z)`(v`z)).
|
| (Actually, Church would have called such a language
| a lambda-K-calculus and Curry might have called it
| a lambda-beta-eta-calculus, but never mind.)
|
| L&S, page 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/
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤