[
Date Prev][
Date Next][
Thread Prev][
Thread Next][
Date Index][
Thread Index]
Re: category theory <-> lambda calculus?
John Baez wrote:
> At some point Joachim Lambek realized that the lambda calculus was
> basically just another way of talking about cartesian closed categories.
> More precisely, if you ask in what sort of category you can do lambda
BTW, there is a neat "diagrammatic" exposition of lambda calculus at
http://www.uq.net.au/~zzdkeena/Lambda/
called:
>>>
To Dissect a Mockingbird:
A Graphical Notation for the Lambda Calculus with Animated Reduction
Abstract
The lambda calculus, and the closely related theory of combinators, are
important in the foundations of mathematics, logic and
computer science. This paper provides an informal and entertaining
introduction by means of an animated graphical notation.
<<<
It (naturally) represents lambda functions ("combinators") as machines
that have an input and an output
|
|
|
__/\__
| |
f = | f |
|_ __|
\/
|
|
|
but because of THE COOL FACT of lambda calulus, namely that the
application operator op() that applies a function on its argument
op()(f,x) = f(x)
is nothing but the *identity* operator
op() = \lambda f x . f x
(i.e. that functions and arguments are identified)
the only diagrammatic operations are "multiplexing" an input
|
|
|
/\
/ \
/ \
| |
| |
and "feeding one line into the other"
| | | |
| | | |
_|____|_ \ |
| | \ |
| op() | = \_/\
|_______| \/
| |
| |
| |
so that
f(x) =
f x f x
| | | |
| | | |
_|____|_ \ |
| | \ |
| op() | = \_/\
|_______| \/
| |
| |
| |
x
|
|
|
__/\__
| |
= | f |
|_ __|
\/
|
|
|
|
|
|
__/\__
| |
= | f(x)|
|_ __|
\/
|
|
|
For example, the diagrams of some commom combinators are
I = \lambda x . x =
|
|
|
__/|\__
| | |
| | |
|_ | _|
\|/
|
|
|
K = \lambda x y . y =
|
|
|
__/ \__
| __ |
| |I| |
| \/ |
|_ | __|
\|/
|
|
|
=
|
|
|
______/\_______
| |
| |
| |
| | |
| | |
| | |
| __/|\__ |
| | | | |
| | | | |
| |_ | _| |
| \|/ |
| | |
| | |
|_____ | ______|
\|/
|
|
and last not least, the first really interesting one:
S = \lambda x y z . x(z)(y(z)) =
| | |
| | |
| | |
| ____|_____/|
| | | |
| | | |
|__/\ |______/\
\/ \/
| |
\ |
\ |
\________/\
\/
|
|
|
To see lambda reduction at work in this framework please refer to the
above mentioned URL, I will not do that in ASCII. It's pretty cool how
one ends up with "movies" of functions that feed on each other, mutate,
pop out of each other, etc.
The diagrammatic reasoning here is somewhat different from that
presented in John Baez' quantum gravity seminar, but it is also somewhat
similar. In fact, it makes me wonder even more if there is a connection
to omega-categories: The above does not really work in typed lambda
calculus (there one would have to unnaturally decide and keep track of
which diagrams were allowed to be connected to each other) so it does
not work in cartesian closed categories.
But the central diagram
| |
| |
\ |
\ |
\_/\
\/
|
|
|
which in essence converts an object to a morphism (a line to a vertex)
should also play a role in omega-categories, shouldn't it?
Urs Schreiber
--
eMail: Urs.Schreiber@uni-essen.de