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

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

По математике

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

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

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

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

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

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

Резюме лямбда-исчисления

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

• ${\ displaystyle v}$
• ${\ displaystyle \ lambda v.E_ {1}}$
• ${\ displaystyle (E_ {1} E_ {2})}$

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

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

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

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

${\ Displaystyle ((\ лямбда vE) а) \ Rightarrow E [v: = а]}$

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

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

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

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

Квадрат 3 - это ${\ displaystyle 3 * 3}$

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

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

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

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

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

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

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

Синтаксис	Имя	Описание
Икс	Переменная	Символ или строка, представляющая комбинаторный термин.
п	Примитивная функция	Один из комбинатор символов I , K , S .
(MN)	заявка	Применение функции к аргументу. M и N - комбинаторные термины.

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

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

Сведение комбинаторной логики

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

( P x ₁ ... x _n ) = E

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

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

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

( I x ) = x

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

(( К х ) у ) = х

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

( К х у ) = х

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

( S x yz ) = ( xz ( yz ))

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

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

(( SKK ) x )

= ( SKK x )

= ( К х ( К х ))

= х

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

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

Полнота основы СК

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

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

1. Т [ х ] => х
2. T [( E ₁ E ₂)] => ( T [ E ₁] T [ E ₂])
3. Т [ λx . E ] => ( K T [ E ]) (если x не встречается свободно в E )
4. Т [ λx . x ] => Я
5. Т [ λx . λy . E ] => T [ λx . Т [ λ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  : = K y
2. [ x ] x  : = I
3. [ x ] ( E₁ E₂ ): = S ([ x ] E₁ ) ([ x ] E₂ )

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

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

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

Т [ λx . λy . ( y x )]

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

= T [ λx . ( S T [ λy . Y ] T [ λy . X ])] (по 6)

= T [ λx . ( SI T [ λy . X ])] (по 4)

= T [ λx . ( SI ( K T [ x ]))] (по 3)

= T [ λx . ( SI ( K x ))] (на 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 )) (на 4)

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

( S ( K ( S I )) ( S ( K K ) I ) xy)

= ( К ( S I ) x ( S ( K K ) I x) y)

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

= ( I y ( S ( K K ) I xy))

= (y ( S ( K K ) I xy))

= (y ( K K x ( I x) y))

= (y ( K ( I x) y))

= (у ( I x))

= (yx)

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

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

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

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

Интересны правила 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 ])

( Хй . ( Е ₁ Е ₂) ) = (( Хе . Е ₁ ) ( Хе . Е ₂ ))

= ( 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 ₂), и

( S T [ λ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 в комбинаторную форму.

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

  Т [ λx . λy . ( y x )]

знак равно

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

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

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

  ( S ( K ( SI )) K x y )

= ( К ( СИ ) х ( К х ) у )

= ( SI ( K x ) y )

= ( I y ( K x y ))

= ( у ( К х у ))

= ( yx )

Точно так же исходная версия преобразования T [] преобразовывала тождественную функцию λf . λx . ( f x ) в ( S ( S ( KS ) ( S ( KK ) I )) ( KI )). По правилу η-редукции λf . Хе . ( е х ) преобразуются в I .

Одноточечная основа

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

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

Нетрудно убедиться, что:

X ( X ( X X )) = ^β K и

Х ( Х ( Х ( Х Х ))) = ^β S .

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

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

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

( X ' X' ) X ' = ^β K и

Х ' ( Х' Х ' ) = ^β S

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

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

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

( C f g x ) = (( f x ) g )

( B f g x ) = ( f ( g x ))

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

В = ( S ( KS ) K )

С = ( S ( S ( K ( S ( KS ) K )) S ) ( KK ))

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

1. Т [ х ] ⇒ х
2. Т [( E₁ E₂ )] ⇒ ( T [ E₁ ] T [ E₂ ])
3. Т [ λx . E ] ⇒ ( K T [ E ]) (если x не свободен в E )
4. Т [ λx . x ] ⇒ I
5. Т [ λx . λy . E ] ⇒ T [ λx . Т [ λ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 . ( y x ) выглядит так:

   Т [ λx . λy . ( y x )]

= Т [ λx . Т [ λy . ( Y x )]]

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

= T [ λx . ( C I x )]

= ( C I ) (η-редукция)

= (Традиционная каноническая запись: )${\ displaystyle \ mathbf {C} _ {*}}$${\ Displaystyle \ mathbf {X} _ {*} = \ mathbf {XI}}$

= (Традиционная каноническая запись: )${\ displaystyle \ mathbf {I} '}$${\ Displaystyle \ mathbf {X} '= \ mathbf {CX}}$

И действительно, ( C I x y ) сводится к ( y x ):

   ( C I x y )

= ( I y x )

= ( у х )

Мотивация здесь является то , что 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.

CL _K по сравнению с CL _I исчисления

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

λx . Е , где х имеет по крайней мере одно свободное вхождение в Е .

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

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

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

L [ I ] = λx . Икс

L [ K ] = λx . λy . Икс

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

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

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

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

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

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

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

Во-первых, термин

Ω = ( S I I ( S I I ))

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

   ( S I I ( S I I ))

= ( I ( S I I ) ( I ( S I I )))

= ( S I I ( I ( S I I )))

= ( S I I ( S I I ))

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

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

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

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

Теперь позвольте

Z = ( C ( C ( B N ( S I I )) Ω ) I )

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

  ( S I I Z )

= ( I Z ( I Z ))

= ( Z ( I Z ))

= ( Z Z )

= ( C ( C ( B N ( S I I )) Ω ) I Z ) (определение Z )

= ( C ( B N ( S I I )) Ω Z I )

= ( B N ( S I I ) Z Ω I )

= ( N ( S I I Z ) Ω I )

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

  ( N ( S I I Z ) Ω I )

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

= Ω

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

  ( N ( S I I Z ) Ω I )

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

= ( Я Я )

= Я

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

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

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

( N A ) = T и

( Н Б ) = F .

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

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

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

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

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

1. ( N АБСУРДУМ) = F или
2. ( N АБСУРДУМ) = T

• Случай 1: F = ( N ABSURDUM) = N (NEGATION ABSURDUM) = ( N A ) = T ; противоречие.
• Случай 2: T = ( N ABSURDUM) = N (NEGATION ABSURDUM) = ( N B ) = F , снова противоречие.

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

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

(РАВНО AB ) = T, если A = B и

(РАВНО АВ ) = F , если A ≠ B .

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

Приложения

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

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

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

Логика

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

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

АК : А → ( В → А ),

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

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

MP : от A и A → B Infer B .

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

${\ Displaystyle X \ Vdash A \ iff A \ in X.}$

Это определение подчиняется условиям выполнения →: с одной стороны, если и таково, что и , то по modus ponens. С другой стороны, если , то по теореме дедукции , таким дедуктивным замыканием является элементом таким образом, что , и . ${\ Displaystyle X \ Vdash от A \ до B}$${\ displaystyle Y \ in W}$${\ Displaystyle Y \ supseteq X}$${\ Displaystyle Y \ Vdash A}$${\ displaystyle Y \ Vdash B}$${\ Displaystyle X \ not \ Vdash от A \ до B}$${\ displaystyle X, A \ not \ vdash B}$${\ Displaystyle X \ чашка \ {A \}}$${\ displaystyle Y \ in W}$${\ Displaystyle Y \ supseteq X}$${\ Displaystyle Y \ Vdash A}$${\ Displaystyle Y \ not \ Vdash B}$

Пусть A - любая формула, не доказуемая в исчислении. Тогда A не принадлежит дедуктивному замыканию X пустого множества, следовательно , и A не является интуиционистски валидным. ${\ Displaystyle X \ not \ Vdash A}$

Смотрите также

• Аппликативные вычислительные системы
• Система B, C, K, W
• Категориальная абстрактная машина
• Комбинаторно-категориальная грамматика
• Явная подстановка
• Комбинатор с фиксированной точкой
• Машина для редукции графа
• Лямбда-исчисление и цилиндрическая алгебра , другие подходы к моделированию количественной оценки и исключения переменных
• Расчет комбинатора SKI
• Суперкомбинатор
• Издеваться над пересмешником

использованная литература

дальнейшее чтение

• Барендрегт, Хендрик Питер (1984). Лямбда-исчисление, его синтаксис и семантика. Исследования по логике и основам математики . Том 103. Северная Голландия . ISBN 0-444-87508-5. |volume=имеет дополнительный текст ( справка )
• Карри, Хаскелл Б .; Фейс, Роберт (1958). Комбинаторная логика . Vol. I. Амстердам: Северная Голландия. ISBN 0-7204-2208-6. |volume=имеет дополнительный текст ( справка )
• Карри, Хаскелл Б .; Хиндли, Дж. Роджер ; Селдин, Джонатан П. (1972). Комбинаторная логика . Vol. II. Амстердам: Северная Голландия. ISBN 0-7204-2208-6. |volume=имеет дополнительный текст ( справка )
• Филд, Энтони Дж .; Харрисон, Питер Г. (1998). Функциональное программирование . Эддисон-Уэсли. ISBN 0-201-19249-7.
• Хиндли, Дж. Роджер ; Meredith, Дэвид (1990), "Основные типа-схема и сгущенное отряд" , журнал символической логики , 55 (1): 90-105, DOI : 10,2307 / 2274956 , JSTOR  2274956 , МР  1043546
• Хиндли, младший ; Селдин, JP (2008). λ-исчисление и комбинаторы: введение . Издательство Кембриджского университета .
• Полсон, Лоуренс К. (1995). Основы функционального программирования . Кембриджский университет.
• Куайн, Западная Вирджиния (1960). «Объяснение переменных». Труды Американского философского общества . 104 (3): 343–347. JSTOR  985250 .Перепечатано как глава 23 книги Куайна « Избранные статьи по логике» (1966), стр. 227–235.
• Schönfinkel, Moses , 1924, « Über die Bausteine ​​der Mathematischen Logik », переведенный как «О строительных блоках математической логики» в От Фреге до Гёделя: справочник по математической логике, 1879–1931 , Жан ван Хейенорт , изд. Издательство Гарвардского университета , 1967. ISBN  0-674-32449-8 . Статья, обосновавшая комбинаторную логику.
• Смуллян, Раймонд , 1985. Поиздеваться над пересмешником . Кнопф. ISBN  0-394-53491-3 . Мягкое введение в комбинаторную логику, представленное в виде серии развлекательных головоломок с использованием метафор наблюдения за птицами.
• ______, 1994. Диагонализация и самореферент . Издательство Оксфордского университета . Главы 17–20 представляют собой более формальное введение в комбинаторную логику с особым упором на результаты с фиксированной точкой.
• Соренсен, Мортен Хайне Б. и Павел Уржичин, 1999. Лекции по изоморфизму Карри – Ховарда . Копенгагенский и Варшавский университет , 1999 г.
• Вольфенгаген, В. Э. (2003). Комбинаторная логика в программировании: Расчеты с объектами на примерах и упражнениях (2-е изд.). Москва: ISBN ООО "Центр ЮрИнфоР" 5-89158-101-9.
• Вольфрам, Стивен (2021). Комбинаторы: взгляд столетия . Wolfram Media . ISBN 978-1-57955-043-1.e ISBN  978-1-57955-044-8 . Празднование развития комбинаторов спустя сто лет после того, как они были представлены Моисеем Шёнфинкелем в 1920 году.

внешние ссылки

• Стэнфордская энциклопедия философии : « Комбинаторная логика » Каталин Бимбо .
• 1920–1931 Блокноты Карри.
• Кинан, Дэвид С. (2001) « Рассечение пересмешника: графическое представление лямбда-исчисления с анимированной редукцией ».
• Ратман, Крис, « Combinator Birds ». Таблица, в которой раскрывается большая часть сущности Smullyan (1985).
• Комбинаторы перетаскивания. (Java-апплет)
• Двоичное лямбда-исчисление и комбинаторная логика.
• Веб-сервер редукции комбинаторной логики