Return to Answer

In one of my comments over at the other thread (this other thread), I had mentioned some discussion at the $n$-Category Café about a differential $\lambda$-calculus (from the looks of it, different to the one alluded to in Andrej Bauer's answer, although I looked only briefly). I'll try to sketch out some of it here, as it seems relevant.

Categorical models of typed $\lambda$-calculus are cartesian closed categories, and the idea was to contemplate the universal (i.e., initial) cartesian closed category that comes equipped with

• A commutative ring object $R$ (finite products suffice to describe what is meant by a commutative ring object),

• A differentiation operator $D\colon R^R \to R^R$ (here $R^R$ is the "function space object" whose existence is given by cartesian closure; the elements of $R^R$ correspond to morphisms $R \to R$), satisfying all the formal expected properties of differentiation (product rule, chain rule, etc.).

This universal cartesian closed category can be constructed syntactically and could be called "the $\lambda$-theory of high school calculus"; I'll call it $\mathit{Diff}$. A model of this theory is by definition a cartesian closed category $C$ together with a functor $S\colon \mathit{Diff} \to C$ which preserves the cartesian closed structure up to isomorphism (meaning the canonical comparison maps $S(a \times b) \to S(a) \times S(b)$ and $S(a^b) \to S(a)^{S(b)}$ are required to be isomorphisms). If the receiving category $C$ consists of concrete structures and structure-preserving maps, then you could call such a model a "denotational semantics" of $\mathit{Diff}$.

Now, there exists no denotational semantics $S\colon \mathit{Diff} \to Set$ which takes the object $R$ to the reals $\mathbb{R}$ as commutative ring. In other words, there is no operator $D\colon \mathbb{R}^{\mathbb{R}} \to \mathbb{R}^{\mathbb{R}}$ that satisfies all the formal properties of differentiation. But, there are other toposes $C$ of interest besides $Set$ which do admit such a semantics, where one can arrange the commutative ring object $R$ in $C$ so that its elements $1 \to R$ correspond exactly to real numbers. There is some flexibility in what one can arrange general morphisms $R \to R$ to be -- certainly they won't correspond to all functions $\mathbb{R} \to \mathbb{R}$, but you can get various interesting subclasses of functions (for which the modeled differentiation operator $D$ coincides with the usual one). For example:

• If $C$ is the topos of functors $CAlg_{fp} \to Set$ where $CAlg_{fp}$ is the category of finitely presented commutative $\mathbb{R}$-algebras, then $\hom(R, R) \cong \mathbb{R}[x]$ is the set of polynomial functions on $\mathbb{R}$.

• If $C$ is the topos of functors $C^{\infty}Alg_{fp} \to Set$ where $C^{\infty}Alg_{fp}$ is the category of finitely presented $C^{\infty}$-algebras (see here for definitions), then $\hom(R, R)$ is isomorphic to the ring of $C^{\infty}$-functions $\mathbb{R} \to \mathbb{R}$.

There were various further ruminations on this, coming under the heading of "snowglobe models" as models "sitting inside $Set$ as a miniature universe", as discussed here.

In one of my comments over at the other thread (this other thread), I had mentioned some discussion at the $n$-Category Café about a differential $\lambda$-calculus (from the looks of it, different to the one alluded to in Andrej Bauer's answer, although I looked only briefly). I'll try to sketch out some of it here, as it seems relevant.

Categorical models of typed $\lambda$-calculus are cartesian closed categories, and the idea was to contemplate the universal (i.e., initial) cartesian closed category that comes equipped with

• A commutative ring object $R$ (finite products suffice to describe what is meant by a commutative ring object),

• A differentiation operator $D\colon R^R \to R^R$ (here $R^R$ is the "function space object" whose existence is given by cartesian closure; the elements of $R^R$ correspond to morphisms $R \to R$), satisfying all the formal expected properties of differentiation (product rule, chain rule, etc.).

This universal cartesian closed category can be constructed syntactically and could be called "the $\lambda$-theory of high school calculus"; I'll call it $\mathit{Diff}$. A model of this theory is by definition a cartesian closed category $C$ together with a functor $S\colon \mathit{Diff} \to C$ which preserves the cartesian closed structure up to isomorphism (meaning the canonical comparison maps $S(a \times b) \to S(a) \times S(b)$ and $S(a^b) \to S(a)^{S(b)}$ are required to be isomorphisms). If the receiving category $C$ consists of concrete structures and structure-preserving maps, then you could call such a model a "denotational semantics" of $\mathit{Diff}$.

Now, there exists no denotational semantics $S\colon \mathit{Diff} \to Set$ which takes the object $R$ to the reals $\mathbb{R}$ as commutative ring. In other words, there is no operator $D\colon \mathbb{R}^{\mathbb{R}} \to \mathbb{R}^{\mathbb{R}}$ that satisfies all the formal properties of differentiation. But, there are other toposes $C$ of interest besides $Set$ which do admit such a semantics, where one can arrange the commutative ring object $R$ in $C$ so that its elements $1 \to R$ correspond exactly to real numbers. There is some flexibility in what one can arrange general morphisms $R \to R$ to be -- certainly they won't correspond to all functions $\mathbb{R} \to \mathbb{R}$, but you can get various interesting subclasses of functions (for which the modeled differentiation operator $D$ coincides with the usual one). For example:

• If $C$ is the topos of functors $CAlg_{fp} \to Set$ where $CAlg_{fp}$ is the category of finitely presented commutative $\mathbb{R}$-algebras, then $\hom(R, R) \cong \mathbb{R}[x]$ is the set of polynomial functions on $\mathbb{R}$.

• If $C$ is the topos of functors $C^{\infty}Alg_{fp} \to Set$ where $C^{\infty}Alg_{fp}$ is the category of finitely presented $C^{\infty}$-algebras (see here for definitions), then $\hom(R, R)$ is isomorphic to the ring of $C^{\infty}$-functions $\mathbb{R} \to \mathbb{R}$.

There were various further ruminations on this, coming under the heading of "snowglobe models" as models "sitting inside $Set$ as a miniature universe", as discussed here.

In one of my comments over at the other thread (this other thread), I had mentioned some discussion at the $n$-Category Café about a differential $\lambda$-calculus (from the looks of it, different to the one alluded to in Andrej Bauer's answer, although I looked only briefly). I'll try to sketch out some of it here, as it seems relevant.

Categorical models of typed $\lambda$-calculus are cartesian closed categories, and the idea was to contemplate the universal (i.e., initial) cartesian closed category that comes equipped with

• A commutative ring object $R$ (finite products suffice to describe what is meant by a commutative ring object),

• A differentiation operator $D: R^R \to R^R$ (here $R^R$ is the "function space object" whose existence is given by cartesian closure; the elements of $R^R$ correspond to morphisms $R \to R$), satisfying all the formal expected properties of differentiation (product rule, chain rule, etc.).

This universal cartesian closed category can be constructed syntactically and could be called "the $\lambda$-theory of high school calculus"; I'll call it $Diff$. A model of this theory is by definition a cartesian closed category $C$ together with a functor $S: Diff \to C$ which preserves the cartesian closed structure up to isomorphism (meaning the canonical comparison maps $S(a \times b) \to S(a) \times S(b)$ and $S(a^b) \to S(a)^{S(b)}$ are required to be isomorphisms). If the receiving category $C$ consists of concrete structures and structure-preserving maps, then you could call such a model a "denotational semantics" of $Diff$.

Now, there exists no denotational semantics $S: Diff \to Set$ which takes the object $R$ to the reals $\mathbb{R}$ as commutative ring. In other words, there is no operator $D: \mathbb{R}^{\mathbb{R}} \to \mathbb{R}^{\mathbb{R}}$ that satisfies all the formal properties of differentiation. But, there are other toposes $C$ of interest besides $Set$ which do admit such a semantics, where one can arrange the commutative ring object $R$ in $C$ so that its elements $1 \to R$ correspond exactly to real numbers. There is some flexibility in what one can arrange general morphisms $R \to R$ to be -- certainly they won't correspond to all functions $\mathbb{R} \to \mathbb{R}$, but you can get various interesting subclasses of functions (for which the modeled differentiation operator $D$ coincides with the usual one). For example:

• If $C$ is the topos of functors $CAlg_{fp} \to Set$ where $CAlg_{fp}$ is the category of finitely presented commutative $\mathbb{R}$-algebras, then $\hom(R, R) \cong \mathbb{R}[x]$ is the set of polynomial functions on $\mathbb{R}$.

• If $C$ is the topos of functors $C^{\infty}Alg_{fp} \to Set$ where $C^{\infty}Alg_{fp}$ is the category of finitely presented $C^{\infty}$-algebras (see here for definitions), then $\hom(R, R)$ is isomorphic to the ring of $C^{\infty}$-functions $\mathbb{R} \to \mathbb{R}$.

There were various further ruminations on this, coming under the heading of "snowglobe models" as models "sitting inside $Set$ as a miniature universe", as discussed here.

In one of my comments over at the other thread (this other thread), I had mentioned some discussion at the $n$-Category Café about a differential $\lambda$-calculus (from the looks of it, different to the one alluded to in Andrej Bauer's answer, although I looked only briefly). I'll try to sketch out some of it here, as it seems relevant.

Categorical models of typed $\lambda$-calculus are cartesian closed categories, and the idea was to contemplate the universal (i.e., initial) cartesian closed category that comes equipped with

• A commutative ring object $R$ (finite products suffice to describe what is meant by a commutative ring object),

• A differentiation operator $D\colon R^R \to R^R$ (here $R^R$ is the "function space object" whose existence is given by cartesian closure; the elements of $R^R$ correspond to morphisms $R \to R$), satisfying all the formal expected properties of differentiation (product rule, chain rule, etc.).

This universal cartesian closed category can be constructed syntactically and could be called "the $\lambda$-theory of high school calculus"; I'll call it $\mathit{Diff}$. A model of this theory is by definition a cartesian closed category $C$ together with a functor $S\colon \mathit{Diff} \to C$ which preserves the cartesian closed structure up to isomorphism (meaning the canonical comparison maps $S(a \times b) \to S(a) \times S(b)$ and $S(a^b) \to S(a)^{S(b)}$ are required to be isomorphisms). If the receiving category $C$ consists of concrete structures and structure-preserving maps, then you could call such a model a "denotational semantics" of $\mathit{Diff}$.

Now, there exists no denotational semantics $S\colon \mathit{Diff} \to Set$ which takes the object $R$ to the reals $\mathbb{R}$ as commutative ring. In other words, there is no operator $D\colon \mathbb{R}^{\mathbb{R}} \to \mathbb{R}^{\mathbb{R}}$ that satisfies all the formal properties of differentiation. But, there are other toposes $C$ of interest besides $Set$ which do admit such a semantics, where one can arrange the commutative ring object $R$ in $C$ so that its elements $1 \to R$ correspond exactly to real numbers. There is some flexibility in what one can arrange general morphisms $R \to R$ to be -- certainly they won't correspond to all functions $\mathbb{R} \to \mathbb{R}$, but you can get various interesting subclasses of functions (for which the modeled differentiation operator $D$ coincides with the usual one). For example:

• If $C$ is the topos of functors $CAlg_{fp} \to Set$ where $CAlg_{fp}$ is the category of finitely presented commutative $\mathbb{R}$-algebras, then $\hom(R, R) \cong \mathbb{R}[x]$ is the set of polynomial functions on $\mathbb{R}$.

• If $C$ is the topos of functors $C^{\infty}Alg_{fp} \to Set$ where $C^{\infty}Alg_{fp}$ is the category of finitely presented $C^{\infty}$-algebras (see here for definitions), then $\hom(R, R)$ is isomorphic to the ring of $C^{\infty}$-functions $\mathbb{R} \to \mathbb{R}$.

There were various further ruminations on this, coming under the heading of "snowglobe models" as models "sitting inside $Set$ as a miniature universe", as discussed here.

In one of my comments over at the other thread, I had mentioned some discussion at the $n$-Category Café about a differential $\lambda$-calculus (from the looks of it, different to the one alluded to in Andrej Bauer's answer, although I looked only briefly). I'll try to sketch out some of it here, as it seems relevant.

Categorical models of typed $\lambda$-calculus are cartesian closed categories, and the idea was to contemplate the universal (i.e., initial) cartesian closed category that comes equipped with

• A commutative ring object $R$ (finite products suffice to describe what is meant by a commutative ring object),

• A differentiation operator $D: R^R \to R^R$ (here $R^R$ is the "function space object" whose existence is given by cartesian closure; the elements of $R^R$ correspond to morphisms $R \to R$), satisfying all the formal expected properties of differentiation (product rule, chain rule, etc.).

This universal cartesian closed category can be constructed syntactically and could be called "the $\lambda$-theory of high school calculus"; I'll call it $Diff$. A model of this theory is by definition a cartesian closed category $C$ together with a functor $S: Diff \to C$ which preserves the cartesian closed structure up to isomorphism (meaning the canonical comparison maps $S(a \times b) \to S(a) \times S(b)$ and $S(a^b) \to S(a)^{S(b)}$ are required to be isomorphisms). If the receiving category $C$ consists of concrete structures and structure-preserving maps, then you could call such a model a "denotational semantics" of $Diff$.

Now, there exists no denotational semantics $S: Diff \to Set$ which takes the object $R$ to the reals $\mathbb{R}$ as commutative ring. In other words, there is no operator $D: \mathbb{R}^{\mathbb{R}} \to \mathbb{R}^{\mathbb{R}}$ that satisfies all the formal properties of differentiation. But, there are other toposes $C$ of interest besides $Set$ which do admit such a semantics, where one can arrange the commutative ring object $R$ in $C$ so that its elements $1 \to R$ correspond exactly to real numbers. There is some flexibility in what one can arrange general morphisms $R \to R$ to be -- certainly they won't correspond to all functions $\mathbb{R} \to \mathbb{R}$, but you can get various interesting subclasses of functions (for which the modeled differentiation operator $D$ coincides with the usual one). For example:

• If $C$ is the topos of functors $CAlg_{fp} \to Set$ where $CAlg_{fp}$ is the category of finitely presented commutative $\mathbb{R}$-algebras, then $\hom(R, R) \cong \mathbb{R}[x]$ is the set of polynomial functions on $\mathbb{R}$.

• If $C$ is the topos of functors $C^{\infty}Alg_{fp} \to Set$ where $C^{\infty}Alg_{fp}$ is the category of finitely presented $C^{\infty}$-algebras (see here for definitions), then $\hom(R, R)$ is isomorphic to the ring of $C^{\infty}$-functions $\mathbb{R} \to \mathbb{R}$.

There were various further ruminations on this, coming under the heading of "snowglobe models" as models "sitting inside $Set$ as a miniature universe", as discussed here.

In one of my comments over at the other thread (this other thread), I had mentioned some discussion at the $n$-Category Café about a differential $\lambda$-calculus (from the looks of it, different to the one alluded to in Andrej Bauer's answer, although I looked only briefly). I'll try to sketch out some of it here, as it seems relevant.

Categorical models of typed $\lambda$-calculus are cartesian closed categories, and the idea was to contemplate the universal (i.e., initial) cartesian closed category that comes equipped with

• A commutative ring object $R$ (finite products suffice to describe what is meant by a commutative ring object),

• A differentiation operator $D: R^R \to R^R$ (here $R^R$ is the "function space object" whose existence is given by cartesian closure; the elements of $R^R$ correspond to morphisms $R \to R$), satisfying all the formal expected properties of differentiation (product rule, chain rule, etc.).

This universal cartesian closed category can be constructed syntactically and could be called "the $\lambda$-theory of high school calculus"; I'll call it $Diff$. A model of this theory is by definition a cartesian closed category $C$ together with a functor $S: Diff \to C$ which preserves the cartesian closed structure up to isomorphism (meaning the canonical comparison maps $S(a \times b) \to S(a) \times S(b)$ and $S(a^b) \to S(a)^{S(b)}$ are required to be isomorphisms). If the receiving category $C$ consists of concrete structures and structure-preserving maps, then you could call such a model a "denotational semantics" of $Diff$.

Now, there exists no denotational semantics $S: Diff \to Set$ which takes the object $R$ to the reals $\mathbb{R}$ as commutative ring. In other words, there is no operator $D: \mathbb{R}^{\mathbb{R}} \to \mathbb{R}^{\mathbb{R}}$ that satisfies all the formal properties of differentiation. But, there are other toposes $C$ of interest besides $Set$ which do admit such a semantics, where one can arrange the commutative ring object $R$ in $C$ so that its elements $1 \to R$ correspond exactly to real numbers. There is some flexibility in what one can arrange general morphisms $R \to R$ to be -- certainly they won't correspond to all functions $\mathbb{R} \to \mathbb{R}$, but you can get various interesting subclasses of functions (for which the modeled differentiation operator $D$ coincides with the usual one). For example:

• If $C$ is the topos of functors $CAlg_{fp} \to Set$ where $CAlg_{fp}$ is the category of finitely presented commutative $\mathbb{R}$-algebras, then $\hom(R, R) \cong \mathbb{R}[x]$ is the set of polynomial functions on $\mathbb{R}$.

• If $C$ is the topos of functors $C^{\infty}Alg_{fp} \to Set$ where $C^{\infty}Alg_{fp}$ is the category of finitely presented $C^{\infty}$-algebras (see here for definitions), then $\hom(R, R)$ is isomorphic to the ring of $C^{\infty}$-functions $\mathbb{R} \to \mathbb{R}$.

There were various further ruminations on this, coming under the heading of "snowglobe models" as models "sitting inside $Set$ as a miniature universe", as discussed here.