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

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

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

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

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


logic combinators theorem-proving theory
person rwallace    schedule 03.09.2009    source источник

Ответы (3)


arrow_upward
7
arrow_downward

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

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

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

  • ``(I E) = E'' выводимо (схема I-аксиомы)

Я полагаю, ваш вопрос спрашивает

можем ли мы вывести формально (оставаясь внутри системы), что такое отдельно определенное I ведет себя точно так же, как ((S K) K) при использовании в качестве функций в редукциях?

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

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

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

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

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

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

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

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

Язык

АЛФАВИТ

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

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

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

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

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

УСЛОВИЯ

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

  • Любая константа является термином
  • Любая переменная является термином
  • Если E — это термин, и F — тоже термин, то (E F) также является термином

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

E F G H

вместо

(((E F) G) H).

Вычет

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

  • ``K E F = E'' выводимо (K-аксиома схема)
  • ``S F G H = F H (G H)'' выводим (схема S-аксиомы)
  • ``I E = E'' выводимо (схема I-аксиомы)

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

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

  • ``E = E'' можно вывести (аксиома рефлексивности)
  • Если "E = F" выводимо, то "F = E" также выводимо ( Симметрия правило вывода)
  • Если "E = F" выводимо, и "F = G" тоже выводимо, то также " E = G" является приводимым (правило Transitivity)
  • Если "E = F" выводимо, то "E G = F G" также можно вывести (правило Лейбница I)
  • Если "E = F" выводимо, то "G E = G F" также можно вывести (правило Лейбница II)

Вопрос

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

Можно ли вывести предложение «I = S K K»?

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

Если E F = G F выводимо, то также E = G выводимый

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

``I E = S K K E'' можно вывести

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

  • это верно для E := K
  • верно для E := S
  • это верно для E := K K
  • .
  • .
  • .

...

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

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

  • Если переменная x не является частью терминов ни E, ни F, и оператор (E x) = (F x) выводимо, то E = F также выводимо (правило вывода Extensionality)

Самое сложное в этой аксиоме, легко приводящее к путанице: x — это объектные переменные, полностью эмансипированные и уважаемые части нашего объектного языка, тогда как E и G< /em> — это метапеременные, не являющиеся частью объектного языка, но используемые только для краткой записи схем аксиом.

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

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

Теперь докажем утверждение, что ``I = S K K''.

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

  • предложение ``I x = x'' является примером схемы I-аксиомы с выражением [E := x]

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

  • Предложение «S K K x = K x (K x)» экземпляр схемы S-аксиомы с экземплярами [E := K, F := K , G := x], поэтому выводимый
  • Утверждение «K x (K x) = x» является примером схемы K-аксиомы с реализациями [E := x, F := K x], поэтому выводимый

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

  • Утверждение "S K K x = K x (K x)" соответствует первая посылка правила транзитивности вывода, а утверждение «K x (K x) = x» соответствует второй посылке этого правила вывода. вывод. Экземпляры: [E := S K K x, F := K x (K x), G = x]. Таким образом, вывод также верен: E = G. Переписывая заключение с теми же конкретизациями, мы получаем утверждение «S K K x = x», таким образом, это выводимо.

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

  • Используя «S K K x = x», мы можем вывести «x = S K< /strong> К х"

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

  • Используя «I x = x» и «x = S K K x», мы можем вывести «< strong>I x = S K K x"

Теперь мы проложили путь к решающему моменту:

  • Утверждение «I x = S K K x» соответствует первой предпосылке Расширения. strong> правило вывода: (E x) = (F x), с экземплярами [E := I, F := S K K]. Таким образом, вывод также должен иметь место, то есть "E = F" с теми же конкретизациями ([E := I< /strong>, F := S K K]), что дает предложение "I = S K K", что было доказано.

Csörnyei, Zoltán (2007): Lambda-calkulus. Функциональная программа alapjai. Будапешт: Typotex. ISBN-978-963-9664-46-3.

person physis    schedule 08.09.2009

arrow_upward
2
arrow_downward

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

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

Так как SKanything = anything, то SKanything является функцией тождества, как и I.

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

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

person Juliet    schedule 03.09.2009
comment
Прошло некоторое время с тех пор, как я играл с комбинаторами SKI, но я, кажется, помню, как доказал, что I = SKK на бумаге, что подразумевает, что I получено из S и K, а не аксиома. Этот пост предоставляется как есть и без каких-либо гарантий. - person Juliet; 03.09.2009
comment
Должно быть, SKчто-нибудь = I. SKчто-нибудь (другое) = другое - person dansalmo; 11.03.2013

arrow_upward
0
arrow_downward

Обычные аксиомы полны для бета-равенства, но не дают эта-равенства. Карри нашел набор из примерно тридцати аксиом к обычным, чтобы получить полноту бета-эта-равенства. Они перечислены в книге Хиндли и Селдина Введение в комбинаторы и лямбда-исчисление.

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

person Charles Stewart    schedule 01.02.2010