Goal expansion in lib reif

[hurufu]

I've searched for a task that is marked as "good first issue" and can be done purely in Prolog, and I think issue 977 was the only one, but it is already claimed. I've reached out to @sblaplace and it told that it is Ok, we can continue to work on it together or me alone, I'm open for any combination of work.

Now, let me describe current state. Currently it is a draft and it has debug code which I will remove.

What was done:

• goal_expansion/2 and predicates that it relies upon were copied from the source1.
• Benchmark code was also copied from there2 and slightly modified, there is a separate task for statistics/2 predicate, but it also needs to be written in Rust and I don't know it. Benchmark can be run from shell command line:

  time scryer-prolog -g 'use_module(library(memberbench)),run,halt.'

  I will remove benchmarking code when task will be done.
• Replaced not working predicate_property/2 invocation with an exception. Another task shall be created for that predicate, it also requires some Rust knowledge.
• Added comments for old and new predicates
• Added unit tests to capture current behavior, so I can change it without worrying so much. Just call reif:testall to run them. I can remove them if they don't comply with module guidelines.
• Added some debug prints to be able to inspect goal expansion, should be removed and replaced with unit tests.

And now the most important point, after all of this I didn't observe any noticeable performance improvement! Am I doing something completely wrong?

[triska]

Thank you a lot for working on this, I greatly appreciate your interest in improving library(reif), and I think many Prolog programmers will eventually benefit from this!

There may well be mistakes in the underlying expansion mechanism of the Prolog engine itself, and such experiments are well suited for finding such issues.

As one immediate comment on the PR itself: Could you please separate the documentation changes from the goal expansion changes? The documentation of library(reif) was most recently discussed in #2407, and the DocLog comments turned out not to be a good fit for documenting this library. I think at least for the time being, it is best to refer directly to the paper, and at the very least to discuss the documentation changes in isolation. I think giving examples for the use of these predicates might indeed be a good idea, best discussed in a separate PR so that we can focus on the expansion mechanism here. Thank you a lot!

[triska]

And now the most important point, after all of this I didn't observe any noticeable performance improvement! Am I doing something completely wrong?

One important test would to check whether the expansion is correctly applied: You can do that by using if_/3 (for example) in a predicate that is declared dynamic with the dynamic/1 directive, and then use clause/2 to inspect the source code, checking whether the expansion is correctly applied. Ideally this is also one aspect ensured by the test suite. You can also use listing/1 from library(format) to display the source of the predicate. For instance, to show a working expansion of library(clpz):

:- use_module(library(clpz)).
:- use_module(library(format)).

:- dynamic(p/2).

p(X, Y) :-
        X #< Y.

Yielding:

?- listing(p/2).
p(A,B) :-
   (  integer(B) ->
      (  integer(A) ->
         B>=A+1
      ;  C is B,
         clpz:clpz_geq(C,A+1)
      )
   ;  integer(A) ->
      D is A+1,
      clpz:clpz_geq(B,D)
   ;  clpz:clpz_geq(B,A+1)
   ).
   true.

[hurufu]

Thanks,

1. I wasn't aware of Docs for library(reif) #2407, sure I can remove documentation from this PR.
2. Ok, so it seems like I need to dig deeper

[UWN]

The expansion in the cited source (happens to) work for SICStus. The variation for SWI works for the examples in the paper. It fails to expand more complex examples. This is partially due to the incompatibilities of module systems. I am not very fond of the expansion code as such and I hope that we might find a cleaner way of doing it which might provide a mechanism that can be used in other code as well. One particular aspect that should be covered is the exact ISO semantics (and thus their errors) of term-to-body conversion.

In any case, the text of Scryer's library(reif) was apparently manually copied and rewritten. The history of edits of meta_predicate declarations, four spaces of indentation instead of the original three, the non-canonical superfluous single quotes around the reified or ';' suggest this.

[triska]

In any case, the text of Scryer's library(reif) was apparently manually copied and rewritten.

I think it would be good to start with restoring the canonical library(reif) straight from the original source as the basis for these changes, this will also make it easier to see what exactly must be changed for Scryer. In this way, also future improvements of library(reif) can be more easily incorporated.

[hurufu]

I think it would be good to start with restoring the canonical library(reif) straight from the original source as the basis for these changes, this will also make it easier to see what exactly must be changed for Scryer. [...]

Funny thing this is how I actually started work on this task, I first modified reif.pl from Scryer to look as close as possible as reif.pl from the original source, and then after inspection I converted it back ;)

[triska]

library(reif) was first added to Scryer more than 5 years ago in b7dd76b, long before Scryer had fully conforming Prolog syntax, a meta_predicate/1 declaration, goal expansion and many other features that are needed to run the actual source of the library. Who has their priorities in order to focus on first implementing the correct fundamentals instead of adding an ad hoc bowdlerization of the library? Certainly not us! But now many of the fundamentals are in place, and it is worth trying to make the original source working!

[hurufu]

Thank you all for help, the problem was that expansion wasn't correctly applied because of (:)/2 and module system incompatibilities.

With the latest commit it seems to work well, here are some benchmarks:

en_memberchk/3:   t=0.010s    % The fastest possible implementation
en_memberd_ifc/3: t=0.030s    % Without goal expansion
en_memberd_ifc/3: t=0.012s    % After goal expansion

I will remove my debug code, maybe write some other benchmarks and this PR is now ready for a discussion on how to wrap it up.

Questions:

1. Should I reformat it exactly as it was done in the original implementation?
2. Should I remove memberbench.pl or is it better to be incorporated into unit tests perhaps?
3. What to do with my ad-hoc unit tests? I think they also might be removed, but on the other hand they are helpful.
4. I see some space to improve the code:
   a. Reduce code duplication
   b. Try harder with elimination of all call/n predicates if possible
5. What to do with statistics/2? It is nice to have for benchmarks, my implementation is very crude and must be removed, but real implementation isn't ready yet.
6. There are some FIXME and TODO items, that needs to be addressed.

[triska]

Thank you so much for working on this, and congratulations on these awesome results!

Regarding the remaining questions, my personal opinion:

1. It is a very worthwhile goal to keep as closely to the original source as possible. This allows us to tell easily (with diff) what exactly is changed specifically for Scryer, and therefore also where Scryer could consider following SICStus more closely for better compatibility. I strongly recommend to keep the differences with the canonical source of library(reif), mentioned in the publication, as small as you possibly can.
2. Good and systematically exhausting tests are very important, I highly recommend to think about tests that test the library as extensively as possible, and maybe also consider whether test cases can be generated and run automatically, so that you only have to start a program and keep it running day and night to test the library and also the expansion day in day out, as long as you want. Tests that run only for a finite amount of time can be added to the src/tests directory of the distribution.
   3. statistics/2 does not occur in library(reif), this is an issue that seems completely separate from the present discussion and should in my opinion be discussed separately, for example in statistics/2 would be useful for benchmarking #321). Until statistics/2 becomes available, you can use the existing predicate time/1 from library(time) for benchmarking. Update: statistics/2 is provided via ADDED: Preliminary support for statistics/2. #2440.

[UWN]

There are a lot of unclear things related. Like:

• the role of goal expansion as such. Does it have to be equivalent? Equivalent in what sense? Some years ago in SWI, I was stuck with goal expansion and clpfd for diadem where the expansion into impure code (with nonvar and such) made it impossible to produce clean generalizations

• the precise formalism to express such expansions. I somewhat hope that there will be one which also could address expansions for library(lambda) but in the meantime I prefer a correct and inefficient implementation before an ad hoc implementation

[UWN]

Further,

• the update semantics of static code. In ISO, we have just the notion of preparation for execution, but there is no indication how to update static code. SICStus offers to abolish predicates separately, but this makes optimizations such as these goal expansions effectively impossible. Once we update the code for the goal expansion, effectively all code that used that goal expansion is somehow invalid.

[hurufu]

[...] Once we update the code for the goal expansion, effectively all code that used that goal expansion is somehow invalid.

I think it might be possible to implement runtime toggle for strict ISO conformance for certification for example, but give users a relaxed default. I'm not sure how this proposal goes with Scryer Prolog spirit though.

[UWN]

As for conformity there is an extension mechanism (5.5, 5.1 e).

The problem behind is that the update semantics of SICStus prevents many optimizations that should remain user transparent (like inlining/unfolding simple goals), and at the same time does not prevent inconsistencies due to updating goal expansion.

Ideally some larger chunks could only be updated together in one fell swoop. Or somehow dependencies are registered that enable a clean recompilation.

[triska]

I have added a preliminary version of statistics/2 in #2440 so that the benchmarks work as expected and with as few modifications as possible!

[triska]

This is starting to look very good, very closely following the master copy of reif.pl! Well done!

I still note the following differences that I think can safely be eliminated by using the original code in these places:

157,160c161,162
<          ;  nonvar(T) -> throw(error(type_error(boolean,T),
<                                type_error(call(If_1,T),2,boolean,T)))
<          ;  throw(error(instantiation_error,
<                                instantiation_error(call(If_1,T),2)))
---
>          ;  nonvar(T) -> throw(error(type_error(boolean,T),_))
>          ;  throw(error(instantiation_error,_))
224,226c226,227
<    ;  nonvar(T) -> throw(error(type_error(boolean,T),
<                                type_error(call(If_1,T),2,boolean,T)))
<    ;  throw(error(instantiation_error,instantiation_error(call(If_1,T),2)))
---
>    ;  nonvar(T) -> throw(error(type_error(boolean,T),_))
>    ;  throw(error(instantiation_error,_))

[hurufu]

I still note the following differences that I think can safely be eliminated by using the original code in these places: [...]

I never knew what to put into the last argument of error/2, on SWI they say to leave it unbound, because it is used for stack trace.

P.S. I have much less free time than I thought, I'll try to finalize this PR soon.

[triska]

Thank you a lot, this is starting to look very good! To make the changes easier to track, could you please, in a final step, reduce the changes to their essence? I think a few commits would suffice, such as:

1. replace reif.pl with the master copy
2. make the Scryer-specific changes to reif.pl (in a small number of commits, maybe even only one commit)
3. add the benchmarks and test cases for library(reif)

This would make it very easy to follow the development, also later. I think an easy way to merge, drop and reorder existing commits is to use git rebase -i origin/master. Thank you a lot!

[UWN]

not sure it makes sense to produce such ad-hoc extra information. If, at all, it would make sense to have here a pair-list for various extra information. But this hard-coded version does not fit into the remaining setting

[hurufu]

I think it is ready for a review. I don't know if I need to write more tests, I like the idea of property testing, but I will need to write the whole framework to do it correctly, and it is way outside of scope of this ticket. There is also room for improvement as not all instances of call/N are expanded as shown in some of the unit tests (I don't quite know how it will interact with the module system though).

Original memberbench.pl also works, with just minor adaptations, but it doesn't fit into Scryer's benchmark framework.

Edit: What to do with the last argument to error/2, should I keep them as per SICStus documentation or remove them?

[triska]

Thank you a lot for working on this!

I understand these changes are meant to address the first point above? What about the other two issues though, for example, what if 1 occurs at the position of a goal, as in (a,1,b)? A faithful expansion must preserve the exact behaviour we would observe without the expansion, is this ensured?

[hurufu]

Yes, I think I've fixed all those issues, maybe I need to write more test cases, but I test at least the following code:

\+ cut_contained((a,b;1), _)

That means that cut_contained/2 must fail thus causing goal expansion mechanism to skip expanding current if_/3

[triska]

Should I squash all commits that add on-top of just porting the original library?

Regarding this point: Personally, I think it is best structured as: (1) one commit that introduces the canonical library(reif), and (2) another commit that adds the goal expansion. The goal expansion can also be introduced in more than one commit, if the changes are incremental and in a sense monotonically building up. (For instance: One commit for the expansion, another commit for a set of test cases, and another commit for an exhaustive search for counterexamples etc.). In this way, it is clear what is now actually added or modified on top of the canonical library(reif).

What would not make sense, at least in my opinion, is to introduce multiple commits with back-and-forth changes of approaches and already obsolete and superseded changes into master. There may be intermittently a sequence of back-and-forth commits in the branch of the PR, arising in the course of this discussion as different approaches are tried and various issues are discussed, but I see no need to introduce this then also to master after it is finally clear how to best resolve it. The final commit message can explain the trade-offs and everything worth knowing in detail, and it can also explain what doesn't work and why.

[triska]

Is it possible to fix it generically?

What exactly is the property we are interested in? Maybe whether it contains, or might contain, !/0 is only a part of the interesting conditions? It seems the interesting property, as a rough guess, is whether "inlining" a predicate is possible without changing the semantics of the predicate where the goal is being inlined? (Or something else?) If so, then maybe a better name and more general property for this can be defined that may also be interesting for other modules, such as library(dcgs).

[triska]

Is it a good idea to throw a non-standard stop(_) term?

Personally, I see no issue with this, at least not in this case: This exception term is locally thrown and caught, with no possibility of interference into or from application code that throws a ball with the same shape.

[triska]

Is loader a good place for cut_contained/2?

Personally, I think there may be a better location, and also better name if we can find out which property is actually essential here. From the comments in the original library(reif), it seems it's not only about !/0 but also about Prolog terms that contain non-callable things such as integers, and also variables.

[hurufu]

Is it possible to fix it generically?

What exactly is the property we are interested in? Maybe whether it contains, or might contain, !/0 is only a part of the interesting conditions? It seems the interesting property, as a rough guess, is whether "inlining" a predicate is possible without changing the semantics of the predicate where the goal is being inlined? (Or something else?) If so, then maybe a better name and more general property for this can be defined that may also be interesting for other modules, such as library(dcgs).

tldr version: I don't know in general case is it safe to skip a particular goal expansion even if I've detected cut in it in a callable position.

---

I wanted to solve it in loader module, to universally prevent unsafe goal expansions that might expand scope of !/0, but it proved too hard (at least for me), because I lacked information about what is the intention behind any given expansion and crucial is it Ok to skip it? Consider for example:

foo:goal_expansion(maplist(A, B), X) :-  ... .

Here the goal expansion expands maplist/2 to something else – doesn't matter. How do I know in the loader module if users wishes to block-off side-effects of cut or not? Loader doesn't have information about intent of a goal expansion, and either I need a static list of known expansion rules that needs this sort of protection or to do a complex analysis of result after goal expansion is applied to deduce if it might or might not interfere with outer goals...

It would be nice to mark some expansion as "inline only" – this information will be enough.

[hurufu]

Also wrapping goal in a call in general case is kinda hard too. Consider a meta-predicate foo/1 which is marked as :- meta_predicate(foo(0)).. And for which there is a registered goal expansion rule. What should I do in a loader module if it encounters something like this:

foo(foo(foo(!);foo(true;true))).

I need to recursively descent into it while verifying every meta-predicate declaration and possible module specifiers and whatnot. It becomes quite hairy, because goals can be arbitrarily complex.

I still want to solve this problem, but I decided to have at least something earlier :)

[triska]

Maybe it helps a bit with this: The goal is to do goal expansion of library(reif) predicates correctly. This does not mean that everything needs to be expanded to the maximum possible extent. It seems that most code that appears in actual programs will make it possible to safely apply the expansion. If the expansion works for that "safe" part, and that part is always correctly detected, and at the same time the expansion is reliably prevented in all situations that may yield wrong results if the expansion were applied, then I would consider that a solid and very promising initial version. Maybe you are aiming for that in any case already, in which case please consider this comment redundant.

[triska]

It would be nice to mark some expansion as "inline only" – this information will be enough.

It seems this is a candidate for an improved expansion mechanism, which we need in any case? (#2532)

[hurufu]

I've rebased everything onto the latest master and squashed some commits and I left only commits which add distinct functionality

[UWN]

?- cut_contained(1,G_0).
   false.
?- cut_contained((1->true),G_0).
   G_0 = (1->true).
?- cut_contained((1,true),G_0).
   false.

How does this fit together? Name, documentation, and behaviour

[hurufu]

I agree, name isn't good. The idea behind it is following:

• If either G_0 or S_0 is an invalid goal (contains numbers in callable positions or free variables or cyclic terms) the predicate fails.
• If G_0 contains an unsafe use of cut (a, !) or similar then S_0 = call(G_0).
• Otherwise S_0 = G_0

I will fix an example provided by you, it is because I ignore left argument of _ -> A term, which clearly shouldn't be ignored.

What is the good name for it? Maybe something like goal_sanitizied or term_goal or term_safe_goal... idk.

[UWN]

p(X) :- if_(1=2,true,(!,X=a)) ; X = b.

?- p(b).
   false, unexpected
   true. % expected, but not found

Please reconsider your approach: This ad hoc fixing leads to the creation of niches for bugs to reside — until they hit.

I believe that it would be better to perform the expansion always, and then take another (general) step to remove all those unnecessary call/2 and call/1s.

[hurufu]

Ok, I think I understand what you mean. Basically to remove call elimination code in libreif and do it universally in the loader for all goals – if call is sufficiently instantiated during compilation it shall be universally unwrapped: call(a, B) ==> a(B).

[hurufu]

I think it can be solved using goal expansion (after fixing unfortunate cuts_outside/1):

safe_goal(G) :- goal_sanitized(G, G).

user:goal_expansion(call(G_0), G) :-
    loader:complete_partial_goal(0, G_0, _, [], G),
    safe_goal(G).

user:goal_expansion(call(G_1,A), G) :-
    loader:complete_partial_goal(1, G_1, _, [A], G),
    safe_goal(G).
    
user:goal_expansion(call(G_2,A,B), G) :-
    loader:complete_partial_goal(2, G_2, _, [A,B], G),
    safe_goal(G).

user:goal_expansion(call(G_3,A,B,C), G) :-
    loader:complete_partial_goal(3, G_3, _, [A,B,C], G),
    safe_goal(G).

[hurufu]

I have fixed examples that were provided. It was mostly because I didn't validate some subterms.

Regarding latest note about call/1 and call/2 safe elimination applied globally. I will take a look into it. This probably will mean discarding a lot of changes, but overall it should be a more clear design.

[hurufu]

I've played a little bit with universal call/N elimination and it works in most cases, but I think it is major modification of what is and what isn't expanded and it far exceeds original scope of task marked as "good first issue" ;)

So I moved this task to "draft" state again. Hopefully in future months I'll have more time to think about it.