misscann0.htm

Миссионеры и каннибалы (введение)

      Сначала вопрос философского характера. Пусть рефал-программа является предикатом. Мы ее суперкомпилируем. Пусть при некоторых входных данных с перемеными суперкомпилятор построил истину. Это одно из очень хороших применений суперкомпиляции. Так мы можем доказывать математические утверждения.

      Где гарантия, что все нормально, что мы не наткнулись на ошибку в суперкомпиляторе. Этот вопрос относится не только к суперкомпилятору для рефала, но также и к суперкомпилятору для Явы.

      Любая программа может содержать ошибки, но почти всегда они как-то вылавливаются. Как обнаружить, что в построенной суперкомпилятором функции вида

   e.1 = T;

не все в порядке.

      Сейчас предлагаю, как мне кажется, полное доказательство. Пришлось принимать меры по обоснованию выводов.

      Постановка задачи.

      Missionaries and Cannibals. Turchin's example from the Refal-5 book.

      Consider the well-known problem ``Missionaries and Cannibals''. Three missionaries and three cannibals come to the bank of a river and see a boat. They want to cross the river. The boat, however, can carry no more than two people. There is a further restriction. At no time should the number of cannibals on either bank of the river (including the moored boat) exceed the number of missionaries (because the missionaries would then be overpowered and eaten). How (if at all) is it possible to cross the river?

     В связи с первоначальными экспериментами в этой области Валентин Федорович мне писал:

      To est' kak "net peremennykh"? A posledovatel'nost' perevozek? Ona-to i est' peremennaja, v to vremja kak nachal'noe i konechnoe sostojanija fiksirovany.

     My opredeljaem the predicate:

<Pred (e.start) (e.crossing-sequence) (e.finish)>

kotoryj proverjaet chto e.crossing-sequence preobrazuet e.start v e.finish.

      Zatem my supercompilliruem Pred s zadannymi znachenijami

e.start = L(MMMCCC)() ,

e.finish= R()(MMMCCC).

      V ideale dolzhno poluchit'cja odno predlozhenie gde sleva konkretnaja crossing-sequence (reshenie zadachi), a sprava "True".

      Tut nuzhna ogovorka. Mnozhestvo reshenij mozhet byt' beskonechnym, vkljuchaja bessmyslennye poezdki tuda-nazad. S etim mozhno borot'sja s pomoshchju filtrov zapreshchajushchikh povtorenie uzhe pojavivshegosja sostojanija, a mozhet byt' kak-nibud' eshche -- pridumajte, u Vas eto khorosho poluchaetsja.

      Uh, esli eto poluchitsja, vo budet krasivo!

      Андрей Немытых. Замечу, что напрашивается аналогия -- данная программа является простым интерпретатором ( в программистском смысле ) некоторого формального языка перевозок-путей, данными в этом языке являются распределённые по берегам миссионеры и каннибалы. Действительно, например, в Рефал-программе данные "ищут" путь в программе от стартовой точки к конечной согласно семантике Рефала.

      С этой точки зрения Валентин Фёдорович предлагает рассматривать задачу специализации интерпретатора не по программе ( как обычно ) , а по данным --- с целью вырезать ( сузить ) из множества программ некоторые программы -- Рефал-пути, соответствующие фиксированному входу и фиксированному выходу.

      Александр Корлюков. Валентин Федорович предлагает для каждой клетки таблицы производить суперкомпиляцию. Я с таким предложением вынужден не согласиться, так как ничего интересного (нового) на таком пути не получится. Для каждой клетки таблицы можно было бы просто пускать на счет Вашу программу из книги по рефалу, и получать конкретную последовательность перевозок.

      Тем более, что клеток в таблице бесконечное количество.

      Я предлагаю использовать суперкомпиляцию для полного заполнения таблицы в несколько этапов.

      Суперкомпилятор позволяет это сделать !

      Для этого в предлагаемой функции

 <Pred (e.start) (e.crossing-sequence) (e.finish)>

специализацию производить не по конкретным начальным и конечным наборах миссионеров и каннибалов, к примеру,

e.start = L(MMMCCC)() ,

e.finish= R()(MMMCCC).

а по некоторым классам, множествам людей.

      Андрей Немытых. Александр же предлагает, как я понимаю, сделать (в терминологии Валентина Фёдоровича) метасистемный переход, параметризовать тем или иным образом вход и выход. С одной стороны он усложняет задачу, ибо предыдущая является её частным случаем. С другой стороны, более общая задача иногда решается проще, ибо внутри неё можно сделать более адекватные обобщения. Кроме того в такой постановке задача более интересна.

      Аркадий Климов. Александр, возможно кто-то чего-то не понял. У Валентина Федоровича, как я понял из вышеприведенной цитаты, исходно дана функция не одного аргумента - начального состояния, а двух - состояния и последовательности перевозок (формально даже трех, но третий - конечное состояние можно легко получить путем перестановки термов исходного). Поэтому данная таблица, где аргумент- только начальное состояние, нельзя называть "ответом" в данной задаче. Возможно это "ответ" в задачке на ту же тему в другой формулировке: когда дается начальное состояние и спрашивается "а можно ли...".

      Возможная путаница связана с тем, что в книжке по рефалу-5 предлагается программка в другой формулировке: дано начальное состояние, и программка порождает последовательность перевозок. Эта программка сама выполняет поиск путем перебора. Там суперкомпилятору действительно нечего делать для фиксированной клетки таблицы. Но, повторяю, теперь-то ВФ предлагает брать в качестве исходной не программку из книжки, а гораздо более простую функцию - предикат, проверяющую применимость пути.

      Читая письмо дальше, я вижу, что ты тоже используешь эту функцию-предикат, суперкомпилируя ее. Тогда непонятно, к чему было замечание выше, о том, что "можно было просто запускать на счет программу из книжки"?