## March 2, 2007

### Classical vs Quantum Computation (Week 16)

#### Posted by John Baez This time in our class on Classical vs. Quantum Computation, we finished up the $\lambda$-theory of commutative rings and moved on to a more interesting example: the $\lambda$-theory for high school calculus!

• Week 16 (Mar. 1) - "Models" of a typed λ-calculus are cartesian closed functors from the cartesian closed category it generates to Set. Models of the λ-theory of commutative rings are commutative rings - so our guess last week was right. The λ-theory of high school calculus. Challenge: what are the models of this like? The "freshman’s paradise", in which every function is differentiable.

Near the end of the class, we had an interesting discussion about models of the λ-theory of high school calculus.

It seems highly unlikely that there are any models in the category $Set$ for which the commutative ring object $R$ gets interpreted as the set $\mathbb{R}$ of real numbers, because then we would get a derivative operator

$D: hom(\mathbb{R},\mathbb{R}) \to hom(\mathbb{R},\mathbb{R})$

which would serve to differentiate all real-valued functions on the real line, satisfying these (slightly redundant) laws:

$D(f+g) = Df + Dg$

$D(f-g) = Df - Dg$

$D(f\cdot g) = (D f)\cdot g + f \cdot (D g)$

$D 1 = 0$

$D 0 = 0$

$D x = 1$

$D(f \circ g) = ((D f) \circ g) \cdot D g$

If such an operator existed, no matter how pathological, surely we would have heard of it by now! Right?

Challenge Problem: Either prove no such operator exists, or construct one.

(This challenge has subsequently been solved by Todd Trimble — but I won’t say how, so you can have the fun of tackling it yourself!)

One can look for other models of the lambda-theory of high school calculus in the category of sets, but it seems the real fun comes from models in other cartesian closed categories, like the category of smooth spaces.

James Dolan also described some interesting ideas about ‘snowglobe models’ of λ-theories. You can read more about these here. The name ‘snowglobe’ comes from the fact that these models live in funny cartesian closed categories that are like their own tiny self-contained worlds inside the category of sets: There may be a nice relation between snowglobe models of the λ-theory of high school calculus and $n$th quantization!

Posted at March 2, 2007 12:23 AM UTC

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

### Re: Classical vs Quantum Computation (Week 16)

In class, Tom Payne asked if we could use the lambda calculus to talk about things like partial differentiation with respect to a given variable: ${\partial \over \partial x}$ and not just the abstract differentiation operator

$D \in hom(hom(R,R), hom(R,R)) .$

I found this fascinating, but I couldn’t think of anything intelligent to say about it.

Later, he emailed me and wrote:

I guess that all we can say is that:

$(x \mapsto {\partial \over \partial x} \phi(x)) = D( x \mapsto \phi(x)),$

where $\phi(x)$ denotes any expression possibly involving $x$ as a free variable.

That’s sort of a commutative law that says that lambda abstraction commutes with differentiation.

I replied:

Good point! But, I still feel confused about this stuff. What kind of entity should ‘${\partial \over \partial x}$’ be in the lambda calculus formalism? A term containing $x$ as a free variable, I guess? Should we take it as basic and use it to define $D$? Or the other way around?

One way to see if we’re doing something right is to see if we can construct ‘partial derivative’ operators that act on $hom(R^n,R)$ (functions of $n$ variables). If we can make sense of things like ${\partial \over \partial x}$, we’re there. But if we just start with the ability to differentiate functions of one variable:

$D \in hom(hom(R,R), hom(R,R))$

how can we define partial derivative operators

$D_i \in hom(hom(R^n,R),hom(R^n,R))?$

I think I’ll post this email to my blog, in hopes that someone else will help out.

Posted by: John Baez on March 7, 2007 6:52 AM | Permalink | Reply to this

### Re: Classical vs Quantum Computation (Week 16)

One way to see if we’re doing something right is to see if we can construct ‘partial derivative’ operators that act on $hom(R^n,R)$ (functions of n variables).

A term $\phi$ of type $Hom(R^n, R)$ can be $\eta$-expanded to $\lambda x_1 ... x_n. \phi(x_1, ..., x_n)$ and now let’s pick a variable $x_i$ to differentiate with respect to.

So, form $\lambda x_i. \phi(x_1, ..., x_n)$ with free variables $x_1$, …, $x_{i-1}$, $x_{i+1}$,… $x_n$. This is a term which I’ll denote $\phi_i$, of type $R^{n-1} \to Hom(R, R)$ and now form $R^{n-1} \stackrel{\phi_i}{\to} Hom(R, R) \stackrel{D}{\to} Hom(R, R)$ which one could denote $\lambda y. (\frac{\partial}{\partial x_i} \phi)(x_1, ..., y, ..., x_n).$

So, unless I’ve badly misunderstood your question, it’s not difficult. But has there been much discussion in class on the categorical handling of free variables? That seems to be crucial here.

Posted by: Todd Trimble on March 7, 2007 1:42 PM | Permalink | Reply to this

### Re: Classical vs Quantum Computation (Week 16)

I think you understood the question and gave a nice solution to the part you quoted. Massaging your construction a little, we indeed get a morphism

$D_i \in hom(hom(R^n,R),hom(R^n,R))$

in the cartesian closed category I was calling $C_{\lambda Th(Calc)}$.

So, high school students should be able to do partial derivatives without any reprogramming! Posted by: John Baez on March 8, 2007 4:22 AM | Permalink | Reply to this

### Re: Classical vs Quantum Computation (Week 16)

Partial derivatives are so artificial I should hope they’re not fundamental here. In calculus what’s fundamental is the tangent-space functor.

Even for functions, we actually don’t have an operator that takes a function and gives back another real-valued function. The value of the derivative f’(x) is a function: multiply by it.

So for functions derivation lives in Hom(Hom(R,R),Hom(R,Hom(R,R))). A function on Rn becomes a function that takes a point and returns the linear approximation at that point. That is: Hom(Hom(Rn,R),Hom(Rn,Hom(Rn,R))). Of course for parametrized curves derivation should live in Hom(Hom(R,Rn),Hom(R,Hom(R,Rn))). We should be able to build partial derivatives from these.

Let’s stop looking for special cases. There’s really a family of operators we’re looking at, living in Hom(Hom(A,B),Hom(A,Hom(A,B))). Now, should there be some sort of naturality connecting operators for different A, B?

Posted by: John Armstrong on March 7, 2007 2:24 PM | Permalink | Reply to this

### Re: Classical vs Quantum Computation (Week 16)

Once I made it into the office I thought of a particular case that should be pointed out: if A is Hom(X,Y) and B is R, we’re looking at functionals of parametrized curves, so this rubric should also encapsulate the calculus of variations.

Posted by: John Armstrong on March 7, 2007 3:03 PM | Permalink | Reply to this

### Re: Classical vs Quantum Computation (Week 16)

One possibility for heading in this type of direction is just to do [a possibly restricted form of] SDG; see for example a lot of earlier discussion starting about here . Introduce a new type D, and some terms $p: R^D \to R$, $v: R^D \to R$ plus an inverse to $\langle p, v \rangle: R^D \to R \times R$ (Kock-Lawvere axiom), and some other structure like the commutative ring structure on R, and see how much one can do (rather a lot, actually). The functoriality of the tangent bundle functor $(-)^D$ (cf. chain rule) would follow from such an approach.

That would be a fine direction to head in, of course. I interpreted John B’s pursuance of differentiation here not as a primary goal of his course, but more in the way of a fun pedagogical exercise which can help illustrate some stuff about models of CCC’s, among other things. But maybe he should speak for himself.

Posted by: Todd Trimble on March 7, 2007 3:34 PM | Permalink | Reply to this

### Re: Classical vs Quantum Computation (Week 16)

John Armstrong wrote:

Partial derivatives are so artificial I should hope they’re not fundamental here. In calculus what’s fundamental is the tangent-space functor.

I’m not trying to reinvent calculus on manifolds. I’m trying to express ‘high school calculus’ — differential calculus as a set of mechanical rules for differentiating polynomials — in the language of the typed lambda-calculus. This is a nice little test of the expressive power of the lambda-calculus.

And, the question at hand is: from the viewpoint of the lambda-calculus, what sort of logical entity is the symbol ${\partial \over \partial x}$ Does it even parse? Normally in the lambda-calculus one can substitute any term of the right type for a free variable like $x$. But people don’t usually do this here: ${\partial \over \partial x^2 + y + 7}$ is not something one sees.

It’s for these reasons I avoided $d/d x$ in my ‘lambda-theory of high school calculus’.

Posted by: John Baez on March 7, 2007 4:36 PM | Permalink | Reply to this

### Re: Classical vs Quantum Computation (Week 16)

I’m not trying to reinvent calculus on manifolds.

Of course you’re not, which is why you didn’t talk about partial derivatives. Many people talk about slippery slopes, but partial derivatives really are one: you can’t introduce them and not be inexorably drawn into calculus on manifolds. Even adding them in multivariable calculus requires all sorts of huge, artificial bulwarks to prevent the course from spinning off into manifolds.

My position is that if you want to add them to a lambda-like structure the natural way would be to lift up to a structure that also encapsulates calculus on all real affine spaces, if not manifolds.

Posted by: John Armstrong on March 7, 2007 10:31 PM | Permalink | Reply to this

### Re: Classical vs Quantum Computation (Week 16)

Of course you’re not, which is why you didn’t talk about partial derivatives.

Not to pick nits – I’m honestly baffled by this statement. If JB wasn’t talking about partial derivatives, then how did we get onto this thread?

Many people talk about slippery slopes, but partial derivatives really are one: you can’t introduce them and not be inexorably drawn into calculus on manifolds.

More substantively, part of the point is to explore the expressive power of the language of typed lambda calculus. We’ve seen in particular that once a derivative operator D is introduced and axiomatized, then partial derivative operators are also expressible in the language. But we are not inexorably led to manifolds within this language, as this language (as it stands) cannot express constructions for gluing together local coordinate patches. For that matter, we don’t even have equalizers in general CCC’s, so we cannot even talk about loci of equations (varieties) in this language. In some respects, then, the language is quite poor.

Posted by: Todd Trimble on March 7, 2007 11:29 PM | Permalink | Reply to this

### Re: Classical vs Quantum Computation (Week 16)

If JB wasn’t talking about partial derivatives, then how did we get onto this thread?

He said when he brought it up that someone in class asked about it. It wasn’t originally part of his plan, or at least that’s how it seemed to me.

I don’t find the suggestions so far to be very satisfying. They show how to apply the original differentiation operator to one variable or another, but they seem to be all tied up in names.

For example, $\lambda x,y.x^2y$ should be the same function as $\lambda y,x.y^2x.$ So what should $\frac{\partial}{\partial x}$ do here?

I come back to my assertion that partial derivatives are artificial, and the natural thing is the total differential. No, we don’t have to push as far as manifolds, but the appropriate definition of D (or a related family of Ds) should be the differential that works for all different domains and codomains. Partial derivatives will be projections from there.

Posted by: John Armstrong on March 8, 2007 12:36 AM | Permalink | Reply to this

### Re: Classical vs Quantum Computation (Week 16)

I don’t find the suggestions so far to be very satisfying. They show how to apply the original differentiation operator to one variable or another, but they seem to be all tied up in names. For example, λx,y.x 2y should be the same function as λy,x.y 2x. So what should ∂∂x do here?

Well, I think I was being reasonably careful in how I defined the partial derivatives. Once you express a function $\phi$ as a function of ordered $n$-tuples (as in my original response), then partial differentiation with respect to the $i^{th}$ variable is of course perfectly unambiguous. In your example, partial differentiation with respect to the first variable listed in the lambda-binder of each of your equivalent lambda expressions leads to the equivalent expressions $\lambda x, y. 2xy = \lambda y, x. 2yx$.

I think basically you’re just sounding a familiar warning to be careful around issues of alpha equivalence. Sure, sure. In informal parlance, as when we teach multivariate calculus, it is customary to consider $x$, $y$, and $z$ as the first, second, and third coordinates, respectively. Only insofar as such tacit conventions are honored can we get away with a symbol like $\frac{\partial}{\partial x}$ – yes, of course. No surprises there, nosiree Bob.

Rest assured that I understand, and agree with, the spirit of your point about the total differential. I think everyone gets that. But this wasn’t a normative discussion – it was a discussion about expressivity.

Posted by: Todd Trimble on March 8, 2007 1:48 AM | Permalink | Reply to this

### Re: Classical vs Quantum Computation (Week 16)

But people don’t usually do this here:

(1)$\frac{\partial}{\partial x^2+y+7}$

I used to think that too, but apparently it was quite common once. See this answer of Francois Ziegler on hsm.

Posted by: Michael Bächtold on August 12, 2018 12:38 PM | Permalink | Reply to this

### Re: Classical vs Quantum Computation (Week 16)

I think what’s puzzling about the notation $\frac{\partial}{\partial x}$ is that it isn’t, quite, a binding construct. Many syntactic constructs that are used in informal mathematics – such as $\int_0^1$ — dx, $\sum_{x=0}^{10}$ and so forth – do actually bind the variable $x$. Such a binding construct can always be decomposed into an operator applied to a lambda: for example, $\sum_{x=0}^{10}\phi$ can be interpreted as $sum(\lambda x.\phi, 0, 10)$, where ‘sum’ is a function of type $((N\to N)\times N\times N)\to N$, perhaps.

However $\frac{\partial}{\partial x}$ doesn’t appear to bind $x$ in the same way. It still makes sense to talk about the function $x\mapsto \frac{\partial}{\partial x}(x^2)$, for example, which suggests that $x$ is still free in $\frac{\partial}{\partial x}(\phi)$. Here’s one way to interpret it, which seems to work: decree that $\frac{\partial}{\partial x}(\phi)$ is an abbreviation for $(D \lambda x.\phi)(x)$ where $\phi$ is an expression, typically (but not necessarily) containing $x$ free. So the $x$ is bound, the function differentiated, and the resulting function is applied to a new, free, $x$.

It works for several variables too. If $\phi$ contains other free variables in addition to $x$, $\frac{\partial}{\partial x}(\phi)$ still has those variables free. You can close them off outside, if you like, so for example $\lambda x,y. \frac{\partial}{\partial x}(x^2y)$ is a function $R\to R\to R$.

I’m not totally sure what you’re after, so perhaps this is irrelevant. But I found it interesting!

Posted by: Robin on March 7, 2007 2:32 PM | Permalink | Reply to this

### Re: Classical vs Quantum Computation (Week 16)

Robin wrote:

I’m not totally sure what you’re after, so perhaps this is irrelevant. But I found it interesting!

I’m not totally sure what I’m after, either! But, Tom’s thought must have been something like this: “Great: high school calculus is so mechanical that we can write a theory in the typed lambda-calculus that encodes lots of the rules for taking derivatives — if we carefully sidestep the expression ${d\over d x}$ and talk about a differentiation operator $D$ instead! But what if we do want to talk about ${d \over d x}$? Since we might want to use other variables besides $x$ here, we should probably call it ${\partial\over \partial x}$. So, let’s find a nice home for partial derivatives in the typed lambda-calculus.”

And, I like your answer: decree that for any term $\phi$,

${\partial \over \partial x}(\phi)$

is an abbreviation for

$(D(x \mapsto \phi))(x)$

I’m now wondering if the slightly subtle nature of this puzzle is related to some ways beginners get confused when manipulating derivatives.

Posted by: John Baez on March 8, 2007 4:13 AM | Permalink | Reply to this

### Re: Classical vs Quantum Computation (Week 16)

John Armstrong wrote:

I don’t find the suggestions so far to be very satisfying.

I should clarify what we’re up to here.

We’re not trying to do calculus better than a typical American high school calculus course. Instead, we’re imagining that high school calculus is nothing but a bunch of mechanical ‘rewrite rules’ for taking derivatives of polynomials. (This is indeed the impression one gets from some students here at U.C. Riverside!) And then, we’re imagining the project of formalizing these rules using the typed lambda-calculus.

And then, Tom and I couldn’t help wondering what concepts can be expressed in this formal system. As Todd said, part of the point is to explore the expressive power of this rather limited form of logic.

The reason I chose high school calculus is, first, because I can’t resist a pun: a lambda-calculus for calculus! Second, this is the first place most kids meet an ‘operator’ — an entity of type

$hom(hom(X,X),hom(X,X)).$

So, it’s a good illustration of how typed lambda-calculi give rise to cartesian closed categories, which have ‘hom-objects’. I’m envisioning differential calculus as a slight embellishment of the Lawvere theory of commutative rings. Commutative rings can be formalized in cartesian categories; derivatives require cartesian closed categories. That pushes us up to ‘higher-order’ categorical logic.

And today in class, I’ll talk about how the ‘rewrite rules’ in high school calculus give a cartesian closed 2-category. In this 2-category, we won’t say

${d\over d x} x^2 = 2 x$

Intead, there will be a morphism from the left side to the right side — a ‘process of computation’.

I don’t expect this to catch on in the high school curriculum, though.

Posted by: John Baez on March 8, 2007 6:14 PM | Permalink | Reply to this

### Re: Classical vs Quantum Computation (Week 16)

“Algebraizing the Calculus” indeed…

Posted by: John Armstrong on March 8, 2007 7:17 PM | Permalink | Reply to this
Weblog: The n-Category Café
Excerpt: Constructing strange 'nonstandard models' of typed λ-calculi.
Tracked: March 10, 2007 5:16 AM

### Calculus on Affine Spaces

It seemed to me that John Armstrong’s comments on the proper viewpoint on differentiation deserved to be taken up more fully, partly for its own sake, partly to see what can and can’t be done in $\lambda$Th(Calc), and partly in the way of tying together some loose strands in this blog entry.

The objects of $C_{\lambda Th(Calc)}$ could be called “affine spaces”, according to the rules (1) 1 is an affine space, (2) if $A$ is an affine space, then so is $R^A$, (3) if $A$ and $B$ are affine spaces, then so is $A \times B$. So we are trying to do calculus on affine spaces.

John A. proposed that differentiation could be seen as a natural family of type

$Hom(A, B) \to Hom(A, Hom(A, B))$

or equivalently of type

$Hom(A, B) \to Hom(A \times A, B)$

(from this point on I am going to switch to exponential notation for internal homs). Intuitively, this should be the mapping

$(f: A \to B) \mapsto \lambda p, v. (Df|_p) \cdot v$

where affine spaces $A$ and $B$ are identified with their tangent spaces at each of their points $p$.

Elsewhere, I had suggested that one way of doing calculus might be to add a new type $D$ and mimic Synthetic Differential Geometry purely in the cartesian closed setting. On objects the tangent bundle of a type $A$ would be $A^D$, and there would be an (internal) derivative operator

$B^A \to (B^D)^{(A^D)}$

arising from the internal hom $(-)^D$. Under the Kock-Lawvere axiom we would have an isomorphism $R^D \cong R \times R$. Very simple calculations which hold generally in cartesian closed categories would then show that $A^D \cong A \times A$ for all types or affine spaces. Thus the internal derivative would be a natural family

$D_{A, B}: B^A \to (B \times B)^{A \times A}$

intuitively described by the mapping

$(f: A \to B) \mapsto \lambda p, v. \langle f(p), (Df|_p)\cdot v \rangle,$

a minor tweak on what John proposed.

The question I want to consider is how much of this family is expressible in the theory $\lambda Th(Calc)$ that John B introduced.

I only got so far; I was getting a little stuck just at the “calculus of variations” point, which might lie just beyond the purview of what one can do just with a commutative ring $R$ and a single derivative operator

$D_{R, R}: R^R \to R^R.$

Here’s what I have so far: suppose we have a family of natural transformations

$D_{A, R}: R^A \to (R \times R)^{A \times A}$

which is definable in $\lambda Th(Calc)$ for some full subcategory of types $A$. Then for any $X$ we can define

$D_{A, R^X}: (R^X)^A \to (R^X \times R^X)^{A \times A}$

as the evident composite

$(R^X)^A \cong (R^A)^X \stackrel{D_{A,R}^X}{\to} [(R \times R)^{A \times A}]^X \cong (R^X \times R^X)^{A \times A}.$

Moreover, if natural operators $D_{A, B}$ and $D_{A, C}$ are defined for the same class of objects $A$, then there is an operator $D_{A, B \times C}$ defined by the evident composite

$(B \times C)^A \cong B^A \times C^A \stackrel{D_{A,B} \times D_{A,C}}{\to} (B \times B)^{A \times A} \times (C \times C)^{A \times A} \cong [(B \times C) \times (B \times C)]^{A \times A}.$

Thus, if we have derivative operators $D_{A, R}: R^A \to (R \times R)^{A \times A}$ for some class of “admissible” types $A$, then we have derivative operators $D_{A, B}: (B \times B)^{A \times A}$ for admissible $A$ and any type $B$.

Clearly $R$ is admissible. If $A$ and $B$ are admissible, so is their product $A \times B$: the requisite map

$D_{A \times B, R}: R^{A \times B} \to (R \times R)^{(A \times B) \times (A \times B)}$ may be defined by a lambda term with a free variable $\phi$ of type $R^{A \times B}$, as

$\lambda a, b; v, w. \langle \phi(a, b), \partial_A(\phi)(a, b)v + \partial_B(\phi)(a, b)w \rangle$

where $\partial_A$ and $\partial_B$ are (with a little good will) partial derivative operators definable from $D_{A,R}$ and $D_{B,R}$, and the algebraic operations of sum and multiplication are defined on every type by the obvious pointwise and coordinatewise definitions which stem from the commutative ring structure on $R$.

Taking stock of what we have so far, we have thus defined internal derivative operators

$D_{R^n, B}: B^{R^n} \to (B \times B)^{R^n \times R^n}$

which are natural in $R^n$ and $B$. It would be nice to extend to all types $A$ in place of $R^n$ (it suffices to do this for types of the form $R^X$; cf. calculus of variations), but I don’t see how to do this yet within the language $\lambda Th(Calc)$. Maybe it’s not possible.(?)

Posted by: Todd Trimble on March 11, 2007 10:07 PM | Permalink | Reply to this

### Re: Classical vs Quantum Computation (Week 16)

Since nobody but Todd Trimble seems to have solved the ‘Challenge Problem’ issued in this week’s lecture, here is his solution:

Ok, we’re trying to see whether there is a derivation $D$ on the algebra $Hom(\mathbb{R}, \mathbb{R})$ of all endofunctions on the usual reals, such that $D$ satisfies the chain rule. Suppose so, and let

$f = D(x \mapsto |x|).$

By evaluating

$DD(x \mapsto |x|^2) = DD(x \mapsto x^2)$

at $0$, we quickly find (using the Leibniz rule) that $f(0)^2 = 1$. So $f(0) = 1$ or $-1$.

By attempting to evaluate

$D(x \mapsto |-x|)= D(x \mapsto |x|)$

at $0$ using the chain rule, we also find $f(0) = f(0)(-1)$.