Einstein's task at Mercury
We continue the week of Einstein’s task on Habré. In addition to the three solutions presented
Let me introduce one more at Mercury .
Recall Wikipedia :
Mercury is a functional-logical programming language with strict typing ...
It would be nice to immediately make a comment here. Despite the fact that mercury was conceived as a typed, and therefore, a safer and faster prologue, it seems to be rather taut with its logic . I will explain. In the prologue, almost the most important tool is the so-called logical variables . Here, perhaps, it’s easier to explain with examples (prologue):
Here we set the relationships between the variables and only specify in the end. In this case, the remaining variables are automatically concretized in accordance with the relationships.
More complex example. A list L of three so far unknown variables A, B and C was specified. The first two elements of the list with the number 5 were specified. At the same time, the variables A and B were automatically specified with the same number. Then C was specified with the same number, since C = Q, a Q = B, and, as it turned out, B = 5.
Created a list of 3 unknown values (non-specific).
We clarified that the first element of the list is equal to the atom
Refined the list even more.
We finally determined the list. In fact, in words, we gave a definition: a list of length 3, which has the first element
This is what is meant. Well, that is, at the prologue, the approach to solving a problem of the form is very natural: they set the form of the solution, then, in the course of the solution, we subsequently clarify the solution until it is completely determined. This approach makes the solution itself (its code) declarative, because it is read as a definition, and not as a sequence of actions of the algorithm (here, perhaps, you need to make a reservation about input-output, which you want, you don't want, but it is imperative in essence).
So, in mercury there are no logical variables ! = (
In other words, mercury does not support partially defined data structures.
For example, if we specify a list, then all its elements must be defined.
This means that the only way to clarify a piece of data is to throw it away, but create more specific one based on it. If we talk about lists, then we can imagine that an undefined list will correspond to a
partially defined one:
but a fully specified one:
(Hi, maybe the data type ).
It should be noted that the same sad fate befell Visual Prolog(rejection of logical variables, or reference domains in Visual Prolog terminology). The reason is that they are 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 coin is that typically-laid tasks have to be substantially redone, and their solution becomes much less expressive. However, the popular languages Haskell, OCaml live fine 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 the logical unification at the code level (in the prologue, it is at the level of the output machine).
Auxiliary module
Well, the zebra puzzle solution itself :
As you can see, the similarity to the prolog solution is visible to the naked eye, although the code is an order of magnitude larger, yes ... =)
Let me introduce one more at Mercury .
Recall Wikipedia :
Mercury is a functional-logical programming language with strict typing ...
It would be nice to immediately make a comment here. Despite the fact that mercury was conceived as a typed, and therefore, a safer and faster prologue, it seems to be rather taut with its logic . I will explain. In the prologue, almost the most important tool is the so-called logical variables . Here, perhaps, it’s 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 the variables and only specify in the end. In this case, the remaining variables are automatically concretized in accordance with the relationships.
?- L=[A,B,C], L=[5,5|_], C=Q, Q=B.
L = [5, 5, 5],
A = 5,
B = 5,
C = 5,
Q = 5.
More complex example. A list L of three so far unknown variables A, B and C was specified. The first two elements of the list with the number 5 were specified. At the same time, the variables A and B were automatically specified with the same number. Then C was specified with the same number, since 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].
We clarified that the first element of the list is equal to the atom
aaa. Moreover, the list itself was partially specified. ?- length(L,3), nth0(0,L,aaa), nth0(1,L,bbb).
L = [aaa, bbb, _G594].
Refined the list even more.
?- length(L,3), nth0(0,L,aaa), nth0(1,L,bbb), nth0(2,L,ccc).
L = [aaa, bbb, ccc].
We finally determined the list. In fact, in words, we gave a definition: a list of length 3, which has the first element
aaa, the second bbb, and the third - ccc. Which is equivalent to the usual: ?- L=[aaa,bbb,ccc].
L = [aaa, bbb, ccc].
This is what is meant. Well, that is, at the prologue, the approach to solving a problem of the form is very natural: they set the form of the solution, then, in the course of the solution, we subsequently clarify the solution until it is completely determined. This approach makes the solution itself (its code) declarative, because it is read as a definition, and not as a sequence of actions of the algorithm (here, perhaps, you need to make a reservation about input-output, which you want, you don't want, but it is imperative in essence).
So, in mercury there are no logical variables ! = (
In other words, mercury does not support partially defined data structures.
For example, if we specify a list, then all its elements must be defined.
This means that the only way to clarify a piece of data is to throw it away, but create more specific one based on it. If we talk about lists, then we can imagine that an undefined list will correspond to a
L = [no, no, no]
partially defined one:
L=[yes(aaa), no, no]
but a fully specified one:
L=[yes(aaa), yes(bbb), yes(ccc)].
(Hi, maybe the data type ).
It should be noted that the same sad fate befell Visual Prolog(rejection of logical variables, or reference domains in Visual Prolog terminology). The reason is that they are 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 coin is that typically-laid tasks have to be substantially redone, and their solution becomes much less expressive. However, the popular languages Haskell, OCaml live fine 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 the logical unification at the code level (in the prologue, it is at the level of the output machine).
Auxiliary module
logic(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 zebra puzzle solution itself :
:- 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 to the prolog solution is visible to the naked eye, although the code is an order of magnitude larger, 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