Я думаю, что Ваш вопрос очень, очень интересный. Если Вы также имели в виду, что Вы хотите знать теоретические корни, стоящие за Вашим вопросом, то, я думаю, мы можем абстрагироваться от Хаскелла и исследовать Ваш вопрос в более общих понятиях алгоритма. Что касается Haskell, я думаю, что следующие два факта имеют значение:
- Функции первоклассных граждан в Хаскеле
- Haskell завершен по Тьюрингу
но я еще не обсуждал (как именно здесь важна сила языка).
Возможность для особых случаев, но теорема об отсутствии действий для всеобъемлющего
Я думаю, в корнях две теоремы информатики дают ответ. Если мы хотим абстрагироваться от технических деталей, мы можем исследовать Ваш вопрос в лямбда-исчислении (или в комбинаторной логике). Можно ли в них определить равенство? Итак, давайте сначала ограничимся областью лямбда-исчисления или комбинаторной логики.
Следует отметить, что оба эти алгоритмических подхода очень минималистичны. В них нет `` предопределенных '' типов данных, даже чисел, логических значений и списков. Но Вы можете имитировать их всех умными способами .
Таким образом, Вы можете имитировать все значимые типы данных даже в таких минималистических «функциональных языках», как лямбда-исчисление и комбинаторная логика. Вы можете использовать лямбда-функции (или комбинаторы) в умной сцене, которая имитирует нужный тип данных.
Теперь давайте сначала попробуем ответить на Ваши вопросы на этих минималистических функциональных языках, чтобы выяснить, является ли ответ специфичным для Хаскеля, или, скорее, простым следствием некоторых более общих теорем.
- Теорема Бёма предусматривает: для любых двух ранее заданных различных выражений (которые останавливают и не замораживают компьютер) всегда можно написать подходящую функцию тестирования, которая правильно решает, являются ли два приведенных выражения семантически то же самое (Csörnyei 2007: 132, = Th 7.2.2). В большинстве практических случаев (списки, деревья, логические значения, числа) теорема Бёма предусматривает, что подходящая конкретная функция равенства всегда может быть записана. См. Пример для списков в Tromp 1999 : Sec 2.
- Теорема Скотта-Карри о неразрешимости исключает возможность написания любой всеобщей функции равенства, значимой для каждой возможной сцены (Чёрный 2007: 140, = Th 7.4.1).
Теорема го
После того, как вы "реализовали" тип данных, вы можете написать для него соответствующую функцию равенства. Для большинства практических случаев (списки, числа, выборки анализа случаев) не существует мистического «типа данных», для которого не хватало бы соответствующей функции равенства. Этот положительный ответ дает теорема Бёма.
Вы можете написать функцию равенства церковных чисел, которая принимает две церковные цифры и отвечает, равны ли они. Вы можете написать другую лямбда-функцию / комбинатор, которая принимает два (церковных) булевых числа и отвечает, равны они или нет. Кроме того, Вы можете реализовать списки в чистом лямбда-исчислении / CL (предложенный способ - использовать понятие катаморфизмов), а затем, Вы можете определить функцию, которая отвечает равенству для списков логических значений. Вы можете написать другую функцию, которая отвечает равенству для списков церковных цифр. Вы также можете реализовать деревья, и после этого вы можете написать функцию, которая отвечает за равенство для деревьев (для булевых и других - для церковных чисел).
Вы можете автоматизировать некоторые из этих заданий, но не все. Вы можете автоматически получить некоторые (но не все) функции равенства автоматически. Если у вас уже есть определенные функции отображения для деревьев и списков и функции равенства для логических чисел и чисел, вы можете автоматически вывести функции равенства и для логических деревьев, логических списков, списков чисел и числовых деревьев.
Теорема о запрете движения
Но нет способа определить единую полностью автоматическую функцию равенства, работающую для всех возможных типов данных. Если вы «внедряете» конкретный данный тип данных в лямбда-исчисление, вам обычно приходится планировать его конкретную функцию равенства для этой сцены.
Более того, нет способа определить лямбда-функцию, которая бы принимала два лямбда-члена и отвечала бы, будут ли два лямбда-члена вести себя одинаково при уменьшении. Более того, нет способа определить лямбда-функцию, которая бы принимала представление ( цитата ) двух лямбда-терминов и отвечала бы, будут ли вести себя два исходных лямбда-термина так же, когда сокращается (Csörnyei 2007: 141, Conseq 7.4.3). Этот ответ no-go предоставляется теоремой Скотта-Карри о неразрешимости (Csörnyei 2007: 140, Th 7.4.1).
В других алгоритмах подходит
Думаю, два приведенных выше ответа не ограничиваются лямбда-исчислением и комбинаторной логикой. Аналогичная возможность и ограничение применяются для некоторых других концепций алгоритма. Например, не существует рекурсивной функции, которая бы брала числа Гёделя двух унарных функций и решала, ведут ли себя эти кодированные функции одинаково экстенсивно (Monk 1976: 84, = Cor 5.18). Это является следствием теоремы Райса (Monk 1976: 84, = Th 5.17). Я чувствую, что теорема Райса формально звучит очень похоже на теорему Скотта-Карри о неразрешимости, но я еще не рассмотрел ее.
Полное равенство в очень ограниченном смысле
Если бы я хотел написать интерпретатор комбинаторной логики, который обеспечивает всестороннее тестирование на равенство (ограничено для термов, терминов с нормальной формой), то я бы реализовал это так:
- Я бы свел оба рассматриваемых комбинаторных логических термина к их нормальным формам,
- и посмотрите, являются ли они идентичными терминам .
Если это так, то их нередуцированные исходные формы также должны быть семантически эквивалентны.
Но это работает только с серьезными ограничениями, хотя этот метод хорошо работает для нескольких практических целей. Мы можем выполнять операции с числами, списками, деревьями и т. Д. И проверять, получаем ли мы ожидаемый результат. Моя квинна (написанная в чистой комбинаторной логике) использует эту ограниченную концепцию равенства, и этого достаточно, несмотря на то, что для этой квинны требуются очень сложные конструкции (деревья терминов, реализованные в самой комбинаторной логике).
Я пока не знаю, каковы пределы этой ограниченной концепции равенства, но я подозреваю, что она очень ограничена, если сравнивать с правильным определением равенства. Мотивация его использования заключается в том, что он вообще вычислим, в отличие от неограниченной концепции равенства.
Ограничения можно увидеть также из того факта, что эта концепция ограниченного равенства может работать только для комбинаторов, которые имеют нормальные формы. Для контрпримера: концепция ограниченного равенства не может проверить, является ли I Ω = Ω , хотя мы хорошо знаем, что эти два термина могут быть взаимно преобразованы друг в друга .
Я должен еще рассмотреть, как существование этой ограниченной концепции равенства связано с отрицательными результатами, требуемыми теоремой Скотта-Карри о неразрешимости и теоремой Райс. Обе теоремы имеют дело с частичными функциями, но я пока не знаю, насколько это важно.
Экстенсиональность
Но есть и другие ограничения концепции ограниченного равенства. Он не может иметь дело с концепцией экстенсиональности. Например, он не замечает, что S K будет каким-либо образом связан с K I , несмотря на то, что S K ведет себя так же, как K I , когда они применяются как минимум к двум аргументам:
Последний пример должен быть объяснен более подробно. Мы знаем, что S K и K I не идентичны как термины: S K ≢ K I . Но если мы применим оба, соответственно, к любым двум аргументам X и Y , мы увидим взаимосвязь:
- S K X Y ⊳ * 1164 * K Y ( X Y ) ⊳ Y
- K I X Y ⊳ * 1184 * I Y ⊳ * 1188 * Y
и, конечно, Y ≡ Y , для любого Y .
Конечно, мы не можем "попробовать" такую связанность для каждого возможного X и Y экземпляров аргумента, потому что может быть бесконечно много таких экземпляров CL-терма, которые можно заменить в эти метавариабельные. Но мы не должны застрять в этой проблеме бесконечности. Если мы расширяем наш объектный язык (комбинаторную логику) с помощью (свободных) переменных:
- К - это термин
- S - это термин
- Любая (свободная) переменная является термином (новая строка, это модификация!)
- Если оба X и Y являются терминами, то также ( X Y ) является термином
- Условия не могут быть получены любым другим способом
и мы соответствующим образом определяем правила редукции соответствующим образом, тогда мы можем сформулировать экстенсиональное определение равенства "конечным" способом, не полагаясь на метавариабельные переменные с бесконечными возможными экземплярами.
Таким образом, если свободные переменные допускаются в терминах комбинаторной логики (объектный язык дополнен своими собственными объектными переменными), то расширяемость может быть реализована до некоторой степени. Я еще не учел это. Что касается приведенного выше примера, мы можем использовать обозначение
S K = 2 K I
(Curry & Feys & Craig 1958: 162, = 5 C 5), исходя из того факта, что S K x y и K I x y могут быть доказаны равными (уже не прибегая к расширению) , Здесь x и y не являются метавариабельными значениями для бесконечно многих возможных случаев CL-членов в схемах уравнений, но являются первоклассными гражданами самого объектного языка. Таким образом, это уравнение является не схемой уравнения, а одним уравнением.
Что касается теоретического исследования, мы можем подразумевать = "объединение" = n случаев для всех n .
В качестве альтернативы, равенство может быть определено так, что его индуктивное определение учитывает также экстенсиональность. Мы добавляем еще одно правило вывода, касающееся экстенсиональности (Csörnyei 2007: 158):
- ...
- ...
- Если E , F - комбинаторы, x - переменная (объект), а x не содержится ни в E ни в F , то из E x = F x мы можем вывести E = F
мошенникважно помнить о том, что не нужно содержать, как показывает следующий контрпример: K x ≠ I , несмотря на то, что оно K x x = I x . «Роли» двух (случайно идентичных) переменных вхождений полностью различаются. Исключая такие случаи, это мотивация ограничения.
-
Использование этого нового правила вывода можно проиллюстрировать, продемонстрировав, как теорема S K x = K Я х можно доказать:
- S K = K I считается удержанным, поскольку S K x = K I x уже подтверждено, см. Доказательство ниже:
- S K x = K I x считается удержанным потому что S K x y = K I x y уже подтверждено, см. Ниже:
- S K x y = K I x y можно доказать, не прибегая к экстенсиональности, нам нужны только знакомые правила преобразования.
Каковы эти оставшиеся правила умозаключений? Вот они (Csörnyei 2007: 157):
Схемы аксиом преобразования:
- `` K E F = E '' вычитается ( K-аксиома схема)
- `` S F G H = F H ( G H ) '' вычитается ( S-аксиома схема)
Схемы аксиомы равенства и правила вывода
- `` E = E '' вычитается ( Отражательная схема аксиомы)
- Если выводится « E = F », то выводится также « F = E » ( Симметрия правило вывода)
- Если выводится " E = F " и " F = G " тоже выводим, то также " E = G"сводится ( Транзитивность правило)
- Если " E = F " вычитается, то " E G = F G"также подлежит вычету ( правило Лейбница I )
- Если " E = F " вычитается, то " G E = G F"также подлежит вычету ( правило Лейбница II )
Ссылки
Приложение
Теорема Бёма
Я еще не объяснил четко, как теорема Бёма связана с тем фактом, что в большинстве практических случаев подходящая функция тестирования на равенство может быть обязательно написана для значимого типа данных (даже в таких минималистических функциональных языках, как чисто лямбда-исчисление или комбинаторная логика ).
Заявление
- Пусть E и F - два разных, замкнутых члена лямбда-исчисления,
- и пусть они оба имеют нормальные формы.
Затем, согласно теореме, существует подходящий способ проверки равенства с применением их к подходящей серии аргументов. Другими словами: существует натуральное число n и ряд замкнутых лямбда-терминов G 1 , G 2 , G 3 , ... G n , так что применение их к этой серии аргументов сводится к false и true соответственно:
- E G 1 G 2 G 3 ... G n ⊳ * 1621 * false
- F G 1 G 2 G 3 ... G n ⊳ * 1643 * true
, где true и false - это два хорошо известных, простеньких, легко управляемых и различимых лямбда-термина:
- true ≡ λ x y . х
- false ≡ λ x y . у
Применение
Как эта теорема может быть использована для реализации практических типов данных в чистом лямбда-исчислении? Неявное применение этой теоремы иллюстрируется способом определения связанного списка в комбинаторной логике ( Tromp 1999 : Sec 2).