Комбинаторный расчет 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 и всех деревьев SK y xy всегда будет оценивать y в два этапа, K y ( xy ) = y , поэтому окончательный результат оценки SK xy всегда будет равен результату оценки y . Мы говорим, что SK x и I «функционально эквивалентны» для любого x, потому что они всегда дают один и тот же результат при применении к любому y .

Из этих определений можно показать, что исчисление SKI не является минимальной системой, которая может полностью выполнять вычисления лямбда-исчисления, поскольку все вхождения I в любом выражении могут быть заменены на ( SKK ), ( SKS ) или ( SK x ) для любой x , и полученное выражение даст тот же результат. Итак, « Я » — это просто синтаксический сахар . Поскольку 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 = λx λy λz. xz (y (λ_.z)), что удовлетворяет условиям X (XX) (X (XX) XXXXX) = K , и X (X (XX (XX (XX))(X (X (XX (XX)))) )) XX = S .

Формальное определение

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

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

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

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

Если Δ — вывод, оканчивающийся выражением вида α( I β)ι, то Δ, за которым следует член αβι, является выводом.
Если Δ — вывод, оканчивающийся выражением вида α(( K β)γ)ι, то Δ, за которым следует член αβι, является выводом.
Если Δ — вывод, оканчивающийся выражением вида α((( 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 ).

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

β знак равно ЧАС α знак равно S ( K α)( SII )

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

SII β = ββ = α(ββ) = α(α(ββ)) =

\ldots

Или, снова непосредственно из полученного определения, 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- .

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

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

или напрямую, как

H αβ = α(ββ) = B α U β = CBU αβ

Y α = U ( Ч α) = BU ( CBU )α

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

Обратное выражение

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

S ( K ( SI )) K αβ →

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

СИ ( К α)β →

I β( К αβ) →

Я ба →

ух ты

Булева логика

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

Т ху = х

и

Fxy = у

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

Т = К

К ху = х

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

Ф = СК

SK xy = K y(xy) = y

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

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

НЕ = ( F )( Т ) = ( SK )( K )

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

( Т ) НЕ знак равно Т ( F )( Т ) = F

( F ) НЕ = F ( F )( Т ) = Т

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

ИЛИ = Т = К

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

( Т ) ИЛИ ( Т ) знак равно Т ( Т )( Т ) знак равно Т

( Т ) ИЛИ ( F ) знак равно Т ( Т )( F ) знак равно Т

( F ) ИЛИ ( Т ) знак равно F ( Т )( Т ) знак равно Т

( F ) ИЛИ ( F ) знак равно F ( Т )( F ) знак равно F

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

И = Ф = СК

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

( Т )( Т ) И знак равно Т ( Т )( F ) знак равно Т

( Т )( F ) И знак равно Т ( F )( F ) = F

( F )( Т ) И знак равно F ( Т )( F ) = F

( F )( F ) И знак равно F ( F )( F ) = F

Поскольку это определяет 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 )

ИЛИ = SI ( КТ как СИ ( КТ ) xy = I x ( КТ x ) y = x T y ) (

И = SS ( K ( KF )) (как SS ( K ( KF )) xy = S Икс ( K ( KF ) x ) y = xy ( KF y ) = xy F )

Связь с интуиционистской логикой

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

И : А \to (Б \to А)

,

КАК : (А \to (B \to C)) \to ((A \to B) \to (A \to C))

.

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

МП

: из

А

и

А \to Б

вывод

Б.

сделать

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

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

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

Примеры сокращения

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

${\textrm {SKI(KIS)}}$ ${\textrm {ЛЫЖИ (КИС)})$
- ${\textrm {SKI(KIS)}}\Rightarrow {\textrm {K(KIS)(I(KIS))}}\Rightarrow {\textrm {KIS}}\Rightarrow {\textrm {I}}$
- ${\textrm {SKI(KIS)}}\Rightarrow {\textrm {SKII}}\Rightarrow {\textrm {KI(II)}}\Rightarrow {\textrm {KII}}\Rightarrow {\textrm {I}}$
${\textrm {KS(I(SKSI))}}$ ${\textrm {KS(I(SKSI)))}$
- ${\textrm {KS(I(SKSI))}}\Rightarrow {\textrm {KS(I(KI(SI)))}}\Rightarrow {\textrm {KS(I(I))}}\Rightarrow {\textrm {KS(II)}}\Rightarrow {\textrm {KSI}}\Rightarrow {\textrm {S}}$
- ${\textrm {KS(I(SKSI))}}\Rightarrow {\textrm {S}}$
${\textrm {SKIK}}\Rightarrow {\textrm {KK(IK)}}\Rightarrow {\textrm {KKK}}\Rightarrow {\textrm {K}}$

См. также

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

Ссылки

^ Шёнфинкель, М. (1924). «О составных элементах математической логики». Математические летописи . 92 (3–4): 305–316. дои : 10.1007/BF01448013 . S2CID 118507515 . Переведено Стефаном Бауэром-Менгельбергом как ван Хейеноорт, Жан , изд. (2002) [1967]. «О составных элементах математической логики» . Справочник по математической логике 1879–1931 гг . Издательство Гарвардского университета. стр. 355–366. ISBN 9780674324497 .
^ Карри, Хаскелл Брукс (1930). «Grundlagen der Kombinatorischen Logik» [Основы комбинаторной логики]. Американский журнал математики (на немецком языке). 52 (3). Издательство Университета Джонса Хопкинса: 509–536. дои : 10.2307/2370619 . JSTOR 2370619 .

Смалльян, Раймонд (1985). Издеваться над пересмешником . Кнопф. ISBN 0-394-53491-3 . Нежное введение в комбинаторную логику, представленное в виде серии развлекательных головоломок с использованием метафор наблюдения за птицами.
— (1994). «Гл. 17–20». Диагонализация и самореференция . Издательство Оксфордского университета. ISBN 9780198534501 . OCLC 473553893 . представляют собой более формальное введение в комбинаторную логику с особым упором на результаты с фиксированной точкой.

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

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

[1] Шёнфинкель, М. (1924). «О составных элементах математической логики». Математические летописи . 92 (3–4): 305–316. дои : 10.1007/BF01448013 . S2CID 118507515 . Переведено Стефаном Бауэром-Менгельбергом как ван Хейеноорт, Жан , изд. (2002) [1967]. «О составных элементах математической логики» . Справочник по математической логике 1879–1931 гг . Издательство Гарвардского университета. стр. 355–366. ISBN 9780674324497 .

[2] Карри, Хаскелл Брукс (1930). «Grundlagen der Kombinatorischen Logik» [Основы комбинаторной логики]. Американский журнал математики (на немецком языке). 52 (3). Издательство Университета Джонса Хопкинса: 509–536. дои : 10.2307/2370619 . JSTOR 2370619 .

[1]

[2]