CCCs and the λ-calculus

August 28, 2006

Posted by John Baez

$MathML-enabled post (click for more details).$

This blog entry is an excuse for continuing our discussion of cartesian closed categories (CCCs) and the λ-calculus in a slightly more organized way. Let’s focus on more or less “traditional” aspects here. If you prefer to talk about categorified or quantized versions of CCCs and the λ-calculus, go to the relevant entry and talk there.

To kick off the discussion, let’s start with a sketchy and highly oversimplified history of CCCs and the λ-calculus.

$MathML-enabled post (click for more details).$

Categorical semantics was born in Lawvere’s celebrated 1963 thesis on algebraic theories:

F. William Lawvere, Functorial Semantics of Algebraic Theories.

Algebraic theories are a simple formalism for reasoning about operations that satisfy equations. For example, since the concept of a “group” involves only some operations (multiplication, inverses…) satisfying equations, this concept can be formalized using an algebraic theory called $Th(Grp)$ .

The role of semantics enters when we consider “models” of an algebraic theory. Loosely speaking, a model is just one of the things the theory seeks to describe. For example, a “model” of $Th(Grp)$ is just a group. Technically, an algebraic theory $T$ is a category with finite products, and a model is a functor that preserves finite products: $Z: T \to Set$ from $T$ to the category of sets. The basic idea is simple: if for example $T = Th(Grp)$ , then $Z$ maps the abstract concept of “group” to a specific set, the abstract concept of “multiplication” to a specific multiplication on the chosen set, and so on, thus picking out a specific group.

Dual to the concept of semantics is the concept of syntax, which deals with symbol manipulation. Just as semantics deals with models, syntax deals with “proofs”. For example, starting from $Th(Grp)$ we can prove consequences of the group axioms merely by juggling equations. In the case of algebraic theories, the syntax often goes by the name of universal algebra:

Stanley Burris and H.P. Sankappanavar, A Course in Universal Algebra.

In fact, universal algebra was around long before Lawvere introduced algebraic theories; he just modernized it with the realization that a model was a functor - hence his thesis title, “Functorial Semantics”.

The relevance of all this to computer science becomes visible when we note that a proof in $Th(Grp)$ , or indeed in any algebraic theory, can be seen as a rudimentary form of computation. The “input” of the computation is a set of assumptions, while the “output” is the equation to be proved.

Treating proofs as computations may seem strained, but it becomes less so when we move to richer formalisms which allow for more complex logical reasoning. One of the most well-known is the lambda calculus, invented by Church and Kleene in the 1930s as a model of computation. Any function computable by the lambda calculus is also computable by a Turing machine, and according to the Church-Turing thesis these are all the functions computable by any sort of systematic process. Moreover, computations in the lambda calculus can actually be seen as proofs.

The aptness of this way of thinking was brought out in Landin’s classic paper

P. Landin, A correspondence between ALGOL 60 and Church’s lambda-notation, Comm. ACM 8 (1965), 89-101, 158-165.

This began a long and fruitful line of research - see for example this:

H. Barendregt, The Lambda Calculus, its Syntax and Semantics, North-Holland, 1984.

The power of the lambda calculus is evident in the textbook developed for MIT’s introductory course in computer science, which is available online:

H. Abelson, G. J. Sussman and J. Sussman, Structure and Interpretation of Computer Programs.

It cites pioneers like Haskell Curry, and it even has a big λ on the cover!

Fans of Oz and the Wizard will be pleased to hear that students call it “the wizard book”, for the obvious reason. It’s used at over 100 colleges and universities, and it has spawned a secret society called The Knights of the Lambda Calculus, whose emblem celebrates the ability of the λ-calculus to do recursion:

lambda

In 1980, Lambek made a great discovery:

Joachim Lambek, From lambda calculus to Cartesian closed categories, in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, eds. J. P. Seldin and J. Hindley, Academic Press, 1980, pp. 376-402.

He showed that just as algebraic theories can be regarded as certain special categories, so can theories formulated in the lambda calculus: to be precise, these correspond to cartesian closed categories or CCCs for short. These are categories with finite products such that the operation

$a \mapsto x \times a$

has a right adjoint, the internal hom

$b \mapsto hom(x,b)$

In other words, we have a natural isomorphism

$HOM(x \times a, b) \cong HOM(a,hom(x,b))$

Here HOM denotes the usual set of morphisms from one object to another, while hom is the “internal hom”, which is itself an object in our category. If this is befuddling, take our category to be Set and take HOM = hom; then the above equation says:

“a function from $x \times a$ to $b$ is the same as a function from $x$ to the set of functions from $a$ to $b$ .”

CCC’s just generalize this idea to other categories!

Lambek’s discovery introduced a semantics for the lambda calculus, since it lets us to speak of “models” of theories formulated in the lambda calculus: $Z: T \to Set$ just as we could for algebraic theories. These are again just functors that preserve finite products. In computer programming, the importance of a model is that it gives a picture of what a program actually accomplishes. A model Z sends any program to an actual function between sets.

There’s no way to list all the interesting references to CCCs and the λ-calculus, but here are some great online places to get started, starting out easy and working up to the harder ones:

Mark Chu-Carroll, Lambda calculus.
Mark Chu-Carroll, Category theory.
Peter Selinger, Lecture notes on the lambda calculus.
Phil Scott, Some aspects of categories in computer science.

and here’s a classic:

Joachim Lambek and Phil J. Scott, Introduction to Higher Order Categorical Logic, volume 7 of Cambridge Studies in Advanced Mathematics, Cambridge U. Press, 1986.

Here are some things I’d like to talk about more:

How do we describe the untyped λ-calculus as a CCC? I hear we just take the free CCC on one object, which I now call CCC[x], and throw in an isomorphism $x \cong hom(x,x)$ Is this enough to make all objects isomorphic, as I’d expect in an untyped world? How do we get an isomorphism $x \times x \cong x$ ? By adjointness we get a morphism $x \times x \to x$ , but why is it an iso?
What’s PCF? It’s a theory formulated in the lambda calculus; the acronym stands for “programming with computable functions”? Robin Houston says: “For anyone who’s unused to the jargon, PCF is simply typed λ-calculus with integers and booleans as base types, extended with primitives for arithmetic and recursion. It’s possibly the simplest typed language that is Turing complete.” You can read the precise definition in Selinger’s notes. But, I’d like to know more! For example, I’d like a description of the CCC corresponding to PCF. Something like “the free CCC containing a natural numbers object, a truth values object and….”
Games and the free cartesian closed category on one object. James Dolan has a description of objects in CCC[x] as games, and morphisms as strategies of a certain funny sort where you can “take back” moves. Daniel Steffen has written about this, but I don’t know how to obtain his work. It would be great if we could coax either of these guys to explain this stuff here.

Okay - enough of this blogorrhea. Someone else say something!

Posted at August 28, 2006 3:19 AM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/908

35 Comments & 1 Trackback

Read the post Categories and computation
Weblog: The n-Category Café
Excerpt: What's the relation between the lambda-calculus, computation and CCCs?
Tracked: August 28, 2006 8:32 AM

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

Over in the original comment thread I tried to understand something John said about natural numbers in terms of models of CCCs.

I’ll try to summarize.

Any CCC $C$ has a canonical model $\mathrm{El} : C \to \mathrm{Set}$ which sends every object $x$ of $C$ to the set $\mathrm{El}(x)$ of morphisms $(1 \to x) \in \mathrm{Hom}_C(1,x)$ .

Denoting internal Hom-objects by the lower case $\mathrm{hom}(x,y) \in \mathrm{Obj}(C)$ , the claim is that for $C$ the free CCC on the single object $x$ we find that

(1)

\mathrm{El} ( \mathrm{hom}( \mathrm{hom}(x,x), \mathrm{hom}(x,x) ) )

is (isomorphic to) the set of natural numbers.

In order to follow this one has to know that in the free CCC $C$ , we have precisely no morphism $1 \to x$ .

Hence $\mathrm{El}(x) = \{\}$ is the empty set.

On the other hand, $\mathrm{Hom}( \mathrm{hom}(x,x), \mathrm{hom}(x,x) )$ contains $\mathbb{N}$ -worth of morphisms, each of which representing the idea of taking an endomorphism $f$ of $x$ and taking it to the $n$ th power, for $n$ some natural number.

I assume this means now that there are also $\mathbb{N}$ -worth of morphisms $1 \to \mathrm{hom}( \mathrm{hom}(x,x), \mathrm{hom}(x,x) )$ . If so, then, by definition, applying $\mathrm{El}$ to this latter expression produces a set with the cardinality of the natural numbers.

This is slightly counterintuitive in light of the fact that $\mathrm{Hom}(\mathrm{El}(x),\mathrm{El}(x))$ contains just a single element, namely the identity on the empty set.

But, after all, we are dealing with internal $\mathrm{hom}$ s, so I am prepared to accept that slightly counterintuitive things may happen.

Hence I was about to say “ok, thanks, now I understand”. But unfortunately I am still confused!

Namely next, John says, we want to pass from the free CCC on $x$ to the category obtained from it by adding lots of isomorphisms, like $x \simeq \mathrm{hom}(x,x)$ .

But this immediately implies that

(2)

\mathrm{El}(\mathrm{hom}(x,x)) = \{\}

is also the empty set!

Not sure if this is troublesome, but naïvely one tends to deduce from this that

(3)

\mathrm{hom}(\mathrm{hom}(x,x),\mathrm{hom}(x,x)) \simeq \mathrm{hom}(x,x) \simeq x \,.

I hope the first step is unjustified, because otherwise, applying $\mathrm{El}$ to this chain of isomorphisms, one finds that there is no natural number at all.

This really confuses me, because from what John said here it sounded like we do want to have all those isomorphisms present.

Personally, it seems to me that we do not want to consider the model $\mathrm{El}$ when thinking about $\lambda$ -calculus. After all, we know that we want a model $N$ of our CCC such that $N(x)$ is the set of $\lambda$ -expressions, not the empty set.

No?

Posted by: urs on August 28, 2006 11:28 AM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

Thanks for re-raising this question in the right location, Urs. I wasn’t trying to duck out of it by closing off comments on the old entry. Honest. $rolleyes$

We’re talking about the free CCC on one object $x$ , which I’ve taken to calling $CCC[x]$ . If we can’t figure out what this is like, we don’t understand CCCs!

So, let’s try to figure out how many morphisms of the form

$f: hom(x,x) \to hom(x,x)$

this category has. Using some heuristic reasoning, I claim there’s one for each natural number. I think various people like James Dolan and maybe Robin Houston and H. Schwichtenberg agree with me - the last guy being the author of this:

H. Schwichtenberg: Functions definable in the simply-typed lambda calculus, Arch. Math Logik 17 (1976), 113-114

which I’ve really got to read sometime.

Urs, on the other hand, has a heuristic argument saying there’s just one morphism

$f: hom(x,x) \to hom(x,x)$

in $CCC[x]$ . And, he’s beginning to unnerve me by repeating this argument so persistently.

Why doesn’t he just knuckle under, with such an array of authorities lined up against him?

It’s good he’s not knuckling under. We should just try to figure this out from scratch - starting from the fact that $CCC[x]$ is the free CCC on one object.

What does this mean? Well, it means that if $A$ is any CCC containing an object $a$ , there is a unique morphism of CCCs

$Z: CCC[x] \to A$

with $Z(x) = a$ . More precisely: unique up to natural isomorphism.

But this opens a can of worms we’ve already seen: what’s a morphism of CCCs? I said this question is separate from the one we’re trying to answer now, but that was dumb. We need to choose a definition of “morphism of CCCs” before we can tell what free CCCs are like!

Urs might like the definition where a morphism of CCCs preserves finite products and internal homs up to isomorphism. That definition might even let him win this argument. So, I’ll choose the other definition, where a morphism of CCCs only needs to preserve finite products.

(I’m not really choosing this just to win the argument. Honest. I explained a while back why I want this: the other definition forces CCC morphisms to be full and faithful, which is very restrictive.)

Okay, so suppose $CCC[x]$ is free in this sense: for any object $a$ in $A$ there exists a unique-up-to-isomorphism finite-product-preserving functor

$Z: CCC[x] \to A$

sending $x$ to $a$ . Let’s try to use this to count the morphisms

$f: hom(x,x) \to hom(x,x)$

If I can show there are at least two, I bet Urs will agree there’s one for each natural number. First, we have the identity morphism - on that we all agree. Second, I claim there is a morphism called “squaring”. To define this, we first duplicate

$\Delta : hom(x,x) \to hom(x,x) \times hom(x,x)$

and then compose

$\circ: hom(x,x) \times hom(x,x) \to hom(x,x)$

I think Urs will agree that “squaring” exists; he just claims it’s the same as the identity!

But, it can’t be. After all, over in $A$ we have the identity and squaring as morphisms

$hom(a,a) \to hom(a,a)$

and for most $A$ they aren’t the same. But that means they can’t be the same in $CCC[x]$ . After all, if they were the same in $CCC[x]$ , we could apply $Z$ and see they’re the same in $A$ !

(Note here we use the fact that $Z$ preserves finite products. Check that I’m not cheating.)

I think that does the job. The moral is definable quantities that are different in general must be different in the free example.

Urs has other questions, but first let’s see if we agree on this.

Posted by: John Baez on August 28, 2006 12:13 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

Urs, on the other hand, has a heuristic argument saying there’s just one morphism $f : \mathrm{hom}(x,x) \to \mathrm{hom}(x,x)$ in $\mathrm{CCC}[x]$ .

Sorry, no!

I never ever doubted that there is one morphism $\mathrm{hom}(x,x) \to \mathrm{hom}(x,x)$ per natural number in $\mathrm{CCC}[x]$ . Not since Robin told me that this is so.

Instead, I expressed worries about what happens to all these morphism under the map $\mathrm{El}$ which you were looking at.

I was almost about to thank you all for your explanations (which of course I do nevertheless :-) and declare that finally I understand what you were all trying to tell me, when I discovered that I still see a problem.

In my latest comment I have an argument that applying your model $\mathrm{El}$ to the category obtained by adding to $\mathrm{CCC}[x]$ isomorphisms like $x \simeq \mathrm{hom}(x,x)$ will necessarily make $\mathrm{El}$ forget that all these morphisms are different.

But this argument relied on a guess, namely that you would want to impose the isomorphism

(1)

\mathrm{hom}(\mathrm{hom}(x,x),\mathrm{hom}(x,x)) \simeq \mathrm{hom}(x,x) \,.

I think it is obvious that imposing this together with $\mathrm{El}(x) = \{\}$ makes things go wrong.

Do we really want our model to send $x$ to the empty set??

Posted by: urs on August 28, 2006 12:51 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

John wrote:

Urs, on the other hand, has a heuristic argument saying there’s just one morphism $f:hom(x,x) \to hom(x,x)$ in CCC[x].

Urs wrote:

Sorry, no! I never ever doubted that there is one morphism $hom(x,x) \to hom(x,x)$ per natural number in CCC[x]. Not since Robin told me that this is so.

Whoops! That’s embarrassing - I’d gotten so involved thinking about how to rigorously prove all these morphisms from $hom(x,x)$ to itself are different, that I didn’t notice you were no longer arguing the other way. Anyway, I had fun arguing with this imaginary opponent that I thought was you.

Instead, I expressed worries about what happens to all these morphisms under the map El which you were looking at.

Okay. We can just work that out. An element of

$hom(hom(x,x),hom(x,x))$

is by definition a morphism

$1 \to hom(hom(x,x),hom(x,x))$

Since the internal hom is adjoint to the product, such morphisms are in 1-1 correspondence with morphisms

$1 \times hom(x,x) \to hom(x,x)$

or in other words, morphisms

$hom(x,x) \to hom(x,x)$

So, you must believe that there is one element of $hom(hom(x,x),hom(x,x))$ per natural number. In other words,

$El((hom(x,x),hom(x,x))) \cong \mathbb{N}$

as monoids. So, that’s what $El$ does here.

But in fact, maybe this isn’t what you’re really worrying about now!

In my latest comment I have an argument the applying your model El to the category obtained by adding to $CCC[x]$ isomorphisms like $x \cong hom(x,x)$ will necessarily make El forget that all these morphisms are different.

I didn’t want to get into this until we saw eye-to-eye on the preliminary issues. I feel I understand the typed lambda calculus with one generating type $x$ ; this corresponds to $CCC[x]$ . I don’t feel I understand the very famous “untyped” lambda calculus, which may correspond to some CCC with only one object, since “types” are objects. And that’s what we’re talking about now. So, don’t trust anything I say!

Maybe the untyped lambda calculus doesn’t correspond to any CCC. But if it does, and if it corresponds to a CCC with just one object, it’s likely to be some “quotient” of $CCC[x]$ . To get such a quotient, my first idea was to throw in an isomorphism between any two objects of $CCC[x]$ . But then we’d need to worry about which diagrams commute! Robin Houston, who actually knows something about this stuff, suggested that we just throw in one isomorphism,

$x \cong hom(x,x).$

This reminds me of some famous stuff Dana Scott did, but I don’t see how it gives us an isomorphism

$x \cong x \times x$

so I’m puzzled. Maybe we don’t really want $x \cong x \times x$ in the so-called “untyped” lambda calculus?

So, all this is much more mysterious to me than $CCC[x]$ . But, I can try to study the quotient

$CCC[x]/\langle x \cong hom(x,x)\rangle$

and work out the elements of various objects. You seem to believe that since $x$ has no elements in $CCC[x]$ , and now we’re making it isomorphic to

$hom(x,x)$

it follows that now $hom(x,x)$ has no elements in the quotient

$CCC[x]/\langle x \cong hom(x,x)\rangle$

But that’s not obvious to me. Why can’t we just turn the argument around, and say that now $x$ has at least one element in the quotient? This seems just as likely to me.

We’d have to actually work it out. We’d take CCC[x], throw in a new isomorphism

$\alpha: x \cong hom(x,x),$

let it generate a new CCC, and see if this created more elements

$1 \to x$

than there used to be, or fewer elements

$1 \to hom(x,x)$

than there used to be. It’s easy to get more elements since we’re throwing in new morphisms. To get fewer elements, you need to get equations between the ones you had.

Posted by: John Baez on August 28, 2006 2:33 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

Thanks for your reply! Yes, that clarifies it. Great. Now I feel like I understand what is going on.

Posted by: urs on August 28, 2006 4:00 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

Maybe we don’t really want x≅x×x in the so-called “untyped” lambda calculus?

I have no idea, but it’s conceivable to me that it has to do with parallel execution: when evaluating the pair, you have to choose a morphism to evaluate first; if the first one evaluates to $\Omega$ , then the second never gets evaluated, and thus the two terms might not be isomorphic.

On the other hand, one can certainly simulate parallel execution in a UTM—that’s integral to lots of proofs in algorithmic number theory.

Posted by: Mike on August 28, 2006 6:13 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

I live in fear that a real expert is going to show up here, and unmask me for the amateur that I am. But that fear isn’t strong enough to shut me up, I’m afraid. :-)

One thing we certainly don’t want is a CCC with one object, for the silly and pedantic reason that a CCC has a terminal object, so a CCC with one object will consist of just the terminal object, and be trivial.

So what about a CCC with two objects? That way we have one terminal object and one intereting one. To give such a thing is just to give a CCC with an object X and isomorphisms $X\cong X\times X\cong$ X^X. (Take the full subcategory consisting of X and 1.)

Categories of this sort provides models for untyped lambda-calculus with surjective pairing. That’s the system you get when you explicitly augment the lambda calculus with some syntax for pairing two terms, and for selecting one element or the other from a pair. These new operations need to have some associated reduction rules of course, and the appropriate choice (in view of the category theory at least) is something like

$\pi$ ₁ $\langle A,B \rangle \to A$
$\pi$ ₂ $\langle A,B \rangle \to B$
$\langle\pi$ ₁ X, $\pi$ ₂ $X\rangle \to X$

But there’s no way to define a surjective pairing operation in plain lambda-calculus, so we shouldn’t force $X\cong X\times X$ in its models.

If you know a bit about the lambda-calculus, you’ll know that we can define a pairing operation like this:

$\langle A,B\rangle$ := $\lambda f.$ f A B
$\pi$ ₁(P) := P ( $\lambda a,b.$ a)
$\pi$ ₂(P) := P ( $\lambda a,b.$ b)

(That’s one of the essential tricks of the trade for untyped lambda calculists.) But this doesn’t contradict what I’ve just said, because with this pairing isn’t surjective: with these definitions it’s not generally true for any term Z that

$\langle\pi$ ₁ Z, $\pi$ ₂ $Z\rangle$

is $\beta\eta$ -equivalent to Z.

Posted by: Robin on August 28, 2006 7:38 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

No expert either, but I think you might like Bart Jacobs’ old paper on this:

B. Jacobs, Simply Typed and Untyped Lambda Calculus Revisited. In: M.P. Fourman, P.T. Johnstone and A.M. Pitts (eds.) Applications of Category Theory in Computer Science (LMS 177, Camb. Univ. Press, 1992), 119 - 142.

or the corresponding chapter 2 in his later book, especially Section 2.5:

B. Jacobs, Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics 141, North Holland, Elsevier, 1999.

or this summary, which has the advantage of being available on the web.

The idea is to use a trick from the original functorial semantics, which works both for the typed and untyped cases: the category of contexts and substitutions does have finite products, so you may take it as a reasonable classifying category. But in which space does it live?

B. Jacobs sets up the notion of context-type structure (CT-structure for short). Briefly, this is a category $B$ with finite products, together with a distinguished subset $T$ of its objects called the types. Then the simple fibration of such a CT-structure is defined by:

Objects: the pairs $(I, X)$ , where $I$ is any object and $X$ is a type,
Morphisms $(I, X) \to (J, Y)$ : the pairs $(u: I \to J, f: I \times X \to Y)$ ,
Composition: $(u, f) (v, g) = (u v, \langle \pi_1 u , f\rangle g)$ ,

with the obvious functor to $B$ .

Finally, this fibration has simple T-products if the weakening functors for types (i.e., the weakening functors from the fibre over some $I$ to the fibre over $I \times X$ for some type $X$ , as opposed to arbitrary $J$ ’s) have right adjoints.

This then allows to state that the $\lambda$ -calculus lives in the category of non-trivial CT-structures whose simple fibration has simple T-products.

That’s it. Don’t really know what to think of it, not sure it definitely illuminates the whole.

Posted by: Tom Hirschowitz on August 29, 2006 2:26 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

Could an expert, eg Robin Houston, please update me on the quest for a semantics of concurrency?

The problem, as I remember studying it 8 years ago, was that there were many possible semantics for different parallel process calculi, but that none were canonical in the same way as the categorical semantic for the lamda-calculus. Is this the reason no-one has settled on, eg, the pi-calculus, as canonical like the lambda-calculus?

Whenever I used to think about this, it would leave me with the impression that there always some extra feature one could add to your process calculus “from the real world” that would confound your attempts to provide a general-purpose semantics. This “something extra” never seemed to be a problem in the serial lambda-calculus world.

(apologies for the non-expert, CS-groupie question; please feel free to update me on the status of other fields, such as linear logic, and Girad’s geometry of interaction; many thanks!)

Posted by: Allan Erskine on August 29, 2006 4:41 AM | Permalink | Reply to this

Re: CCCs and the λ-calculus

Allan: I’m afraid I know terrifyingly little about the semantics of concurrency, so you won’t get an expert answer from me.

That said, I don’t think the situation has fundamentally changed in the past eight years, and I get the impression that the field is still rather fragmented and tends to trade in isolated insights rather than unified theories. On a positive note, some effort is being made to change that.

Posted by: Robin on August 29, 2006 12:27 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

I’m trying to get a CCC that corresponds perfectly to the syntax of the untyped lambda calculus….

Robin wrote:

One thing we certainly don’t want is a CCC with one object, for the silly and pedantic reason that a CCC has a terminal object, so a CCC with object will consist of just the terminal object, and be trivial.

Whoops! Yes, that would be taking the “untyped” idea a wee bit too far. $rolleyes$

So what about a CCC with two objects? That way we have one terminal object and one interesting one. To give such a thing is just to give a CCC with an object X and isomorphisms $X \cong X \times X \cong X^X$ . (Take the full subcategory consisting of X and 1.)
Categories of this sort provides models for untyped lambda-calculus with surjective pairing.

That’s interesting - but what I’ve been after all along, in my blundering way, is simply to understand what CCC corresponds to the ordinary untyped lambda-calculus, with no further bells and whistles. In other words: I want a CCC containing an object $x$ , such that morphisms from $x$ to $x$ are precisely lambda-terms. And, I want to describe this CCC in terms of the free CCC on one object! I want to say “it’s the free CCC on one object $x$ equipped with isomorphisms….”

At first, I had naively thought “untyped” meant there was just one type - namely, all objects (or at least most of them) were isomorphic, so you could apply any one as an operation to any other. That’s why I was trying to throw in enough isomorphisms to make all objects isomorphic.

But, you seem to be hinting strongly (though never quite saying!) that we should just take the free CCC on one object and throw in an isomorphism

$x \cong hom(x,x),$

accepting the fact that this doesn’t make $x \cong x \times x$ . Is this true? Is the CCC I’m looking for

$CCC[x]/\langle x \cong hom(x,x) \rangle ?$

It also sounds like you’re saying that if we want to go further and get the CCC corresponding to “the lambda-calculus with a surjective pairing”, we should also throw in an isomorphism . This will make all objects isomorphic except $1$ . (Hey, a pun!)

This extra refinement is far less interesting to me, but it’s still really interesting, so I’ll ask a subsidiary question. Do we demand any coherence laws on this extra isomorphism $x \cong x \times x$ or not? I bet not.

Posted by: John Baez on August 30, 2006 4:11 AM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

As said here and there, it seems the (typed or untyped) $\lambda$ -calculus may not directly be seen as a CCC. Instead, following Lawvere’s old idea, its category of contexts (in the untyped case, something like finite lists of pairwise distinct variables) and substitutions might be a CCC, with the additional property, again in the untyped case, that $\mathrm{hom}(y,x) \approxeq x$ .

Briefly, in the untyped case:

The cartesian structure is given by concatenation of contexts (modulo variable renaming).

The exponential $\mathrm{hom}(C, D)$ of two contexts $C$ and $D$ is $D$ itself.

The iso between $\mathrm{HOM}(C \times (x1: X1, \ldots, xn: Xn),D)$ and $\mathrm{HOM}(C, D)$ is given by successively $\lambda$ -abstracting over the $xi$ ’s (i.e., using currying), and in the other direction by successively applying the $xi$ ’s. The two composed functions are the identity, respectively by $\beta$ - and $\eta$ -conversion.

Also, in addition to the references in my previous post, there is this chapter by A. M. Pitts on categorical logic:

Pitts, A. M. 2000. Categorical logic. In Handbook of Logic in Computer Science: Volume 5: Logic and Algebraic Methods Handbook Of Logic In Computer Science. Oxford University Press, Oxford, 39-123.

Posted by: Tom Hirschowitz on August 30, 2006 8:20 AM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

But, you seem to be hinting strongly (though never quite saying!) that we should just take the free CCC on one object and throw in an isomorphism x $\cong$ hom(x,x), accepting the fact that this doesn’t make $x\cong x\times x$ . Is this true? Is the CCC I’m looking for $CCC[x]/\langle x\cong hom(x,x)\rangle$ ?

Yes, I believe this. (Whether there exists a rigorous proof is another matter…)

Tom suggested looking at Bart Jacobs’s fibrational definition of model, and in fact Jacobs proves (Lemma 2.5.2 in his book) that his definition is equivalent to the above.

It also sounds like you’re saying that if we want to go further and get the CCC corresponding to “the lambda-calculus with a surjective pairing”, we should also throw in an isomorphism . This will make all objects isomorphic except 1 . (Hey, a pun!)

Yes.

Do we demand any coherence laws on this extra isomorphism $x\cong x\times x$ or not?

I don’t think you need to. (When dealing with structures defined by universal properties, you don’t usually need coherence laws, right?) Another way of saying that there’s such an isomorphism is to say there are two projection maps p, $q: x\to x$ that exhibit $x$ as the product of $x$ and $x$ .

Posted by: Robin on August 30, 2006 2:33 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

What does CCC[x]/(x ~ hom(x,x)) mean? Are you inverting a certain map from x to hom(x,x), or adding a new one? Once you have done this, is it true/obvious that what you have is still a CCC?

Posted by: D. on August 30, 2006 5:44 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

Good question. I guess we’re being a bit sloppy with the notation.

Say that an object X of a CCC is reflexive if it’s isomorphic to $X\Rightarrow X$ . The category I assumed John was talking about is the free CCC on a reflexive object.

In other words, we’re adding a new isomorphism between X and $(X\Rightarrow X)$ , and also demanding that the category be cartesian closed.

Posted by: Robin on August 30, 2006 5:58 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

and also demanding that the category be cartesian closed.

Good. So I assume the question is: is there a solution to that demand?

Since we expect that $\lambda$ -calculus is a solution, can’t we explicitly construct this somehow?

I am looking for something like this:

We start with $x$ being some set of $\lambda$ -expressions. I guess we want to impose some normal form or something, such that there is a sufficient degree of uniqueness.

With $x$ in hand, we can maybe just declare $\mathrm{hom}(x,x)$ to equal the set $x$ .

The object 1 must then be the 1-element set.

What next?

You said the morphisms in $\mathrm{Hom}(\mathrm{hom}(x,x),\mathrm{hom}(x,x))$ must be precisely those that take an endo to an $n$ -th power.

This then also tells us what $\mathrm{Hom}(x,x)$ is.

In particular, the hom-set $\mathrm{Hom}(x,x) \simeq \mathbb{N}$ is not isomorphic to the internal hom-set $\mathrm{hom}(x,x) = x$ .

I guess we also identify $\mathrm{hom}(1,x) \simeq x$ .

This is so far consistent for instance with

(1)

\mathrm{Hom}(1\times x,x) \simeq \mathrm{Hom}(x,\mathrm{hom}(1,x)) \,.

Now, is $x \times x$ isomorphic to $x$ ?

Using

(2)

\mathrm{Hom}(x \times x, x) \simeq \mathrm{Hom}(x, \mathrm{hom}(x,x)) = \mathrm{Hom}(x, x) \simeq \mathbb{N}

it looks like there should be an identity morphism in $\mathrm{Hom}(x \times x, x)$ .

Hm. Okay, I don’t really know what i am doing here. The above is really a question: can we take the $\lambda$ -calculus and explicitly construct a CCC of the sort that we are expecting?

Posted by: urs on August 30, 2006 7:07 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

So I assume the question is: is there a solution to that demand?

Well, it’s clear on general principle that there must be a solution, since we can give a presentation of this category in terms of generators and relations. But of course that’s intractably unwieldy, so the interesting question is whether we can present the category in a manageable way.

The set Hom(x,x) should be the set of $\beta\eta$ -equivalence classes of untyped $\lambda$ -terms. (You seem to be assuming that the imposition of the isomorphism $x \cong (x\Rightarrow x)$ doesn’t change this set, whereas it does.)

If we want to describe all the morphisms, rather than just the endomorphisms of x, then we need to consider a special kind of typed $\lambda$ -calculus, with one base type $X$ . In addition to the usual operations of simply-typed $\lambda$ -calculus with pairing, there should be an isomorphism $x \cong (x \Rightarrow x)$ , so let’s introduce two new primitives Q and U (for ‘quote’ and ‘unquote’):

$Q : (X\to X) \to X$
$U : X\to (X\to X)$

with reduction rules

$Q(U s) \to s$
$U(Q t) \to t$

The resulting theory ought to describe our category, I think. I.e. for each type T, the set Hom(1, T) can be described as the set of equivalance classes of terms of type T.

Posted by: Robin on August 30, 2006 8:01 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

The set $\mathrm {Hom}(x,x)$ should be the set of $\beta\eta$ -equivalence classes of untyped $\lambda$ -terms. (You seem to be assuming that the imposition of the isomorphism $x \simeq (x \Rightarrow x)$ doesn’t change this set, whereas it does.)

I might be missing something elementary.

The fact $x \simeq (x \Rightarrow x)$ does imply

(1)

\mathrm{Hom}(x,x) \simeq \mathrm{Hom}((x \Rightarrow x),(x \Rightarrow x)) \,.

So if $\mathrm{Hom}((x \Rightarrow x),(x \Rightarrow x)) \simeq \mathbb{N}$ … ?

I am surprised that you say that $\mathrm{Hom}(x,x)$ should be the set of (equivalence classes of) $\lambda$ -terms. It seemed to me that in all our previous discussion, in particular for example in John’s comment here, we were thinking of $x$ as the set of $\lambda$ -terms, regarded as data, and of $\mathrm{hom}(x,x)$ as the same set, but with the elements now regarded as code, so to say.

Posted by: urs on August 31, 2006 9:25 AM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

Whilst $Hom(hom(x,x),hom(x,x))\cong\mathbb{N}$ in CCC[x], this is no longer true in the category we’ve been calling CCC[x]/ $\langle x\cong hom(x,x)\rangle$ .

Why does it surprise you that I’m claiming Hom(1,x) is the same as Hom(x,x)? We have

Hom(1,x) $\cong$ Hom(1, hom(x,x)) $\cong$ Hom(x,x)

so they ought to be the same.

Posted by: Robin on August 31, 2006 1:11 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

$\mathrm{Hom}(\mathrm{hom}(x,x),\mathrm{hom}(x,x)) \simeq \mathbb{N}$ […] is no longer true in the category we’ve been calling $\mathrm{CCC}[x]/\langle x \simeq \mathrm{hom}(x,x)\rangle$ .

Oh. Okay.

Somebody might maybe remind me then, why $\mathrm{Hom}(\mathrm{hom}(x,x),\mathrm{hom}(x,x)) \simeq \mathbb{N}$ was relevant for our purposes in the first place. I had that impression that we were trying to find the Church numerals here. But apparently I was ill-informed about this from the get go.

Why does it surprise you that I’m claiming $\mathrm{Hom}(1,x)$ is the same as $\mathrm{Hom}(x,x)$ ?

Right, that shouldn’t surprise me.

So implicitly you are saying that I was wrong in my previous comment to start by trying to model $x$ itself as the set of $\lambda$ -terms.

You say that this set is already $\mathrm{Hom}(1,x)$ (which I understand).

Okay, nice. Thanks for your help!

Now I am finally beginning to see how the category $\mathrm{CCC}[x]/\langle x \simeq \mathrm{hom}(x,x)\rangle$ indeed gives us $\lambda$ -caculus.

But really just beginning.

Let me see. Is the claim now that as soon as we form $\mathrm{CCC}[x]$ on an abstract object $x$ and then divide out by $x \simeq \mathrm{hom}(x,x)$ , that we then automatically know that $\mathrm{Hom}(1,x)$ is in bijection with the set $\Lambda$ of equivalence classes of $\lambda$ -terms?

Posted by: urs on August 31, 2006 1:59 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

Er, and one more thing. In $\mathrm{CCC}[x]$ we had $\mathrm{Hom}(1,x) = \{\}$ . So this, too, changes now drastically.

What remains of the nature of $\mathrm{CCC}[x]$ ?

Posted by: urs on August 31, 2006 2:02 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

Urs wrote:

What remains of the nature of CCC[ $x$ ]?

The way I think of it is this: if you’re in CCC[ $x$ ], it’s like being in a CCC and only knowing it has some object $x$ in it. Of course that has lots of consequences, since you’re in a CCC… you get a whole bunch of other objects, and morphisms, and equations.

Similarly, being in CCC[ $x$ ]/ $\langle x \cong hom(x,x)\rangle$ is like being in a CCC and only knowing it has some object $x$ in it, together with some isomorphism $x \cong hom(x,x)$ . Of course this has even more consequences…

These are both examples of “free” structures, obtained by left adjoints. In a “free” structure, nothing is there that doesn’t need to be - including equations.

Janis Joplin explained it clearly in one of her songs:

Freedom’s just another word for nothin’ left to lose…

Posted by: John Baez on September 1, 2006 2:31 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

Good, thanks.

Personally, I feel a lack of concrete things to hold on to in this discussion, but that’s just my ignorance.

I would enjoy having a list of concrete statements - to help my orientation in our discussion - of the following sort.

Untyped $\lambda$ -calculus is the image of

(1) $\mathrm{El} : \mathrm{CCC}[x]/\langle x \simeq \mathrm{hom}(x,x)\rangle \to \mathrm{Set} \,,$

where $\mathrm{El}$ is the canonical model.

Is that true? Is that what we were trying to discuss?

If not, is there a statement along these lines that is true?

Posted by: urs on September 1, 2006 3:11 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

Somebody might maybe remind me then, why $Hom(hom(x,x),hom(x,x))\cong\mathbb{N}$ was relevant for our purposes in the first place. I had that impression that we were trying to find the Church numerals here.

Yeah, it’s just that in the simply-typed case, the Church numerals are the only definable terms of type $(x\to x)\to(x\to x)$ , whereas in the untyped case there are lots of definable terms that are not Church numerals.

Posted by: Robin on August 31, 2006 2:18 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

D. wrote:

What does $CCC[x]/\langle x &cong; hom(x,x)\rangle$ mean? Are you inverting a certain map from $x$ to $hom(x,x)$ , or adding a new one? Once you have done this, is it true/obvious that what you have is still a CCC?

Roughly speaking, I’m adding an isomorphism between $x$ and $hom(x,x)$ and then doing the bare minimum it takes to make the result into a cartesian closed category.

This is a categorified version of how we build new groups, rings and other algebraic structures from old ones by throwing in new relations - for example, the ring of polynomial functions on the circle:

$\mathbb{R}[x,y]/\langle x^2 + y^2 = 1\rangle$

One big difference is that instead of throwing in an equation, we’re throwing in an isomorphism. Another big difference is that in general, the resulting gadget is defined up to equivalence instead of up to isomorphism.

The general theory of “defining categories with extra structure in terms of generators and relations” is less developed than for sets with extra structure. So, before one publishes papers about things like

$CCC[x]/\langle x &cong; hom(x,x)\rangle$

one needs to carefully go through the literature, see if the necessary constructions have already been defined, and if not, do it oneself. This work is somewhat boring, and it usually succeeds in the end - so I feel okay about skipping it when posting to a mere blog.

The business of “defining sets with extra structure in terms of generators and relation” was formalized at a high level of generality in the discipline of univeral algebra. This was later polished up and generalized from sets to other categories using the theory of algebraic theories and monads (also known as “triples”).

Later, people started categorifying all this stuff - that’s what we need to make precise concepts like “the free symmetric monoidal category on the category $C$ ” or “the free cartesian closed category on one object $x$ equipped with an isomorphism $x \cong hom(x,x)$ .

First Lawvere started thinking about monads on Cat instead of on Set - he called them doctrines. These suffice to describe categories with extra algebraic structure satisfying equational laws - for example, symmetric monoidal categories, or compact closed symmetric monoidal categories.

Categories with extra “structure” defined by universal properties - e.g. cartesian closed categories - are trickier: there is not such a thing as “the” object $x \times y$ or $\hom(x,y)$ ; it’s really just defined up to canonical isomorphism. This is why I put “structure” in quotes - for a category to be cartesian closed is a funny thing. We can treat it as a structure, but then it’s a property-like structure.

To deal thoroughly with these issues, we eventually need to start weakening the concepts of monads and their algebras, and start thinking about pseudomonads and their lax and pseudo algebras. This is where Australian category theory comes into play, especially these papers:

R. Blackwell, H. Max Kelly, and A. John Power, Two-dimensional monad theory, J. of Pure and Applied Algebra, 59 (1989), 1-41.
Steve Lack, A coherent approach to pseudomonads, Advances in Mathematics 152 (2000), 179-202.
Eugenia Cheng, A. John Power and Martin Hyland, Pseudo-distributive laws, Electronic notes in theoretical computer science, 83 (2004)

It’s tough going, but the same issues show up over and over when one is trying to categorify familiar constructions, and eventually we need to get good at this sort of thing.

There are probably also a bunch of specific references on defining CCCs by “generators and relations” (objects, morphisms and equations between morphisms), but I don’t know them yet. If anyone does, I’d be glad to hear!

Posted by: John Baez on August 31, 2006 6:36 AM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

Urs writes:

I would enjoy having a list of concrete statements - to help my orientation in our discussion - of the following sort.

Untyped $\lambda$ -calculus is the image of

(1) $\mathrm{El} : \mathrm{CCC}[x]/\langle x \cong \mathrm{hom}(x,x)\rangle \to \mathrm{Set} \,,$

where El is the canonical model.

Is that true? Is that what we were trying to discuss?

Yes, I’m trying to get people to assent to a statement very much like this! However, I need to get the details right if I’m ever going to get a roomful of logicians to agree with me.

First of all, it’s a bit vague to say that “untyped λ-calculus” is the image of some functor El. Second of all, we need to consider something like $\alpha\beta\eta$ -reduction equivalence classes of $\lambda$ -terms, if we want things that are in 1-1 correspondence with elements of $hom(x,x)$ in the category you mention.

Keeping all this in mind, let me try to state the claim a bit more precisely:

There’s an obvious way to define a one-to-one correspondence between $\alpha\beta\eta$ -equivalence classes of λ-terms in the untyped λ-calculus, and elements of $\mathrm{hom}(x,x)$ , where $x$ is the generating object of

$\mathrm{CCC}[x]/\langle x \cong \mathrm{hom}(x,x)\rangle.$

The main fudge here is the word “obvious” - I’m trying to say a specific recipe does the job, but I’m being too hasty to specify that recipe in detail.

Let me just give some examples of how this recipe works. The $\lambda$ -term

$\lambda a.a$

gets sent to the identity morphism

$1 : x \to x$

The $\lambda$ -term

$\lambda a.a a$

corresponds to the composite

$x \stackrel{\Delta}{\to} x \times x \stackrel{\alpha \times 1}{\to} \mathrm{hom}(x,x) \times x \stackrel{ev}{\to} x$

where we are using duplication, followed by our chosen isomorphism $\alpha: x \to \hom(x,x)$ on the first argument, followed by the evaluation map.

The $\lambda$ -term

$\lambda a.(\lambda b.a b)$

is a little more interesting. People often abbreviate this as

$\lambda a b.a b$

meaning the operation that takes two operations and lets the first operate on the second. Since this has two inputs, we can think of it as the composite

$x \times x \stackrel{\alpha \times 1}{\to} \mathrm{hom}(x,x) \times x \stackrel{ev}{\to} x$

However, by adjointness - or “currying”, in $\lambda$ -lingo - we can turn the above morphism into a morphism from $x$ to $\mathrm{hom}(x,x)$ . Then, by composing with $\alpha^{-1}$ , we can turn this into a morphism from $x$ to $x$ . And this is what the $\lambda$ -term

$\lambda a.(\lambda b.a b)$

gets sent to!

Robin Houston seems to agree that something like this works. As far as I can understand, Tom Hirschowitz also seems to agree. But, he emphasized that $\lambda$ -terms are not giving us the whole cartesian closed category, just the morphisms in $\mathrm{hom}(x,x)$ , and he gave us a reference which tackles this problem. Basically, unless I’m making a horrible mistake, it should be easy to see how to define the whole CCC in terms of the λ-calculus, not just this one hom-set.

Posted by: John Baez on September 2, 2006 8:20 AM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

John Baez says:

Basically, unless I’m making a horrible mistake, it should be easy to see how to define the whole CCC in terms of the $\lambda$ -calculus, not just this one hom-set.

Ok, I’ll try to be a bit more precise:

Let us take as objects of our candidate CCC the contexts, i.e., finite lists of variables.

Let us take as morphisms between two contexts $\Gamma = x_1, \ldots, x_m$ and $\Delta = y_1, \ldots, y_n$ the lists of n terms with free variables among $\Gamma$ . We write these morphisms: $\langle e_1, \ldots, e_n \rangle : \Gamma \to \Delta.$

The identity on a context $\Gamma = x_1, \ldots, x_m$ is $\langle x_1, \ldots, x_m \rangle : \Gamma \to \Gamma.$

Composition is defined by substitution: if $\Gamma$ and $\Delta$ are as above, $\Theta = z_1, \ldots, z_p$ , and $e = \langle e_1, \ldots, e_n \rangle : \Gamma \to \Delta$ and $f = \langle f_1, \ldots, f_p \rangle : \Delta \to \Theta,$ their composition $e \, \, f: \Gamma \to \Theta$ is $\langle g_1, \dots, g_p \rangle$ , where for each $i \in \{ 1, \ldots, p \}$ , $g_i = f_i \, \, \{ y_j \mapsto e_j \, \, | \, \, 1 \leq j \leq n \} \}.$

There appears to be subtle issues with variable renaming, so let us say that variables are in fact merely their index in the context, and we just write them as usual for readability.

Then, context concatenation is easily shown to yield products: again with $\Gamma$ and $\Delta$ as above, $\Gamma \times \Delta$ is merely $\Gamma, \Delta$ (with our convention on variables doing the nasty job of renaming), and the projections are: $\pi_1 = \langle x_1, \ldots, x_m \rangle$ and $\pi_2 = \langle y_1, \ldots, y_n \rangle.$

Of course, the terminal object is the emty context.

Exponentiation is a bit trickier. It uses the idea that a map to a product should roughly be the same as a product of maps. Additionally, the untypedness complicates the matter here, because $\Gamma^{\Delta}$ is just $\Gamma$ , which is weird at first sight. Anyway, given $f = \langle f_1, \ldots, f_m \rangle : (\Theta \times \Delta) \to \Gamma$ define its transpose across $HOM((\Theta \times \Delta), \Gamma) \approxeq HOM(\Theta, \Gamma^{\Delta}) \approxeq HOM(\Theta, \Gamma)$ to be $g = \langle g_1, \ldots, g_m \rangle,$ where each $g_i$ is $g_i = \lambda y_1. \ldots. \lambda y_n.f_i.$

The evaluation map is merely $\mathrm{ev} = \langle \mathrm{ev}_1, \ldots, \mathrm{ev}_m \rangle : (\Gamma^{\Delta} \times \Delta) \to \Gamma,$ where each $\mathrm{ev}_i$ is $\mathrm{ev}_i = (x_i\, y_1\, \ldots\, y_n) : (\Gamma^{\Delta} \times \Delta) \to x_i.$

Well, I guess that’s it. Actually, I glossed over some issues, most notably, the fact that $\Gamma^{\Delta}$ is not equal to $\Gamma$ , but merely isomorphic to it.

Does this make any sense?

Posted by: Tom Hirschowitz on September 4, 2006 2:45 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

Tom Hirschowitz writes:

Does this make any sense?

Yes! Thanks a million for writing it up in such detail. $thumbsup$

I had already guessed the basic idea, and your reference to Oldager’s Categorical semantics of simple type theory seemed to confirm my guess, but all his talk of fibrations made me worried that I was missing something. In fact it all works as simply as I’d hoped. Yay!

Posted by: John Baez on September 5, 2006 8:36 AM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

it all works as simply as I’d hoped. Yay!

Nice. So do I understand correctly that the statement now is not just

There’s an obvious way to define a one-to-one correspondence between $\alpha\beta\eta$ -equivalence classes of $\lambda$ -terms in the untyped $\lambda$ -calculus, and elements of $\mathrm{hom}(x,x)$ , where $x$ is the generating object of

(1) $\mathrm{CCC}[x]/\langle x \simeq \mathrm{hom}(x,x) \rangle$

#

but even

There’s an obvious way to define a one-to-one correspondence between $\lambda$ -terms in the untyped $\lambda$ -calculus, various reductions and operations on these $\lambda$ -terms and the category

(2) $\mathrm{CCC}[x]/\langle x \simeq \mathrm{hom}(x,x) \rangle$

Posted by: urs on September 19, 2006 1:00 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

When Tom Hirschowitz says “There appears to be subtle issues with variable renaming, so let us say that variables are in fact merely their index in the context” this suggests to me that one quotients by $\alpha$ equivalence. Perhaps you can avoid this with some clever trick.

Oldager, in the link that John posted above, considers terms up to $\beta$ and $\eta$ equivalence (page 13) but I don’t know if this is necessary or a convenience.

Posted by: Tom Ellis on February 7, 2014 7:00 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

Since I’ve just spent some time looking at this I thought I would summarise my understanding as it relates to John’s comment.

Oldager is providing a treatment of simply-typed lambda calculus, not untyped lambda calculus. The definitions of the classifying categories of the simply-typed lambda calculus with and without product types are both CCCs. It seems the fibrations are only needed to define what a model is in the case where you do not assume product types.

At the end he explains how to reduce the untyped lambda calculus to a single-typed lambda calculus, and presumably the classifying category is essentially what Tom Hirschowitz described above.

Posted by: Tom Ellis on February 7, 2014 6:50 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

Appendix A of Luke Ong’s course notes on Correspondence between operational and denotational semantics of PCF contains a precise description of the additional structure a CCC needs in order to be a model of PCF.

I don’t know whether this implies cpo-enrichment: presumably not. It’s interesting though that all the concrete models I know about, including the free one, are in fact cpo-enriched. (Does anyone here know one that isn’t?)

Posted by: Robin on September 15, 2006 4:01 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

(Actually I really doubt that the free model of PCF is cpo-enriched. I was guilty of some very sloppy thinking there.)

Posted by: Robin on September 16, 2006 11:08 PM | Permalink | Reply to this

Re: CCCs and the λ-calculus

Thanks for this link! Too bad Ong’s categorical treatment in Appendix A doesn’t include a general concept of “model” as some kind of structure-preserving functor. But, I guess I could dream up a definition of this sort, by reading this appendix more carefully.

Posted by: John Baez on September 21, 2006 6:07 AM | Permalink | Reply to this

Re: CCCs and the λ-calculus

$MathML-enabled post (click for more details).$

Urs writes:

Nice. So do I understand correctly that the statement now is not just

There’s an obvious way to define a one-to-one correspondence between $\alpha\beta\eta$ -equivalence classes of $\lambda$ -terms in the untyped $\lambda$ -calculus, and elements of $\mathrm{hom}(x,x)$ , where $x$ is the generating object of

(1) $\mathrm{CCC}[x]/\langle x \simeq \mathrm{hom}(x,x) \rangle$

#

but even

There’s an obvious way to define a one-to-one correspondence between $\lambda$ -terms in the untyped $\lambda$ -calculus, various reductions and operations on these $\lambda$ -terms and the category

(2) $\mathrm{CCC}[x]/\langle x \simeq \mathrm{hom}(x,x) \rangle$

?

Yeah, something sorta like that. Your statement is deliberately vague, so my agreement must be equally vague - but yeah, that’s the idea.

Tom Hirschowitz explained some of the details here.

One key nuance - which Tom didn’t mention, since we all remember it - is that we need an equivalence relation on $\lambda$ -terms called $\alpha\beta\eta$ -equivalence to get composition of morphisms to be strictly associative!

That’s precisely where I think categorification enters the game: it’s better if we don’t use such an equivalence relation, since then we should be able to set up a cartesian closed 2-category or maybe even $\infty$ -category, where “processes of computation” show up as a 2-morphisms!

I’m planning to teach a course on this stuff this fall, partially to organize my thoughts, partially because it’s so darn fun. I hope Derek Wise will take notes, which we can scan and put on the web. There will be tons of pictures….

By the way, I also plan to teach a course on quantization and cohomology.

(I’ll do these as the Tuesday and Thursday sessions of the quantum gravity seminar, respectively.)

Posted by: John Baez on September 21, 2006 6:01 AM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

August 28, 2006