Pull to refresh

Задача Эйнштейна на Mercury

Reading time6 min
Views2.9K
Продолжаем неделю задачи Эйнштейна на Хабре. В дополнение к трём представленным решениям
  1. Регулярным языком
  2. Хаскеллем
  3. Прологом

позвольте представить еще одно на Mercury.

Напомним Википедию:

Mercury — язык функционально-логического программирования со строгой типизацией…

Тут сразу неплохо бы сделать замечание. Несмотря на то, что mercury задумывался как типизируемый, а значит, более безопасный и быстрый пролог, с логикой у него, по-моему, туговато. Поясню. В прологе чуть ли не важнейшим его инструментом являются так называемые логические переменные. Тут, пожалуй, проще пояснить примерами (пролог):

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

Тут мы задаём связи между переменными и лишь в конце конкретизируем. При этом остальные переменные автоматически конкретизируются в соответствие со связями.

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

Более сложный пример. Задали список L из трех пока неизвестных переменных A, B и C. Конкретизировали первые два элемента списка с числом 5. При этом автоматически переменные A и B конкретизировались тем же числом. Далее тем же числом конкретизировалось и С, поскольку C=Q, a Q=B, а, как выяснили, B=5.

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

Создали список из 3 неизвестных значений (неконкретизированных).

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

Уточнили, что первый элемент списка равен атому aaa. При этом сам список частично конкретизировался.

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

Еще больше уточнили список.

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

Окончательно определили список. Фактически, говоря словами, мы дали определение: список длины 3, у которого первый элемент aaa, второй bbb, а третий — ccc. Что равносильно обычному:

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


Вот это и имеется в виду. Ну, то есть на прологе весьма естественным является подход к решению задачи вида: задали форму решения, потом, в ходе решения последовательно уточняем решение, пока оно полностью не будет определено. Такой подход делает само решение (его код) декларативным, потому что оно читается как определение, а не как последовательность действий алгоритма (тут, пожалуй, надо сделать оговорку о вводе-выводе, который хочешь-не хочешь, но императивен по своей сути).

Так вот, в mercury нет логических переменных! =(
Иными словами, mercury не поддерживает частично-определенные структуры данных.
Скажем, если мы задаём список, то все его элементы обязаны быть определены.
Это значит, что единственный способ уточнить некоторый кусок данных — это выкинуть его, но на его основе создать более конкретизированный. Если говорить о списках, то можно представить, что неопределенный список будет соответствовать

L = [no, no, no]


частично определенный:

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


а полностью конкретизированный:

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


(Привет, тип данных maybe).

Следует отметить, что та же печальная участь постигла и Visual Prolog (отказ от логических переменных, или reference domains в терминологии Visual Prolog). Причина в том, что нужны они довольно редко в этом суровом императивном мире, а без них код компилятора/виртуальной машины/стратегия исполнения резко упрощается. Обратная сторона медали — типично-проложные задачи приходится существенно переделывать, при этом решение их становится гораздо менее выразительным. Впрочем, популярные языки Haskell, OCaml прекрасно живут и без этих возможностей =).

Вот на этом подходе и основана идея логического программирования на mercury.
Заметим, что при таком подходе, нам придется и логическую унификацию тоже программировать на уровне кода (в прологе она находится на уровне машины вывода).

Вспомогательный модуль logic (mercury поддерживает классы типов, как и 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).


Ну и само решение 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(")").


Как видим, сходство с пролог-решением видно невооруженным глазом, хотя кода на порядок больше, да… =)

$ 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
Tags:
Hubs:
+13
Comments20

Articles