Кто-нибудь на самом деле публикует «структурированные доказательства»?

В 1995 году Лесли Лэмпорт опубликовала в журнале American Mathematical Monthly эссе под названием «Как написать доказательство». В эссе Лэмпорт представил концепцию структурированного доказательства , в котором традиционное доказательство высокого уровня дополняется последовательностью более низких уровней. Каждый уровень доказательства расширяет каждый шаг более высокого уровня на подшаги. Количество деталей на самом низком уровне довольно велико — доказательство Лэмпортом иррациональности квадратного корня из 2 занимает 1,5 страницы.

По данным Google Scholar, эссе цитируется более 250 раз, но я никогда не видел доказательств, опубликованных в таком формате. В PDF или на бумаге мельчайшие детали могут быть ошеломляющими; но я думаю, что современные веб-платформы публикации могли бы очень хорошо приспособиться к этому (с иерархическими сворачиваемыми подразделами для каждой части доказательства).

Во всяком случае, есть ли примеры доказательств, опубликованных в формате, предложенном Лэмпортом ?

Мне нравится идея с разборкой! Вы спрашивали об этом на matheducators.stackexchange.com ? Кажется, это было бы особенно полезно для студентов.
Не совсем тот же формат, но посмотрите на работы Роланда Бэкхауса или Ричарда Берда.
Я знаю некоторые учебники, которые работают таким образом. Хотя вместо того, чтобы встраивать поддоказательства, они были представлены как отдельные теоремы/леммы.
Структурированное доказательство появляется в статье Лэмпорта на Paxos research.microsoft.com/en-us/um/people/lamport/pubs/… (§2.1). Тем не менее, я не уверен, демонстрирует ли это доказательство те преимущества, которые, как обычно предполагается, имеет структурированное доказательство, такие как большая удобочитаемость и отсутствие неявной логики... (Я думаю, что его шаг 4 в доказательстве леммы нуждается в большем обосновании, и Шаг 5 говорит нечто отличное от того, что он хочет сказать.)
Где-то в инете есть целая книга, полная структурированных доказательств (а-ля Лэмпорт, а может быть, даже и в его соавторстве). Насколько я помню, его цель — доказать правильность некоторого программного обеспечения, но значительная его часть — это базовая математика; может кто найдет?
Кстати: это должен быть вопрос mathoverflow или math.stackexchange.
О, нашел эту книгу! Томас Л. Родехеффер, Протокол часов Наяды: спецификация, проверка модели и доказательство правильности , research.microsoft.com/apps/pubs/?id=183826 .
Очевидно, что research.microsoft.com/en-us/um/people/lamport/tla/… — хорошее введение в структурированные доказательства с множеством примеров.
Все до сих пор в комментариях и один текущий ответ указывает на то, что вы можете найти множество структурированных доказательств, и в каждом из них есть рука Лэмпорта. Так что, по-видимому, никто , кроме Лэмпорта и его коллег из MS, его не использует.
Также есть доказательство для системы Memoir (390 страниц).
pf2html— это latex2htmlстиль, который реализует разборные иерархически структурированные доказательства для Лэмпорта pf.sty.

Ответы (1)

В то время как большинство людей используют более традиционные стили доказательства, более исчерпывающий структурированный стиль доказательства, который предлагает Лэмпорт, похоже, принят, по крайней мере, в духе, автоматизированными системами доказательства, такими как Coq и собственный TLA+ Лэмпорта . Вводя в цикл очень неинтуитивного игрока (машину), эти системы вынуждают математика быть более точным в отношении каждого шага и предположения и поощряют иерархическую структуру за счет использования синтаксиса стиля языка программирования.

Эти системы проверки, как правило, довольно дороги в использовании, и вы, как правило, не захотите помещать их длинные доказательства в середину бумаги — лучше приложить их в качестве дополнительной информации. Однако они оказываются весьма ценными в критических приложениях, где важно иметь дело со всеми возможными пограничными случаями, например, при разработке микропроцессоров или криптографических протоколов.

Современные доказательства Coq, написанные на ssreflect (например, github.com/hivert/Coq-Combi ), на самом деле не такие длинные! Проблемы, насколько я могу различить (к сожалению) несколько издалека, заключаются в том, что (1) формат Coq не поддерживает удобочитаемость для человека (очень трудно следовать доказательству Coq на ручке и бумаге), (2) что отсутствие экстенсиональности функций и (отсутствие) хорошей поддержки setoids делают многие математические конструкции неприемлемо трудными для работы (забудьте о кодировании кортежа элементов $A$ в виде карты $\left\{1,2,\ldots ,n\право\} \к A$; ...
... ssreflect люди, наоборот, похоже, определяют карты между конечными множествами как кортежи с определенными свойствами только потому, что кортежи знают, как быть равными!), и (3) что инфраструктура все еще находится в постоянном движении, и доказательства могут не соответствовать следующее обновление Coq или ssreflect. Но это абсолютно то, что однажды сработает.
И тут я подумал: «Почему, черт возьми, мой LaTeX не работает?». Этот вопрос действительно должен быть на mathoverflow.
Спасибо! Это интересно, хотя я не верю, что это примеры именно того, о чем я просил.
Кто-нибудь на самом деле публикует «структурированные доказательства»?
СпросиСетьПолитика конфиденциальности1y, 0v