Вопрос о логике и корреспонденции Карри-Howard
Вы могли объяснить меня, каково основное соединение между основными принципами логического программирования и явлением синтаксического подобия между системами типов и стандартной логикой?
2 ответа
Переписка Карри-Ховарда касается не логического, а функционального программирования. Фундаментальная механика Пролога обосновывается в теории доказательств с помощью техники разрешения Джона Робинсона, которая показывает, как можно проверить, являются ли логические формулы, выраженные в виде предложений Хорна, удовлетворительными, то есть можно ли найти термины, которые можно подставить вместо их логических переменных, чтобы они были истинными.
Таким образом, логическое программирование - это задание программ в виде логических формул, а вычисление программы - это некоторая форма доказательного вывода, в Prolog reolution, как я уже говорил. В отличие от этого, соответствие Карри-Ховарда показывает, как доказательства в специальной формулировке логики, называемой естественной дедукцией, соответствуют программам в лямбда-исчислении, причем тип программы соответствует формуле, которую доказывает доказательство; вычисление в лямбда-исчислении соответствует важному явлению в теории доказательств, называемому нормализацией, которое преобразует доказательства в новые, более прямые доказательства. Таким образом, логическое программирование и функциональное программирование соответствуют разным уровням в этих логиках: логические программы соответствуют формулам логики, в то время как функциональные программы соответствуют доказательствам формул.
Есть еще одно различие: используемые логики, как правило, разные. Логическое программирование обычно использует более простые логики - как я уже говорил, Prolog основан на формулах Хорна, которые представляют собой сильно ограниченный класс формул, где импликации не могут быть вложенными, и нет дизъюнкции, хотя Prolog восстанавливает всю силу классической логики, используя правило разрезания. В отличие от них, функциональные языки программирования, такие как Haskell, активно используют программы, типы которых имеют вложенные импликации и украшены всевозможными формами полиморфизма. Они также основаны на интуиционистской логике, классе логик, который запрещает использование принципа исключенной середины, на котором основан вычислительный механизм Робинсона.
Некоторые другие моменты:
- Можно основывать логическое программирование на более сложных логиках, чем формулы Хорна; например, Лямбда-пролог основан на интуиционистской логике, с механизмом вычислений, отличным от резолюции.
- Дейл Миллер назвал доказательно-теоретическую парадигму, лежащую в основе логического программирования, поиск доказательств как программирование метафорой, для контраста с доказательствами как программами метафорой, которая является другим термином, используемым для соответствия Карри-Ховарда.
Логическое программирование в основном связано с целенаправленным поиском доказательств. Структурные отношения между типизированными языками и логикой обычно связаны с функциональными языками, хотя иногда и с императивными, и с другими языками, но не с языками логического программирования напрямую. Эта связь связывает доказательства с программами.
Таким образом, поиск доказательства логического программирования может использоваться для поиска доказательств, которые затем интерпретируются как функциональные программы. Кажется, это самые прямые отношения между ними (как вы и просили).
Такой способ построения целых программ непрактичен, но он может быть полезен для заполнения утомительных деталей в программах, и есть несколько важных примеров этого на практике. Базовым примером этого является структурное выделение подтипов, которое соответствует заполнению нескольких шагов доказательства с помощью простого доказательства вывода. Гораздо более сложным примером является система классов типов Haskell, которая включает определенный вид целенаправленного поиска - в крайнем случае, это включает в себя полную по Тьюрингу форму логического программирования во время компиляции.