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.
Supplementary reading:
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 realvalued functions on the real line, satisfying these (slightly redundant) laws:
$D(f+g) = Df + Dg$
$D(fg) = 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 lambdatheory 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 selfcontained 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!
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 replied: