Classical vs Quantum Computation (Week 14)

February 16, 2007

Classical vs Quantum Computation (Week 14)

Posted by John Baez

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

This time in our course on Classical vs. Quantum Computation, we sketched how a typed λ-calculus serves as a presentation of a cartesian closed category, and how every cartesian closed category arises this way. Since the students seemed to be struggling with the levels of abstraction involved, we slowed down to tackle an example:

Week 14 (Feb. 15) - The cartesian closed category generated by a typed λ-calculus, and how this construction gives a functor C:λCalc→CartC: λCalc \to Cart. The ‘internal language’ of a cartesian closed category, and how this gives a functor L:Cart→λCalcL: Cart \to λCalc. CC and LL are adjoint, and in fact give an equivalence between typed λ-calculi and and cartesian closed categories. Example 1: the λ-theory of commutative rings.

Supplementary reading:
- Joachim Lambek and Phil Scott, Introduction to Higher-Order Categorical Logic, Cambridge U. Press, 1988. Part 1, Section 11: the cartesian closed category generated by a typed λ-calculus.

Last week’s notes are here; next week’s notes are here.

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

At the end of class we raised a puzzle: what is a cartesian closed functor

$F: C_{\lambda Th(CommRing)} \to Set$

where $\lambda Th(CommRing)$ is the typed $\lambda$ -calculus for commutative rings, and $C_{\lambda Th(CommRing)}$ is the cartesian closed category generated by this $\lambda$ -calculus?

Only one student claimed to know the answer — so I urged him not to say what it was, and I began leading everyone else to the solution through a process of Socratic dialogue. There are, in fact, some nasty subtleties lurking in here.

Next time we’ll finish solving this puzzle and tackle a better example: the typed $\lambda$ -calculus for high school calculus.

Posted at February 16, 2007 10:04 PM UTC

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

19 Comments & 2 Trackbacks

Read the post Classical vs Quantum Computation (Week 13)
Weblog: The n-Category Café
Excerpt: Lambek and Scott's definition of a typed lambda-calculus.
Tracked: February 16, 2007 10:43 PM

Re: Classical vs Quantum Computation (Week 14)

the typed λ-calculus for high school calculus

What do you mean by ‘high school calculus’? Do you mean a Tarski high-school algebra (like the natural numbers under addition, multiplication, and exponentiation), accidentally typing ‘calculus’ twice? Or do you mean some rule-based version of differential calculus with no reference to εs and δs (something like a differential algebra)?

Posted by: Toby Bartels on February 17, 2007 8:53 PM | Permalink | Reply to this

Re: Classical vs Quantum Computation (Week 14)

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

Charles Dicken’s novels, originally published in installments, had a cliff-hanger at each end to keep the readers coming back for more. I too need to keep up some suspense — so I won’t explain precisely yet what I mean by ‘high-school calculus’.

But, if you’ve ever taught college-level calculus — or TA’ed it, as you surely have, Toby! — you’ll know that American kids can come out of high school ‘knowing calculus’ and in fact know only a limited set of rules for manipulating integrals and derivatives.

So, one can imagine different $\lambda$ -calculi that summarize different high school courses…

I’ll mainly talk about a very rudimentary one.

Posted by: John Baez on February 18, 2007 7:33 PM | Permalink | Reply to this

Re: Classical vs Quantum Computation (Week 14)

The notes say:

We also have terms including [my emphasis]

and list +, ⋅, 0, and 1. In fact only one basic (non-derived) term is missing, which is −: hom(R,R). Yet this one is important; the existential ring-theory axiom

Given an element x, there exists an element −x such that x + −x = 0.

cannot be stated as a λcalculus relation. Thus we need an extra term for − (just as we need it for 0 and 1, which are also often given only in existential axioms). And this really only works because identities and inverses are unique; as well, it forces us to accept as ring homomorphisms only functions that preserve them (which is automatic for − and 0 but not for 1).

I know that you know this, John, but it’s an interesting fact for those that haven’t seen it. (At least it was interesting to me when I first saw it!)

Posted by: Toby Bartels on February 17, 2007 9:28 PM | Permalink | Reply to this

Re: Classical vs Quantum Computation (Week 14)

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

Whoops! I really forgot to include negatives. Maybe I have rigs on the brain…

You’re right, this is a great example of how existential quantifiers can — hence should! — be avoided by introducing extra operations. So, I’ll talk about it next time.

Posted by: John Baez on February 18, 2007 7:45 PM | Permalink | Reply to this

Re: Classical vs Quantum Computation (Week 14)

John wrote:

[…] a great example of how existential quantifiers can — hence should! — be avoided by introducing extra operations.

Of course, sometimes they can’t be; the unicity is vital here.

For example, consider the notion of directed set: a set equipped with a reflexive, transitive relation such that * it has an element; and * any two elements have a common upper bound.

(So in summary, any finite subset has a common upper bound.) There are important examples where least upper bounds fail to exist, but mere upper bounds are not unique.

These are not so simple to describe logically, thus not so easy to interpret internal to broad classes of categories. It’s even a good question to ask what the proper notion is of morphism of directed sets. (It is actually weaker than monotone function!)

Posted by: Toby Bartels on February 20, 2007 12:59 AM | Permalink | Reply to this

Re: Classical vs Quantum Computation (Week 14)

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

So what is the proper notion of morphism of directed set?

And if you can answer that, what’s the proper notion of morphism of filtered category?

You’re good at leaving cliff-hangers!

Posted by: Tom Leinster on February 20, 2007 9:37 PM | Permalink | Reply to this

Re: Classical vs Quantum Computation (Week 14)

Tom asked me:

So what is the proper notion of morphism of directed set?

Hey, did I say that I know the answer?

What I meant was that we only care about the behaviour of functions on directed sets in the limit, that is ‘eventually’. You can do anything that you like with the function, as long as somewhere farther down things are (and remain) correct. So an eventually monotone function should be just as good as a monotone function. To be precise, a function f from the directed set D to the directed set E is eventually monotone if there is some x in D, such that whenever x ≤ y ≤ z in D, then f(y) ≤ f(z) in E.

But I forgot that the same thing goes for equality of functions on directed sets; we should count them as equivalent if they are eventually equal. Then any eventually monotone function is equivalent to a monotone function, so the morphisms wouldn’t really be more general than the monotone functions!

But is even this the correct notion of morphism? I’ve thought of a lot more that I could say, involving such ideas as eventuality filters, the equation f; g = g, and the axiom of choice. Since I never came to a clear answer, I won’t go into this now. But the short version is that I don’t know the answer to my own question!

Posted by: Toby Bartels on February 28, 2007 10:46 PM | Permalink | Reply to this

Re: Classical vs Quantum Computation (Week 14)

You remind me of my advisor, Irving Segal, who always wrote ‘unicity’ where I’d write ‘uniqueness’.

Posted by: John Baez on February 20, 2007 1:19 AM | Permalink | Reply to this

Re: Classical vs Quantum Computation (Week 14)

John wrote in part:

You remind me of my advisor, Irving Segal

In that we both know proper English? ^_^

Posted by: Toby Bartels on February 20, 2007 2:15 AM | Permalink | Reply to this

Re: Classical vs Quantum Computation (Week 14)

I thought that “unicity” was a mistake only made by native French speakers, and those infected by them. What’s wrong with “uniqueness”?

Posted by: Tom Leinster on February 20, 2007 4:22 PM | Permalink | Reply to this

Re: Classical vs Quantum Computation (Week 14)

I wondered the same. Actually I believe “uniqueness” is preferable here.

The OED gives the first definition of “unicity” as “the fact of being or consisting of one in number or kind; oneness”. Whereas “uniqueness” is defined as “the fact or condition of being unique or unequalled”. Illustrative quotations for “unicity” include “The most unquestionable unity or unicity of the Godhead” – here it obviously means “oneness”, not “the quality of there being at most one”. Later usages may have blurred this distinction.

The only argument I thought of for the alleged superiority of “unicity” is a fussy, prescriptivist one: the Latinate suffix ‘-ity’ is in conformity with the Latin root ‘unus’, whereas the suffix ‘-ness’ is of Germanic origin. Some people decry linguistic hybrids such as “uniqueness”. I think that’s silly!

Posted by: Todd Trimble on February 20, 2007 9:29 PM | Permalink | Reply to this

Re: Classical vs Quantum Computation (Week 14)

The OED gives the first definition of “unicity” as “the fact of being or consisting of one in number or kind; oneness”. Whereas “uniqueness” is defined as “the fact or condition of being unique or unequalled”.

What’s the difference between ‘consisting of one in kind’ and ‘being unique’? Particularly since the OED’s first definition of ‘unique’ is ‘Of which there is only one’. In the quotation, ‘unicity of Godhead’, they seem to be claiming something more than merely that there is only one God, since it touches on unitarianism. But the trinity is called a Mystery for good reason, and any subtleties that may apply in theology are probably not relevant in predicate logic.

The only argument I thought of for the alleged superiority of “unicity” is a fussy, prescriptivist one: the Latinate suffix ‘-ity’ is in conformity with the Latin root ‘unus’, whereas the suffix ‘-ness’ is of Germanic origin.

The only relevant etymology is this: The word ‘unicity’ was imported into English directly from mediaeval Latin (according to the OED, in 1691), while ‘uniqueness’ was created within English much later (in or around 1820, by Coleridge or perhaps a lost or oral predecessor). So the latter is not needed; I’ll stick with the former.

Of course, the prescriptivist sound in my ‘proper English’ above was a joke. You may say what you like, but I like cognates and classical etymologies.

Posted by: Toby Bartels on February 21, 2007 10:33 PM | Permalink | Reply to this

Re: Classical vs Quantum Computation (Week 14)

The word ‘unicity’ was imported into English directly from mediaeval Latin (according to the OED, in 1691), while ‘uniqueness’ was created within English much later (in or around 1820, by Coleridge or perhaps a lost or oral predecessor). So the latter is not needed; I’ll stick with the former.

Well, maybe Coleridge felt the need for such a word, because for him “unicity” carried with it other significations (“oneness”, “unity”, “unification”, etc.) which he didn’t intend. “Uniqueness” is preferable insofar as it’s sharper, i.e., when you say “unicity” here, you really mean “uniqueness”. Of course, everyone here understood that.

Of course, the prescriptivist sound in my ‘proper English’ above was a joke. You may say what you like, but I like cognates and classical etymologies.

Me too! And, I too am having fun. But apparently I’m not unique in thinking that, jocularly or not, you were in fact hinting that there is something wrong with “uniqueness”. (Plus, I thought your emoticon looked a little smug – I was provoked!) If not, then I have no quarrel.

Peace.

Posted by: Todd Trimble on February 22, 2007 4:05 PM | Permalink | Reply to this

Re: Classical vs Quantum Computation (Week 14)

Todd suggests:

Coleridge felt the need for such a word, because for him “unicity” carried with it other significations (“oneness”, “unity”, “unification”, etc.) which he didn’t intend.

I still don’t see what’s the difference between oneness and unicity/uniqueness. If you can convince me that ‘uniqueness’ is more precise than ‘unicity’, than I may start using it!

I thought your emoticon looked a little smug – I was provoked!

It’s a chibi smiley. (Chibi emote with their eyes, rather then their mouths, since these have much more detail. So do actual flesh-and-blood people, for that matter. Only traditional illustrations emote primarily with the mouth.) I like it for the emphasis on the eyes, and because you don’t have to turn your head to read it in plain text. But chibi emoticons are less versatile than sideways or (obviously) graphical emoticons.

Posted by: Toby Bartels on February 22, 2007 10:35 PM | Permalink | Reply to this

Re: Classical vs Quantum Computation (Week 14)

My favorite involving 4 languages is
Macadamization

anyone top that?

jim

Posted by: jim stasheff on February 22, 2007 5:51 PM | Permalink | Reply to this

Re: Classical vs Quantum Computation (Week 14)

My favorite involving 4 languages is Macadamization anyone top that?

Cool! And an interesting challenge…

In his book Adventures of a Mathematician, Ulam tells of a student overheard in a Paris restaurant saying, “Kolego, pozaluite mnia ein stueckele von diesem faschierten poisson” – a combination of Polish, Russian, Yiddish, German, and French!

Posted by: Todd Trimble on February 22, 2007 10:44 PM | Permalink | Reply to this

Re: Classical vs Quantum Computation (Week 14)

Toby wrote:

In that we both know proper English? ^_^

In that you both know lots of fancy words and like to flaunt it.

For example, Segal decried the use of ‘Propositions’ alongside ‘Definitions’, ‘Theorems’ and ‘Corollaries’. He claimed this was a effete Bourbakian innovation. He preferred Newton’s term ‘Scholium’. So, in our book on algebraic and constructive field theory, we have not Propositions but Scholia.

At the time, I cringed but didn’t argue. But now that I think of it, surely Euclid’s Elements had ‘Propositions’, at least starting with its Latin translations. And wouldn’t this term have been used in the early English translations of the Elements too?

Posted by: John Baez on February 22, 2007 6:12 AM | Permalink | Reply to this

Re: Classical vs Quantum Computation (Week 14)

John wrote:

Segal decried the use of ‘Propositions’ alongside ‘Definitions’, ‘Theorems’ and ‘Corollaries’. He claimed this was a effete Bourbakian innovation. He preferred Newton’s term ‘Scholium’.

surely Euclid’s Elements had ‘Propositions’, at least starting with its Latin translations. And wouldn’t this term have been used in the early English translations of the Elements too?

Yes, Heath’s translation of Euclid has Propositions. Ironically, he also has Scholia —but these are the commentary, by then considered part of the traditional text (like in the Talmud), but not written by Euclid. I have also read (can’t remember where, sorry), that a Scholium is properly a corollary of (some internal point in) the proof of a theorem (whilst a Corollary proper is a corollary of the mere statement of the theorem). For that matter, I’ve also heard that Euclid’s Propositions should really be thought as constructions, and even translated into the imperative mood, but I can’t remember who said that either.

I don’t know the true history of any of these terms.

Posted by: Toby Bartels on February 22, 2007 10:57 PM | Permalink | Reply to this

Re: Classical vs Quantum Computation (Week 14)

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

I don’t know the history either, but Scholium is a general term for comments appearing in the margins of a manuscript, which become incorporated into the manuscript tradition. You’ll see people quote them as “Scholium on <such-and-such a work>”, sometimes with speculation on who wrote the scholium.

Posted by: Tim Silverman on February 23, 2007 7:05 PM | Permalink | Reply to this

Read the post Classical vs Quantum Computation (Week 15)
Weblog: The n-Category Café
Excerpt: The λ-theory of commutative rings.
Tracked: February 23, 2007 3:39 AM

The n-Category Café

Skip to the Main Content

February 16, 2007