>> (the assertive) "a sorted X has property p(X)".
Sure, but X is a variable, implicitly universally quantified, and p(X) <- sorted(X) is only going to be true for some values of X. Unless you apply some stricter constraints, for example, as indicated below, you can't really know for which values the relation is true.
Are you saying that, in a purely declarative context, p(X) :- sorted(X) is always true? That depends entirely on the definition of sorted/1. For instance, the following is trivially always false:
p(X):- sorted(X).
sorted(X):- false.
And the following always true:
p(X):- sorted(X).
sorted(X):- true.
Normally, sorting predicats will do something more interesting- including declaring properties of X that would probably answer your question.
I'm still a bit unsure about what you are trying to say and what you mean with inlining properties etc so apologies if I haven't addressed your concerns.
Sure, but X is a variable, implicitly universally quantified, and p(X) <- sorted(X) is only going to be true for some values of X. Unless you apply some stricter constraints, for example, as indicated below, you can't really know for which values the relation is true.
Are you saying that, in a purely declarative context, p(X) :- sorted(X) is always true? That depends entirely on the definition of sorted/1. For instance, the following is trivially always false:
And the following always true: Normally, sorting predicats will do something more interesting- including declaring properties of X that would probably answer your question.I'm still a bit unsure about what you are trying to say and what you mean with inlining properties etc so apologies if I haven't addressed your concerns.