SKI-исчисление

Комбинаторное SKI-исчисление (М.Э. Шейнфинкель, начало 1920х) – простая, но очень ёмкая математическая модель вычислительного устройства. Относится к системам правил переписывания, рассмотренным ранее.

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

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

Грамматика

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

Пример формулы:

S (K S) K I

Её следует читать как

((S*(K*S))*K)*I

Как и в элементарной арифметике, непоставленные скобки прижимаются к левому краю: выражение A B C интерпретируется как (A B) C.

Правило преобразования

В SKI-исчислении три правила преобразования:

I x     → x
K x y   → x
S x y z → (x z) (y z)

Покажем, как работает нормализация согласно этим правилам:

S (K S) K I → (K S I) (K I) → S (K I)

Порядок вычислений

Есть два широких класса порядков вычислений (с большим количество разных вариаций): энергичный и ленивый. Основное различие – работа с выражением вида A*B.

Энергичный порядок (или, как ещё говорят, аппликативный) регламентирует следующую процедуру преобразования A*B:

Преобразовать B, получив b.
Сделать некоторые преобразования с A, получив a.
Если можно со всем выражением сделать преобразование, оно делается, а далее всё повторяется до достижения нормальной формы.

Ленивый порядок отличается от аппликативного отсутствием пункта 1. При дальнейшем рассмотрении SKI-исчисления мы будем использовать т.н. “нормализующий ленивый порядок”. Он очень прост: нужно на каждом шаге применять преобразование к самой левой букве среди тех, к которым можно его применить.

Есть важный (но нетривиально доказываемый) факт: “нормализующий ленивый порядок” приводит выражение к нормальной форме, если она есть.

Экстенсиональная эквивалентность

Рассмотрим две формулы: I и S K K. Они разные! Тем не менее, если “скормить” каждой из них что-нибудь (обозначим это “что-нибудь” x), то в результате нормализации получится одно и то же:

I x → x
S K K x → (K x) (K x) = K x (K x) → x

Такие формулы называются экстенсионально эквивалентными. Почти всегда интересна именно экстенсиональная эквивалентность формул, а не их равенство.

Реализация произвольных зависимостей

Допустим, что мы хотим найти формулу F, для которой выполнено

F x → ... → G

то есть, F x преобразуется (за некоторое количество преобразований к G).

Алгоритм довольно прост: если G = x, то в качестве F можно взять I. Если G вообще не содержит x, то в качестве F можно взять K G. В противном случае G = A*B и в качестве F можно взять S a b так, чтобы

a x → ... → A
b x → ... → B

Эти две задачи “меньше” исходной. Решив их, мы решаем исходную.

Важные комбинаторы

Алгоритм реализации произвольных зависимостей мы проиллюстрируем на примере важнейших формул, которые ещё неоднократно нам встретятся.

Дупликатор D – формула, для которой D x → ... → x x. Согласно алгоритму, в качестве D можно взять S a b, где

a x → ... → x
b x → ... → x

Согласно тому же алгоритму, можно взять a = I и b = I. Итог: D = S I I.

Транспозиция T – формула, для которой T x y → ... → y x. Получение формулы для этой зависимости состоит из двух частей: сначала получим формулу, в которую можно преобразовать T x, а затем уже получим T.

Применяя алгоритм, получаем T x → ... → S a b, где

a y → ... → y
b y → ... → x

Берём a = I и b = K x. Осталось реализовать зависимость T x → ... → S I (K x).

Нужно взять T = S a b, где

a x → ... → S I
b x → ... → K x

В качестве a можно взять K (S I), а в качестве b – просто K (хотя алгоритм предписывает брать S (K K) I). Итог: T = S (K (S I)) K.

Композиция B – формула, для которой B f g x → ... → f (g x). Согласно алгоритму, B f g → ... → S (K f) g. Далее можно заметить, что достаточно релаизовать зависимость B f → ... → S (K f). Соответственно, B = S (K S) K.

Арифметика Чёрча

Появится позже…