Перекрестное опыление

Robert S. Boyer

J Strother Moore

В 2005 году премия ACM за достижения в области программных систем была присуждена Роберту Бойеру, Джею Муру и Мэту Кауфману за "пионерскую разработку эффективного доказывателя теорем (известного как доказыватель Бойера-Мура)".

Эта разработка, по сути дела, началась с диссертации Мура 1973 под названием "Вычислительная логика", которую, кстати можно скачать. (Диссертация Бойера также доступна). Программной статьей считается текст Бойера и Мура 1975 года "Proving Theorems about LISP Functions",  которая и по сей день будоражит ум и легко читается.

Мне кажется, что материал "ожил" из-за упрощений, которые делаются сразу:

1. Авторы рассматривают preLISP, где есть только ноль, булевы и cons-пары.
2. Все функции считаются тотальными.

Система нацелена на доказывание утверждений вроде

(EQUAL (REVERSE (REVERSE A)) A)

Здесь A - сколемовская константа: то есть, вместо A подразумевается любое выражение. Цель системы - показать, что вычисление может завершиться только с результатом TRUE. 

В основе системы - интерпретатор, понимающий сколемовские константы. 

Не будем пересказывать все технические приемы того, как система пытается доказать теорему - все они за исключением одного достаточно очевидны. Изюминкой является прием перекрестного опыления (cross-fertilization).

Без этого приема система практически ничего не доказывает. Суть приема: достаточно часто при доказательстве по индукции возникают утверждения (которые нужно доказать) вида

(IMPLIES 

  (EQUAL S T) 

  (EQUAL E1 E2))

В выражениях E1 и E2 могут присутствовать  выражения S и Т. Утверждение может упроститься, если избавиться от предпосылки. Эвристика перекрестного опыления советует избавиться от предпосылки так: нужно заменить все вхождения T в выражении E2 на S и удалить предпосылку. То есть переписать:

(IMPLIES 

  (EQUAL S T) 

  (EQUAL E1 E2)) ⇒ (EQUAL E1 E2{T/S})

Можно было бы переписывать и по-другому, но такое переписывание лучше всего работает.

Как получилась мощная система?

1. Упростили: отбросили все ненужное.
2. Нашли интересное нетривиальное решения для "часто встречающегося на практике случая" - эвристика перекрестного опыления.

Авторы довели идеи до конечных продуктов - NQTHM, ACL2 и других доказывателей теорем. Среди прочего: придумали собственный алгоритм Бойера-Мура нахождения подстроки в строке, придумали потрясающе простой и красивый алгоритм (бесспорная жемчужина программирования) нахождения победителя при голосовании абсолютным большинством -  MJRTY, работающий линейное время. Работа про MJRTY заслуживает особого упоминания: Бойер и Мур приводят в статье программу не Фортране корректность которой они доказали с помощью своих же доказывателей теорем! (Статью с описанием MJRTY больше десяти лет отказывались печатать и она была опубликована лишь по счастливой случайности в 1991).

Сколько понадобилось усилий самих авторов системы, чтобы ей продуктивно воспользоваться? 20 часов умственных усилий и система доказывает корректность всего за 55 минут!

The entire effort of specifying MJRTY and getting the 61 verification conditions proved required about 20 man hours. Most of the time was spent identifying problems caused by incorrectly written invariants, overcoming inadequacies in the theorem-prover by identifying appropriate lemmas, and struggling with the still awkward interface to our Fortran verification condition generator. It requires about 55 minutes of computer time to prove the final list of 66 theorems. The time was measured on a Foonly F2 Computer (about 30 percent as fast as a DEC 2060) running small INTERLISP-10. A total of 42 minutes was required for theorem-proving, 8 minutes for garbage collection, and 5 minutes for printing out the proofs. (отсюда)

К большинству работающих примеров, распространяемых с системами, написаны весьма занимательные комментарии, вроде:

This is a formalization, in the Nqthm logic, of a card trick theorem that de Bruijn taught Huet, Huet taught Moore, and Moore taught me. Mine differs from a treatment of the same problem by Moore in that he uses oracles to simulate shuffling, whereas I use a merge predicate. (link)

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

To run this list of events takes about 1 hour of cpu time on a Sun-3/280.  To develop this list of events took about 15 hours of work. (оттуда же)

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