Расчет комбинатора SKI - SKI combinator calculus

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

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

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

я избыточно, так как ведет себя так же, как SKK,[4] но включен для удобства.

Неформальное описание

Неформально и используя жаргон языка программирования, дерево (ху) можно рассматривать как "функцию" Икс применительно к «аргументу» у. Когда "оценивается" (т.е., когда функция «применяется» к аргументу), дерево «возвращает значение», т.е., превращается в другое дерево. Конечно, все три из «функции», «аргумента» и «значения» являются либо комбинаторами, либо двоичными деревьями, и если они являются двоичными деревьями, их тоже можно рассматривать как функции всякий раз, когда возникает необходимость.

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

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

я возвращает свой аргумент:[4]

яИкс = Икс

K, применительно к любому аргументу Икс, дает постоянную функцию с одним аргументом KИкс, который при применении к любому аргументу возвращает Икс:[4]

Kху = Икс

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

Sxyz = xz(yz)

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

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

Из этих определений можно показать, что исчисление SKI не является минимальной системой, которая может полностью выполнять вычисления лямбда-исчисления, поскольку все вхождения я в любом выражении можно заменить на (SKK) или же (SKS) или же (SK что бы ни)[4] и получившееся выражение даст тот же результат. Итак "я"просто синтаксический сахар. С я является необязательным, система также называется исчислением SK или комбинаторным исчислением SK.

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

ιИкс = ИксSK

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

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

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

Условия:Набор Т терминов определяется рекурсивно по следующим правилам.

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

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

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

Предполагая, что последовательность является действительным производным для начала, ее можно расширить с помощью этих правил. [1]

Рекурсивная передача параметров и цитирование

К = λq.λi.q
цитирует q и игнорирует i
S = λx.λy.λz. ((Xz) (yz))
формирует двоичное дерево, параметры которого могут передаваться от корня к ветвям и считываться с помощью identityFunc = ((SK) K) или считывать цитируемую лямбду q с помощью Kq.

ЛЫЖНЫЕ выражения

Самостоятельное применение и рекурсия

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

SIIα = яα (яα) = αα

Одно интересное свойство этого состоит в том, что выражение SII(SII) неприводимый:

SII(SII) = я(SII)(я(SII)) = я(SII)(SII) = SII(SII)

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

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

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

β = S(Kα) (SII)

тогда:

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

Выражение разворота

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

S(K(SI))Kαβ →
K(SI) α (Kα) β →
SI(Kα) β →
яβ (Kαβ) →
яβα →
βα

Логическая логика

Расчет комбинатора SKI также может реализовывать Логическая логика в виде если-то-еще структура. An если-то-еще структура состоит из логического выражения, которое либо истинно (Т) или ложь (F) и два аргумента, такие что:

Тху = Икс

и

Fху = у

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

Т = K
Kху = Икс

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

F = SK
SKху = Kу (ху) = y

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

Булево НЕТ (который возвращает противоположность заданного логического значения) работает так же, как и если-то-еще структура, с F и Т как второе и третье значения, поэтому его можно реализовать как постфиксную операцию:

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

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

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

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

ИЛИ ЖЕ = Т = K

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

(Т)ИЛИ ЖЕ(Т) = Т(Т)(Т) = Т
(Т)ИЛИ ЖЕ(F) = Т(Т)(F) = Т
(F)ИЛИ ЖЕ(Т) = F(Т)(Т) = Т
(F)ИЛИ ЖЕ(F) = F(Т)(F) = F

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

И = F = SK

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

(Т)(Т)И = Т(Т)(F) = Т
(Т)(F)И = Т(F)(F) = F
(F)(Т)И = F(Т)(F) = F
(F)(F)И = F(F)(F) = F

Потому что это определяет Т, F, НЕТ (как постфиксный оператор), ИЛИ ЖЕ (как инфиксный оператор), и И (как постфиксный оператор) с точки зрения обозначения SKI, это доказывает, что система SKI может полностью выражать логику.

Поскольку расчет SKI полный, также можно выразить НЕТ, ИЛИ ЖЕ и И как префиксные операторы:

НЕТ = S(SI(KF))(KT) (в качестве S(SI(KF))(KT)Икс = SI(KF)Икс(KTИкс) = яИкс(KFИкс)Т = ИксFT)
ИЛИ ЖЕ = SI(KT) (в качестве SI(KT)ху = яИкс(KTИкс)у = ИксТу)
И = SS(K(KF)) (в качестве SS(K(KF))ху = SИкс(K(KF)Икс)у = ху(KFу) = хуF)

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

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

АК: А → (B → А),
В КАЧЕСТВЕ: (А → (B → C)) → ((А → B) → (А → C)).

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

Депутат: из А и А → B, сделать вывод B.

Аксиомы АК и В КАЧЕСТВЕ, и правило Депутат завершены для имплицитного фрагмента интуиционистская логика. Для того, чтобы комбинаторная логика была моделью:

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

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

Рекомендации

  1. ^ 1924. "Über die Bausteine ​​der Mathematischen Logik", Mathematische Annalen 92С. 305–316. Перевод Стефана Бауэра-Менгельберга как «О строительных блоках математической логики» в Жан ван Хейеноорт, 1967. Справочник по математической логике, 1879–1931 гг.. Harvard Univ. Пресс: 355–66.
  2. ^ Карри, Хаскелл Брукс (1930). "Grundlagen der Kombinatorischen Logik" [Основы комбинаторной логики]. Американский журнал математики (на немецком). Издательство Университета Джона Хопкинса. 52 (3): 509–536. Дои:10.2307/2370619. JSTOR  2370619.
  3. ^ Вольфрам, Стивен. «История символических систем». Новый вид науки в Интернете. Получено 2019-06-17.
  4. ^ а б c d е ж Вольфрам, Стивен. «Комбинаторы». Новый вид науки в Интернете. Получено 2019-06-17.
  • Смуллян, Раймонд, 1985. Издеваться над пересмешником. Кнопф. ISBN  0-394-53491-3. Мягкое введение в комбинаторную логику, представленное в виде серии развлекательных головоломок с использованием метафор наблюдения за птицами.
  • --------, 1994. Диагонализация и самооценка. Oxford Univ. Нажмите. Гл. 17-20 представляют собой более формальное введение в комбинаторную логику с особым акцентом на результаты с фиксированной точкой.

внешняя ссылка