8
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Just for the sake of clarity: are you asking whether anyone has ever rewritten a mathematical theory in the internal language of the underlying category (for using theorem prover to prove stuff on such math-theories)? Or are you interested in knowing if anyone have done model theory in the type theory (of some kind of category) ? $\endgroup$ – Giorgio Mossa Apr 10 '16 at 15:05
  • $\begingroup$ I'm not asking about work people have done in a particular internal language in a theorem prover (though references for that would be welcome). I'm asking if someone has done the work of implementing "Internal Languages" as essentially DSLs in a theorem prover so I can use the internal language for any particular model that I'm interested in and get all the benefits of a nice syntax. For CCCs this seems easy since the syntax can be easily expressed in Coq/Agda etc but Topoi seems more difficult. $\endgroup$ – Max New Apr 11 '16 at 15:22
7
$\begingroup$

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.

$\endgroup$
5
$\begingroup$

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!

$\endgroup$
  • $\begingroup$ Do you have a reference for Type Theory + Prop ~~ topos? This was my intuition but I haven't seen anyone else say it until now. $\endgroup$ – Max New Apr 9 '16 at 21:17
  • $\begingroup$ Also, for model-specific logics, specific axioms will be specific to the models but the structure of the logic overall is still just higher-order logic, right? I'm imagining that you would externally characterize features of your model (like the Next-time functor in the step-indexing paper) and then just reflect them as axioms in your internal language. Coming up with nice and complete axiomatizations would still be hard math but my hope is that the machine can automate some of the plumbing. $\endgroup$ – Max New Apr 9 '16 at 21:22
  • $\begingroup$ For step-indexing in particular it would make sense to extend the topos logic with a modal operator. This will in general be a feature of any situation in which you care about a subtopos, or you have a (co)monad that you want to study, etc. $\endgroup$ – Andrej Bauer Apr 10 '16 at 0:04
  • $\begingroup$ For the Type theory + Prop, you just stare at every rule and see that if you interpret Prop as the subobject classifier, it's all valid in a topos. $\endgroup$ – Andrej Bauer Apr 10 '16 at 0:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.