Далее пойдет рассказ о самом, на мой взгляд, хардкорном способе программирования.
Предмет поста непростой, путь будет долгим, а в качестве печеньки в конце я расскажу, как считать числа Фибоначчи на языке Unlambda.
Для знатоков: статья скорее имеет целью объяснить, как это работает, нежели дать строгое формальное описание.
λ-исчисление было изобретено Алонзо Чёрчем для формализации понятия алгоритма и вычислимости. Функции в λ-исчислении следует понимать именно так — как некий алгоритм, обрабатывающий входные данные.
Бестиповое λ-исчисление
Предположим, что у нас есть функции от одного аргумента. Причем и их аргумент, и возвращаемое значение — тоже функции от одного аргумента.
Здесь математики возразят: у нас получается множество, совпадающее с множеством функций из себя в себя, чего в теории множеств быть не может (даже в случае бесконечных множеств множество функций строго больше). Но это не помешало американцу Скотту построить декартово-замкнутую категорию, введя особую топологию на частично упорядоченных множествах, т.е. представленный объект действительно существует, но это уже совсем другая история.
Итак, казалось бы, что мы можем сделать, имея под рукой лишь такой абстрактный и необозримый набор странных функций? Для начала неплохо бы определиться, как эти функции записывать. В λ-исчислении приняты такие правила:
- Пусть f и a — некоторые функции. Тогда f a обозначает применение функции f к функции a, или, в терминологии λ-исчисления, аппликация.
- Пусть F — выражение, свободно содержащее переменную x, либо вообще её не содержащее. Тогда λx.F обозначает функцию от переменной x, значение которой задается выражением F, и называется это λ-абстракцией.
Тогда λx.f x = f, так как эта функция принимает аргумент x и возвращает значение f x, что и делает сама функция f. Это называется η-преобразованием.
Например, λx.x2 — функция возведения в квадрат, а (λx.x2) 3 — применение этой функции к аргументу 3. Интуиция подсказывает, что значение этого выражения — 9, что и утверждает единственная аксиома λ-исчисления, называемая β-редукцией:
- (λx.F) a = F[x := a]
где F[x := a] означает выражение F, в котором вместо x подставлено a. Вместе с этой аксиомой λ-исчисление становится Тьюринг-полным языком программирования, т.е. на нем можно реализовать любой алгоритм (в разумном понимании того, что же такое алгоритм). Возникает естественный вопрос — как?
Несложно набросать тождественную функцию, просто возвращающую свой аргумент: λx.x
Функция-константа тоже не вызывает осложнений: λx.c, где c не зависит от x. Действительно, при любом аргументе функция возвратит c.
Казалось бы, вот и все. Мы ведь даже не умеем строить функции от нескольких аргументов! Да нет, умеем, просто мы пока об этом не знаем.
Рассмотрим такой пример: λx.λy.x+y. Для большей наглядности, расставим скобки: λx.(λy.(x+y)) — это функция, возвращающая другую функцию, возвращающую сумму. Как это работает? Давайте применим ее к некоторому аргументу: (λx.(λy.(x+y))) a = λy.(a+y). Получившуюся функцию применим к другому аргументу: (λy.(a+y)) b = a+b. Такой прием называется карринг, или каррирование (в честь Хаскелла Карри), и работает для любого числа аргументов. Договоримся, что если функция имеет вид λx.(λy.(λz.(F))), то мы будем записывать её как λxyz.F. Ещё договоримся, что (f a b c) обозначает
(((f a) b) c). Теперь функции многих аргументов записываются очень просто: λxy.x+y, а их применение — (f a b).
Небольшое отступление: я уже не раз использовал числа и арифметические операции, несмотря на то, что статья о бестиповом λ-исчислении, и формально ни о каких числах и операциях мы пока не знаем. Это сделано для улучшения понимания, и вскоре мы узнаем, что и то, и другое в λ-исчислении можно реализовать.
Управляющие конструкции
Теперь ответим на вопрос, как в λ-исчислении сделать цикл. Так как мы имеем дело только с функциями, то, очевидно, с помощью механизма рекурсии. Но в λ-исчислении мы не можем вызвать функцию изнутри себя, поэтому применяется несколько иной подход — функция передается сама себе в качестве аргумента.
Рассмотрим такую функцию: w = λx.x x. Она применяет свой единственный аргумент к самому себе (помните, у нас ведь что ни возьми — функция). Попробуем применить эту функцию к самой себе: w w = (λx.x x) w = (x x)[x := w] = w w. Упс, воспользовавшись β-редукцией, мы пришли к тому, с чего начали. Это — один из простейших примеров бесконечного цикла в λ-исчислении, примечательный тем, что не делает абсолютно ничего.
Еще один важный вопрос: как реализовать условный оператор? Здесь важно понять, что else-ветвь в нем не может отсутствовать. У нас все объекты — функции, которые обязаны вернуть значение, и мы не можем «ничего не делать». Определим такие объекты:
- true = λxy.x
- false = λxy.y
Теперь, если bool — логическое значение в смысле данных определений, то (bool if else) — в точности нужная нам конструкция. Если bool = true, то результатом будет выражение if, иначе выражение else.
Теперь попробуем решить классическую задачу на циклы и рекурсию — вычисление факториала. Пусть у нас уже реализованы числа, арифметические операции (которые мы теперь будем записывать в префиксной нотации, в стиле λ-исчисления), функция dec, уменьшающая свой аргумент на 1, а также функция zero, с помощью которой мы можем проверить число на равенство нулю.
g = λrn.(zero n) 1 (* n (r (dec n)))
Посмотрим внимательно: функция проверяет n на равенство нулю, возвращает 1 в случае успеха, иначе возвращает (* n (r (dec n))) — произведение n и значения некой функции r от n-1. Что такое функция r? Это своего рода хак, чтобы сделать рекурсию — в качестве r мы будем передавать саму функцию g, а значит написанное выражение действительно вычисляет факториал: g(n) = n * g(n-1). Так как неудобно каждый раз передавать функции саму себя, сделаем такую окончательную реализацию факториала:
f = g g
Таким образом, g «запомнит» свой первый аргумент, и останется только передать ей нужное число для вычислений.
Дальше — хуже.
Комбинатор неподвижной точки
Оказывается, в лямбда-исчислении для любой функции f существует такой аргумент x, что f x = x. Более того, этот x всегда можно найти! Эту работу выполняет так называемый комбинатор неподвижной точки. Один из его вариантов, придуманный нашим любимым Хаскеллом Карри:
Y = λf.(λx.f (x x)) (λx.f (x x))
Посмотрим, как это работает:
Y f = (λx.f (x x)) (λx.f (x x)) = f ((λx.f (x x)) (λx.f (x x))) = f (Y f)
Таким образом, Y f — действительно неподвижная точка функции f, так как f (Y f) = Y f.
Числа и арифметика
Как Вы уже могли догадаться, все приведённые выше реализации необходимых объектов и структур не единственны — прелесть λ-исчисления в том, что Вы сами решаете, как реализовать базовые необходимые Вам вещи. Но если в отношении циклов и условий вроде как выявлены самые простые реализации, то с числами дела обстоят по-другому — практичных реализаций чисел необозримо много, для каждой задачи можно придумай свой, специфичный вариант. Тем не менее, существует общепринятая реализация чисел — «нумералы Чёрча», придуманные тем самым Алонзо Чёрчем.
Определим неотрицательное число N как функцию, принимающую некоторую функцию f, аргумент x и N раз вычисляющую значение f от x:
- 0: x
- 1: f(x)
- 2: f(f(x))
- 3: f(f(f(x)))
Таким образом, в λ-исчислении наши числа выглядят так:
- 0: λfx.x
- 1: λfx.f x
- 2: λfx.f (f x)
- 3: λfx.f (f (f x))
Функция inc:
inc = λnfx.f (n f x)
n раз применили функцию, и применим еще разок, чтобы получить n+1.
Как сложить m и n? Нужно применить f к x сначала m, а затем n раз:
add = λmnfx.m f (n f x)
Умножение делается проще, нужно m раз применять (n f) к x:
mult = λmnf.m (n f)
Возведение в степень — и того проще:
pow = λmn.n m
Напишем функцию, проверяющую, ноль ли наш аргумент:
λn.n (λx.false) true
Если аргумент — ноль, то он (как Вы помните из определения) просто возвратит второй аргумент, т.е. true, иначе он будет много (ну, как минимум, один) раз применять функцию λx.false к чему-то там. Вот и пригодились те самые константы, о которых мы говорили — возвращаемое значение будет false.
Теперь кое-что потруднее — вычитание. Для начала сделаем функцию, возвращающую число на 1 меньше (или что-нибудь, если аргумент — 0). Вот она:
dec = λnfx.n (λgh.h (g f)) (λu.x) (λu.u)
Думаю, теперь даже у самых стойких сдают нервы в связи с вопросом «как это, черт возьми, работает?». Попробуем понять.
Для начала посмотрим на кусок n (λgh.h (g f)) (λu.x) — нечто неведомое n раз применяется к (λu.x). Давайте уподобимся нумералам Чёрча и поприменяем:
- Первый раз: (λgh.h (g f)) (λu.x) = λh.h ((λu.x) f) = λh.h x = λh.h (0 f x) (по определению нуля)
- Второй раз: (λgh.h (g f)) (λh.h x) = λh.h ((λh.h x) f) = λh.h (f x) = λh.h (1 f x) (здесь нужно понимать, что h внутри скобок и h внешняя — разные переменные)
- Третий раз: (λgh.h (g f)) (λh.h (f x)) = λh.h ((λh.h (f x)) f) = λh.h (f (f x)) = λh.h (2 f x)
Итак, мы видим, что после n применений, наше выражение имеет вид:
dec n = λfx.(λh.h ((n-1) f x)) ((λu.u)) = λfx.(λu.u) ((n-1) f x) = λfx.(n-1) f x = (n-1)
Профит!
Но что функция вернет в случае нуля?
dec 0 = λfx.(λu.x) (λu.u) = λfx.x = 0
Замечу, что 0 и false в наших определениях совпадают.
Теперь несложно написать и вычитание:
sub = λmn.(n dec) m
Комбинаторы
Комбина́торы — это λ-функции, не содержащие свободных переменных, т.е. любая переменная в них связана λ-абстракцией.
Примеры не комбинаторов:
- λx.y
- λxyz.y (z t)
Примеры комбинаторов:
- I = λx.x — функция, возвращающая свой аргумент
- K = λxy.x — генератор констант
- S = λxyz.(x z) (y z)
- Y = λf.(λx.f (x x)) (λx.f (x x)) — теперь Вы знаете, почему он назывался комбинатором
- B = λxyz.x (y z)
- C = λxyz.x z y
- W = λxy.x y y
И еще один интересный факт: возможно выбрать конечный набор комбинаторов, через которые можно выразить любую другую λ-функцию! Такими наборами являются, например, SKI и BCKW.
Unlambda
Unlambda — чистый функциональный язык программирования, использующий комбинаторную логику. А именно, для создания функций в нем используется набор SKI. Применение функции F к функции G записывается как `FG, что избавляет нас от ненужных скобок. Применение нескольких аргументов подряд: ```fxyz. Помимо встроенных функций s, k, i в языке имеется возможность вывода на экран (.x обозначает функцию, аналогичную i, но в качестве побочного эффекта выводящую символ x на экран), а также механизмы для ввода и отложенных вычислений, но о них здесь речи идти не будет.
Давным-давно, в далекой-далекой галактике, я нашел некий туториал по unlambda, который заканчивался примерно такими словами:
Сейчас я хотел объяснить, как в этом языке можно написать цикл, вычисляющий числа Фибоначчи, но уже тут я бессилен:
```s``s``sii`ki
`k.*``s``s`ks
``s`k`s`ks``s``s`ks``s`k`s`kr``s`k`sikk
`k``s`ksk
Что ж, давайте попробуем.
К слову, программа выводит число Фибоначчи в виде соответствующего числа звездочек на экране.
Опишем цикл:
- Выводим N звездочек
- Выводим перевод на новую строку (в ublambda это делает функция r)
- Складываем N с запомненным предыдущим числом Фибоначчи
Пока всё будем записывать в стиле (уже) привычного нам λ-исчисления.
Вывести N звездочек: N print i — N раз применим print к тождественной функции, заодно выведем N звездочек. В итоге мы получим тождественную функцию. Давайте её к чему-нибудь применим! ((N print i) newline) (cycle (+ N M) N), где M — предыдущее число Фибоначчи. Итак, получилась такая функция одного прохода цикла:
cycle = λcnm.((n print i) newline) (c (+ n m) n)
передадим циклу самого себя в качестве параметра, и инициализируем его единичкой и нулем:
fib = cycle cycle 1 0
Осталось, как я и обещал, перевести это на unlambda. Ох.
Неплохо бы познакомить читателя с алгоритмом перевода выражений из λ-исчисления в набор SKI (что, кстати говоря, и показывает, что через SKI можно выразить любую функцию). Итак, сам алгоритм:
- λx.F, где F не зависит от x — нам нужна константная функция со значением F, значит, это K F
- λx.x — это I по определению
- λx.F G, где F и G — выражения, (возможно) свободно содержащие x. Нам нужно подставить значение x в оба выражения, а затем применить первое ко второму. Этим занимается комбинатор S: S F G
Всё более-менее очевидно, кроме последнего. Посмотрим на определение комбинатора S:
S = λxyz.(x z) (y z)
Применим его к F, потом к G:
S F G = (λyz.(F z) (y z)) G = λz.(F z) (G z)
Действительно, это то, что нам нужно.
Алгоритм перевода λx.F сводится к таким действиям:
- ` заменить на ``s
- x заменить на i
- G, не зависящее от x, заменить на `kG
Теперь переведем на unlambda необходимые нам «кирпичики»:
0 = `ki
1 = i
add:
``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`k
s``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`
ks``s``s`ks``s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk
`kk``s``s`ks``s`kk`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``
s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks`
`s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk
``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`k
k`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`kk``s`
kki
cycle:
``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`k
s``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`
ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk
`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`k
k`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`kk`ki`
`s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`kk``s`kk`k.*
``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`kk``s`kk`k
i``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`kk``s`kk`
kr``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk
`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`k
k`ks``s``s`ks``s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`
kk`ks``s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s
`kk`ks``s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``
s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks`
`s`kk`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk
`kk``s`kki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`
kk`ki
И готовая программа:
````
``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`k
s``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`
ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk
`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`k
k`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`kk`ki`
`s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`kk``s`kk`k.*
``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`kk``s`kk`k
i``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`kk``s`kk`
kr``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk
`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`k
k`ks``s``s`ks``s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`
kk`ks``s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s
`kk`ks``s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``
s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks`
`s`kk`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk
`kk``s`kki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`kk`ki
``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`k
s``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`
ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk
`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`k
k`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`kk`ki`
`s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`kk``s`kk`k.*
``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`kk``s`kk`k
i``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`kk``s`kk`
kr``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk
`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`k
k`ks``s``s`ks``s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`
kk`ks``s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s
`kk`ks``s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``
s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks`
`s`kk`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk
`kk``s`kki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`kk`ki
``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`k
s``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`
ks``s``s`ks``s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk
`kk``s``s`ks``s`kk`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``
s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks`
`s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk
``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`k
k`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s`ks``s`kk`kk``s`kki
i`ki
Да, да, мне самому очень страшно. К слову, в сборнике программ на unlambda аналогичный код занимает не намного меньше места. Видимо, автор языка владеет секретными древними техниками чрезвычайно компактного и оптимизированного перевода из λ-исчисления в unlambda. Тем не менее, обещание я сдержал. Спасибо тем, кто дочитал до конца.
Автор: lisyarus
