Einstein's task at Mercury

We continue week of the task of Einstein on Habré. In addition to the three solutions presented

1. Regular language
2. Haskell
3. The prologue

Let me introduce one more to Mercury .

Recall Wikipedia :

Mercury is a functional logic programming language with strong typing ...

Here at once it would be nice to make a comment. Despite the fact that mercury was conceived as a typed, and therefore safer and faster prologue, in my opinion, it was tough with the logic . I will explain. In the prologue, the so-called logical variables are almost his most important tool. Here, perhaps, it is easier to explain with examples (prologue):
')

 ?- A=B, C=B, B=D, D=123. A = 123, B = 123, C = 123, D = 123. 

Here we set the relationships between variables and only at the end we specify. In this case, the other variables are automatically instantiated according to the connections.

 ?- L=[A,B,C], L=[5,5|_], C=Q, Q=B. L = [5, 5, 5], A = 5, B = 5, C = 5, Q = 5. 

More complicated example. We set the list of L out of the three as yet unknown variables A, B, and C. Concretized the first two elements of the list with the number 5. At the same time, the variables A and B were automatically specified by the same number. Further, the same number also specified C as C = Q, a Q = B, and, as it turned out, B = 5.

 ?- length(L,3). L = [_G328, _G331, _G334]. 

Created a list of 3 unknown values ​​(non-specific).

 ?- length(L,3), nth0(0,L,aaa). L = [aaa, _G461, _G464]. 

It was clarified that the first element of the list is equal to the atom aaa . At the same time, the list itself was partially specified.

 ?- length(L,3), nth0(0,L,aaa), nth0(1,L,bbb). L = [aaa, bbb, _G594]. 

Further clarified the list.

 ?- length(L,3), nth0(0,L,aaa), nth0(1,L,bbb), nth0(2,L,ccc). L = [aaa, bbb, ccc]. 

Finally determined the list. In fact, in words, we gave a definition: a list of length 3, in which the first element is aaa , the second is bbb , and the third is ccc . Which is equivalent to the usual:

 ?- L=[aaa,bbb,ccc]. L = [aaa, bbb, ccc]. 

That is what is meant. Well, that is, on the prologue, the approach to solving a problem of the form is quite natural: we set the form of the solution, then, during the solution, we consistently refine the solution until it is completely determined. Such an approach makes the decision itself (its code) declarative, because it is read as a definition, and not as a sequence of actions of the algorithm (here, perhaps, it is necessary to make a clause on input-output that you want or do not want, but is essentially imperative).

So, there are no logical variables in mercury! = (
In other words, mercury does not support partially-defined data structures.
Say, if we specify a list, then all its elements must be defined.
This means that the only way to clarify a certain piece of data is to throw it out, but on its basis create a more specific one. If we talk about lists, then you can imagine that an undefined list will correspond to

 L = [no, no, no] 

partially defined:

 L=[yes(aaa), no, no] 

and fully concretized:

 L=[yes(aaa), yes(bbb), yes(ccc)]. 

(Hello, data type maybe ).

It should be noted that the same sad fate befell the Visual Prolog (the rejection of logical variables, or reference domains in the terminology of Visual Prolog). The reason is that they are quite rarely needed in this harsh imperative world, and without them, the compiler / virtual machine code / execution strategy is greatly simplified. The flip side of the medal is that typical typical tasks have to be significantly reworked, and their solution becomes much less expressive. However, the popular languages ​​of Haskell, OCaml live well and without these features =).

It is on this approach that the idea of ​​logical programming on mercury is based.
Note that with this approach, we will also have to program logical unification at the code level (in the prologue it is at the output machine level).

Auxiliary logic module (mercury supports type classes, like haskell):

 :- module logic. :- interface. :- import_module list, maybe. :- typeclass unifiable(T) where [ func unify(T, T) = T is semidet ]. :- instance unifiable(maybe(T)). :- instance unifiable(list(T)) <= unifiable(T). :- pred unify(T, T, T) <= unifiable(T). :- mode unify(in, in, out) is semidet. :- pred member(T, T, list(T), list(T)) <= unifiable(T). :- mode member(in, out, in, out) is nondet. :- pred member(T, list(T), list(T)) <= unifiable(T). :- mode member(in, in, out) is nondet. :- implementation. :- import_module maybe, list. :- instance unifiable(maybe(T)) where [ func(unify/2) is unify_maybe ]. :- instance unifiable(list(T)) <= unifiable(T) where [ func(unify/2) is unify_lists ]. :- func unify_maybe(maybe(T), maybe(T)) = maybe(T) is semidet. unify_maybe(no, yes(E)) = yes(E). unify_maybe(yes(E), no) = yes(E). unify_maybe(no, no) = no. unify_maybe(yes(E), yes(E)) = yes(E). :- func unify_lists(list(T), list(T)) = list(T) is semidet <= unifiable(T). unify_lists([], []) = []. unify_lists([H|T], [H1|T1]) = [unify(H, H1) | unify_lists(T, T1)]. :- pred unify_lists(list(T), list(T), list(T)) <= unifiable(T). :- mode unify_lists(in, in, out) is semidet. unify_lists(L1, L2, unify_lists(L1, L2)). unify(A, B, unify(A, B)). member(E, E, [], []) :- fail. member(E0, E1, [H | T], [H1 | T1]) :- ( H0 = unify(E0, H), H1 = H0, E1 = H0, T=T1 ; H1 = H, member(E0, E1, T, T1) ). member(E, !L) :- member(E,_,!L). 

Well, the solution itself zebra puzzle :

 :- module einstein. :- interface. :- import_module io. :- pred main(io::di, io::uo) is det. :- implementation. :- import_module maybe, list, solutions, logic. :- type house ---> house(maybe(nationality), maybe(color), maybe(pet), maybe(cigarettes), maybe(drink)). :- type nationality ---> englishman; spaniard; norwegian; ukrainian; japanese. :- type color ---> red; yellow; blue; green; ivory. :- type pet ---> dog; snails; fox; horse; zebra. :- type cigarettes ---> kools; chesterfields; winston; lucky_strike; parliaments. :- type drink ---> orange_juice; tea; coffee; milk; water. :- instance unifiable(house) where [ unify( house(N, C, P, S, D), house(N1, C1, P1, S1, D1)) = house(unify(N, N1), unify(C, C1), unify(P, P1), unify(S, S1), unify(D, D1)) ]. unknown_house = house(no,no,no,no,no). solve(!Street):- % The Englishman lives in the red house logic.member(house(yes(englishman),yes(red),no,no,no), !Street), % The Spaniard owns the dog logic.member(house(yes(spaniard),no,yes(dog),no,no), !Street), % The Norwegian lives in the first house on the left unify([house(yes(norwegian),no,no,no,no),unknown_house,unknown_house,unknown_house,unknown_house], !Street), % Kools are smoked in the yellow house. logic.member(house(no,yes(yellow),no,yes(kools),no), !Street), % The man who smokes Chesterfields lives in the house % next to the man with the fox. next(house(no,no,yes(fox),no,no), house(no,no,no,yes(chesterfields),no), !Street), % The Norwegian lives next to the blue house next(house(yes(norwegian),no,no,no,no), house(no,yes(blue),no,no,no), !Street), % The Winston smoker owns snails. logic.member(house(no,no,yes(snails),yes(winston),no), !Street), % The lucky strike smoker drinks orange juice logic.member(house(no,no,no,yes(lucky_strike),yes(orange_juice)), !Street), % The Ukrainian drinks tea logic.member(house(yes(ukrainian),no,no,no,yes(tea)), !Street), % The Japanese smokes parliaments logic.member(house(yes(japanese),no,no,yes(parliaments),no), !Street), % Kools are smoked in the house next to the house where the horse is kept. next(house(no,no,yes(horse),no,no), house(no,no,no,yes(kools),no), !Street), % Coffee is drunk in the green house logic.member(house(no,yes(green),no,no,yes(coffee)), !Street), % The green house is immediately to the right (your right) of the ivory house left(house(no,yes(ivory),no,no,no), house(no,yes(green),no,no,no), !Street), % Milk is drunk in the middle house. unify([unknown_house,unknown_house,house(no,no,no,no,yes(milk)),unknown_house,unknown_house], !Street), % And, finally, zebra and water :) logic.member(house(no,no,yes(zebra),no,no), !Street), logic.member(house(no,no,no,no,yes(water)), !Street). next(H1, H2, !Street):- left(H1, H2, !Street); left(H2, H1, !Street). left(H1, H2, !Street):- unify([H1,H2,unknown_house,unknown_house,unknown_house], !Street); unify([unknown_house,H1,H2,unknown_house,unknown_house], !Street); unify([unknown_house,unknown_house,H1,H2,unknown_house], !Street); unify([unknown_house,unknown_house,unknown_house,H1,H2], !Street). main --> { solutions(pred(S::out) is nondet :- solve([unknown_house,unknown_house,unknown_house,unknown_house,unknown_house], S), L)}, print_solutions(L). print_solutions(L) --> write_string("Total solutions: "), write_int(length(L)), nl, nl, print_every_sol(L). print_every_sol([]) --> []. print_every_sol([S|SS]) --> print_sol(S), print_every_sol(SS). print_sol([]) --> []. print_sol([H|HH]) --> print_house(H), nl, print_sol(HH). print_maybe(no) --> write_string("unknown"). print_maybe(yes(T)) --> write(T). print_house(house(N, C, P, S, D)) --> write_string("house("), print_maybe(N), write_string(", "), print_maybe(C), write_string(", "), print_maybe(P), write_string(", "), print_maybe(S), write_string(", "), print_maybe(D), write_string(")"). 

As you can see, the similarity with the prologue-solution can be seen with the naked eye, although the code is an order of magnitude more, yes ... =)

$ time ./einstein
Total solutions: 1

house(norwegian, yellow, fox, kools, water)
house(ukrainian, blue, horse, chesterfields, tea)
house(englishman, red, snails, winston, milk)
house(spaniard, ivory, dog, lucky_strike, orange_juice)
house(japanese, green, zebra, parliaments, coffee)

real 0m0.031s
user 0m0.015s
sys 0m0.015s