Решение логических задач на языке Haskell: в своём ли уме Валет?

Сегодня я хотел бы подвести итоги под результатами августовского конкурса по функциональному программированию, который ежемесячно проводится под эгидой ФП(ФП). На этот раз в качестве задачи участникам была предложена несколько переформулированная задача из книги Р. М. Смаллиана «Алиса в стране смекалки»:

Тройка думает, что Туз не в своём уме. Четвёрка думает, что Тройка и Двойка обе не могут быть не в своём уме. Пятёрка думает, что Туз и Четвёрка либо оба не в своём уме, либо оба в своём уме. Шестёрка думает, что Туз и Двойка оба в своём уме. Семёрка думает, что Пятёрка не в своём уме. Валет думает, что Шестёрка и Семёрка обе не могут быть не в своём уме. В своём ли уме Валет?

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

Для начала немного теории

Для понимания дальнейших рассуждений необходимо сделать небольшой экскурс в формальную логику. Сразу же прошу прощения у тех своих читателей, кому данный экскурс не нужен в силу их знаний и умений. Нижеследующие рассуждения достаточно поверхностны и иногда терминологически неаккуратны, однако для понимания принципа решения представленной задачи они достаточны. Заинтересованных читателей могу адресовать к какому-нибудь учебнику по формальной логике.

В формальной логике формула называется «общезначимой» (или «тождественно истинной», или «тавтологией»), если при любых значениях переменных, входящих в неё, она принимает значение «ИСТИНА». Например, общезначимой является формула (X || not X), поскольку при любом значении X (которое может быть True или False соответственно), эта формула истинна. Соответственно, тождественно ложной формулой называется такая, которая принимает значение «ЛОЖЬ» при любых значениях входящих в неё переменных. Например, формула (X && not X) является тождественно ложной.

Если же формула на одних значениях переменных принимает значение «ИСТИНА», а на других — «ЛОЖЬ», то такая формула не является ни общезначимой, ни тождественно ложной. Например, формула X && Y не является ни тождественно истинной, ни тождественно ложной, потому как может принимать значения как «ИСТИНА», так и «ЛОЖЬ» в зависимости от значений своих переменных.

Задачи из книги Р. М. Смаллиана сформулированы таким образом, что для ответа на поставленный в задаче вопрос необходимо составить соответствующую логическую формулу и проверить её общезначимость. Что же касается душевного состояния, то считается, что субъект не в своём уме, если он всегда говорит только ложные утверждения, а, соответственно, субъект в своём уме, если он всегда говорит только истинные утверждения. Это определяет, что задачи необходимо решать именно в рамках формальной логики, и интуиционизм здесь не подходит, поскольку в последнем случае надо было бы делать предположение о том, что некий субъект в своём уме только на основании того, что его высказывание внутренне непртиворечиво. Но это слишком тонкая материя, чтобы быть рассмотренной в этой небольшой заметке.

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

Реализация

В качестве прекрасного языка реализации для подобных задач является язык Prolog. И участник, занявший первое место в конкурсе, выбрал именно его для решения. Однако далее мы напишем решение на не менее прекрасном языке Haskell, заодно покажем, как сформулировать программу на нём так, чтобы она читалась практически так же, как и условие задачи.

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

валет туз двойка = думает что (шестёрка туз двойка) и (семёрка туз двойка) обеНеМогутБытьНеВСвоёмУме

Это было ужасно, и от этого подхода пришлось отказаться. Но на помощи пришла нотация do, в которой можно было описать всё, что необходимо, и именно в той форме, в которой хотелось. В итоге на свет появилось такое определение:

вСвоёмЛиУмеВалет = выводРезультата $
  do туз    <- варианты душевного состояния
     двойка <- варианты душевного состояния
     let тройка   = думает что туз неВСвоёмУме
         четвёрка = думaeт что тройка и двойка обеНеМогутБытьНеВСвоёмУме
         пятёрка  = думaeт что туз и четвёрка либоОбаНеВСвоёмУмеЛибоОбаВСвоёмУме
         шестёрка = думaeт что туз и двойка обаВСвоёмУме
         семёрка  = думает что пятёрка неВСвоёмУме
         валет    = думaeт что шестёрка и семёрка обеНеМогутБытьНеВСвоёмУме
     return валет

На первый взгляд это определение вызывает крайне смешанные чувства. С одной стороны написание программы при помощи русских букв традиционно вызывает некоторое недоразумение. И ладно бы, если ключевые слова тоже были бы на русском языке, но нет. А потому смешение языков в тексте программы выглядит крайне спорно. Но с другой стороны, данная программа категорически выглядит именно как формулировка самой задачи.

Но тут возникает несколько вопросов. Во-первых, необходимо определить кучу комбинаторов, типа что, неВСвоёмУме, и и т. д. Интуиция сразу подсказывает, что эти комбинаторы частью будут «заглушками», которые никогда использоваться не будут, а частью будут просто синонимами для уже имеющихся стандартных функций. Ну а во-вторых, проницательный читатель уже заметил, что в этом определении терм думает используется двумя различными способами — использования для тройки и семёрки отличается от использования для остальных субъектов. Что это? Разное количество аргументов при одинаковом типе результата свидетельствует о том, что это две разных функции с разными сигнатурами типов. Как такое может быть?

Вопрос простой — это разные термы, просто выглядят они одинаково для человека. Компьютер же их различает — в одном терме думает все символы кириллические, а в другом — буква e взята из латинского алфавита. Да, это ужасно-ужасно-ужасно! Это более, чем ужасно. Это невозможно. За это надо, как минимум, бить по рукам, ведь такая программа получается абсолютно неподдерживаемой. Но, поскольку в данном случае мы имеем «программу одного запуска», то можно. Хоть и выглядит катастрофично.

Функция выводРезультата является служебной и необходима только для вывода на экран заключения о душевном состоянии валета. Она написана крайне конкретно:

выводРезультата x | and x     = putStrLn "Валет в своём уме."
                  | all not x = putStrLn "Валет не в своём уме."
                  | otherwise = putStrLn "Невозможно сделать вывод о душевном состоянии валета."

В первом охранном выражении, как видно, мы делаем проверку на общезначимость формулы x. Во втором охранном выражении, соответственно, — на тождественную ложность то же формулы. Ну а последнее охранное выражение соответствует тому, что формула x не является ни общезначимой, ни тождественно ложной. Здесь, конечно, опять можно было бы переопределить все эти стандартные функции and, all и т. д., но этого можно и не делать, поскольку эта функция не является описанием задачи. Её саму уже даже можно было не называть по-русски.

Здесь надо упомянуть, что мы работаем в рамках монады [], то есть в определении функции вСвоёмЛиУмеВалет нотация do относится к спискам. Это значит, что последнее выражение в do вернёт список, в котором в данном случае должно быть ровно 4 элемента — по одному элементу для рассчитанного значения душевного состояния валета на 4 возможных комбинации душевных состояний туза и двойки. Как видно в определении, термы туз и двойка определяются через генерацию из элементов списка, и из определения функции варианты будет ясно, что и туз, и двойка последовательно принимают значения от «ИСТИНА» до «ЛОЖЬ».

Ну а вот скопом определения всех комбинаторов:

вСвоёмУме   = True

и           = (&&)
или         = (||)
не          = not
неВСвоёмУме = not

либоОбаНеВСвоёмУмеЛибоОбаВСвоёмУме = (==)
обеНеМогутБытьНеВСвоёмУме          = или
обаВСвоёмУме                       = и

думает _ x f     = f x
думaeт _ x _ y f = f x y

что       = undefined
душевного = undefined
состояния = undefined

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

Осталось упомянуть, что представленная функция вСвоёмЛиУмеВалет отлично решает поставленную задачу и выводит на экран удивлённому пользователю ответ:

Валет в своём уме.

Заключение

Программа написана, она решает задачу. Однако не всё так просто. Дело в том, что в книге-источнике, конечно же, задачи подобраны так, чтобы они не содержали противоречий. Это значит, что если формализовать задачу в подобном стиле, что интерпретатор языка Haskell всегда найдёт тот или иной ответ. Но как быть в случае общего подхода? Если сформулировать задачу так, чтобы она была внутренне противоречива? Данный подход не даст ответа — программа зациклится и никогда не посчитает тот вариант душевного состояния валета, на котором найдено противоречие. Это, похоже, проблема останова — формулировка задачи противоречива тогда и только тогда, когда написанная в таком стиле программа не может найти ответа.

Однако можно использовать другой стиль, который позволит дать ответ и на вопрос о том, является ли формализованная задача корректно сформулированной. В этом случае надо использовать стандартную функцию guard из модуля Control.Monad, даже, возможно, определив для неё синоним в виде терма думает. Но решение этой задачи я оставляю вдумчивому читателю. Кто заинтересован — прошу писать в комментариях. Это действительно несложно.

Исходный код представленного в заметке модуля вы можете получить здесь.

Ну а мне остаётся лишь поблагодарить своих добрых коллег: Дмитрия Антонюка (lomeo), Дмитрия Астапова (dastapov) и Михаила Байкова (аккаунта на Хаброхабре нет).

Мои предыдущие статьи о конкурсах по ФП на Хаброхабре:

• Решение задачи о перегорающих лампочках на языке Haskell
• Фреймворк для решения задач о переправах на языке Haskell
• Конструирование и вычисление арифметических выражений на языке Haskell
• Расшифровка кода на языке Haskell (конкурс по ФП в январе 2012)
• Шахматные задачи на мат в один ход: решение на языке Haskell
• Измерение объёмов при помощи двух заданных сосудов: решение на языке Haskell
• Трансмутации слов друг в друга: решение на языке Haskell
• Решение арифметических задач — вероятностный подход против регулярных выражений
• Поиск кратчайшего расстояния между точками в трёхмерном пространстве
• Управление лифтами: решение на языке Haskell

Автор: Darkus