Как работает Джинн?

Хорошо, поэтому я понимаю, что, вероятно, буду сожалеть об этом всю оставшуюся жизнь, но... Как работает Джинн?

В документации говорится, что он использует алгоритм, который является "расширением LJ" и указывает на длинную запутанную бумагу о LJT. Насколько я могу судить, это сложная система высокоформализованных правил для определения, какие логические утверждения верны или ложны. Но это даже не объясняет, как вы превращаете подпись типа в исполняемое выражение. Предположительно, всякое сложное формальное мышление каким-то образом связано, но картина крайне неполна.

Это похоже на то время, когда я попытался написать интерпретатор Pascal в BASIC. (Не смейтесь, мне было всего двенадцать...) Я потратил несколько часов, пытаясь понять это, и в конце концов мне пришлось сдаться. Я просто не мог понять, как черт вы получаете от гигантской строки, содержащей целую программу, к чему-то, что вы можете сравнить с известными фрагментами программы, чтобы решить, что на самом деле делать.

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

Я подозреваю, что то, что делает Джинн, принципиально просто, но мне не хватает важной детали, которая объясняет, как вся эта сложная логическая гимнастика связана с исходным кодом Haskell...

Ответ 1

Джинн является доказательством теоремы. Кажется, ваш вопрос: что доказывает теорема в программировании?

Сильно типизированное программирование имеет очень тесную связь с логикой. В частности, традиционные функциональные языки в традиции ML тесно связаны с Intuitionist Пропозициональной логикой.

Лозунг: "Программы - это доказательства, предложение, которое доказывает программа, - это его тип".
В общем, вы можете думать о

 foo :: Foo

что foo является доказательством формулы foo. Например, тип

 a -> b

соответствует функциям от a до b, поэтому, если у вас есть доказательство a и доказательство a -> b, у вас есть доказательство b. Таким образом, функция отлично соответствует логике. Аналогично

(a,b)

Соответствует соединению (логике и). Таким образом, логическая тавтология a -> b -> a & b соответствует типу Haskell a -> b -> (a,b) и имеет доказательство:

\a b -> (a,b)

это "правило введения", Пока fst :: (a,b) -> a и snd :: (a,b) -> b соответствуют правилам 2 "и исключения"

аналогично, a OR b соответствует типу Haskell Either a b.

Это соответствие иногда называют "изоморфизмом Карри-Говарда" или "Корреспонденция Карри-Говарда" после Haskell Карри и Уильям Элвин Говард

В Хаскелле эта история осложняется нетоальностью.

Джинн - это "просто" доказательство теоремы.

Если вы заинтересованы в попытке написать клон, на первой странице результатов Google для "Simple Test Prover" есть этот документ, в котором описывается написание доказательства теоремы для LK, который, как представляется, написан на SML.

Изменить: как "как доказать теорему?" Ответ в том, что в некотором смысле это не сложно. Это просто проблема поиска:

Рассмотрим задачу, которая была скопирована так: мы имеем множество предложений, которые мы знаем, как доказать S, и предложение, которое мы хотим доказать P. Что нам делать? Прежде всего, мы спрашиваем: у нас уже есть доказательство P в S? Если это так, мы можем использовать это, если не можем сопоставить шаблон на P

case P of
   (a -> b) -> add a to S, and prove b (-> introduction)
   (a ^ b)  -> prove a, then prove b (and introduction)
   (a v b)  -> try to prove a, if that doesn't work prove b (or introduction)

если ни одна из них не работает

for each conjunction `a ^ b` in S, add a and b to S (and elimination)
for each disjunction `a v b` in S, try proving `(a -> P) ^ (b -> P)` (or elimination)
for each implication `a -> P` is S, try proving `a` (-> elimination)

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

Что касается: "Как можно преобразовать доказательства в Haskell?"

Каждое правило вывода в формальной системе соответствует некоторой простой конструкции Haskell, поэтому, если у вас есть дерево правил вывода, вы можете создать соответствующую программу - Haskell - это язык доказательств в конце концов.

Внедрение внедрения:

\s -> ?

Или введение

Left
Right

И введение

\a b -> (a,b)

И устранение

fst
snd

и т.д.

augustss говорит в своем ответе, что они, как он реализовал это в Джинне, немного утомительны для SO-ответа. Я уверен, однако, что вы можете понять, как реализовать его самостоятельно.

Ответ 2

В наиболее общих терминах, согласно изоморфизму Карри-Говарда, существует соответствие между типами и предложениями, а также значениями и доказательствами. Джинн использует это соответствие.

Будь более конкретным, скажите, что вы хотите найти термин Haskell типа (a, b) -> (b, a). Сначала вы переводите тип в оператор в логике (Djinn использует пропозициональную логику, т.е. Без квантификаторов). Логическая инструкция (A and B) is true implies (B and A) is true. Следующий шаг - доказать это. Для пропозициональной логики всегда можно механически доказать или опровергнуть утверждение. Если мы можем опровергнуть это, то это означает, что не может быть никакого соответствующего члена в (завершение) Haskell. Если мы сможем доказать это, то есть член Хаскелла этого типа, и, кроме того, член Хаскелла имеет ту же структуру, что и доказательство.

Последнее утверждение должно быть квалифицированным. Существуют различные наборы аксиом и правил вывода, которые вы можете выбрать, чтобы доказать утверждение. Существует только соответствие между доказательством и термином Хаскелла, если вы выберете конструктивную логику. "Обычная", т.е. Классическая логика имеет такие вещи, как A or (not A) как аксиому. Это соответствовало бы типу Haskell Either a (a -> Void), но там нет слова Хаскелла этого типа, поэтому мы не можем использовать классическую логику. По-прежнему верно, что любое пропозициональное утверждение может быть доказано или опровергнуто в конструктивной логике высказываний, но оно гораздо более активно участвует в этом, чем в классической логике.

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

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

В качестве заключительного комментария для вас: Either a (a -> Void) может быть реализовано, если у вас есть Scheme call/cc. Выберите более конкретный тип, например Either a (a -> Int), и выясните, как.

Ответ 3

Возможно, я смотрю на все это неправильно. Возможно, вся эта формальная логика - всего лишь отвлечение. Вместо того, чтобы смотреть на правила вычета для LJT или что-то еще, может быть, я должен это делать, глядя на Haskell.

Есть, что, 6 возможных выражений в Haskell? И каждый из них устанавливает ограничения типа на переменные, которые он использует, не так ли? Поэтому, возможно, я просто создаю одну новую переменную для каждого аргумента в типе функции и начинаю видеть, какие выражения я могу построить.

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

Все становится интереснее, если вы позволяете вашему коду вызывать существующие функции верхнего уровня. Помимо забавных проблем с полиморфными типами, возникает вопрос о том, какие функции будут или не помогут вам.

Очевидно, мне придется уйти и подумать об этом некоторое время...