search

RedPRL / sml-redprl

The People's Refinement Logic
http://www.redprl.org/
MIT License
227 stars 18 forks source link

Ideas for derivations/extraction #2

Closed jonsterling closed 8 years ago

jonsterling commented 8 years ago

In JonPRL, we constructed explicit derivations as the syntheses of the sequent judgment, rather than merely extracting programs. This was perhaps useful for a couple reasons:

  1. It was helpful for debugging.
  2. It helped dispel the myth that PRLs have only programs, but not proofs
  3. @vrahli was planning to translate the JonPRL derivations to Coq, so that they could be checked against the Nuprl in Coq development.

However, there's some serious problems with producing concrete derivation:

  1. It's a duplication of work and it is not clear what use it is: the refiner is the definition of the logic, and so the proof is already present (but it exists spread out in time, rather than in a single location). In some sense, when you start from a semantical perspective like we do, the proof theory is pretty arbitrary, so it is not clear to me what sense it makes to set it in stone in the grammar of our language.
  2. It is likely to become unwieldy for large proofs. It's very plausible that we could come up with a proof that we can execute, but which we cannot easily store in memory. There's a lovely example of this in the Chalmers Cubical implementation here, where a particular approach to proving univalence results in absolutely outrageous memory usage.
  3. It is a pain to implement!

Does anyone have any thoughts on what ought to be done here? I'm inclined to abandon the construction of explicit derivations, because I don't see much use in it. But I also don't want to scuttle any of @vrahli's intended work; however, I do not know whether there is even anymore any potential for checking Red JonPRL derivations in Coq, because we actually are implementing a different type theory from Nuprl:

@jozefg

jozefg commented 8 years ago

Of course the slickest thing would be to have this be some how optional, like you could run jonprl --skeptical my-dev.jonprl and have it print out evidence. One interesting option would be to see if we can implement this with functors somehow... Like we have all the evidence built up behind a signature with one implementation. One is an actual ABT and let's you construct the evidence as we have it right now and the other is just unit and doesn't cost anything.

Then the refiner just pokes and prods this interface and you can vary the refiner to use a different "evidence" module.. Maybe this is just overkill. Personally I like evidence because I think it makes for a good answer to "what's the trusted base of JonPRL" and it may/may not be helpful to implement separate compilation? Maybe? Not sure..

jonsterling commented 8 years ago

I like your idea about using functors... We'd essentially separate the implementation of the correctness conditions of the judgments from their synthesis; then, in one version of the "synthesizer", an extract term would be produced, and in another version of the synthesizer, a derivation would be produced.

One possible issue is that when we introduce dependent refinement, we'll need a way to "quote" the synthesis of a judgment back into a program; I suppose that in the main synthesizer, this would be the identity, whereas in the derivation synthesizer, we would need to implement extraction (again). In fact, we could probably arrange things such that when it needs to extract a program, the derivation synthesizer could shell out to the main synthesizer.

My personal feeling is that the presence of concrete derivations is totally irrelevant to the question of "what's the trusted base of JonPRL" (because the trusted base is literally the refiner itself; and if the refiner did not produce even any extracts, this would not change the fact that it is the trusted basis). However, it is very difficult to explain this to people, since they are used to a tradition where you have a typechecker, and then a refiner is just a technical instrument that is used to produce terms that will be fed into the typechecker. So, it is probably useful PR-wise to have the ability to produce derivations.

I think maybe what we ought to do, then, is to factor this as you suggested, but not necessarily implement the derivation-synthesizer until we need it.