Комбинаторная логика

Комбинаторная логика - это обозначение, которое устраняет необходимость в количественно выраженных переменных в математической логике. Он был введен Мозесом Шенфинкелем и Хаскеллом Карри, а в последнее время использовался в информатике в качестве теоретической модели вычислений и также как основа для разработки языков функционального программирования. Он основан на комбинаторах, которые были введены Шёнфинкелем в 1920 году с целью предоставления аналогичного способа построения функций - и удаления любого упоминания переменных - особенно в логика предиката. Комбинатор - это функция высшего порядка, которая использует только приложение функции и ранее определенные комбинаторы для определения результата на основе своих аргументов.

Содержание

• 1 В математике
• 2 В вычислениях
• 3 Резюме лямбда-исчисления
• 4 Комбинаторные исчисления
  • 4.1 Комбинаторные термины
  • 4.2 Сокращение в комбинаторной логике
  • 4.3 Примеры комбинаторы
  • 4.4 Полнота базиса SK
    • 4.4.1 Преобразование лямбда-члена в эквивалентный комбинаторный член
    • 4.4.2 Объяснение преобразования T []
  • 4.5 Упрощения преобразования
    • 4.5.1 η-редукция
    • 4.5.2 Одноточечный базис
    • 4.5.3 Комбинаторы B, C
      • 4.5.3.1 CL K в сравнении с расчетом CL I
  • 4.6 Обратное преобразование
• 5 Неразрешимость комбинаторного исчисления
• 6 Приложения
  • 6.1 Компиляция функциональных языков
  • 6.2 Логика
• 7 См. Также
• 8 Ссылки
• 9 Дополнительная литература
• 10 Внешние ссылки

В математике

Комбинаторная логика изначально задумывалась как «предварительная логика», которая проясняет роль количественно определенных переменных в логике, по сути, путем их устранения. Другой способ устранения количественных переменных - это логика функтора предиката Quine . Хотя выразительная сила комбинаторной логики обычно превосходит логику первого порядка, выразительная сила логики функтора предиката идентична таковой логики первого порядка ( Куайн 1960, 1966, 1976 гг.).

Первоначальный изобретатель комбинаторной логики, Моисей Шёнфинкель, ничего не опубликовал по комбинаторной логике после своей оригинальной статьи 1924 года. Хаскелл Карри заново открыл комбинаторы, работая инструктором в Принстонском университете в конце 1927 года. В конце 1930-х годов Алонзо Черч и его студенты в Принстоне изобрели соперника формализм для функциональной абстракции, лямбда-исчисление, которое оказалось более популярным, чем комбинаторная логика. Результатом этих исторических непредвиденных обстоятельств было то, что до тех пор, пока теоретическая информатика не начала проявлять интерес к комбинаторной логике в 1960-х и 1970-х годах, почти все работы по этому предмету были выполнены Хаскеллом Карри и его учениками или Роберт Фейс в Бельгии. Карри и Фейс (1958) и Карри и др. (1972) рассматривают раннюю историю комбинаторной логики. Более современное рассмотрение комбинаторной логики и лямбда-исчисления вместе можно найти в книге Барендрегта, в которой рассматриваются модели Дана Скотт, разработанные для комбинаторной логики в 1960-е и 1970-е годы.

В вычислениях

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

Комбинаторную логику можно рассматривать как вариант лямбда-исчисления, в котором лямбда-выражения (представляющие функциональную абстракцию) заменены ограниченным набором комбинаторов, примитивные функции без свободных переменные. Лямбда-выражения легко преобразовать в комбинаторные выражения, а комбинаторное сокращение намного проще, чем лямбда-сокращение. Следовательно, комбинаторная логика использовалась для моделирования некоторых нестрогих языков функционального программирования и аппаратного обеспечения. Самой чистой формой этого представления является язык программирования Unlambda, единственными примитивами которого являются комбинаторы S и K, дополненные вводом / выводом символов. Unlambda не является практическим языком программирования, но представляет некоторый теоретический интерес.

Комбинаторной логике можно дать множество интерпретаций. Многие ранние работы Карри показали, как преобразовать наборы аксиом традиционной логики в уравнения комбинаторной логики (Hindley and Meredith 1990). Дана Скотт в 1960-х и 1970-х годах показала, как объединить теорию моделей и комбинаторную логику.

Краткое описание лямбда-исчисления

Лямбда-исчисление связано с объектами, называемыми лямбда-термами, которые могут быть представлены следующими тремя формами строк:

• $v\; \{\backslash \; displaystyle\; v\}$
• $\lambda \; v.\; E\; 1\; \{\backslash \; displaystyle\; \backslash \; lambda\; v.E\_\; \{1\}\}$
• $(E\; 1\; E\; 2)\; \{\backslash \; displaystyle\; (E\_\; \{1\}\; E\_\; \{2\})\}$

где $v\; \{\backslash \; displaystyle\; v\}$- имя переменной, взятое из предопределенного бесконечного набора имен переменных, а $E\; 1\; \{\backslash \; displaystyle\; E\_\; \{1\}\}$и $E\; 2\; \{\backslash \; displaystyle\; E\_\; \{2\}\}$- лямбда-термины.

Термины формы $\lambda \; v.\; E\; 1\; \{\backslash \; displaystyle\; \backslash \; lambda\; v.E\_\; \{1\}\}$называются абстракциями. Переменная v называется формальным параметром абстракции, а $E\; 1\; \{\backslash \; displaystyle\; E\_\; \{1\}\}$- телом абстракции. Член $\lambda \; v.\; E\; 1\; \{\backslash \; displaystyle\; \backslash \; lambda\; v.E\_\; \{1\}\}$представляет функцию, которая, примененная к аргументу, связывает формальный параметр v с аргументом, а затем вычисляет результирующее значение $E\; 1\; \{\backslash \; displaystyle\; E\_\; \{1\}\}$- то есть возвращает $E\; 1\; \{\backslash \; displaystyle\; E\_\; \{1\}\}$, где каждое вхождение v заменено аргументом.

Термины формы $(E\; 1\; E\; 2)\; \{\backslash \; displaystyle\; (E\_\; \{1\}\; E\_\; \{2\})\}$называются приложениями. Вызов или выполнение функции модели приложения: функция, представленная $E\; 1\; \{\backslash \; displaystyle\; E\_\; \{1\}\}$, должна быть вызвана с $E\; 2\; \{\backslash \; displaystyle\; E\_\; \{2\}\}$в качестве аргумента, и вычисляется результат. Если $E\; 1\; \{\backslash \; displaystyle\; E\_\; \{1\}\}$(иногда называемый applicationand) является абстракцией, термин может быть сокращен: $E\; 2\; \{\backslash \; displaystyle\; E\_\; \{2\}\}$, аргумент, можно подставить в тело $E\; 1\; \{\backslash \; displaystyle\; E\_\; \{1\}\}$вместо формального параметра $E\; 1\; \{\backslash \; displaystyle\; E\_\; \{1\}\}$, и результатом является новый лямбда-термин, эквивалентный старому. Если лямбда-термин не содержит подтермов в форме $((\lambda \; v.\; E\; 1)\; E\; 2)\; \{\backslash \; displaystyle\; ((\backslash \; lambda\; v.E\_\; \{1\})\; E\_\; \{2\})\}$тогда оно не может быть сокращено и, как говорят, находится в нормальной форме.

Выражение $E\; [v:\; =\; a]\; \{\backslash \; displaystyle\; E\; [v:\; =\; a]\}$представляет результат взятия члена E и замены в нем всех свободных вхождений v на a. Таким образом, мы пишем

$((\lambda \; v.\; E)\; a)\; \Rightarrow \; E\; [v:\; =\; a]\; \{\backslash \; displaystyle\; ((\backslash \; lambda\; vE)\; a)\; \backslash \; Rightarrow\; E\; [v:\; =\; a]\}$

По соглашению, мы берем $(abc)\; \{\backslash \; displaystyle\; (abc)\}$как сокращение для $((ab)\; c)\; \{\backslash \; displaystyle\; ((ab)\; c)\}$( то есть приложение левоассоциативное ).

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

Квадрат x равен $x\; \ast \; x\; \{\backslash \; displaystyle\; x\; *\; x\}$

(Использование "$\ast \; \{\backslash \; displaystyle\; *\}$" для обозначения умножения.) x здесь - формальный параметр функции. Чтобы вычислить квадрат для определенного аргумента, скажем 3, мы вставляем его в определение вместо формального параметра:

Квадрат 3 равен $3\; \ast \; 3\; \{\backslash \; displaystyle\; 3\; *\; 3\}$

To оценить получившееся выражение $3\; \ast \; 3\; \{\backslash \; displaystyle\; 3\; *\; 3\}$, нам пришлось бы прибегнуть к нашим знаниям умножения и числа 3. Поскольку любое вычисление - это просто композиция вычисления вычисления подходящие функции на подходящих примитивных аргументах, этого простого принципа подстановки достаточно, чтобы уловить основной механизм вычислений. Более того, в лямбда-исчислении такие понятия, как «3» и «$\ast \; \{\backslash \; displaystyle\; *\}$» могут быть представлены без какой-либо необходимости во внешне определенных примитивных операторах или константах. В лямбда-исчислении можно идентифицировать термины, которые при соответствующей интерпретации ведут себя как число 3 и как оператор умножения q.v. Кодирование Чёрча.

Известно, что лямбда-исчисление по вычислительной мощности эквивалентно многим другим правдоподобным моделям вычислений (включая машины Тьюринга ); то есть любое вычисление, которое может быть выполнено в любой из этих других моделей, может быть выражено в лямбда-исчислении, и наоборот. Согласно тезису Черча-Тьюринга, обе модели могут выражать любые возможные вычисления.

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

Комбинаторные исчисления

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

Комбинаторные термины

Комбинаторные термины имеют одну из следующих форм:

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

Чтобы сократить обозначения, общее соглашение таково, что $(E\; 1\; E\; 2\; E\; 3....\; E\; n)\; \{\backslash \; displaystyle\; (E\_\; \{1\}\; E\_\; \{2\}\; E\_\; \{3\}...\; E\_\; \{n\})\}$или даже $E\; 1\; E\; 2\; E\; 3...\; E\; n\; \{\backslash \; displaystyle\; E\_\; \{1\}\; E\_\; \{2\}\; E\_\; \{3\}...\; E\_\; \{n\}\}$, обозначает термин $(...\; ((E\; 1\; E\; 2)\; E\; 3)...\; E\; n)\; \{\backslash \; displaystyle\; (...\; ((E\_\; \{1\}\; E\_\; \{2\})\; E\_\; \{3\})...\; E\_\; \{n\})\}$. Это то же общее соглашение (левоассоциативность), что и для множественного применения в лямбда-исчислении.

Редукция в комбинаторной логике

В комбинаторной логике каждый примитивный комбинатор имеет правило редукции вида

(P x 1... x n) = E

, где E - термин, упоминающий только переменные из набора {x 1... x n }. Таким образом, примитивные комбинаторы ведут себя как функции.

Примеры комбинаторов

Простейшим примером комбинатора является I, тождественный комбинатор, определяемый как

(Ix) = x

для всех членов x. Другой простой комбинатор - K, который производит постоянные функции: (K x) - это функция, которая для любого аргумента возвращает x, поэтому мы говорим

((Kx) y) = x

для всех членов x и y. Или, следуя соглашению для множественного приложения,

(Kxy) = x

Третий комбинатор - S, который является обобщенной версией приложения:

(Sxyz) = (xz (yz))

Sприменяет x к y после первой подстановки z в каждый из них. Или, другими словами, x применяется к y внутри среды z.

Данные S и K, Iсами по себе не нужны, поскольку его можно построить из двух других:

((SKK ) x)

= ( SKK x)

= (K x (K x))

= x

для любого члена x. Обратите внимание, что хотя ((SKK ) x) = (I x) для любого x, (SKK ) само по себе не равно I . Мы говорим термины экстенсивно равны. Экстенсиональное равенство отражает математическое понятие равенства функций: две функции равны, если они всегда производят одинаковые результаты для одних и тех же аргументов. Напротив, сами термины вместе с сокращением примитивных комбинаторов охватите понятие интенсионального равенства функций: две функции равны, только если они имеют идентичные реализации, вплоть до раскрытия примитивных комбинаторов, когда эти комбинаторы применяются к достаточному количеству аргументов.Существует много способов реализовать функцию идентичности; (SKK ) и I входят в число этих способов. (SKS ) - это еще один. Мы будем использовать слово «эквивалент» для обозначения экстенсионального равенства, оставляя за собой равные для идентичных комбинаторных терминов.

Более интересным комбинатором является комбинатор с фиксированной точкой или Y комбинатор, который может использоваться для реализации рекурсии.

Полнота базиса SK

Sи K могут быть составлены для создания комбинаторов, которые экстенсивно равны любому лямбда-члену и, следовательно, согласно тезису Чёрча, любой вычислимой функции вообще. Доказательство состоит в том, чтобы представить преобразование T [], которое преобразует произвольный лямбда-член в эквивалентный комбинатор.

T [] может быть определено следующим образом:

1. T [x] =>x
2. T [(E₁ E₂)] =>(T [E₁] T [E₂])
3. T [λx.E] =>(K T [E]) (если x не встречается в свободном месте в E)
4. T [λx.x] =>I
5. T [λx.λy.E] =>T [λx.T [λy.E]] (если x встречается бесплатно в E)
6. T [λx. (E₁ E₂)] =>(S T [λx.E₁] T [λx.E₂]) (если x встречается свободно в E₁ или E₂)

Обратите внимание, что T [], как указано, не является хорошо типизированной математической функцией, а скорее средство переписывания терминов: хотя оно в конечном итоге дает комбинатор, преобразование может генерировать промежуточные выражения, которые не являются ни лямбда-терминами, ни комбинаторами, с помощью правила (5).

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

Это связано с процессом абстракции скобок, который берет выражение E, построенное из переменных и приложения, и производит выражение комбинатора [x] E, в котором переменная x не свободна, так что [x] E x = E. Очень простой алгоритм абстракции скобок определяется индукцией по структуре выражений следующим образом:

1. [x] y: = Ky
2. [x] x: = I
3. [x] (E₁ E₂): = S ([x] E₁) ([x] E₂)

Абстракция скобок индуцирует перевод от лямбда-терминов к выражениям комбинатора, интерпретируя лямбда-абстракции с использованием алгоритма абстракции скобок.

Преобразование лямбда-члена в эквивалентный комбинаторный член

Например, мы преобразуем лямбда-член λx.λy. (yx) в комбинаторный член:

T [λx. λy. (yx)]

= T [λx.T [λy. (yx)]] (на 5)

= T [λx. (S T [λy.y] T [λy.x])] (на 6)

= T [λx. (SI T [λy.x])] (на 4)

= T [λx. (SI (KT [x]))] (на 3)

= T [λx. (SI (Kx)) ] (на 1)

= (S T [λx. (SI )] T [λx. (K x)]) (на 6)

= (S(K(SI )) T [λx. (K x)]) (на 3)

= (S(K(SI )) (S T [λx. K ] T [λx.x])) (на 6)

= (S(K(SI )) (S(KK ) T [λx.x])) (на 3)

= (S(K(SI )) (S(KK ) I)) (by 4)

Если мы применим этот комбинаторный термин к любым двум членам x и y (подавая их в порядке очереди в комбинатор «справа»), он уменьшится следующим образом:

(S(K(SI)) (S(KK) I) xy)

= (K(SI) x (S(KK) Ix) y)

= (SI(S(KK) Ix) y)

= (I y (S(KK) Ixy))

= (y (S(KK) Ixy))

= (y (KKx (I x) y))

= (y (K(Ix) y))

= (y (I x))

= (yx)

Комбинаторное представление, ( S(K(SI )) (S(KK ) I)) намного длиннее, чем представление в виде лямбда-члена λx.λy. (yx). Это типично. В общем, конструкция T [] может расширить лямбда-член длины n до комбинаторного члена длины Θ (n).

Объяснение преобразования T []

Преобразование T [] мотивировано желанием устранить абстракцию. Два особых случая, правила 3 ​​и 4, тривиальны: λx.x явно эквивалентно I, а λx.E явно эквивалентно (K T [E]), если x не выглядит свободным в E.

Первые два правила также просты: переменные преобразуются в самих себя, а приложения, которые разрешены в комбинаторных терминах, преобразуются в комбинаторы просто путем преобразования аппликатора и аргумента в комбинаторы.

Интересны правила 5 и 6. Правило 5 просто говорит, что чтобы преобразовать сложную абстракцию в комбинатор, мы должны сначала преобразовать его тело в комбинатор, а затем исключить абстракцию. Правило 6 фактически устраняет абстракцию.

λx. (E₁ E₂) - это функция, которая принимает аргумент, например a, и заменяет его на лямбда-член (E₁ E₂) вместо x, получая (E₁ E₂) [x: = a]. Но подстановка a в (E₁ E₂) вместо x - это то же самое, что замена его в E₁ и E₂, поэтому

(E₁ E₂) [x: = a] = (E₁ [x: = a] E₂ [ x: = a])

(λx. (E₁ E₂) a) = ((λx.E₁ a) (λx.E₂ a))

= (S λx.E₁ λx. E₂ a)

= ((S λx.E₁ λx.E₂) a)

По экстенсиональному равенству

λx. (E₁ E₂) = (S λx.E₁ λx.E₂)

Следовательно, чтобы найти комбинатор, эквивалентный λx. (E₁ E₂), достаточно найти комбинатор, эквивалентный (S λx.E₁ λx. E₂) и

(ST [λx.E₁] T [λx.E₂])

, очевидно, отвечает всем требованиям. E₁ и E₂ содержат строго меньше приложений, чем (E₁ E₂), поэтому рекурсия должна заканчиваться лямбда-термом без каких-либо приложений вообще - либо переменной, либо члена формы λx.E.

Упрощения преобразования

η-редукция

Комбинаторы, генерируемые преобразованием T [], могут быть уменьшены, если мы примем во внимание правило η-редукции:

T [λx. (E x)] = T [E] (если x не является свободным в E)

λx. (E x) - функция, которая принимает аргумент x и применяет функцию E к Это; это экстенсивно равно самой функции E. Поэтому достаточно преобразовать E в комбинаторную форму.

Принимая во внимание это упрощение, приведенный выше пример выглядит следующим образом:

T[λx.λy.(yx)] ]

=...

= (S(K(SI )) T [λx. (K x)])

= (S(K(SI )) K ) (по η-редукция)

Этот комбинатор эквивалентен более раннему, более длинному:

(S(K(SI )) Kxy)

= (K(SI ) x (K x) y)

= (SI (Kx) y)

= (I y (K xy))

= (y (K xy))

= (yx)

Аналогично исходная версия преобразование T [] преобразовало тождественную функцию λf.λx. (fx) в (S(S(KS ) (S(KK ) I)) (KI )). С помощью правила η-редукции λf.λx. (f x) преобразуется в I.

одноточечный базис

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

X≡ λx. ((X S)K)

Нетрудно проверить, что:

X(X(XX)) = K и

X(X(X(XX))) = S.

Поскольку {K, S} является основой, отсюда следует, что {X } также является основой. В языке программирования Iota в качестве единственного комбинатора используется X .

Другой простой пример одноточечного базиса:

X'≡ λx. (X KSK) с

(X'X') X'=Kи

X'(X'X') = S

На самом деле существует бесконечно много таких баз.

Комбинаторы B, C

В дополнение к S и K, статья Шёнфинкеля включала два комбинатора, которые теперь называются B и C со следующими сокращениями:

(Cfgx) = ((fx) g)

(Bfgx) = (f (gx))

Он также объясняет, как они в поворот можно выразить только с помощью S и K:

B= (S(KS ) K)

C= (S(S(K(S(KS ) K)) S ) (KK ))

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

1. T [x] ⇒ x
2. T [(E₁ E₂)] ⇒ (T [E₁] T [E₂ ])
3. T [λx.E] ⇒ (K T [E]) (если x не является свободным в E)
4. T [λx.x] ⇒ I
5. T [λx.λy.E] ⇒ T [λx.T [λy.E]] (если x свободен в E)
6. T [λx. ( E₁ E₂)] ⇒ (S T [λx.E₁] T [λx.E₂]) (если x свободен как в E₁, так и в E₂)
7. T [λx. (E₁ E₂)] ⇒ (C T [λx.E₁] T [E₂]) (если x свободен в E₁, но не в E₂)
8. T [λx. (E₁ E₂)] ⇒ ( B T [E₁] T [λx.E₂]) (если x свободен в E₂, но не E₁)

Использование комбинаторов B и C, преобразование λx.λy. (yx) выглядит следующим образом:

T[λx.λy.(yx)] ]

= T [λx.T [λy. (yx)]]

= T [λx. (C T [λy.y] x)] (по правилу 7)

= T [λx. (CIx)]

= (CI) (η-сокращение)

= $C\; \ast \; \{\backslash \; displaystyle\; \backslash \; mathbf\; \{C\}\; \_\; \{*\}\}$(традиционное каноническое обозначение: $X\; \ast \; =\; XI\; \{\backslash \; displaystyle\; \backslash \; mathbf\; \{X\}\; \_\; \{*\}\; =\; \backslash \; mathbf\; \{XI\}\}$)

= $I\; \prime \; \{\backslash \; displaystyle\; \backslash \; mathbf\; \{I\}\; \text{'}\}$(традиционное каноническое обозначение: $X\; \prime \; =\; CX\; \{\backslash \; displaystyle\; \backslash \; mathbf\; \{X\}\; \text{'}=\; \backslash \; mathbf\; \{CX\}\}$)

И действительно, (CIxy) сокращается до (yx):

(CIxy)

= (I yx)

= (yx)

Мотивация здесь в том, что B и C являются ограниченными версиями S . В то время как S принимает значение и подставляет его как в приложение, так и в свой аргумент перед выполнением приложения, C выполняет замену только в приложении, а B только в споре.

Современные названия комбинаторов взяты из докторской диссертации Хаскелла Карри 1930 г. (см. Система B, C, K, W ). В исходной статье Шенфинкеля то, что мы сейчас называем S, K, I, Bи C, называлось S, C, I, Zи T соответственно.

Уменьшение размера комбинатора, которое является результатом новых правил преобразования, также может быть достигнуто без введения B и C, как показано в разделе 3.2.

CLKв сравнении с CL I исчислением

Следует проводить различие между CLK, описанным в этой статье, и исчислением CLI. Различие соответствует различию между вычислением λ K и λ I. В отличие от исчисления λ K, исчисление λ I ограничивает абстракции до:

λx.E, где x имеет хотя бы одно свободное вхождение в E.

Как следствие, комбинатор K не присутствует ни в исчислении λ I, ни в исчислении CLI. Константы CLI: I, B, Cи S, которые образуют основу, из которой могут быть составлены все члены CLI(по модулю равенства). Каждый член λ I может быть преобразован в равный комбинатор CLIв соответствии с правилами, аналогичными приведенным выше для преобразования членов λ K в комбинаторы CLK. См. Главу 9 в Barendregt (1984).

Обратное преобразование

Преобразование L [] из комбинаторных членов в лямбда-члены тривиально:

L[I] = λx.x

L[K] = λx.λy.x

L[C] = λx.λy.λz. (xzy)

L[B] = λx.λy.λz. (x (yz))

L[S] = λx.λy.λz. (xz (yz))

L [(E₁ E₂)] = (L [E₁] L [E₂])

Обратите внимание, однако, что это преобразование не является обратным преобразованием какой-либо из версий T [], которые мы видели.

Неразрешимость комбинаторного исчисления

A нормальная форма - это любой комбинаторный термин, в котором встречающиеся примитивные комбинаторы, если таковые имеются, не применяются к достаточному количеству аргументов для упрощения. Непонятно, имеет ли общий комбинаторный термин нормальную форму; эквивалентны ли два комбинаторных члена и т. д. Это равносильно неразрешимости соответствующих проблем для лямбда-членов. Однако прямое доказательство выглядит следующим образом:

Во-первых, член

Ω= (SII(SII))

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

(SII(SII))

= (I(SII) (I(SII)))

= (SII(I(SII)))

= (SII(SII))

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

Теперь предположим, что N был комбинатором для обнаружения нормальных форм, такой что

$(N\; x)\; =\; \{T,\; если\; x\; имеет\; нормальную\; форму\; F,\; в\; противном\; случае.\; \{\backslash \; Displaystyle\; (\backslash \; mathbf)\; \{N\}\; \backslash \; x)\; =\; \{\backslash \; begin\; \{cases\}\; \backslash \; mathbf\; \{T\},\; \{\backslash \; text\; \{if\}\}\; x\; \{\backslash \; text\; \{имеет\; нормальную\; форму\}\}\; \backslash \backslash \backslash \; mathbf\; \{F\},\; \{\backslash \; text\; \{иначе.\}\}\; \backslash \; end\; \{cases\}\}\}$

(Где T и F представляют собой общепринятые кодировки Чёрча истинного и ложного, λx.λy. x и λx.λy.y, преобразованные в комбинаторную логику. Комбинаторные версии имеют T= Kи F = (KI).)

Теперь пусть

Z = (C(C(BN(SII)) Ω) I)

теперь рассмотрим член (SIIZ). Имеет ли (SIIZ) нормальную форму? Это происходит тогда и только тогда, когда также выполняется следующее:

(SIIZ)

= (I Z (I Z))

= (Z (I Z))

= (ZZ)

= (C(C(BN(SII)) Ω) IZ) (определение Z)

= (C(BN(SII)) ΩZ I)

= (BN(SII) Z ΩI)

= (N(SIIZ) ΩI)

Теперь нам нужно применить N к (SIIZ). Либо (SIIZ) имеет нормальную форму, либо нет. Если он имеет нормальную форму, то вышесказанное сокращается следующим образом:

(N(SIIZ) ΩI)

= (KΩI) (определение N)

= Ω

, но Ω не имеет нормальной формы, Итак, мы получили противоречие. Но если (SIIZ) не имеет нормальной формы, вышесказанное сокращается следующим образом:

(N(SIIZ) ΩI)

= (KIΩI) (определение N)

= (II)

= I

, что означает, что нормальная форма (SIIZ) - это просто I, еще одно противоречие. Следовательно, гипотетический комбинатор нормальной формы N не может существовать.

Комбинаторный логический аналог теоремы Райса гласит, что не существует полного нетривиального предиката. Предикат - это комбинатор, который при применении возвращает либо T, либо F . Предикат N является нетривиальным, если есть два аргумента A и B такие, что N A = T и N B = F . Комбинатор N является полным тогда и только тогда, когда N M имеет нормальную форму для каждого аргумента M. Тогда аналог теоремы Райса говорит, что каждое полное pr edicate тривиально. Доказательство этой теоремы довольно просто.

Доказательство: Путем сокращения до абсурда. Предположим, что существует полный нетривиальный предикат, скажем N . Поскольку N предполагается нетривиальным, существуют комбинаторы A и B такие, что

(NA) = T и

(NB) = F.

Определить ОТРИЦАТЕЛЬСТВО ≡ λx. (если (N x), то B иначе A) ≡ λx. ((N x) BA)

Определить АБСУРДУМ ≡ (Y ОТРИЦАНИЕ)

Теорема о фиксированной точке дает: АБСУРДУМ = (ОТРИЦАНИЕ АБСУРДМ), для

АБСУРДУМ (Д ОТРИЦАТЕЛЬСТВО) = (ОТРИЦАНИЕ (Д ОТРИЦАНИЕ)) ≡ (ОТРИЦАНИЕ ABSURDUM).

Поскольку N должно быть полным либо:

1. (NABSURDUM) = For
2. (NABSURDUM) = T

• Случай 1: F = (N ABSURDUM) = N (NEGATION ABSURDUM) = (N A) = T, противоречие.
• Случай 2 : T = (N АБСУРДМ) = N (ОТРИЦАТЕЛЬНЫЙ АБСУРД) = (N B) = F, снова противоречие.

Следовательно (N ABSURDUM) не является ни T, ни F, что противоречит предположению о том, что N будет - полный нетривиальный предикат. Q.E.D.

Из этой теоремы неразрешимости сразу следует, что не существует полного предиката, который мог бы различать термины, имеющие нормальную форму, и термины, не имеющие нормальной формы. Также следует, что не существует никакого полного предиката, скажем EQUAL, такого что:

(EQUAL AB) = T, если A = B и

(EQUAL AB) = F, если A ≠ B.

Если бы EQUAL существовало, то для всех A λx. (EQUAL x A) должно было бы быть полным нетривиальным предикатом.

Приложения

Компиляция функциональных языков

Дэвид Тернер использовал свои комбинаторы для реализации языка программирования SASL.

Кеннет Э. Айверсон использовал примитивы на основе о комбинаторах Карри в его языке программирования J, преемнике APL. Это позволило Айверсону называться неявным программированием, то есть программированием в функциональных выражениях, не содержащих переменных, а также мощными инструментами для работы с такими программами. Оказывается, неявное программирование возможно на любом APL-подобном языке с пользовательскими операторами.

Логика

Изоморфизм Карри – Ховарда подразумевает связь между логикой и программирование: каждое доказательство теоремы интуиционистской логики соответствует сокращению типизированного лямбда-члена и наоборот. Более того, теоремы можно отождествить с сигнатурами функционального типа. В частности, типизированная комбинаторная логика соответствует системе Гильберта в теории доказательств.

Комбинаторы K и S соответствуют аксиомам

AK: A → (B → A),

AS: (A → (B → C)) → ((A → B) → (A → C)),

и применение функции соответствует отстранению (modus ponens) правило

MP: из A и A → B вывести B.

Исчисление, состоящее из AK, ASи MP, является полным для импликационного фрагмента интуиционистской логики, который можно рассматривать как следует. Рассмотрим множество W всех дедуктивно замкнутых наборов формул, упорядоченных по включению. Тогда $⟨W,\; \subseteq ⟩\; \{\backslash \; displaystyle\; \backslash \; langle\; W,\; \backslash \; substeq\; \backslash \; rangle\}$- это интуиционистский фрейм Крипке, и мы определяем модель $⊩\; \{\backslash \; displaystyle\; \backslash \; Vdash\}$в этом кадре по

$X\; ⊩\; A\; ⟺\; A\; \in \; X.\; \{\backslash \; displaystyle\; X\; \backslash \; Vdash\; A\; \backslash \; iff\; A\; \backslash \; in\; X.\}$

Это определение подчиняется условиям выполнения →: с одной стороны, если $X\; ⊩\; A\; \to \; B\; \{\backslash \; displaystyle\; X\; \backslash \; Vdash\; A\; \backslash \; to\; B\}$и $Y\; \in \; W\; \{\backslash \; displaystyle\; Y\; \backslash \; in\; W\}$таково, что $Y\; \supseteq \; X\; \{\backslash \; displaystyle\; Y\; \backslash \; supseteq\; X\}$и $Y\; ⊩\; A\; \{\backslash \; displaystyle\; Y\; \backslash \; Vdash\; A\}$, затем $Y\; ⊩\; B\; \{\backslash \; displaystyle\; Y\; \backslash \; Vdash\; B\}$по modus ponens. С другой стороны, если $Икс\; ⊮\; A\; \to \; B\; \{\backslash \; displaystyle\; X\; \backslash \; not\; \backslash \; Vdash\; A\; \backslash \; to\; B\}$, то $X,\; A\; ⊬\; B\; \{\backslash \; displaystyle\; X,\; A\; \backslash \; не\; \backslash \; vdash\; B\}$по теореме дедукции, следовательно, дедуктивное замыкание $X\; \cup \; \{A\}\; \{\backslash \; displaystyle\; X\; \backslash \; cup\; \backslash \; \{A\; \backslash \}\}$- элемент $Y\; \in \; W\; \{\backslash \; displaystyle\; Y\; \backslash \; in\; W\}$такой, что $Y\; \supseteq \; X\; \{\backslash \; displaystyle\; Y\; \backslash \; supseteq\; X\}$, $Y\; ⊩\; A\; \{\backslash \; displaystyle\; Y\; \backslash \; Vdash\; A\}$и $Y\; ⊮\; B\; \{\backslash \; displaystyle\; Y\; \backslash \; not\; \backslash \; Vdash\; B\}$.

Пусть A будет любой формулой, которая не доказуема в исчислении. Then A does not belong to the deductive closure X of the empty set, thus $X\; ⊮\; A\; \{\backslash displaystyle\; X\backslash not\; \backslash Vdash\; A\}$, and A is not intuitionistically valid.

See also

• Applicative computing systems
• B, C, K, W system
• Categorical abstract machine
• Combinatory categorial grammar
• Explicit substitution
• Fixed point combinator
• Graph reduction machine
• Lambda calculus and Cylindric algebra, other approaches to modelling quantification and eliminating variables
• SKI combinator calculus
• Supercombinator
• To Mock a Mockingbird

References

Further reading

• Barendregt, Hendrik Pieter (1984). The Lambda Calculus, Its Syntax and Semantics. Исследования по логике и основам математики. Volume 103. North Holland. ISBN 0-444-87508-5.CS1 maint: ref=harv (link )
• Curry, Haskell B. ; Feys, Robert (1958). Combinatory Logic. Vol. I. Amsterdam: North Holland. ISBN 0-7204-2208-6.
• Curry, Haskell B. ; Hindley, J. Roger ; Seldin, Jonathan P. (1972). Combinatory Logic. Vol. II. Amsterdam: North Holland. ISBN 0-7204-2208-6.
• Field, Anthony J.; Harrison, Peter G. (1998). Functional Programming. Addison-Wesley. ISBN 0-201-19249-7.
• Hindley, J. Roger ; Meredith, David (1990), "Principal type-schemes and condensed detachment", Journal of Symbolic Logic, 55(1): 90–105, doi :10.2307/2274956, JSTOR 2274956, MR 1043546
• Hindley, J. R. ; Seldin, J. P. (2008). λ-calculus and Combinators: An Introduction. Cambridge University Press.
• Paulson, Lawrence C. (1995). Foundations of Functional Programming. University o f Cambridge.
• Quine, W. V. (1960). "Variables explained away". Труды Американского философского общества. 104(3): 343–347. JSTOR 985250.Reprinted as Chapter 23 of Quine's Selected Logic Papers (1966), pp. 227–235
• Schönfinkel, Moses, 1924, "Über die Bausteine der mathematischen Logik," translated as "On the Building Blocks of Mathematical Logic" in From Frege to Gödel: a source book in mathematical logic, 1879–1931, Jean van Heijenoort, ed. Harvard University Press, 1967. ISBN 0-674-32449-8. The article that founded combinatory logic.
• Smullyan, Raymond, 1985. To Mock a Mockingbird. Кнопф. ISBN 0-394-53491-3. A gentle introduction to combinatory logic, presented as a series of recreational puzzles using bird watching metaphors.
• --------, 1994. Diagonalization and Self-Reference. Oxford Univ. Нажмите. Chapters 17–20 are a more formal introduction to combinatory logic, with a special emphasis on fixed point results.
• Sørensen, Morten Heine B. and Paweł Urzyczyn, 1999. Lectures on the Curry–Howard Isomorphism. University of Copenhagen and University of Warsaw, 1999.
• Wolfengagen, V. E. (2003). Combinatory logic in programming: Computations with objects through examples and exercises (2nd ed.). Moscow: "Center JurInfoR" Ltd. ISBN 5-89158-101-9..

External links

• Stanford Encyclopedia of Philosophy : "Combinatory Logic " by Katalin Bimbó.
• 1920–1931 Curry's block notes.
• Keenan, David C. (2001) "To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction. "
• Rathman, Chris, "Combinator Birds. " A table distilling much of the essence of Smullyan (1985).
• Drag 'n' Drop Combinators. (Java Applet)
• Binary Lambda Calculus and Combinatory Logic.
• Combinatory logic reduction web server