misscann1.htm
Миссионеры и каннибалы (продолжение)
Андрей Немытых. Отвечая на просьбу Александра, пересылаю ниже несколько реплик по поводу задачи миссионеры и каннибылы. Во первых, жизнь показывает, что каннибалов существенно больше миссионеров, и в этом смысле ответ задачи очевиден, то есть решать её не надо. Тем не менее, временно встанем на идеалистическую точку зрения.
Александр Корлюков. Пусть рефал-программа является предикатом. Мы ее суперкомпилируем. Пусть при некоторых входных данных с перемеными суперкомпилятор построил истину. Это одно из очень хороших применений суперкомпиляции. Так мы можем доказывать математические утверждения.
Андрей Немытых. Такая постановка задачи меня несколько смущает, на мой взгляд, доказывать математические утверждения никакая программа не может. Другое дело, что некоторые преобразования программ-предикатов можно , с большой натяжкой, трактовать таким образом. Кроме того, если иметь ввиду конкретный преобразователь, то он имеет право расширять область определения предиката по своему усмотрению, и потому, если на результат смотреть лишь формально, то необходимо чтобы преобразуемый предикат был определён на всех входных данных. ( Не циклился ни на одном из них, и не ломался по Recognition Impossible. )
Тем не менее, наблюдения Алекандра очень интересны с точки зрения познания окружаюшего мира человека, способ жизни которого предполагает непрерывные размышления над конкретными объектами природы.
Замечу, что напрашивается аналогия -- данная программа является простым интерпретатором ( в программистском смысле ) некоторого формального языка перевозок-путей, данными в этом языке являются распределённые по берегам миссионеры и каннибалы. Действительно, например, в Рефал-программе данные "ищут" путь в программе от стартовой точки к конечной согласно семантике Рефала. С этой точки зрения Валентин Фёдорович предлагает рассматиривать задачу специализации интерпретатора не по программе ( как обычно ) , а по данным --- с целью вырезать ( сузить ) из множества программ некоторые программы -- Рефал-пути, соответсвующие фиксированному входу и фиксированному выходу.
Александр же предлагает, как я понимаю, сделать (в терминалогии Валентина Фёдоровича) метасистемный переход, параметризовать тем или иным образом вход и выход. С одной стороны он усложняет задачу, ибо предудущая является её частным случаем. С другой стороны, более общая задача иногда решеатся проще, ибо внутри неё можно сделать более адекватные обобщения. Кроме того в такой постановке задача более интересна.
$ENTRY Go {
= <Prout <MissCann (( ) ('mmmccc') ( ))
(CC C CC C MM MC MM C CC M MC)>> ;
}
Данные: ( ) ('mmmccc') ( )
Программа: CC C CC C MM MC MM C CC M MC
Интерпретатор: текст программы.
Представляю компанию людей в виде тройки ( e.m ) ( e.p ) ( e.c ), где e.m - последовательность символов 'm', каждый из которых соответствует одному миссионеру, e.c - последовательность символов 'c', каждый из которых соответствует одному каннибалу, e.p - последовательность пар миссионер-каннибал, при этом миссионеры расположены сначала, а потом каннибалы.
Описывается "поле зрения"
Александр Корлюков. Предусмотрел два варианта суперкомпиляции этой программы - они отличаются в двух местах в функции Miss (парные предложения, одно из которых закомментировано). Один вариант для случая, когда я хочу доказывать невозможность решения, другой - для поиска конкретной перевозки. Далее будет объяснено на примерах более подробно. Теперь примеры суперкомпиляций. (1). Три миссионера и три каннибала. Ищутся решения, предложение с ложью игнорируется путем "отождествление невозможно".
Андрей Немытых. См. замечание выше -- нужно это делать аккуратно.
Александр Корлюков. Результат замены я искусственно сделал не просто T, а с остатком пути, тогда получается именно такая программа (иначе ничего не понятно). e.1 можно игнорировать при анализе ответа.
Андрей Немытых. Вы совершенно верно обходите то о чём я написал в предыдущей ремарке. Вы делаете это и в дальнейших примерах.
Александр Корлюков. Суперкомпилятор строит не одно решение, а множество всех решений. Видно, что последовательности C M MC CC и M C CC MC относятся к бессмысленным. Можно, конечно, за счет усложнения программы удалять и эти перевозки.
Андрей Немытых. Что вполне естественно - более менее содержательный интерпретатор умеет интерпретировать бесконечные циклы, и более того, если язык достаточно содержателен, то автоматически их выявить невозможно.
Александр Корлюков. Я поступил так. Внес изменения в программу, оставив перевозки MM, MC, MC с левого берега на правый и M, C с правого на левый. Смысл в том, чтобы увеличивать количество людей справа и тем самым приближаться к решению. Замечу, что такое изменение программы могло оказаться неудачным, например, для трех миссионеров и трех каннибалов, как я попробовал, перевозки из этого класса не существует.
Аркадий Климов. А почему исключил СС? Еще можно попробовать оставить только такие перевозки, в которых в лодке сидит хотя бы один каннибал - в функции гребца :-).
Андрей Немытых. На мой взгляд, текст данного письма является почти готовой замечательной статьёй. "Доказательство теорем" -- этот термин я бы выкинул совсем, слишком уж он мне не нравится в данном контексте. Можно было бы сформулировать так -- использование суперкомпилятора ( как инструмента ) в работе математика. ( В том смысле, как используется калькулятор. ) Работа , на мой взгляд, совершенно замечательная, исчерпывающая и поучительна.
На самом деле, продолжая аналогию с интерпретатором, можно говорить, что проведён исчерпывающий анализ суперкомпиляции нестандартного интерпретатора, -- и результат экспериментов тоже замечателен, суперкомпилятор выкинул максимальное число недостижимых путей интерпретации. Ровно в том смысле, в каком рассматривает Валентин Фёдорович нестандарный процесс интерпретации Рефал-программы в статье JFP-93. И видимо, здесь естественным и очень интересным был бы следующий ход -- рассмотрение - изучение в том же контексте других интерпретаторов.
А именно, очень интересен интерпретатор идея которого описана в упомянутой мной выше статье Валентина Фёдоровича. Я позволю себе кратко сформулировать основную цель этого интерпретатора, точнее его суперкомпиляции.
Рассмотрим программу на Рефале
$ENTRY Go { e.1 = <Fab e.1 ()>; }
Fab {
'a' e.1 (e.2) = <Fab e.1 (e.2 'b')>;
s.x e.1 (e.2) = <Fab e.1 (e.2 s.x)>;
(e.2) = <Fbc e.2 ()>;
}
Fbc {
'b' e.1 (e.2) = <Fbc e.1 (e.2 'c')>;
s.x e.1 (e.2) = <Fbc e.1 (e.2 s.x)>;
(e.2) = e.2;
}
Рассмотрим множество формальных синтаксических путей --
последовательностей шагов Рефал-машины ( не семантических ) этой
программы. В них есть заведомо семантически недостижимые. Например
такой:
&nb