Вопрос о логике и соответствии Карри-Говарда

Question

Не могли бы вы объяснить, какова основная связь между основами логического программирования и феноменом синтаксического сходства между системами типов и традиционной логикой?

Answer 1

Соответствие Карри-Ховарда касается не логического программирования, а функционального программирования. Фундаментальная механика Пролога обоснована в теории доказательств техникой разрешения Джона Робинсона , которая показывает, как можно проверить, являются ли логические формулы, выраженные в предложениях Рога, выполнимыми то есть, можете ли вы найти термины для замены их логических переменных, которые делают их истинными.

Таким образом, логическое программирование связано с определением программ в качестве логических формул, а вычисление программы, как я уже сказал, является некой формой логического вывода в теории Пролога. В отличие от этого соответствие Карри-Говарда показывает, как доказательства в специальной формуле логики, называемой естественным выводом , соответствуют программам в лямбда-исчислении с типом программы, соответствующей формуле, которую доказательство доказывает; Вычисления в лямбда-исчислении соответствуют важному явлению в теории доказательств, называемому нормализацией, которое превращает доказательства в новые, более прямые доказательства. Таким образом, логическое программирование и функциональное программирование соответствуют различным уровням в этих логиках: логические программы соответствуют формулам логики, в то время как функциональные программы соответствуют доказательствам формул.

Есть еще одно отличие: используемая логика, как правило, различна. Логическое программирование обычно использует более простую логику & mdash; Как я уже сказал, Prolog основан на клаузлах Хорна, которые представляют собой строго ограниченный класс формул, в которых значения не могут быть вложенными, и в них нет дизъюнкций, хотя Prolog восстанавливает всю силу классической логики, используя правило сокращения. Напротив, функциональные языки программирования, такие как Haskell, интенсивно используют программы, типы которых имеют вложенные значения и украшены всевозможными формами полиморфизма. Они также основаны на интуиционистской логике, классе логик, который запрещает использование принципа исключенной середины, на котором основан вычислительный механизм Робинсона.

Некоторые другие пункты:

1. Логическое программирование возможно основать на более сложной логике, чем предложения Хорна; например, лямбда-пролог основан на интуиционистской логике, с вычислительным механизмом, отличным от разрешения.
2. Дейл Миллер назвал теоретико-доказательную парадигму логического программирования поиском в качестве метафоры , в отличие от доказательств в виде метафоры программ, которая является еще одним термином, используемым для карри. -Направление корреспонденции.

Answer 2

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

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

Создание целых программ таким способом не практично, но может быть полезно для заполнения утомительных деталей в программах, и есть некоторые важные примеры этого на практике. Основным примером этого является структурный подтип, который соответствует заполнению нескольких этапов доказательства с помощью простого доказательства соответствия. Гораздо более сложный пример - система классов типов в Haskell, которая включает в себя особый вид целенаправленного поиска - в крайнем случае это включает в себя Тьюрингово-логическую форму программирования во время компиляции.