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.

[silene]

Suggested change

	It is incompatible with `vm_compute` and `native_compute`.

[Janno]

Thanks for looking at the draft!

I just remembered and re-read your comment in coq/coq#13881 (comment). I suppose there really is no way to return unreduced terms from vm_compute, is there?

In any case, I'll probably try to expand on "incompatible" a little bit. It seems to me that at least some vm casts could be preserved in terms that use MSP with enough care.

[silene]

Currently no, but that does not mean that it is that farfetched.

First, the VM is already able to manipulate and return axioms, existential variables, and free variables (which are fully normalized values, but from an operational point of view, they are fully unreduced terms). So, extending accumulators to support arbitrary Gallina term is trivial. One has to be a bit careful with open terms so that bound values are properly kept around. But, accumulators are already able to accumulate information (hence their name), so no major change here either.

Second, if the reduction is only delayed rather than just fully blocked, one has to make sure that the bytecode is still around to restart the reduction. But again, the VM already supports similar patterns, e.g., for the return clause of match constructs. The kernel even has some mechanisms to ensure that Gallina terms and their corresponding bytecode stay synchronized, because this is needed when caching weakly-reduced toplevel definitions (though, this fragile piece of code is probably not exercised as much as it should be).

The hardest part will be to make sure that the Gallina term in the accumulator and the corresponding bytecode agree on what the bound variables are. Currently, there is absolutely no similar mechanism in the bytecode compiler. To give a concrete example, consider

Definition foo x := let y := x in block (x + y).

The blocked Gallina term has two bound variables (x and y), while the corresponding bytecode has only one bound value x (y was optimized away by the compiler). Restarting the reduction by pushing two values on the VM stack would quickly lead to a memory corruption.

[Janno]

Thank you very much for the detailed explanation. Are there already plans/ideas for handling the binder discrepancies?

Somewhat orthogonal: It just occurred to me while trying to explain this to coworkers that both vm_compute and native_compute are currently trivially compatible with MSP. MSP must not (and does not) change the normal forms of terms and both vm_compute and native_compute perform full normalization. The only difference from MSP is in the result of weak head reduction (and even there it only changes the shape of arguments to the head constructor/constant/etc, not to the head itself). I should expand on this a bit in this document to avoid confusion.

So until vm_compute/native_compute supports weak head reduction I don't think they are affected at all. All we need is to treat the primitives as boxing/unboxing operators of some box type.

[silene]

Are there already plans/ideas for handling the binder discrepancies?

No. In fact, last time I suggested that the bytecode compiler should handle let-in constructs in a slightly more predictable way, the idea did not live long: coq/coq#13234

[aspiwack]

MSP must not (and does not) change the normal forms of terms and both vm_compute and native_compute perform full normalization

If this is the intention, then support un vm_compute is Very Easy™ (I don't remember how native compute works, but I don't see why it would be a problem). You simply reserve one extra tag, and otherwise compile block t like fun x => t (better: compile it as a 0-argument closure), so that block t is a weak-head normal form. When it comes to reconstruction, force the closure and evaluate t (which is exactly what you do with functions). This should let you control the order of reduction as you need (I say “should” because your document doesn't really specify the semantics of block/unblock/run (it should!)).

You need to use a different tag for block t than for fun x => t because it's going to behave differently (e.g. the normal form of fun x => t is fun x => t', but if I understand correctly, the normal form of block t is t' (in both case I take t' to be the normal form of t)).

Supporting weak-head reduction in the VM is essentially the same problem as @silene describes above. Normalisation-by-evaluation really is a surprising sweet spot: you simplify the problem a lot when you're only asking to reconstruct normal-form terms.

[Janno]

(I say “should” because your document doesn't really specify the semantics of block/unblock/run (it should!)).

Sorry for that. I actually opened this PR way too early by accident and that's why the document is still in pretty rudimentary shape. The actual idea was to pass around a draft (in the form of a PR against a fork of this repo, not this repo directly) in order to collect additional challenging use cases for reduction before we (possibly) resume work on discussing/specifying/implementing MSP (and kred). But I somehow ended up targeting the wrong repo and now I am getting super useful feedback here so I really want keep this PR open.

I'll update the document with some more details on MSP next week. For now, the best summary is the old prototype itself. The PR description is probably slightly outdated but the code was very close to the desired semantics. The primitives are in theories/Force/Force.v and there are tests that should be helpful to illustrate the intended spec in test-suite/success/force.v

Your description of supporting MSP in the absence of weak-head reduction sounds correct to me except that block t simply reduces to block t'. @block T t has type Blocked T which can be thought of a record containing T. Both unblock and run function as projections in this simplified view. I don't remember the exact reason but Blocked T cannot be convertible to T. It probably involves canonicity.

This should let you control the order of reduction as you need

I really wonder if this could end up helping simplify the discussion around bytecode compilation/optimization. I see that coq/coq#13234 contains strong arguments for pattern matching being the only viable solution for predictable reduction performance and that also matches my personal experience (although I can almost never use vm_compute so I don't know much about the performance pitfalls there). MSP would indeed be one possible way to specify the order of reduction even in vm_compute. If that could help simplify the bytecode compilation by making some "optimizations" unnecessary, maybe it could also make implementing weak-head reduction easier in the long run by keeping the bytecode very close to the original terms. (Weak-head reduction in vm_compute would be incredibly useful independently of anything discussed here.)

[silene]

MSP would indeed be one possible way to specify the order of reduction even in vm_compute. If that could help simplify the bytecode compilation by making some "optimizations" unnecessary

MSP does not make the above optimization unnecessary. (The only purpose of this optimization is to allow the garbage collector to free memory earlier in some very rare cases. This optimization is not even part of OCaml's bytecode compiler, for good reasons. It is specific to Coq.) And except for peephole ones, there is no other optimization in the bytecode compiler anyway. So, MSP and bytecode optimizations are two completely separate issues.

[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.