14
$\begingroup$

I'm a computer scientist, not a mathematician, so apologies if I've messed up a lot of things greatly.

I've been reading about synthetic differential geometry, and trying to formalize it in Coq. While dealing with the axiomatic specification is quite pleasing, actually constructing a (computable / effective) model of this seems frightfully hard.

The simplest model that I could find comes from Differential Geometry in Toposes: Ryszard Paweł Kostecki is $\mathbf{Set}^{\mathbb R- \mathbf{Alg}}$: That is, functors from $\mathbb R$ algebras to $\mathbf{ Set}$. This is quite painful to formalize within Coq, and at the end, I don't think what's left will be computable (since the reals are not computable)

My questions are (in descending order of importance)

  • How do I get a computable model of SDG, in the sense that, I should at the end of the whole process be abel to use a computable version of (say) the derivative operator within Coq. Is this possible? If yes, what model of synthetic differential geometry is this?

  • Does restricting to the case of discrete differential geometry make life any easier for me? Is there a study of "synthetic discrete differential geometry"?

EDIT: adding more details about what I'm looking for

I know that one can impement differentiable programming languages by using implementations of automatic differentiation. There's a categorical interpretation to this, for example, see The simple essence of automatic differentiation.

What I'm looking for is a way to perform computational differential geometry. So, not only do I want to be able to be able to calculate the value of $f'(x_0)$ at a given $x_0$, I want to be able to compute the differential of $f$ as a computable function. So, for example, I want there to exist an operator $d: (f : M \rightarrow N) \rightarrow (T_x M \rightarrow T_{f(x)}N)$.

Ideally, I want this setup such that I can:

  • prove things about the operator $d$ within the axiomatic system as laid out by SDG (in Coq).
  • Create a computable model that satisfies those axioms (implement the axiomatic system in Coq)
  • Finally, extract out runnable Haskell / OCaml code that allows computable access to things like the differential map $d$, such that when I feed it in $f(x) = x +2$, I should get $d f \equiv 1$ ($\equiv$ reasoning between equality of functions extentionally).

I don't know if this is too much of an ask, or indeed, a coherent ask. The goal really for me is to have a verified, computable differential geometry (or at least, discrete differential geometry) library, with proofs that can be done easily, which is the whole point of SDG.

Improve this question
$\endgroup$
6
  • 2
    $\begingroup$ Are you looking for the differential $\lambda$-calculus? Please explain what it is that you are trying to accomplish at the end of the day, i.e., what sort of computer science application are you shooting for? You expect SDG will give you something, but until we know what you expect to get from it, it's difficult to answer the question. $\endgroup$
    – Andrej Bauer
    Commented Nov 19, 2019 at 11:26
  • $\begingroup$ Thank you for your time! I've amended the question with what I am looking for. If it's still vague, I'd be happy to clarify. I didn't know about the existence of the differential $\lambda$-calculus, I'll take a look at it now! $\endgroup$
    – Siddharth Bhat
    Commented Nov 19, 2019 at 12:28
  • 1
    $\begingroup$ Have you looked at modal Homotopy Type Theory? See also the article Cartan Geometry in Modal Homotopy Type Theory by Wellen. $\endgroup$
    – David Roberts ♦
    Commented Nov 19, 2019 at 12:35
  • 2
    $\begingroup$ "since the reals are not computable": there are many computable models for reals suitable for SDG. For instance, one can use the locale of reals, defined by completing the rationals. This construction can then be instantiated in the effective topos, for example. $\endgroup$
    – Dmitri Pavlov
    Commented Nov 19, 2019 at 14:19
  • 1
    $\begingroup$ @SiddharthBhat: See ncatlab.org/nlab/show/locale+of+real+numbers for an overview. The canonical textbook reference is Picado and Pultr, Frames and Locales. $\endgroup$
    – Dmitri Pavlov
    Commented Nov 20, 2019 at 19:04

1 Answer 1

Reset to default
3
$\begingroup$

I still don't quite understand what OP wants, but let me just cite a few papers that I think might be relevant to such questions. First, there are a lot of literature that describe how to work with real numbers in a computationally meaningful way. To give a few examples:

I think that ideas presented in these papers can be used to implement a library in a proof assistant with the goal of extracting computable functions on real numbers.

If you really want to work with SDG, I'd like to mention that there are other options. Differential λ-calculus was already mentioned in the comments. I also would like to mention tangent categories, which generalize both differential categories (which are a categorical model of differential λ-calculus and SDG).

The question is at which level of abstraction you want to work. Differential categories is the simplest setup and tangent categories is the most general since they generalize both differential categories and SDG, but it is also simpler (in some sense) than SDG since it is more abstract. All of these frameworks are abstractions of the usual differential geometry (and also other settings in which the differential operator occurs). The more abstract framework, the more models it has, but it also means that it allows to prove less theorems in specific models.

It seems that you do not really care about other models and wants to work formalize just ordinary differential geometry. If this is true, I'd say it does not make sense to start with a complicated framework such as SDG. Abstract framework does not really help if you care about program extraction since you still need to construct specific models in a proof assistant. They are useful if you want to reason abstractly about such structures.

If you want to implement a library with a program extraction, I'd suggest to start with a direct implementation of real numbers as described in the papers I cited at the beginning (or any other similar paper). Then you can implement an abstract framework on top of that. You will need a concrete model of such a framework anyway if you want to get a concrete implementation of real functions.

Improve this answer
$\endgroup$
6
  • $\begingroup$ I was under the impression that it was easier to perform the proofs of (1. Prove diffgeo theorems inside SGD, 2. exhibit a model of SGD) versus the direct process of Prove diffgeo without SGD. Is not the point of topoi that reasoning within the internal logic of the topos is "easier"? If this is not the point, then why does SGD exist? $\endgroup$
    – Siddharth Bhat
    Commented Nov 20, 2019 at 15:56
  • 1
    $\begingroup$ @SiddharthBhat It's hard to tell which of the options is easier without trying them both. One of my points is that there are other abstract settings, which might be easier to work with since they do not require the whole theory of topoi, only basic categories. Since your question was "how to get a computational model of SDG", I might suggest that you formalize differential or tangent categories first. Then you can construct examples of such categories out of existing library for real numbers. Then you can move to a more complicated setting of SDG. $\endgroup$
    – Valery Isaev
    Commented Nov 20, 2019 at 16:09
  • $\begingroup$ I see, thank you. I now understand the perspective the answer is written from. I'll have to read about these other axiomatizations --- I'll try the axiomatizations you referenced and see how it goes. Thanks a ton! $\endgroup$
    – Siddharth Bhat
    Commented Nov 20, 2019 at 16:13
  • 1
    $\begingroup$ @SiddharthBhat For example, if you use tangent categories, then you can work with the category of manifolds directly and don't think about topoi and $C^\infty$-rings. If you work with differential categories, then it is even simpler than that. One of its models is the category of Euclidean spaces and smooth maps. So, if you already have a library that defines these notions, it is very easy to construct the structure of a differential category. Since it is a very simple framework, you cannot prove many interesting things in it. But then you can move to tangent categories and eventually SDG. $\endgroup$
    – Valery Isaev
    Commented Nov 20, 2019 at 16:20
  • 1
    $\begingroup$ @SiddharthBhat Proofs in differential and tangent categories also do not refer to limits or anything like that. The proofs there are more categorical. If you want to see more "syntactic" proofs as in SDG, then you need to use some form of internal language for such categories. Differential λ-calculus is such a language for differential categories and I don't think that such a language was described for tangent categories. Also, if you want to formalize this, then it might be even harder to use the internal language since you need to juggle the syntax and its model at the same time. $\endgroup$
    – Valery Isaev
    Commented Nov 20, 2019 at 16:30

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .