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

    Продолжаем неделю задачи Эйнштейна на Хабре. В дополнение к трём представленным решениям
    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
    Поделиться публикацией

    Похожие публикации

    Комментарии 20

      –9
      Интересный язык. Первый раз о нем слышу.

      Владимир, а вы знакомы с С++? Если да, то надеюсь на продолжение недели Задачи Эйнштейна с этим языком.
        –1
        Тебя же убили, че ты тут делаешь?
        –3
        а что еще умеет делать этот язык, крмое решения этой задачи?
          +2
          Тьюринг-полнота Вам о чем-нибудь говорит? =)
          Ну а по факту библиотек, конечно, там мало, да и средств разработки тоже.
          Пока меня прельщает сама концепция.
            +8
            ну да, Brainfuck тоже полон по Тьюрингу.
              +6
              какой вопрос, такой ответ, не обессудьте =)
          –2
          Введение бы какое в язык.
            0
            если память не изменяет, то товарищ xonix уже писал введение в него :)
              0
              Таки вводной статьи с моей стороны не было, моя вина. Только кидал ссылку на неплохой перевод вводной pdf-ки с официального сайта.
            +1
            Неделя задач Эйнштейна?
              +1
              Я правильно понял, что пришлось писать унификацию с нуля не Mercury. Ее нет в Mercury (в общем виде)?
              Я тогда не понимаю почему язык зовется логическим, если там нет ни переменных, ни унификации.
              Я все время думал что Mercury — строго типизированный Prolog с плюшками… Теперь придется читать про него :) Мне аж интересно стало
                +1
                В mercury есть унификация на уровне pattern matching. Чтобы достичь нечто похожего на унификацию логических переменных действительно надо городить некую надстройку. Строго-типизированными прологами с плюшками были Turbo/PDC/Visual Prolog (до версии 5.2 включительно). Теперь, когда убрали ссылочные домены, получился функциональный язык с недетерминизмом, правда, туда еще ООП вставили.
                +1
                Хм… последняя статья будет на брейнфаке?
                  +1
                  Если кто-нибудь решит задачу на брейнфаке, то появляются решения на Ook!, COW, SmallFuck, DoubleFuck :) Так что он скорее всего не будет последним.
                  –1
                  > типизируемый, а значит, более безопасный и быстрый

                  Это миф.
                    +1
                    Похоже, придётся пояснить.

                    Это утверждение логично разбивается на два.

                    Первое — „Типизируемый язык более безопасен”. Под безопасностью обычно понимается защищённость программы от ошибок пользователя, где типизация приводит лишь к тому что ошибка появится в другом месте, и защищённость программы от ошибок программиста, где типизация приведёт к тому, что ошибка возникнет в другое время. Но все ошибки всё-равно возникнут и их всё-равно нужно будет исправлять. Разработчики, использующие языки с опциональной типизацией, используют её очень редко, обычно только в виде контракта в интерфейсах библиотек, т.к. справедливо считают что время потраченное на типизацию всего *и* исправление ошибок превосходит время потраченное только на исправление ошибок, хоть и выявленных позднее. Так же не стоит считать что типизпция (даже как в Haskell) избавит вас ото всех ошибок. Самые опасные и трудноуловимые ошибки — логические — никакая система типов не поймает.

                    Второе — „типизируемый язык более производителен” легко опровергается примером.
                    en.wikipedia.org/wiki/Stalin_(Scheme_implementation)
                    Да, c2.com/cgi/wiki?SufficientlySmartCompiler
                      0
                      >и защищённость программы от ошибок программиста, где типизация приведёт к тому, что ошибка возникнет в другое время. Но все ошибки всё-равно возникнут и их всё-равно нужно будет исправлять.

                      Именно. Огромная разница, возникнет ошибка на этапе компиляции и в runtime. Представьте, что runtime это уже production система. Есть принцип Fail-Fast который заключается в том, что система должна зафейлиться как можно раньше с момента обнаружения сбоя, чтоб не наделать нехороших дел. В идеале, это должно происходить на этапе компиляции.
                      Приведу пример, где mercury более безопасен чем ocaml. В mercury case должен охватывать весь домен, иначе не скомпилируется (очень просто: предикат декларирован как детерминируемый (det), а выводится (inferred) как полу-детерминированный (semidet) — ошибка компиляции), а в ocaml match может не охватывать весь домен, будет просто warning и exception в runtime.

                      >Второе — „типизируемый язык более производителен” легко опровергается примером.

                      Речь не о теории а о практике. На практике гораздо легче оптимизировать типизируемый язык и именно поэтому типизируемые языки в среднем по скорости обгоняют на порядки нетипизируемые.
                        0
                        > Представьте, что runtime это уже production система.

                        Ну да, если вы не пишете тесты, то немного спасёт только типизация. При разработке же никакой разницы когда система упадёт, если смогла вывести достаточно информации для выяснения причины ошибки.

                        Нетипизированные языки давно вымерли, кроме скриптовых, а динамически-типизируемые отстают далеко не на порядок.
                    +2
                    Реквестирую решение задачи на cmd и shell-скриптах.
                      0
                      Осталось только на C++, Java, C#, Perl и Python написать — и будет отличная коллекция!

                      Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.

                      Самое читаемое