В чем разница между доказательствами и программами (или между предложениями и типами)?

26

Учитывая, что соответствие Карри-Говарда так широко распространено / расширено, есть ли разница между доказательствами и программами (или между предложениями и типами)? Можем ли мы действительно идентифицировать их?

день
источник
1
Кажется, больше подходит для cstheory.stackexchange.com
Если op захочет, @ me в комментарии, и я могу перенести его для вас.
2
Джон Кроссли написал статью на эту тему, которую я случайно увидел где-то недавно: [В чем разница между доказательствами и программами?] [ Citeseerx.ist.psu.edu/viewdoc/… - я еще не читал, но это пришло рекомендовано ...
TJ Ellis
1
@TJ Эллис, спасибо за ссылку, но после краткого обзора кажется, что статья не отвечает на вопрос, заданный в заголовке (или ответ «они одинаковые»).
Макс Талдыкин
@TJ Эллис, ты видел это сообщение на reddid / r / compsci? Я сделал это;) @max, я чувствовал себя так, поэтому я отправляю этот вопрос.

Ответы:

20

Языки программирования, которые люди используют изо дня в день, не очень хорошо вписываются в соответствие Карри-Ховарда, потому что их системы типов слишком слабы. Чтобы сказать что-то интересное, используя Curry-Howard для императивных программ, нужно иметь более сложную систему типов. Книга « Адаптация доказательств как программ» ставит этот угол с целью синтеза императивных программ. Поскольку зависимые типы становятся все более и более популярными, безусловно, в исследовательских функциональных языках ( Agda , Epigram ), различие становится более размытым. Конечно, вы можете выполнять синтез / извлечение программ в программе проверки теорем Кок (и, вероятно, в других), которая, конечно, основана на Карри-Ховарде.

Переписка Карри-Ховарда может также использоваться в ситуациях, когда доказательства не так четко соответствуют программам (или они не являются программами, которые кто-либо когда-либо будет запускать). Одним из примеров этого является проверка подлинности . Предложения соответствуют заявлениям о том, кто на что уполномочен. Доказательства предоставляют необходимые доказательства наличия предложения, поэтому запрос на авторизацию разрешается. Чтобы закодировать доказательства, вводятся термины доказательства (через Curry-Howard). Условия подтверждения отправляются между сторонами в качестве подтверждения действительности запросов на авторизацию, но они не считаются программами.

Дэйв Кларк
источник
1
Вы должны упомянуть зависимо типизированные языки, так как в них грань между доказательствами и предложениями размыта.
Охад Каммар
1
Верно. Давайте не будем забывать программу синтеза / извлечения Coq.
Дейв Кларк,
К T(е,К)¬К T(е,К)TеК
1
@Kaveh: задайте это как отдельный вопрос. В комментарии вы можете сказать, что «перевод Годеля-Генцена является преобразованием с прохождением продолжения», но что-то менее загадочное не подойдет. :)
Нил Кришнасвами
@Neel, сделано: cstheory.stackexchange.com/q/5245/186
Каве
10

В Coq есть 2 типа (Prop и Set), они используются программистом для разделения того, что является доказательствами, которые не будут генерировать фактический код, и частью доказательства, которая будет использоваться для извлечения исполняемого кода (вашей программы).

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

AFAIK нет автоматического способа различить оба. Это может быть что-то интересное для исследования? Или, может быть, кто-то может указать, что это явно невозможно?

С зависимыми типами не только нет четкого различия между доказательствами и программами, но также нет различия между программами и типами! Единственное отличие будет в том, где появляется тип (или программа), что делает его частью места «программы» или места «типа» данного термина.

Надеюсь, пример прояснит ситуацию:

Когда вы используете функцию тождественности с зависимыми типами, вам нужно передать тип, с которым вы собираетесь использовать функцию! Тип используется в качестве значения в вашей «программе»!

Нетипизированное лямбда-исчисление:

λИкс,Икс

С зависимыми типами:

id: (A: Set) -> A -> A

(λA,(λИкс,Икс))

Если вы используете эту функцию, вы бы сделали это, как в следующем примере:

id Naturals 1

Обратите внимание, что «тип» (в данном случае набор натуральных чисел), передаваемый как значение, отбрасывается, поэтому он никогда не будет вычислен, но все же он находится в части «программа» термина. Это то же самое, что произойдет с «доказательственными» частями, они должны быть там, чтобы термин проверял, но во время вычислений они будут отброшены.

Флавио Ботельо
источник
6

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

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

Конечно, чтобы сделать это следствие несущим информацию более значимым, чем изложение очевидного, вам нужно показать, что программа работает для любого и всех случаев ввода, выводимого из некоторого класса с логическим значением. (И так же для вывода.)

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

Икс:ИксT

Это довольно упрощенно, но я думаю, что это говорит об устойчивости идеи. (Даже если некоторым людям это не понравится. ;-))

Марк Хаманн
источник
очень хороший ответ.
до
Следует, конечно, предположить, что вы имеете в виду конечное доказательства и завершающие программы. Некоторые классы бесконечных программ прекрасно работают как бесконечные доказательства. Это непроизводительные программы без прерывания, которые вы должны остерегаться.
Рен Романо
Я думаю, что это немного сложно, в зависимости от того, как вы определяете конечное и бесконечное в отношении доказательств. В общем, все доказательства, которые мы принимаем, являются конечными, потому что они должны убедить человека за небольшое конечное время. Доказательство, которое опирается на индукционную схему (т. Е. Большинство «бесконечных» доказательств), по этой мере все еще конечно, у них просто есть символические шаги, которые представляют бесконечное, но регулярное вычисление. Действительно бесконечное доказательство, которое, я думаю, большинство из нас отвергнет как действительное доказательство, было бы тем, в котором вы буквально должны были рассмотреть бесконечное число различных фактов для подтверждения.
Марк Хаманн
5

Доказательство неуместно?

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

Но когда вы доказываете некоторую теорему, вас интересует только существование доказательства.

Конечно, с эстетической точки зрения некоторые доказательства являются более простыми / красивыми / вдохновляющими / и т.д. (например, доказательства из Книги).

Макс Талдыкин
источник
4

Если вы принимаете переписку Карри – Ховарда, тогда вопрос в основном философский. «Различны ли доказательства и программы? Конечно. Как? Ну, мы называем доказательства« доказательствами », а программы -« программами ».

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

Это слова естественного языка, используемые для классификации различных областей математического исследования. Что заметил Карри и Говард, так это то, что эти две разные области фактически изучают одно и то же. Заметить эту связь важно, потому что она говорит, что эти разные исследователи должны разговаривать друг с другом. Но на другом уровне заметить связь - значит поверить в разницу между ними. При решении проблемы иногда выгоднее думать о ней как о проблеме программирования, тогда как в других случаях выгоднее думать о ней как о логической проблеме. Эта разница в перспективе, я думаю, важная разница между ними. Но является ли различие во взглядах разницей в идентичности - это глубокий философский вопрос, который был исследован, по крайней мере, еще во времена ФрегеUeber Sinn und Bedeutung .

Рен Романо
источник