Perhaps you could clarify what you think the difference is between the “declarative”
and what you get by
If they’re not similar enough, then it’s going to be difficult using a language for the latter (details aside) to express the former.
Well to quote myself “Prolog as a language for expressing symbolic relationships, defined as a parameterised enumeration of possibilities.”. I.e. an enumeration or a search.
Not how you’d interface via Z3, AMPL, SQL and so on. You’re not defining how to prove/solve/query, just what the results should look like. Meanwhile, in Prolog you are constraining how to search as a primary concern, not what to find.
Well, what we’re actually doing is taking advantage of clever code written previously.
If the problem to be solved, can be solved elegantly using a library e.g. clpfd, then great.
The clpfd source code itself contains e.g. cuts and recursion - all the nasty things that are part of normal programming 
If there’s not yet a library to conveniently model the problem space desired in whatever someone chooses to define as “declarative” style, then writing such a library would be nice… but expect the library to contain nasty code (cuts and recursion)
Prolog is a general-purpose language - declarative aspects can be used when they conveniently present themselves (and when the programmer has sufficient intelligence and knowledge to take advantage of those opportunities). To me it is an evolution of programming, past the tedium/inflexibility of imperative programming languages, but of course it’s not the ultimate programming language.
I’m still not quite understanding your point but it sounds like you’re uncomfortable with “recursion”, which is a procedural notion, in a so-called declarative specification. But I think any pure Prolog program also has a declarative interpretation so let me try the following for this specific example.
Partial specification: merged(L1,L2,L3) is true if L1 and L2 are definite lists of the same length and the length of L2, also definite, is equal to the number of elements in L1 that are -1. (Note that I used an adjective rather than a verb as the predicate name to encourage a declarative interpretation.)
From this specification, merged([],[],[]) is true since L1 and L3 have the same length (i.e., 0) and L2’s length is equal to the number of -1’s in L1, (also 0).
From earlier posts: if merged(L1,L2,L3) is true, then merged([-1|L1],[X|L2],[X|L3]) is also true.
And if merged(L1,L2,L3) is true and X is not -1, then merged([X|L1],L2,[X|L3]) is true.
I think this is a reasonable, albeit informal, declarative specification of the predicate of interest, and nowhere did I say anything about recursion. Now it’s a straight forward step to formally write this as a pure Prolog predicate specifying the three cases when merged/3 is true:
merged([],[],[]).
merged([-1|L1],[X|L2],[X|L3]) :- merged(L1,L2,L3).
merged([X|L1],L2,[X|L3]) :- dif(X,-1), merged(L1,L2,L3).
Does this not fit your definition of a declarative specification (:- means “if” and , means “and”)? And it’s the same program as @jan posted modulo some renaming and some imprecision about the definition of L2.
The reason purity comes into play is that it enhances the ability to interpret a program declaratively since the commutative property of logical ‘and’ and ‘or’ are preserved. I can write the clauses of merged/3, and the subgoals of any clause (to the extent that it’s possible with this example), in any order without changing the declarative (or procedural, for that matter) meaning. If I introduce impure goals (ones that don’t commute) then I’m forced into a procedural interpretation since order becomes important, e.g., ‘and’ becomes the procedural ‘and-then’.
A couple of other points: constraints can be used to “convert” subgoals which don’t commute into ones which do, in order to maintain purity. And so-called green cuts have a declarative meaning of true so they can be used without sacrificing purity since their only effect is on performance (which is not a concern for the declarative interpretation).
Now all this comes to a screeching halt when you throw performance into the mix, but I don’t consider that a component of the “declarative specification” that we’ve been talking about.
Possibly the feeling of discomfort is because the recursive specification has an implicit assumption that the 3-clause merged/3 specification defines a real predicate (and isn’t just a possibly meaningless set of symbols). The 3 “partial” specifications are meaningful only if the merged/3 predicate exists.
In grad school, we spent several weeks going through various fixed-point theorems … and one day I suddenly realized that one of the fixed-point theorems that the professor had been droning on about is simply a proof that the recursive specification does indeed correspond to an actual predicate (the predicate is the “fixed point”).
The predicate, of course, might not terminate; but a separate proof-by-induction (also recursive!) can show that this 3-clause specification of merged/3 will terminate.
1 Like