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

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

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

В математике

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Чтобы сократить обозначения, общее соглашение заключается в том, что ⁠ ⁠ ${\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})}$ . Это то же общее соглашение (левая ассоциативность), что и для множественного применения в лямбда-исчислении.

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

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

( П х ₁ ... х _n ) = Е

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

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

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

( Я х ) = х

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

(( К х ) у ) = х

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

( К х у ) = х

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

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

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

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

(( словацкие крон ) х )

= ( словацкие кроны x )

= ( К х ( К х ))

= х

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

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

Полнота базы СК

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

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

1. Т [ х ] ⇒ х
2. Т [( Э ₁ Э ₂)] ⇒ ( Т [ Э ₁] Т [ Э ₂])
3. T [ λx . E ] ⇒ ( K T [ E ]) (если x не встречается свободно в E )
4. Т [ λ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. Очень простой алгоритм абстракции скобок определяется индукцией по структуре выражений следующим образом: ^[6]

1. [ х ] у  := К у
2. [ х ] х  := Я
3. [ Икс ]( E₁ E₂ ) = S ([ Икс ] E₁ )([ Икс ] E₂ )

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

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

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

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

= T [ λ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)

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

= ( С Я ( С ( К К ) Я х) у)

= ( Я у ( С ( К К ) Я ху))

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

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

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

= (y ( I x))

= (yx)

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

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

Преобразование 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 ₂) а ) знак равно (( λx . E ₁ а ) ( λx . E ₂ а ))

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

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

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

λ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. Поэтому достаточно преобразовать E в комбинаторную форму.

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

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

= ...

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

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

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

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

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

= ( СИ ( К x ) y )

= ( Я у ( К х у ))

= ( у ( К х у ))

= ( ух )

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

На основе одного пункта

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

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

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

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

X ( X ( X ( X X ))) = ^β S .

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

Еще один простой пример одноточечной основы:

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

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

X' ( X' X' ) = ^β S

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

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

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

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

( Б ж г х ) = ( ж ( г х ))

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

В = ( С ( КС ) К )

С = ( С ( С ( К ( С ( КС ) К )) С ) ( КК ))

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

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

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

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

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

= Т [ λ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 ):

  ( С I х у )

= ( Я у х )

= ( у х )

Мотивация здесь в том, что 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 работы Тромпа (2008).

КЛ_Кпротив CL_яисчисление

Необходимо провести различие между 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 [ I ] = λx . x

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

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 [ ], которые мы видели.

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

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

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

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

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

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

( Н А ) = Т и

( Н Б ) = Ф .

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

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

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

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

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

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

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

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

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

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

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

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

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

Приложения

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

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

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

Логика

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

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

АК : А → ( Б → А ),

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

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

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

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

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

Это определение подчиняется условиям выполнения →: с одной стороны, если , и таково, что и , то по modus ponens. С другой стороны, если , то по теореме о дедукции , таким образом, дедуктивное замыкание является элементом таким, что , , и . ${\displaystyle X\Vdash A\to B}$ ${\displaystyle Y\in W}$ ${\displaystyle Y\supseteq X}$ ${\displaystyle Y\Vdash A}$ ${\displaystyle Y\Vdash B}$ ${\displaystyle X\not \Vdash A\to B}$ ${\displaystyle X,A\not \vdash B}$ ${\displaystyle X\cup \{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
• Суперкомбинатор
• Издеваться над пересмешником

Ссылки

1. Шёнфинкель 1924, Статья, положившая начало комбинаторной логике. Английский перевод: Шёнфинкель (1967).
2. Карри 1930.
3. Селдин 2008.
4. Барендрегт 1984.
5. Хиндли и Мередит 1990.
6. Тернер 1979.
7. Лачовски 2018.
8. Голдберг 2004.
9. Энгелер 1995.
10. Черлин 1991.

Литература

• Барендрегт, Хендрик Питер (1984). Лямбда-исчисление, его синтаксис и семантика. Исследования по логике и основаниям математики . Том 103. Северная Голландия . ISBN 0-444-87508-5.
• Cherlin, Edward (1991). "Чистые функции в APL и J". Труды международной конференции по APL '91 - APL '91 . стр. 88–93. doi :10.1145/114054.114065. ISBN 0897914414. S2CID  25802202.
• Карри, Хаскелл Брукс (1930). «Основы комбинаторной логики». Американский журнал математики (на немецком языке). 52 (3). Издательство Университета Джона Хопкинса: 509–536. doi :10.2307/2370619. JSTOR  2370619.
• Карри, Хаскелл Брукс ; Фейс, Роберт (1958). Комбинаторная логика . Том I. Амстердам: Северная Голландия. ISBN 0-7204-2208-6.
• Карри, Хаскелл Брукс ; Хиндли, Дж. Роджер ; Селдин, Джонатан П. (1972). Комбинаторная логика . Том II. Амстердам: Северная Голландия. ISBN 0-7204-2208-6.
• Энгелер, Э. (1995). Комбинационная программа (PDF) . Биркхойзер. стр. 5–6.
• Field, Anthony J.; Harrison, Peter G. (1998). Функциональное программирование . Addison-Wesley. ISBN 0-201-19249-7.
• Голдберг, Майер (2004). «Построение одноточечных базисов в расширенных лямбда-исчислениях». Information Processing Letters . 89 (6): 281–286. doi :10.1016/j.ipl.2003.12.005.
• Hindley, J. Roger ; Meredith, David (1990). «Основные схемы типов и сгущенное отделение». Journal of Symbolic Logic . 55 (1): 90–105. doi :10.2307/2274956. JSTOR  2274956. MR  1043546. S2CID  6930576.
• Hindley, J. Roger ; Seldin, Jonathan P. (2008) [1986]. Лямбда-исчисление и комбинаторы: Введение (2-е изд.). Cambridge University Press . ISBN 9780521898850.
• Lachowski, Łukasz (2018). «О сложности стандартного перевода лямбда-исчисления в комбинаторную логику». Reports on Mathematical Logic . 2018 (53): 19–42. doi : 10.4467/20842589RM.18.002.8835 . Получено 9 сентября 2018 г.
• Полсон, Лоуренс К. (1995). Основы функционального программирования. Кембриджский университет.
• Куайн, Уиллард Ван Орман (1960). «Переменные объяснены». Труды Американского философского общества . 104 (3): 343–347. JSTOR  985250. Перепечатано как Глава 23 Куайна (1996)
• Куайн, Уиллард Ван Орман (1996) [1960]. «Переменные объяснены». Избранные статьи по логике (Enl. ed., 2. печатное издание). Кембридж, Массачусетс: Harvard University Press . стр. 227–235. ISBN 9780674798373.
• Шёнфинкель, Моисей (1924). «Über die Bausteine ​​der Mathematischen Logik» (PDF) . Mathematische Annalen (на немецком языке). 92 (3–4): 305–316. дои : 10.1007/bf01448013. S2CID  118507515. Статья, основавшая комбинаторную логику. Английский перевод: Шёнфинкель (1967)
• Шенфинкель, Моисей (1967) [1924]. Ван Хейеноорт, Жан (ред.). Über die Bausteine ​​der mathematischen Logik [ О строительных блоках математической логики ]. От Фреге до Гёделя: справочник по математической логике, 1879–1931. Перевод Бауэра-Менгельберга, Стефана. Кембридж, Массачусетс, США: Издательство Гарвардского университета . стр. 355–366. ISBN 978-0674324497. OCLC  503886453.
• Селдин, Джонатан П. (3 марта 2008 г.). «Логика Карри и Черча» (PDF) . Получено 17 сентября 2023 г.
• Смаллиан, Рэймонд (1985). Издевательство над пересмешником и другие логические головоломки, включая удивительное приключение в комбинаторной логике . Кнопф. ISBN 0-394-53491-3. Мягкое введение в комбинаторную логику, представленное в виде серии развлекательных головоломок с использованием метафор наблюдения за птицами.
• Смаллиан, Рэймонд (1994). Диагонализация и самореференция . Oxford logic guides. Том 27. Оксфорд и Нью-Йорк: Oxford University Press . ISBN 978-0198534501. Главы 17–20 представляют собой более формальное введение в комбинаторную логику с особым акцентом на результатах с фиксированной точкой.
• Sørensen, Morten Heine B; Urzyczyn, Paweł (2006) [1999]. Лекции об изоморфизме Карри–Ховарда (PDF) . Исследования по логике и основаниям математики. Т. 149 (1-е изд.). Elsevier . стр. 442. ISBN 978-0444520777. Архивировано из оригинала (PDF) 2005-10-16 . Получено 2017-04-22 .
• Tromp, John (2008). "Binary Lambda Calculus and Combinatory Logic" (PDF) . В Calude, Cristian S. (ред.). Randomness And Complexity, from Leibniz To Chaitin . World Scientific Publishing Company. Архивировано из оригинала (PDF) 2016-03-04.
• Тернер, Дэвид А. (1979). «Еще один алгоритм для абстракции скобок». Журнал символической логики . 44 (2): 267–270. doi :10.2307/2273733. JSTOR  2273733. S2CID  35835482.
• Вольфенгаген, В. Э. (2003). Комбинаторная логика в программировании: Вычисления с объектами в примерах и упражнениях (2-е изд.). М.: ООО «Центр ЮрИнфоР». ISBN 5-89158-101-9.
• Вольфрам, Стивен (2021). Комбинаторы: взгляд на столетие. Wolfram Media . ISBN 978-1-57955-043-1. Празднование развития комбинаторов, спустя сто лет после того, как они были представлены Шёнфинкелем (1924)(Электронная книга: ISBN 978-1-57955-044-8 ) 

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

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