The n-Category Café

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))?$$

James Dolan has had some vaguely related ideas about this stuff, which I may try to explain in class someday…

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

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.

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.(?)

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)$.

Contradiction.