Исчисление комбинатора SKI

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

Все операции в лямбда-исчислении могут быть закодированы посредством исключения абстракций в исчислении SKI в виде бинарных деревьев , листьями которых являются один из трех символов S , K и I (называемых комбинаторами ).

Хотя наиболее формальное представление объектов в этой системе требует бинарных деревьев, для более простого набора они часто представляются в виде выражений в скобках, как сокращение для дерева, которое они представляют. Любые поддеревья могут быть заключены в скобки, но часто в скобки заключаются только правые поддеревья, при этом левая ассоциативность подразумевается для любых не заключенных в скобки приложений. Например, ISK означает (( IS ) K ). Используя эту нотацию, дерево, левое поддерево которого является деревом KS , а правое поддерево — деревом SK, можно записать как KS ( SK ). Если требуется большая ясность, можно также включить подразумеваемые скобки: (( KS )( SK )).

Неформально, и используя жаргон языка программирования, дерево ( xy ) можно рассматривать как функцию x, примененную к аргументу y . При оценке ( т. е . когда функция «применяется» к аргументу) дерево «возвращает значение», т. е . преобразуется в другое дерево. «Функция», «аргумент» и «значение» являются либо комбинаторами, либо бинарными деревьями. Если они являются бинарными деревьями, их также можно рассматривать как функции, если это необходимо.

Операция оценки определяется следующим образом:

( x , y и z представляют собой выражения, составленные из функций S , K и I , и заданных значений):

Я возвращаю свой аргумент:

Я х = х

При применении K к любому аргументу x получается константная функция K x с одним аргументом , которая при применении к любому аргументу y возвращает x :

К ху = х

S — оператор подстановки. Он принимает три аргумента, а затем возвращает первый аргумент, примененный к третьему, который затем применяется к результату второго аргумента, примененного к третьему. Более ясно:

S xyz = xz ( yz )

Пример вычисления: SKSK оценивается как KK ( SK ) по правилу S. Затем, если мы оцениваем KK ( SK ), мы получаем K по правилу K. Поскольку никакое другое правило не может быть применено, вычисление останавливается здесь.

Для всех деревьев x и всех деревьев y , SK xy всегда будет оцениваться как y в два шага, K y ( xy ) = y , поэтому конечный результат оценки SK xy всегда будет равен результату оценки y . Мы говорим, что SK x и I «функционально эквивалентны» для любого x , потому что они всегда дают один и тот же результат при применении к любому y .

Из этих определений можно показать, что исчисление SKI не является минимальной системой, которая может полностью выполнять вычисления лямбда-исчисления, поскольку все вхождения I в любом выражении могут быть заменены на ( SKK ) или ( SKS ) или ( SK x ) для любого x , и полученное выражение даст тот же результат. Таким образом, « I » — это просто синтаксический сахар . Поскольку I является необязательным, система также называется исчислением SK или комбинаторным исчислением SK .

Можно определить полную систему, используя только один (несобственный) комбинатор. Примером является йота- комбинатор Криса Баркера, который можно выразить в терминах S и K следующим образом:

ι x = x SK

Можно восстановить S , K , и I из комбинатора йота. Применение ι к самому себе дает ιι = ι SK = SSKK = SK ( KK ), что функционально эквивалентно I . K можно построить, применив ι дважды к I (что эквивалентно применению ι к самому себе): ι(ι(ιι)) = ι(ιι SK ) = ι( ISK ) = ι( SK ) = SKSK = K . Применение ι еще раз дает ι(ι(ι(ιι))) = ι K = KSK = S .

Простейшим возможным членом , образующим базис, является X = λf.f λxyz.xz (yz) λxyz.x, который удовлетворяет XX = K и X (XX) = S.

Термины и производные в этой системе можно определить и более формально:

Термины : Множество терминов T определяется рекурсивно по следующим правилам.

1. S , K и I — термины.
2. Если τ ₁ и τ ₂ являются членами, то (τ ₁ τ ₂ ) является членом.
3. Ничто не является термином, если этого не требуют первые два правила.

Выводы : Вывод — это конечная последовательность терминов, определяемая рекурсивно следующими правилами (где α и ι — слова в алфавите { S , K , I , (, )}, а β, γ и δ — термины):

1. Если Δ — это вывод, заканчивающийся выражением вида α( I β)ι, то Δ, за которым следует термин αβι, является выводом.
2. Если Δ — это вывод, заканчивающийся выражением вида α(( K β)γ)ι, то Δ, за которым следует термин αβι, является выводом.
3. Если Δ — вывод, оканчивающийся выражением вида α((( S β)γ)δ)ι, то Δ, за которым следует член α((βδ)(γδ))ι, является выводом.

Предполагая, что последовательность является допустимым выводом, ее можно расширить, используя эти правила. Все вывода длины 1 являются допустимыми выводами.

SII — это выражение, которое берет аргумент и применяет этот аргумент к себе:

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

Это также известно как комбинатор U , U x = xx . Одним из интересных его свойств является то, что его самоприменение неприводимо:

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

Или, используя уравнение непосредственно в качестве определения, мы немедленно получаем U U = U U .

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

( S ( K α)( SII ))β = K αβ( SII β) = α( I β( I β)) = α(ββ)

или его можно рассматривать как непосредственное определение еще одного комбинатора, H xy = x ( yy ).

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

β = H α = S ( K α)( SII )

тогда самоприменение этого β является неподвижной точкой этого α:

SII β = ββ = α(ββ) = α(α(ββ)) =${\displaystyle \ldots}$

Или, снова непосредственно из полученного определения, H α( H α) = α( H α( H α)).

Если α выражает «вычислительный шаг», вычисляемый αρν для некоторых ρ и ν, что предполагает, что ρν' выражает «остальную часть вычисления» (для некоторого ν', которое α «вычислит» из ν), то его неподвижная точка ββ выражает все рекурсивное вычисление, поскольку использование той же функции ββ для вызова «остальной части вычисления» (с ββν = α(ββ)ν) является самим определением рекурсии: ρν' = ββν' = α(ββ)ν' = ... . α придется использовать некое условное выражение, чтобы остановиться на некотором «базовом случае» и не делать рекурсивный вызов затем, чтобы избежать расхождения.

Это можно формализовать,

β = H α = S ( K α)( SII ) = S ( KS ) K α( SII ) = S ( S ( KS ) K )( K ( SII )) α

как

Y α = SII β = SII ( H α) = S ( K ( SII )) H α = S ( K ( SII ))( S ( S ( KS ) K )( K ( SII ))) α

что дает нам одну из возможных кодировок комбинатора Y. Более короткая вариация заменяет два его ведущих подтерма просто на SSI , поскольку H α( H α) = SHH α = SSIH α.

Это становится намного короче с использованием комбинаторов B,C,W , как эквивалента

Y α знак равно S ( КУ )( SB ( КУ ))α знак равно U ( B α U ) = BU ( CBU )α = SSI ( CBU )α

А с помощью псевдо- синтаксиса Haskell это становится исключительно коротким Y = U . (. U ).

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

• Это Y , автор Хаскелл Карри :

H gx = g ( xx ) ; Y g = H g ( H g ) ; Y = SSI(SB(KU)) = SSI(S(S(KS)K)(K(SII)))

• Θ Тьюринга :

ЧАС знак равно г ( hhg ) ; Θ г знак равно ЧЧ г  ; Θ = U(B(SI)U) = SII(S(K(SI))(SII))

• Y' (с SK-кодированием Джона Тромпа ^[3] ):

H gh = g ( hgh ) ; Y' g = H g H  ; Y' = WC(SB(C(WC))) = SSK(S(K(SS(S(SSK))))K)

• Θ₄ по Р.Статману: ^[4]

H gyz = g ( yyz ) ; Θ₄ g = H g ( H g )( H g ) ; Θ₄ = B(WW)(BW(BBB))

• или вообще,

H что-то = г ( hчто-то ); Y _H  г = H _____ H __  г

(где вместо "_" идет что угодно) или любое другое определение промежуточного комбинатора H с соответствующим ему определением Y для правильного запуска. В частности, ^[5]

L abcdefghijklmnopqstuvwxyzr = r ( это комбинатор с фиксированной точкой ) ; Y = LLLLLLLLLLLLLLLLLLLLLLLLLL

S ( K ( SI )) K меняет местами два следующих за ним члена:

С ( К ( СИ )) К αβ →

К ( СИ )α( К α)β →

СИ ( К α)β →

Я β( К αβ) →

Я βα →

βα

Таким образом, он эквивалентен CI . И в общем случае S ( K ( S f )) K эквивалентен C f для любого f .

Исчисление комбинаторов SKI также может реализовывать булеву логику в форме структуры if-then-else . Структура if-then-else состоит из булева выражения, которое является либо истинным ( T ), либо ложным ( F ), и двух аргументов, таких что:

Т ху = х

и

F ху = у

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

Т = К

К ху = х

Второй вариант тоже довольно прост:

Ф = СК

SK xy = K y(xy) = y

После определения значений true и false вся булева логика может быть реализована в терминах структур if-then-else .

Логическое НЕ (возвращающее противоположность заданному логическому значению) работает так же, как структура if-then-else , с F и T в качестве второго и третьего значений, поэтому его можно реализовать как постфиксную операцию:

НЕ = λb.b ( F )( T ) = λb.b ( SK )( K )

Если это поместить в структуру if-then-else , можно показать, что это дает ожидаемый результат.

( Т ) НЕ = Т ( Ф )( Т ) = Ф

( Ф ) НЕ = Ф ( Ф )( Т ) = Т

Булевое ИЛИ (которое возвращает T, если любое из двух окружающих его булевых значений равно T ) работает так же, как структура if-then-else с T в качестве второго значения, поэтому его можно реализовать как инфиксную операцию:

ИЛИ = Т = К

Если поместить это в структуру if-then-else , можно показать, что это дает ожидаемый результат:

( Т ) ИЛИ ( Т ) = Т ( Т )( Т ) = Т

( Т ) ИЛИ ( Ж ) = Т ( Т )( Ж ) = Т

( Ф ) ИЛИ ( Т ) = Ф ( Т )( Т ) = Т

( Ф ) ИЛИ ( Ф ) = Ф ( Т )( Ф ) = Ф

Логическое И (которое возвращает T, если оба из двух окружающих его логических значений равны T ) работает так же, как структура if-then-else с F в качестве третьего значения, поэтому его можно реализовать как постфиксную операцию:

И = Ф = СК

Если поместить это в структуру if-then-else , можно показать, что это дает ожидаемый результат:

( Т )( Т ) И = Т ( Т )( Ф ) = Т

( Т )( Ф ) И = Т ( Ф )( Ф ) = Ф

( Ф )( Т ) И = Ф ( Т )( Ф ) = Ф

( Ф )( Ф ) И = Ф ( Ф )( Ф ) = Ф

Поскольку это определяет T , F , NOT (как постфиксный оператор), OR (как инфиксный оператор) и AND (как постфиксный оператор) в терминах нотации SKI, это доказывает, что система SKI может полностью выражать булеву логику.

Поскольку исчисление SKI является полным , можно также выразить NOT , OR и AND как префиксные операторы:

НЕ = S ( SI ( KF ))( KT ) (так как S ( SI ( KF ))( KT ) x = SI ( KF ) x ( KT x ) = I x ( KF x ) T = x FT )

ИЛИ = СИ ( КТ ) (так как СИ ( КТ ) ху = I х ( КТ х ) у = х Т у )

И = СС ( К ( КФ )) (как СС ( К ( КФ )) xy = S x ( К ( КФ ) x ) y = xy ( КФ y ) = xy F )

Комбинаторы K и S соответствуют двум известным аксиомам пропозициональной логики :

АК : А → ( Б → А ) ,

АС : ( А → ( Б → В )) → (( А → В ) → ( А → В )) .

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

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

Аксиомы AK и AS , а также правило MP являются полными для импликационного фрагмента интуиционистской логики . Для того, чтобы комбинаторная логика имела в качестве модели:

• Импликативный фрагмент классической логики потребовал бы комбинаторного аналога закона исключенного третьего , т. е . закона Пирса ;
• Полная классическая логика потребовала бы комбинаторного аналога аксиомы высказывания F → A.

Эта связь между типами комбинаторов и соответствующими логическими аксиомами является примером изоморфизма Карри–Ховарда .

Может быть несколько способов сделать сокращение. Все они эквивалентны, пока вы не нарушаете порядок операций

• ${\displaystyle {\mathsf {SKI(KIS)}}}$
  • ${\displaystyle {\mathsf {SKI(KIS)}}\Rightarrow {\mathsf {K(KIS)(I(KIS))}}\Rightarrow {\mathsf {KIS}}\Rightarrow {\mathsf {I}}}$
  • ${\displaystyle {\mathsf {SKI(KIS)}}\Rightarrow {\mathsf {SKII}}\Rightarrow {\mathsf {KI(II)}}\Rightarrow {\mathsf {KII}}\Rightarrow {\mathsf {I}}}$
• ${\displaystyle {\mathsf {KS(I(SKSI))}}}$
  • ${\displaystyle {\mathsf {KS(I(SKSI))}}\Rightarrow {\mathsf {KS(I(KI(SI)))}}\Rightarrow {\mathsf {KS(I(I))}}\Rightarrow {\mathsf {KS(II)}}\Rightarrow {\mathsf {KSI}}\Rightarrow {\mathsf {S}}}$
  • ${\displaystyle {\mathsf {KS(I(SKSI))}}\Rightarrow {\mathsf {S}}}$
• ${\displaystyle {\mathsf {SKIK}}\Rightarrow {\mathsf {KK(IK)}}\Rightarrow {\mathsf {KKK}}\Rightarrow {\mathsf {K}}}$

• Комбинаторная логика
• Система B, C, K, W
• Комбинатор с фиксированной точкой
• Лямбда-исчисление
• Функциональное программирование
• Язык программирования Unlambda
• Языки программирования Iota и Jot , разработанные еще проще, чем SKI.
• Издеваться над пересмешником

• О'Доннелл, Майк «Комбинаторное исчисление SKI как универсальная система».
• Кинан, Дэвид С. (2001) «Анатомировать пересмешника».
• Ратман, Крис, «Птицы-комбинаторы».
• «Комбинаторы Drag 'n' Drop (Java Applet)».
• В книге «Исчисление мобильных процессов, часть I (PostScript)» (авторы — Милнер, Парроу и Уокер) на страницах 25–28 представлена ​​схема редукции комбинаторного графа для исчисления SKI.
• Язык программирования Nock можно рассматривать как язык ассемблера, основанный на комбинаторном исчислении SK, точно так же, как традиционный язык ассемблера основан на машинах Тьюринга. Инструкция Nock 2 («оператор Nock») — это комбинатор S, а инструкция Nock 1 — это комбинатор K. Другие примитивные инструкции в Nock (инструкции 0,3,4,5 и псевдоинструкция «implicit cons») не являются необходимыми для универсальных вычислений, но делают программирование более удобным, предоставляя возможности для работы со структурами данных двоичного дерева и арифметикой; Nock также предоставляет еще 5 инструкций (6,7,8,9,10), которые можно было бы построить из этих примитивов.