Аксиомы комбинаторной логики

Question

Я провожу несколько экспериментов по доказательству теорем с помощью комбинаторной логики, и это выглядит многообещающе, но есть один камень преткновения:уже отмечалось, что в комбинаторной логике верно, что, например,I = SKK, но это не теорема, ее нужно добавить как аксиому.Кто-нибудь знает полный список аксиом, которые необходимо добавить?

Редактировать:Вы, конечно, можете доказать вручную, что I = SKK, но если я чего-то не упускаю, то это не теорема в системе комбинаторной логики с равенством.При этом вы можете просто макросом расширить I до SKK...но я все еще упускаю что-то важное.Взяв набор предложений p(X) и ~p(X), которые легко разрешают противоречия в обычной логике первого порядка, и преобразуя их в SK, выполняя замену и оценивая все вызовы S и K, моя программа генерирует следующее (где я использую ' для обратного кавычка Unlambda):

''eq '''''''''''s 'k s'''''s 'k s'''s 'k k 'k eq '''s ''s 'k s 'k 'k k'''s 'k k 'k false 'правда' правда

Похоже, мне нужен соответствующий набор правил для обработки частичных вызовов 'k и ', я просто не понимаю, какими должны быть эти правила, и вся литература, которую я могу найти в этой области, была написана для целевая аудитория математиков, а не программистов.Я подозреваю, что ответ, вероятно, будет довольно простым, если вы его поймете.

Answer 1

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

• Предложение ``Э = Э'' выводимо (Рефлексивность схема аксиом, созданная для каждого возможного термина, обозначенного здесь метапеременной Э)

Таким образом, я полагаю, что в дальнейшем Ваши вопросы исследуют другой подход:когда комбинатор я не определяется как просто псевдоним для сложного термина ((СК) К), но представлен как автономный базовый комбинатор константа сама по себе, чья операционная семантика объявлена явно по аксиоме схема

• ``(я Э) = Э'' выводимо (Я-аксиома схема)

Полагаю, Ваш вопрос задается

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

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

Я думаю, нам нужно принять такой подход к построению комбинаторной логики, чтобы разрешить также использование переменных в объектном языке.Ой, конечно, я имею в виду «просто» бесплатно ценности.Использование связанных переменных было бы мошенничеством, мы должны оставаться в сфере комбинаторной логики.Использование бесплатных переменных — это не мошенничество, это честный инструмент.Таким образом, мы можем провести необходимое Вам формальное доказательство.

Помимо простых аксиом равенства и правил вывода (транзитивность, рефлексивность, симметрия, правила Лейбница), мы должны добавить экстенсиональность правило вывода равенства.Вот тут-то и важны свободные переменные.

В Чёрниеи 2007:157-158, я нашел следующий подход.Я думаю, что таким образом можно доказать.

Некоторые замечания:

На самом деле большинство аксиом схемы аксиом, состоящее из бесконечного числа экземпляров аксиомы.Экземпляры должны быть созданы для всех возможных Э, Ф, г условия.Здесь я использую курсив для обозначения метапеременных.

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

Теперь давайте посмотрим на нашу структуру:

Язык

АЛФАВИТ

Константы:Следующие три называются константами: К, С, я.

Я добавил константу я только потому, что Ваш вопрос предполагает, что мы не определили комбинатор я как просто псевдоним/макрос для сложного термина С К К, но это отдельная константа сама по себе.

Константы я буду обозначать жирными римскими заглавными буквами.

Знак заявления:Знака @ для ``application'' достаточно (префиксная запись с арностью 2).В качестве синтаксического сахара я использую здесь скобки вместо явного знака приложения:Я буду использовать явные как открывающие, так и закрывающие знаки.

Переменные:Хотя логика комбинатора не использует связанные переменные, область видимости и т. д., мы можем ввести свободные переменные.Я подозреваю, что они не только являются синтаксическим сахаром, но и могут усилить систему дедукции.Я предполагаю, что Ваш вопрос потребует их использования.Алфавитом переменных будет любое перечислимое бесконечное множество (непересекающееся из констант и знаков скобок), я буду обозначать их здесь неформатными римскими строчными буквами x, y, z...

УСЛОВИЯ

Термины определяются индуктивно:

• Любая константа – это термин
• Любая переменная является термином
• Если Э это термин, и Ф это тоже термин, тогда тоже (Э Ф) это термин

Иногда я использую практические соглашения в качестве синтаксического сахара, например.писать

Э Ф г ЧАС

вместо

(((Э Ф) г) ЧАС).

Вычет

Схемы аксиом преобразования:

• ``К Э Ф = Э'' выводимо (К-аксиома схема)
• ``С Ф г ЧАС = Ф ЧАС (г ЧАС)'' выводимо (S-аксиома схема)
• ``я Э = Э'' выводимо (Я-аксиома схема)

Я добавил третью аксиому преобразования (я правило) только потому, что Ваш вопрос предполагает, что мы не определенный комбинатор я как псевдоним/макрос для С К К.

Схемы аксиом равенства и правила вывода

• ``Э = Э'' выводимо (Рефлексивность аксиома)
• Если "Э = Ф"выводимо, то"Ф = Э" также выводимо (Симметрия правило вывода)
• Если "Э = Ф"выводимо, и"Ф = г" тоже выводимо, тогда также "Э = г"приводима (Транзитивность правило)
• Если "Э = Ф"выводимо, то"Э г = Ф г" также выводимо (Правило Лейбница I)
• Если "Э = Ф"выводимо, то"г Э = г Ф" также выводимо (Правило Лейбница II)

Вопрос

Теперь давайте разберемся в Вашем вопросе.Я предполагаю, что определенная до сих пор система выводов недостаточно сильна, чтобы доказать Ваш вопрос.

Это предложение"я = С К К"выводимый?

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

Если Э Ф = г Ф выводимо, то также Э = г выводима

не справится с задачей:мы видим, что это не дает того, чего мы хотим.Используя его, мы можем доказать, что

``я Э = С К К Э'' выводимо

для каждого Э термина «экземпляр», но эти результаты представляют собой лишь отдельные экземпляры и не могут использоваться в целом для дальнейших выводов.Мы имеем только конкретные результаты (бесконечно много), не имея возможности их обобщить:

• это справедливо для Э := К
• держится за Э := С
• это справедливо для Э := К К
• .
• .
• .

...

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

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

• Если переменная x не является частью термов Э ни Ф, и утверждение (Э х) = (Ф x) выводимо, то Э = Ф также выводимо (Экстенсиональность правило вывода)

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

(Примечание:Точнее, правило вывода экстенсиональности следует формализовать более тщательно, введя метапеременная Икс из всех возможных объект переменные x, y, z..., а также другой вид метапеременная Э из всех возможных экземпляры терминов.Но это различие между двумя видами метапеременных и объектными переменными здесь не столь дидактично и не слишком сильно влияет на Ваш вопрос.)

Доказательство

Докажем теперь утверждение, что «я = С К К''.

Шаги для левой стороны:

• предложение ``я x = x'' является экземпляром Я-аксиома схема с установкой [Э := х]

Шаги для правой стороны:

• Предложение "С К К х = К Икс (К x)» является экземпляром S-аксиома схема с экземплярами [Э := К, Ф := К, г := x], следовательно, оно выводимо
• Предложение "К Икс (К x) = x» является экземпляром К-аксиома схема с экземплярами [Э := х, Ф := К x], следовательно, оно выводимо

Транзитивность равенства:

• Заявление "С К К х = К Икс (К x)» соответствует первой посылке транзитивность правило вывода и утверждение "К Икс (К x) = x» соответствует второй посылке этого правила вывода.Экземпляры [Э := С К К Икс, Ф := К Икс (К Икс), г = х].Таким образом, справедлив и вывод: Э = г.Переписав заключение с теми же экземплярами, получим утверждение "С К К x = x", таким образом, это выводимо.

Симметрия равенства:

• С использованием "С К К x = x», мы можем сделать вывод «x = С К К Икс"

Транзитивность равенства:

• С использованием "я х = х» и «х = С К К х", мы можем сделать вывод "я х = С К К Икс"

Теперь мы подготовили почву для решающего момента:

• Предложение "я х = С К К x» соответствует первой посылке Расширение правило вывода:(Э х) = (Ф x), с экземплярами [Э := я, Ф := С К К].Таким образом, вывод также должен иметь место, а именно: «Э = Ф" с теми же экземплярами ([Э := я, Ф := С К К]), что дает предложение "я = С К К", quod Erat DemonStrandum.

---

Чёрньей, Золтан (2007): Лямбда-исчисление.Функциональные функции программируются автоматически. Будапешт:Типотекс.ISBN-978-963-9664-46-3.

Answer 2

Вам не нужно определять Я как аксиому.Начните со следующего:

I.x = x
K.x y = x
S.x y z = x z (y z)

С SKчто-либо = что-либо, затем SKчто-либо является тождественной функцией, как и I.

Так, I = SKK и I = SKS.Нет необходимости определять I как аксиому, вы можете определить его как синтаксический сахар, который является псевдонимом SKK.

Определения S и K — это всего лишь аксиомы.

Answer 3

Обычные аксиомы полны для бета-равенства, но не дают эта-равенства.Карри нашел набор из примерно тридцати аксиом помимо обычных, чтобы получить полноту для бета-эта-равенства.Они перечислены в Hindley & Seldin's. Введение в комбинаторы и лямбда-исчисление.

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