Enzo Crance (Oct 26 2022 at 16:02): Enzo Crance (Oct 26 2022 at 16:02):I have a term quantifying over 5 values, and I want to substitute 4 of them and leave the last one abstracted.
Term' = (x5\ Term x1 x2 x3 x4 x5)
This triggers Non deterministic pruning, delay to be implemented. The message is unclear, what is Elpi trying to tell me here?
My guess is that it has something to do with variables dependencies: Elpi unification variables depending on x1 ... x4 would now become variables that depend on ground terms, which is forbidden in Elpi IIRC.
Enrico Tassi (Oct 26 2022 at 19:48):HO unification is a beast. The well behaved "pattern fragment" is what all \lambda Prolog implementations are built on. That is, unification variables are applied to a list of names which is duplicate free. In this case HO unification is as well behaved as FO unification is. This fragment is magic since if all terms in your program are in the fragment, then animating your program generates no terms outside the fragment at runtime. Elpi takes some liberty, and also allows unification of a variable which sees the entire context with a term which is not in the fragment. But refuses to unify a variable outside the fragment with a term. The Teyjus \lambda Prolog implementation delays such problems, since one may discover late that the variable discards the offending arguments, and the unif problem is again the good fragment. Elpi implement that (you have a command line flag for compatibility with Teyjus) but it is off in Coq-Elpi. According to my experience, most of the times it is easy to rewrirte a clause to so that the hard problems are done last in order to avoid this. Eg. a hard problem is F X = T, if you consider it before knowing what F or X are. Once you know, it may become reasonable again.
Enrico Tassi (Oct 26 2022 at 19:51):All this to say that, without looking at your code, I'm not so sure I can help you more. The unification problem you write is OK, so it is not the root of the problem.
Non deterministic pruning may suggest that Term' does not see all the variables x1 .. x4 but may see more complex terms.
Finally note that Elpi tries hard to support \eta, so your problem should be indistinguishable from Term' = Term x1 x2 x3 x4.
Enzo Crance (Oct 27 2022 at 07:42):Let me give some details to check I have understood.
Term is an Elpi multi-argument function with content, not a unification variable, but it contains some variables like X2^8 c12 c13 c14 at universe instance positions (all the rest is ground). I expected the unification problem I showed to just be a beta-reduction operation, where I give values for the arguments, not some F X = T because in my case I know F and X, it's just that F still contains some variables. So as the universe instances are still not elaborated, the variables are now X2^8 Arg1 Arg2 c14 where Arg1 Arg2 are ground terms. And this is the kind of HO problem that is in general very hard to solve, right?
A solution could be to call the Coq elaborator on the term before doing the reduction (goodbye, @pi-dummy). But I wonder if there's another way.
Enrico Tassi (Oct 27 2022 at 08:55):One way is to use prune Term []which would assert X2 sees no name, hence it is a FO term. see https://github.com/LPCIC/coq-elpi/blob/96b3a3d72f8b6d93ec6d7611c1575a056e13688e/elpi-builtin.elpi#L317
Enrico Tassi (Oct 27 2022 at 08:57):The better way would be to have Elpi support some syntax to say that a _ is FO, eg sees no context, and use the feature for universe instance variables (eg generate a pruned unif variable from the start).
Last updated: Oct 13 2024 at 01:02 UTC