Best effort reification

[bakaq]

I was thinking about a reify_si_t/2 predicate that "does it's best" to safely reify a goal for use with library(reif), because this would make a lot of predicates usable with if_/3. This is the best I could come with:

:- meta_predicate reify_si_t(0, ?).

%% reify_si_t(Goal, T).
%
% Best effort reification of a goal for usage with `library(reif)`.
reify_si_t(Goal, T) :-
    (   ground(Goal) ->
        (   call(Goal) ->
            T = true
        ;   T = false
        )
    ;   instantiation_error(reify_si_t/2)
    ).

?- reify_si_t(atom_si(a), T).
   T = true.
?- reify_si_t(atom_si(1), T).
   T = false.

Is there any problem with this, and/or can this be actually be more general and not only for ground goals? I think this is fine, but I don't know if cutting the alternatives of a ground goal is sound here.

?- reify_si_t((true;false), T).
   % Is this ok?
   T = true.

[hurufu]

I'm afraid it's too simplistic to be useful. Maybe a solution is to have some sort of a database of predicate modes that are "safe", and then check against that spec:

reif_goal_spec(length(_,_)).
reif_goal_spec(maplist(A,_)) :- callable(A).

reify_si_t(G_0, T) :-
    reif_goal_spec(G_0) -> (G_0, T = true; \+ G_0, T = false); instantiation_error(reify_si_t/2).

I didn't run that code, so it can have some bugs. Also maybe it is a good idea to disallow running arbitrary goals for a reif_goal_spec/1 and use mini-language: reif_goal_spec(my_predicate(?,-,-,+))., with the default meaning of argument modes.

[bakaq]

I'm afraid it's too simplistic to be useful.

It's already useful in the sense that you wouldn't need to use low level stuff like (->)/2 to implement things like atom_si_t/2 in application code.

What you are suggesting here is really interesting though, but I think it would be better if we have a general way to add and query predicate metadata, because this would be useful for a lot of other stuff also.

[hurufu]

If the point is to reduce number of (->)/2 then I agree, those Prolog control constructs are very hard to decipher. It sometimes takes me a long time to fully understand what will happen in a complex predicate with a lot of -> and ;. If \+ is sprinkled on top it can take even longer, and sometimes the only way for me is to run that predicate in isolation to observe its solutions.

[triska]

For a sound groundness check, you can use must_be(term, T) from library(error)!

[bakaq]

Ok, with that it becomes like this:

reify_si_t(Goal, T) :-
    must_be(term, Goal),
    ( call(Goal) -> T = true ; T = false ).

Really simple! But is cutting the alternatives in call(Goal) sound for ground non-cyclic goals? I haven't been able to give a counterexample, but feels a bit wrong.

[bakaq]

Also, cyclic goals (which I never even considered could be a thing) have to be the most cursed way to do a loop in Prolog:

?- X = (portray_clause("Why does this work!!??"), call(X)), call(X).

[bakaq]

Solution with call_semidet/1 that I think is also sound. This works for non-ground goals, unlike the OP implementation. But this errors for goals that succeed more than once, even if they are ground.

call_semidet(Goal) :-
    (   call_nth(Goal, 2) ->
        error(mode_error(semidet,Goal),call_semidet/1)
    ;   once(Goal)
    ).

reify_si_t(Goal, T) :-
    ( call_semidet(Goal) -> T = true ; T = false ).

If both must_be(term, Goal) and call_semidet(Goal) are actually sound ways to do this, then I think the best we can do with a simple implementation is this:

reify_si_t(Goal, T) :-
    (   acyclic_term(Goal) ->
        (   ground(Goal) ->
            (   call(Goal) ->
                T = true
            ;   T = false
            )
        ;   call_semidet(Goal) ->
            T = true
        ;   T = false
        )
    ;   type_error(term, Goal, reify_si_t)
    ).

This is already getting a bit more complicated than I would like, but (if it is sound, which I'm still not sure) it's already very useful!

[bakaq]

By "sound" here I mean "if Goal is monotonic, then reify_si_t(Goal,T) is also monotonic".

[hurufu]

IMHO, name is too general for a very specific use-case: reification of an outcome of a semi-deterministic predicates (ground or not). Maybe something like semidet_goal_si_t or semidet_reif_si_t is better name?

[hurufu]

I have a question that is tangentially related to the OP. Is there a mathematical procedure to prove monotonicity of a predicate? For example if predicate foo/1 and bar/1 are monotonic then disjunction foo(X);bar(X) is also monotonic. My gut feeling is that any combination of monotonic predicates is monotonic, but I don't have a proof for it.

[bakaq]

Ok, I think I have some basis for my intuition that it's undecidable, at least for a definition of monotonicity that involves termination in some way. We usually say that non-termination (and errors) are fine for a monotonic predicate, and that means that a general algorithm would need to prove that "for each execution of the predicate that terminates (and doesn't error), it behaves monotonically" (for some definition of "monotonically"), and this is getting dangerously close to the halting problem, which is the undecidable problem.

[jjtolton]

I think it can be determined that it either is monotonic or not sure. It most likely cannot be easily be shown to be not monotonic in general. I have learned, for instance, that even !/0 can be used monotonically if you REALLY know what you are doing. Of course, the subset for is monotonic may not be particularly useful in general. I'm basing this off of @UWN's post, particularly regarding category 1 constructs which are monotonic without qualification and possibly up to category 7. At least mechanically, you could recursively determine with interpreter techniques whether or not a predicate resolves to these categories.

I do not think beyond category 7 it is possible in general. You would need a type system after that or a subset of Prolog only, because I suspect it is not possible even for category 8 to determine in general if a variable is properly guarded against uninstantiation without some kind of static typing.

[jjtolton]

An interesting thing to investigate might be clpz's monotonicity flag.

[jjtolton]

My intuition is that it's in general undecidable. I've been wanting to do this for quite a while:

1. Define exactly what "monotonic" means in the context of Prolog. People just use the term in a kind of informal way in analogy to things like "monotonicity of entailment" in formal logic, and the concepts often don't map too well to Prolog. This is actually very tricky, see Monotonicity of var/1 in library(diadem) #2230 for example.

I sidestepped this by just saying "that which is in the set of things up to category 7 in Ulrich's post is the set of things that are provably monotonic in general" :P

I leave the burden of proving or falsifying that statement to someone with a higher paygrade than me.

[triska]

One comment on terminology: The halting problem is indeed not decidable. However, it is semi-decidable: There is an algorithm that correctly answers every "yes"-instance of the problem ("Does this program halt?"). It is true: Problems that are not decidable are often called "undecidable", the terms are frequently used synonymously. Yet, there is a difference between semi-decidable problems and those problems that are not even semi-decidable. The latter are strictly harder.

Note that in the case of the halting problem, the "yes" instances are the "easy" instances: We can write an algorithm that always correctly detects that a program halts. The non-halting programs are the tough problems, impossible to always correctly detect with an algorithm! There is no algorithm that correctly detects all "yes"-instances of the non-halting problem ("Does this program not halt?"). For this problem (i.e., the non-halting problem), the designation undecidable truly fits.

Other examples of undecidable problems are the uniform halting problem ("Does the program halt on all inputs?") and satisfiability of first-order Horn clauses. Note that unsatisfiability of first-order Horn clauses is also not decidable, yet it is semi-decidable.

[UWN]

si means safe inference, but this here is not safe at all. It just insists on groundness. I do not think that such a generic predicate makes much sense, it rather invites to write code that is not monotonic at all.