Has the notion of 'semidet' in Prolog been settled?
That's a really excellent question!
From the Mercury determinism categories where this is also explained quite authoritatively:
6.1 Determinism categories
For each mode of a predicate or function, we categorise that mode according to how many times it can succeed, and whether or not it can fail before producing its first solution.
If all possible calls to a particular mode of a predicate or function which return to the caller (calls which terminate, do not throw an exception and do not cause a fatal runtime error)
- have exactly one solution, then that mode is deterministic (det);
- either have no solutions or have one solution, then that mode is semideterministic (semidet);
- have at least one solution but may have more, then that mode is multisolution (multi);
- have zero or more solutions, then that mode is nondeterministic (nondet);
- have exactly zero solutions, i.e, fail without producing a solution, then that mode has a determinism of failure (failure).
(emphases mine)
Note that whether or not a choice point is left is not even mentioned in this definition, nor in the whole section. Mercury is not the same as Prolog, but the point is that this definition is in principle 100% applicable also to Prolog. Clearly, it then corresponds to your variant (1).
In my opinion, this is right in this way: Whether or not a choice point is left is rather immaterial, and depends on—for example—how powerful and versatile your system's argument indexing is. A good indexing scheme may prevent the creation of choice points that other systems introduce. A notion that depends on particular idiosyncrasies of a specific Prolog system and may break from one version to the next (with the introduction of better argument indexing etc.) is not very robust, and not of much value.
It is true that we often say "the predicate is deterministic" when we mean: "the predicate is deterministic and no choice points are left", but even so the main point is almost always also in such cases that the predicate succeeds exactly once. Note that "deterministic" is a rather overloaded adjective with other meanings too. In the SWI documentation, this ambiguity carries over to semi deterministic. However, even SWI back-pedals a bit from this rather implementation-oriented definition in other places:
2.2.2 Testing semi-deterministic predicates
Semi-deterministic predicates are predicates that either fail or succeed exactly once and, for well behaved predicates, leave no choicepoints.
So a semi-deterministic predicate that is not well behaved (?) can also leave choice points...
In the discussion, note especially the following: Ulrich is here using the weaker and more robust notion to obtain a predicate that is applicable for both definitions.
So, no matter which variant you pick, call_semidet/1
is useful! From this, the meaning of the quote becomes clearer. When Ulrich says:
(The implementation might be improved, but prior to optimizing and bechnmarking the actual meaning needs to be settled.)
it is evidently not meant that the meaning of "semidet" must be settled between the two variants, but that it should first be clear what call_semidet/1
actually guarantees: It is a lot more useful than what people thought Ulrich posted. For example, the definition that Jan gives:
call_semidet(Goal) :- call_cleanup(Goal, Det=true), ( Det == true -> true ; throw(error(mode_error(semidet,Goal),_)) ).
works only with your second definition of "semidet".
The classification currently being used e.g. in SWI-Prolog is, as @mat mentioned, taken from Mercury. The mode names used (det
, semidet
, multi
, and nondet
) are very poor (and also insufficient) choices. They are not only abbreviations but require new users to lookup the documentation to understand their meaning! Ironically, the description of the meaning of each of these modes already suggests the best non-abbreviated and clear names. Remembering that we're talking about the number of solutions: zero
, one
, zero_or_one
, zero_or_more
, one_or_more
(and possibly, due to its usefulness, error
, which can be used to indicate that a given call mode results in an error). These are, btw, the mode names in use in Logtalk.
Mixing the specification of the number of solutions for a predicate (in a given mode) with issues with leftover choice-points is also a poor choice, ridden with ambiguity, as @mat also described. Code optimization issues are orthogonal to the specification of the number of solutions. Also, any mode other than zero
may leave a spurious choice-point when the solutions are exhausted. Thus, this is more general than just a distinction between the poorly named det
and semidet
modes.