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

Не путать с комбинационной логикой , разделом цифровой электроники.

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

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

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

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

В вычислительной технике

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

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

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

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

Основная статья: лямбда-исчисление

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

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

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

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

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

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

$((\lambda v.E)a)\Rightarrow E[v:=a]$

По соглашению мы принимаем $(abc)$ как сокращение для $((ab)c)$ (т.е. приложение остается ассоциативным ).

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

Квадрат х равен $x*x$

(С использованием " $*$", чтобы указать умножение.) x здесь является формальным параметром функции. Чтобы вычислить квадрат для определенного аргумента, скажем, 3, мы вставляем его в определение вместо формального параметра:

Квадрат 3 это $3*3$

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

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

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

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

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

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

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

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

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

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

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

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

( п Икс ₁ ... Икс п ₎ знак равно E

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

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

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

( я х ) = х

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

(( K Икс ) y ) знак равно Икс

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

( К Икс у ) знак равно Икс

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

( S Икс yz ) знак равно ( xz ( yz ))

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

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

(( СКК ) x )

= ( СКК х )

знак равно Кх ( ( Кх ) )

= х

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

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

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

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

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

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

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

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

Например, мы преобразуем лямбда-терм λ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)

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

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

знак равно ( я y ( S ( K K ) я ху))

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

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

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

= (у ( я х))

= (ух)

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

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

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

( λx .( E ₁ E ₂) а ) знак равно (( λx . E ₁ а ) ( λx . E ₂ а ))

знак равно ( S λx . E ₁ λx . E ₂ а )

знак равно (( S λx . E₁ λx . E ₂) а )

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

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

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

( S Т [ λx . E ₁] T [ λx . E ₂])

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

Упрощения трансформации

η-редукция

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

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

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

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

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

= ...

знак равно ( S ( K ( SI )) T [ λx .( K x )])

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

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

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

знак равно ( K ( SI ) Икс ( K Икс ) y )

знак равно ( SI ( K Икс ) y )

знак равно ( я y ( K x y ))

знак равно ( у ( К Икс у ))

= ( ух )

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

Однобалльная основа

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

Икс ≡ λx .((x S ) K )

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

Икс ( Икс ( Икс ) ) = ^б К и

Икс ( Икс ( Икс ( Х Х ))) = ^б С. ​

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

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

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

( Х' Х' ) Х' = ^б К и

Х' ( Х' Х' ) = ^б С

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

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

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

( C ж г Икс ) знак равно (( ж Икс ) г )

( B ж г Икс ) знак равно ( ж ( г Икс ))

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

B знак равно ( S ( KS ) K )

C знак равно ( S ( S ( K ( S ( KS ) K )) S ) ( KK ))

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

1. Т [ х ] ⇒ х
2. Т [( E₁ E₂ )] ⇒ ( Т [ E₁ ] Т [ E₂ ])
3. Т [ λx . E ] ⇒ ( K T [ E ]) (если x не свободен в E )
4. Т [ λx . х ] ⇒ Я
5. Т [ λx . λy . Е ] ⇒ Т [ λ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₂ )] ⇒ ( BT T [ E₁ ] [ , λ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)

знак равно Т [ λx .( C I x )]

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

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

= $\mathbf {I} '$ (традиционные канонические обозначения: $\mathbf {X} '=\mathbf {CX}$)

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

  ( С я х у )

= ( я y x )

= ( у Икс )

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

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

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

CL _K против _I Расчет

Необходимо проводить различие между исчислением CL _K , описанным в этой статье CL _I. , и исчислением Это различие соответствует разнице между _{λ K} и λ _I. исчислением В отличие от исчисления λ _K , исчисление λ _I ограничивает абстракции:

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

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

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

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

L [ я ] знак равно λx . Икс

L [ K ] знак равно λx . λy . Икс

L [ C ] знак равно λx . λy . λz .( Икс z y )

L [ B ] знак равно λx . λy . λz .( Икс ( y z ))

L [ S ] знак равно λx . λy . λz .( Икс z ( y z ))

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

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

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

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

Неопределимость предикатами

Неразрешимые выше проблемы (эквивалентность, существование нормальной формы и т. д.) принимают в качестве входных данных синтаксические представления терминов в подходящей кодировке (например, кодировке Чёрча). Можно также рассмотреть игрушечную тривиальную модель вычислений, в которой мы «вычисляем» свойства терминов с помощью комбинаторов, применяемых непосредственно к самим терминам в качестве аргументов, а не к их синтаксическим представлениям. Точнее, пусть предикат является комбинатором, который при применении возвращает либо T , либо F (где T и F представляют собой общепринятые кодировки Чёрча истинного и ложного, λx . λy . x и λx . λy . y , преобразованные в комбинаторную логику комбинированные версии имеют T = K и F = ( K I ) ). Предикат N является нетривиальным , если существуют два аргумента A и B такие, NA что = T и N B = F . Комбинатор N является полным , если N M имеет нормальную форму для каждого аргумента M . Аналог теоремы Райса для этой игрушечной модели гласит, что каждый полный предикат тривиален. Доказательство этой теоремы довольно простое.

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

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

( N А ) = Т и

( N B ) знак равно F .

Определим ОТРИЦАНИЕ ≡ λx .(если ( N x ), то B else A ) ≡ λx .(( N x ) B A )

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

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

АБСУРДУМ ≡ ( ОТРИЦАНИЕ Y ) = (ОТРИЦАНИЕ ( ОТРИЦАНИЕ Y )) ≡ (ОТРИЦАНИЕ АБСУРДУМ).

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

1. ( N ABSURDUM) = F или
2. ( N абсурд) = T

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

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

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

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

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

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

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

Приложения

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

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

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

Логика

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

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

АК : А → ( Б → А ),

КАК : ( А → ( В → С )) → (( А → В ) → ( А → С )),

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

МП из А и А → Б выводится Б. :

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

$X\Vdash A\iff A\in X.$

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

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

См. также

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

Литература

• Барендрегт, Хендрик Питер (1984). Лямбда-исчисление, его синтаксис и семантика. Исследования по логике и основам математики . Том. 103. Северная Голландия . ISBN  0-444-87508-5 .
• Черлин, Эдвард (1991). «Чистые функции в APL и J». Материалы международной конференции по APL'91-APL'91 . стр. 88–93. дои : 10.1145/114054.114065 . ISBN  0897914414 . S2CID   25802202 .
• Карри, Хаскелл Брукс (1930). «Grundlagen der Kombinatorischen Logik» [Основы комбинаторной логики]. Американский журнал математики (на немецком языке). 52 (3). Издательство Университета Джонса Хопкинса: 509–536. дои : 10.2307/2370619 . JSTOR   2370619 .
• Карри, Хаскелл Брукс ; Фейс, Роберт (1958). Комбинаторная логика . Том. I. Амстердам: Северная Голландия. ISBN  0-7204-2208-6 .
• Карри, Хаскелл Брукс ; Хиндли, Дж. Роджер ; Селдин, Джонатан П. (1972). Комбинаторная логика . Том. II. Амстердам: Северная Голландия. ISBN  0-7204-2208-6 .
• Энгелер, Э. (1995). Комбинированная программа (PDF) . Биркхойзер. стр. 5–6.
• Филд, Энтони Дж.; Харрисон, Питер Г. (1998). Функциональное программирование . Аддисон-Уэсли. ISBN  0-201-19249-7 .
• Гольдберг, Майер (2004). «Построение одноточечных базисов в расширенных лямбда-исчислениях». Письма об обработке информации . 89 (6): 281–286. дои : 10.1016/j.ipl.2003.12.005 .
• Хиндли, Дж. Роджер ; Мередит, Дэвид (1990). «Основные тип-схемы и конденсированные отряды» . Журнал символической логики . 55 (1): 90–105. дои : 10.2307/2274956 . JSTOR   2274956 . МР   1043546 . S2CID   6930576 .
• Хиндли, Дж. Роджер ; Селдин, Джонатан П. (2008) [1986]. Лямбда-исчисление и комбинаторы: Введение (2-е изд.). Издательство Кембриджского университета . ISBN  9780521898850 .
• Лаховский, Лукаш (2018). «О сложности стандартного перевода лямбда-исчисления в комбинаторную логику» . Доклады по математической логике . 2018 (53): 19–42. дои : 10.4467/20842589RM.18.002.8835 . Проверено 9 сентября 2018 г.
• Полсон, Лоуренс К. (1995). Основы функционального программирования . Кембриджский университет.
• Куайн, Уиллард Ван Орман (1960). «Переменные объяснены». Труды Американского философского общества . 104 (3): 343–347. JSTOR   985250 . Перепечатано как глава 23 Куайна (1996).
• Куайн, Уиллард Ван Орман (1996) [1960]. «Переменные объяснены». Избранные статьи по логике (Enl. Ed., 2. Печатное издание). Кембридж, Массачусетс: Издательство Гарвардского университета . стр. 227–235. ISBN  9780674798373 .
• Шенфинкель, Моисей (1924). «О строительных блоках математической логики» (PDF) . Математические анналы (на немецком языке). 92 (3–4): 305–316. дои : 10.1007/bf01448013 . S2CID   118507515 . Статья, положившая начало комбинаторной логике. Английский перевод: Шенфинкель (1967)
• Шенфинкель, Моисей (1967) [1924]. Ван Хейеноорт, Жан (ред.). строительных блоках логики математической О От Фреге до Гёделя: справочник по математической логике, 1879–1931. Перевод Бауэра-Менгельберга, Стефана. Кембридж, Массачусетс, США: Издательство Гарвардского университета . стр. 355–366. ISBN  978-0674324497 . OCLC   503886453 .
• Селдин, Джонатан П. (3 марта 2008 г.). «Логика Карри и Черча» (PDF) . Проверено 17 сентября 2023 г.
• Смалльян, Раймонд (1985). Посмеяться над пересмешником и другими логическими головоломками, включая удивительное приключение в области комбинаторной логики . Кнопф. ISBN  0-394-53491-3 . Нежное введение в комбинаторную логику, представленное в виде серии развлекательных головоломок с использованием метафор наблюдения за птицами.
• Смуллян, Раймонд (1994). Диагонализация и самореференция . Оксфордские руководства по логике. Том. 27. Оксфорд и Нью-Йорк: Издательство Оксфордского университета . ISBN  978-0198534501 . Главы 17–20 представляют собой более формальное введение в комбинаторную логику с особым упором на результаты с фиксированной точкой.
• Соренсен, Мортен Хейне Б; Уржичин, Павел (2006) [1999]. Лекции по изоморфизму Карри – Говарда (PDF) . Исследования по логике и основам математики. Том. 149 (1-е изд.). Эльзевир . п. 442. ИСБН  978-0444520777 . Архивировано из оригинала (PDF) 16 октября 2005 г. Проверено 22 апреля 2017 г.
• Тромп, Джон (2008). «Двоичное лямбда-исчисление и комбинаторная логика» (PDF) . В Калуде, Кристиан С. (ред.). Случайность и сложность: от Лейбница до Хайтина . Мировое научное издательство. Архивировано из оригинала (PDF) 4 марта 2016 г.
• Тернер, Дэвид А. (1979). «Другой алгоритм абстракции скобок». Журнал символической логики . 44 (2): 267–270. дои : 10.2307/2273733 . JSTOR   2273733 . S2CID   35835482 .
• Вольфенгаген, ВЕ (2003). Комбинаторная логика в программировании: Вычисления с объектами на примерах и упражнениях (2-е изд.). ООО «Центр ЮрИнфоР». Москва: ISBN  5-89158-101-9 .
• Вольфрам, Стивен (2021). Комбинаторы: взгляд на столетие . Вольфрам Медиа . ISBN  978-1-57955-043-1 . Праздник развития комбинаторов спустя сто лет после того, как их представил Шенфинкель (1924) (электронная книга: ISBN   978-1-57955-044-8 )

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

• Стэнфордская энциклопедия философии : « Комбинаторная логика » Каталин Бимбо .
• 1920–1931 Блокноты Карри.
• Кинан, Дэвид К. (2001) « Препарировать пересмешника: графическое обозначение лямбда-исчисления с анимированной редукцией » .
• Ратман, Крис, « Птицы-комбинаторы ». Таблица, отражающая большую часть сути Смалляна (1985).
• Комбинаторы перетаскивания. (Java-апплет)
• Бинарное лямбда-исчисление и комбинаторная логика.
• Веб-сервер комбинационной логической редукции
• Вольфрам, Стивен (29 апреля 2020 г.). Комбинаторы: празднование 100-летия . Проект Wolfram Physics на YouTube . Проверено 26 сентября 2023 г.