Determinism [or other] specifiers beyond those of Covington &al Table 2?

[dcnorris]

The Further Reading on this page of @triska's The Power of Prolog mentions Coding Guidelines for Prolog by Covington &al, from which I reproduce the following:

Table 2. Predicate determinism specifiers for the template of Figure 4

---

• det Must succeed exactly once and leave no choice-points.
• semidet Must either fail or succeed exactly once and leave no choice-points.
• multi Must succeed at least once but may leave choice-points on the last success.
• nondet May either fail or succeed any number of times and may leave choice-points on last success.

---

These are to be used in documentation headers such as,

%% remove_duplicates(+List, -Processed_List) is det
%
% Removes the duplicates in List, giving Processed_List.
% Elements are considered to match if they can
% be unified with each other; thus, a partly uninstantiated
% element may become further instantiated during testing.
% If several elements match, the last of them is preserved

Questions:

1. Is there a richer or more precise set of determinism specifiers one might use? For example, what if you don't leave choice-points on last success of a multi predicate?
2. Is there a better or orthogonal set of specifiers, dealing with various forms of the algebraic properties we aim to preserve by using pure Prolog?

My basic hope is that, by adopting a highly evolved documentation convention I might force myself deliberately and consistently to consider the most important properties of each predicate I write.

[hurufu]

IMO determinism is dependent on the mode in which predicate is used, so it might all be true: foo(-A) is nondet. and foo(+A) is semidet.

[hurufu]

Also it would be interesting to document exceptions...

[dcnorris]

Indeed, on p.22 Covington &al give an example of documenting mode-dependent determinism:

The basic template can easily be extended to deal with multiple modes, e.g.,

%% age(+Name:atom, -Age:integer) is semidet
%% age(-Name:atom, +Age:integer) is nondet
%
% ...

[hurufu]

Is there a standard convention to mark non-terminating predicates? For example that will give couple of answer and then will loop forever.

[hurufu]

Also, number of answers and choice points depends on selected evaluation strategy, for example enabling tabling may improve determinism of a given predicate...

[UWN]

Questions:

1. Is there a richer or more precise set of determinism specifiers ...

All these specifiers come from Mercury and are highly procedural leading to code such as the one you mention. There is not even an attempt to state under what conditions the predicate has a declarative meaning.

There are somewhat related declarative properties, like functional dependency. So far rather unbeknownst to Prolog.

[dcnorris]

I'd read Date's Relational Databases book back in the late 90's, and was impressed at the time by how well-developed the theory was, mathematically — with what seemed to me nontrivial theorems e.g. about normalization. How strange that I haven't connected any of that with my Prolog programming! When you talk about 'algebraic properties', are you then invoking principally relational algebra?

[UWN]

invoking principally relational algebra?

I would not go that far to embrace all of it. But at least there are many useful properties that only rely on declarative (that is oriented around the notion of set of solutions) notions and not procedural ones that are (I believe) more useful than the highly procedural properties you mentioned and which are still closely related.

[hurufu]

I was writing some code recently and it just occurred to me. Is it a sane idea to document the class of a relation?

%% length(List, Integer) is bijection.
%
length([], 0).
length([_|T], N) :- ... .

UPDT: length/2 isn't the best example, because infinitely many lists correspond to any given integer, but still maybe for some other relations it makes sense.

[bakaq]

This is interesting, but length/2 in specific isn't a bijection. length(Ls, 1) has infinite solutions for example, while it would only have 1 if it was a bijection. length/2 is indeed a function though (because it's functional and total).

[dcnorris]

What if [a properly chosen set of] designators could be treated like holes in a proof assistant? You could then state what designators you require for an implementation, and a proof engine would go to work to show what properties need to be asserted for sub-predicates.

(I'm thinking along lines of #2722.)