Lambda the Ultimate

Done.

Non-declarative style means I'm writing it all up myself from scratch.

Declarative could be seen in some sense as taking that non-declarative engine and putting a DSL in front of it. If the engine does what you want then great! But otherwise of course it won't work well as-is and will have to be manhandled. No surprise?

What would be claimed to be any gordian knot end-run around this seems-to-little-me fact of life?

or, Are there accidental complexities in Prolog that somewhat go away with this approach instead? Or other approaches?

The paper seems to be, in part, about FP embeddings, which is a generalization. Approaches like supercompilation and SMT solvers get at optimized search for generalized domains like that. I agree automation here isn't easy: the synthesis community is tackling it, but experiences so far suggests hints and DSLs like sketching go a long way.

Indeed, from the synthesis mentality, most languages are equivalent (they compile language-of-the-week, including FPs, to constraints), so embeddings are almost an implementation/usability choice. The linguistic challenges are on efficient translations or primitives/DSLs for guidance (e.g., sketching).

Compiling language of the week of constraints sounds intriguing - any reference to somewhere where I can read more about that?

http://homes.cs.washington.edu/~emina/

This is more about DSLs, but you can find surrounding literature from here working with C, SQL, Java, etc.

Thanks!

Implementing search strategies or tactics can be very nice to the extent they're easily composed, reused, and abstracted. I wonder if the approach presented here would be more amenable to such treatment.

In what way is Datalog forward-chaining?

Datalog programs can be solved via forward chaining, though they don't require it.

Do you mean bottom up evaluation (eg with magic sets)? I thought that was distinct to forward-chaining (as in Rete) where you derive all consequences of facts as they are added to the KB, rather than searching (forwards or backwards) to find solutions to a particular query.

But if it is ok to use a library to make this nicer in Ocaml, why is that not also ok in Prolog?

Indeed. And you don't even need a library to make it nicer. Unfortunately the examples in the paper are doing Prolog an injustice to the point that they are mostly strawman attacks.

In the first example, the authors are simply comparing apples to oranges. It is true that unrestricted search in Prolog will be unfair in enumerating solutions (page 3, right column), but they are comparing this to restricted search using reify_part with a certain limit to the depth of the search (page 6, bottom left). Obviously, restricting the search space with some domain-specific magic number is perfectly doable in Prolog as well:

?- between(0, 4, N), length(R, N), append([t,t,t], X, R), boollist(X), boollist(R).
N = 3, R = [t, t, t], X = [] ;
N = 4, R = [t, t, t, t], X = [t] ;
N = 4, R = [t, t, t, f], X = [f].

(I would even argue that this is better because it uses a magic number to express a property of all desired solutions, which the programmer can observe, not of the search procedure, which is hidden.)

The second example doesn't actually have to have anything to do with search! The authors' first formulation of the many0 predicate is too general, and they specialize it in a way that is not a good choice in this case.

As long as you are working in a reasonably pure subset of Prolog, if your predicate is too general, this is because there is some clause that is too general. You can fix this clause by adding more goals in its body (making it less general) without touching any other clauses. You need not, as the authors do, throw the entire definition away and rewrite it with different control flow; all you need to do is add some conditions.

In this case, the unwanted generality comes from the fact that empty sequences are matched unconditionally, even if there might be a next element matching the goal. So we only need to change the clause that talks about empty matches to express more precisely what we actually mean. This is easy to do using the \+ negation operator:

many1(P, S, S) :-
    \+ call(P, S, _).  % new goal in this pre-existing clause, rest unchanged
many1(P, S, Rest) :-
    call(P, S, Srem), many1(P, Srem, Rest).

This more specialized variant of many0 can be used in both of the ways the authors consider:

?- many1(charA, [a, a, b], R).
R = [b] ;
false.  % no more solutions

?- many1(charA, S, []).
S = [] ;
S = [a] ;
S = [a, a] ;
S = [a, a, a] ;
S = [a, a, a, a] ; ...

Negation in Prolog has its own problems, but often it's not as bad as adding cuts. It's unfortunate that the paper doesn't even mention negation except at one point in the Conclusions where it's simply lumped in with committed choice.

The paper's general point is true---you must often be aware of Prolog's search strategy and must be able to work with it. But it's not clear that there can be any formalism for declarative programming on truly infinite Herbrand universes that doesn't have this property. Datalog and Answer Set Programming have cleaner semantics than Prolog, but at the price of giving up infinite universes.

Gergo Barany wrote:

In the first example, the authors are simply comparing apples to oranges. It is true that unrestricted search in Prolog will be unfair in enumerating solutions (page 3, right column), but they are comparing this to restricted search using reify_part with a certain limit to the depth of the search (page 6, bottom left). Obviously, restricting the search space with some domain-specific magic number is perfectly doable in Prolog as well:

?- between(0, 4, N), length(R, N), append([t,t,t], X, R), ...
N = 3, R = [t, t, t], X = [] ;
N = 4, R = [t, t, t, t], X = [t] ;
N = 4, R = [t, t, t, f], X = [f].

(I would even argue that this is better because it uses a magic number to express a property of all desired solutions, which the programmer can observe, not of the search procedure, which is hidden.)

The argument in the paper however was different. I should stress that the search procedure is not at all hidden in Hansei. Just the opposite. The search is exposed; moreover, it is programmable, in Hansei itself. In your example, you add the 'between' and 'length' goals to the original goal -- you change the model. The point in the paper is that Hansei lets you use different search procedures on the very same model without changing it. One search procedure may restrict the space with some domain-specific magic number. Another one, applied to the same model, produces first N answers, if there are that many. If the search space is very large, one is better off with approximate search procedures relying on probabilistic sampling. Hansei has an importance sampling procedure that seems to work well in practice. One is free to write one's own search procedures.

A search procedure may also be non-deterministic. On one hand Hansei separates models and search procedures. OTH, since search procedures are just regular OCaml code, they may just as well use Hansei primitives themselves. Therefore, a search procedure also may be a model. This nesting of inference was one of the main design goals of Hansei.

Gergo Barany wrote:

 many1(P, S, S) :-
     \+ call(P, S, _).  % new goal in this pre-existing clause, rest unchanged
 many1(P, S, Rest) :-
     call(P, S, Srem), many1(P, Srem, Rest).

This more specialized variant of many0 can be used in both of the ways the authors consider:

 ?- many1(charA, [a, a, b], R).
 R = [b] ;
 false.  % no more solutions

 ?- many1(charA, S, []).
 S = [] ;
 S = [a] ;
 S = [a, a] ;
 S = [a, a, a] ;
 S = [a, a, a, a] ; ...

Negation in Prolog has its own problems, but often it's not as bad as adding cuts. It's unfortunate that the paper doesn't even mention negation except at one point in the Conclusions where it's simply lumped in with committed choice.

manyplus(P,S,R) :- call(P,S,R1), many1(P,R1,R).