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

Question

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

Answer 1

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

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

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

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

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

Answer 2

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

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

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