Implementing "Internal" Languages

Question

One of the most practical consequences of the "Curry-Howard-Lambek" correspondence is that the syntax of many lambda-calucli/logics can be used to perform constructions in a sufficiently structured category.

For instance, Synthetic Differential Geometry has models in topoi that contain and embedding of the category of smooth manifolds, so you can use higher-order logic to construct smooth functions and solve differential equations.

As another example, in this paper, they notice that "step-indexing" is really just working with presheaves over the naturals (another topos), so you can use the syntax of higher order logic to define step-indexed logical relations without the tedious manipulation of steps.

Finally, Andrej Bauer shows in this MO question that you can do a lot with the "internal language" of the topos of graphs.

My question is, has anyone realized this vision literally in a theorem prover? For instance, if I show that a category I care about is Cartesian Closed, I could then move to "internal mode" where I write lambda-calculus syntax (with some model-specific axioms) and then can move back to "external mode" and manipulate them as objects in my model?

In the extreme I would even want topos theory and higher-order logic, so I could write my step-indexed logical relations without steps, or teach classical mechanics with a theorem prover using SDG. This seems to me to be a very powerful idea as someone could implement extensional dependent type theory once and provide nice tooling and then use it with wildly different applications as described above.

Answer 1

In Extending Type Theory with Forcing by Guilhem Jaber, Nicolas Tabareau and Matthieu Sozeau, 2012, intuitionistic forcing is presented as an internalization of the presheaf construction, implemented as a type-preserving translation in the style of Bernardy and Lasson's parametricity translation.

This means that you can define terms in your usual type theory, and then "translate them" into a "forcing layer" where they are interpreted as translations at a different translation type. For example, the translation induced by indexing over decreasing natural numbers lets you use your usual terms in a post-translation theory where a later modality is definable. This sounds rather close to your idea of working internally in the topos of trees.

It seems that they have a new, simpler Coq plugin implementing these ideas at CoqHott/coq-forcing, and in particular SI.v builds this forcing translation for step-indexing. Unfortunately, while it does the work of building the model, there is no example of using it for step-indexed definitions in practice (the only thing translated instead of defined in the forcing layer is Forcing Translate eq, which isn't terribly informative). You could try to experiment to see how (in)convenient this is to use.

Answer 2

If you're going to work only in the internal language then you can just use a proof assistant. There is a minor technicality of having or not having powersets, since proof assistants are typically type theories, but Coq's Prop is consistent with an interpretation of Coq in a topos.

You're suggesting however to use the machine as a sort of translation tool that would get you from the internal language to the interpretation in a model. This is a fine idea, except I think it would not be as useful as one might expect. It is true that the translation from the internal language to the model is mechanical, but unfortunately it produces convoluted translations that need a lot of massaging before they're useful. (If you ever tried to use the Lawvere-Tierney interpretation of topos logic in a sheaf topos you'll know.)

There is one more problem, namely the reverse translation. We often start with a known concept or object in the model, and would like a good description or axomatization of it in the internal language. This is typically hard work and real math. I do not see how current proof assistants could help.

On the technical side of things one would have to worry about formalizing:

• the syntax and the rules of the internal language
• the model
• the interpretation

That is a lot of work, too. Some projects along these lines have been done (for instance the interpretation of $\lambda$-calculus in a cartesian closed category). I am not aware of anyone formalizing toposes, for instance.

In summary, using a proof assistant to help check that you're not doing anything wrong in the internal language is a good idea (in fact, it is a very good idea, as attested by homotopy type theory, where we used Coq and Agda to develop new theorems which were only later unformalized into English), but using it to get statements about models is unlikely to work without a lot of extra work. Which is not to say that you shouldn't try!