Reduction

[Janno]

Rendered: https://github.com/bluerock-io/ceps/blob/janno/reduction/text/XXX-reduction.md

Note that the document does not directly propose anything yet. It is intended to serve as a collection of existing challenges. The kind of examples we collect will hopefully guide us in figuring out what exactly we want to propose.

[JasonGross]

Another reduction use case:

• reducing PHOAS passes (must be fast, integrate with Qed, and have the ability to force normalization under lambdas before later applying them) --- currently my solution is to convert to de Bruijn and back

[Janno]

currently my solution is to convert to de Bruijn and back

Does that mean you replace terms by de Bruijn indices, reduce, and then substitute back the original terms?

[JasonGross]

I have a pass that converts from PHOAS representation to de Bruijn representation and a pass that converts from de Bruijn representation to PHOAS, and I compose these passes to force reduction under lambdas. (Though there's an additional benefit to doing it this way, which is that this also works in extracted code, which an alternative reduction strategy would not.)

[MSoegtropIMC]

@Janno: thanks for the initiative and outing together the overview.

I have similar "reification with user terms" problems as you described above. I solve this with an Elpi program which produces positive symbol lists via symbol set operations (take all symbols from modules X Y z, but exclude this or that). This is easy to manage and reliable. In general I think it would make sense to have symbol set operations build into Coq.

An issue not mentioned here is using Coq by non experts and hiding everything which is not at the "user level", which is defined by a well defined set of symbols. Positive list reduction doesn't work here. Imagine I have Z in my "user level" but not positives. If I have a computation in Z which results in a literal Z I would like to do the computation. But this usually requires expanding Pos functions. One more wants a positive list of what is allowed in the final result, not on what is reduced. I don't have a good algorithm in mind for this. One way would be to set a backtracking point when one introduced symbols not in the user level and go back there if the final result is not in the user level. But I guess one could speed this up substantially by storing some meta informations on what king of symbols a reduction of a definition might contain. This also requires some sort of symbol set handling in Coq.

For debugging reduction it would help if one could ask which symbols are contained in the result instead of printing the term (a display option like "Set Printing Symbols" with a few options like naming only the modules or user defined symbol sets involved.