Заметки на полях

λ-исчисление и комбинаторы

Внимание! Математика!

λ-исчисление (ака Лямбда-исчисление, ака ЛИ) — это формальная система в математической логике для описания вычислений с помощью абстракции и аппликации функций, использующая связывание переменных и подстановку.

Зачем оно?

Эта система была разработана американским математиком Алонзо Чёрчем для формализации и анализа понятия вычислимости. Т.е. определения может ли некоторая логика быть вычислена и какой результат у этих вычислений.

Немного истории

Алонзо Чёрч разработал лямбда-исчисление в 1930х годах, когда только появлялись первые компьютеры. Но основы этого были заложены немецким математиком Шейнфинкелем в его трудах по комбинаторной логике - откуда были использованы определения базовых комбинаторов, которые будут рассмотрены ниже. Помимо Чёрча и Шейнфинкеля в ЛИ сделали вклад и другие великие математики, как то: X.Карри, А.Тьюринг, К. Гёдель, Р. Петер и другие. Чёрч и Тьюринг в конечном итоге в своих исследованиях пришли к одному и тому же, но каждый со своей системы. И - любое валидное лямбда-выражение может быть переложена на машину Тьюринга и наоборот.

Понятия и правила

Комбинаторы

Что такое комбинатор? Комбинатор - это функция, которая не содержит “свободных” переменных.

Причём здесь птицы?

Ещё немного истории

Математик Шейнфинкель дал названия комбинаторам. Позже его труд о комбинаторной логике был переведён немецким математиком Генрихом Беманом и был предоставлен миру. Когда математик Х. Карри изучал переведённый вариант, он выделил комбинаторы по первым буквам для упрощения работы с ними. Затем другой американский математик Р. Смаллиан использовал названия комбинаторов в своей книге “To Mock a Mockingbird” и “закрепил” за каждым из комбинаторов название птицы, выражая некоторую метафору.

I - idiot

λx.x

const I = x => x

I - identity

M - mockingbird

λf.ff

const M = f => f(f)

M(I) == I(I) == I

Подумайте чему будет равно M(M)

MM - Ω-комбинатор. М - также называют ω

K - kestrel

λab.a

const K = a => b => a

Примеры

K(M)(I) == M
K(I)(M) == I
K(I)(x)(y) == y

В Haskell K реализован как const. Почему K, а не C? Потому что в эту штуку придумал немецкий математик Schönfinkel и назвал это Konstante Funktion

KI - kite

λab.b

const KI = a => b => b

KI также можно выразить через предыдущие комбинаторы

K(I)(a)(b) === KI(a)(b)
KI === K(I)

C - cardinal

λfab.fba

const C = f => a => b => f(b)(a)

B - bluebird

λfga.f(ga)

const B = f => g => a => f(g(a))

B - комбинатор является ничем иным как композицией.

S - starling

λfgx.fx(gx)

const S = f => g => x => f(x)(g(x))

T - thrush

λaf.fa

const T = a => f => f(a)

V - vireo

λabf.fab

const V = a => b => f => f(a)(b)

B1 - blackbird

λfgab.f(gab)

const B1 = f => g => a => b => f(g(a)(b))

Табличка комбинаторов

Символ Птица λ-запись Смысл
I Idiot λa.a Идентичность
M Mockingbird λf.ff Самоприменение
K Kestrel λab.a Первый, константа
KI Kite λab.b = K(I) = C(K) Второй
C Cardinal λfab.fba Обратный порядок
аргументов
B Bluebird λfga.f(ga) Композиция
S Starlink λfgx.fx(gx) Коннектор
T Thrush λaf.fa = C(I) “Подать” аргумент
к функции
V Vireo λabf.fab = B(C)(T) “Связать” два аргумента
B1 Blackbird λfgab.f(gab) Композиция композиций

Boolean as functions

Для чего используется boolean ? Для ветвления логики. В конечном итоге любое ветвление логики сводится к

const result = some_boolean ? true_branch_expr : false_branch_expr

Но у нас нет в распоряжении ? или : - у нас есть только функции. То есть нужно найти, что-то похожее на:

const result = some_function true_branch_expr false_branch_expr

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

True | False

Какая функция из известных нам принимает два аргумента по-одному и возвращает первый? Это K:

K(true_branch_expr)(false_branch_expr) == true_branch_expr

const True = x => y => x 
// или 
const True = x => y => K(x)(y)

А что насчёт false_branch_expr ? Какая функция из известных нам принимает два аргумента по-одному и возвращает второй? Это KI:

KI(true_branch_expr)(false_branch_expr) == false_branch_expr

const False = x => y => y
// или
const False = x => y => KI(x)(y)

Итак, мы можем сказать, что: True == K и False == KI

Not (!)

Что есть отрицание? Функция (сюрприз-сюрприз), которая возвращает False (т.е. функцию KI), когда в качестве аргумента приходит True (K) и наоборот:

Not(True) == False 
Not(False) == True

То есть функция Not выбирает, что вернуть True или False, в зависимости от того, что приходит в качестве аргумента - прямо как наша исходная функция, только наоборот:

some_function true_branch_expr false_branch_expr => true_branch_expr
Not some_function true_branch_expr false_branch_expr => false_branch_expr

Тогда мы можем представить Not как:

const Not = p => p(False)(True)

Где p - может быть либо True/K либо False/KI

Not(True) == False
Not(False) == True
Not(True)(1)(2) == 2
Not(False)(1)(2) == 1

А теперь давайте посмотрим повнимательнее. Вот обычная boolean функция:

boolean_function(True)(False)

А вот логика Not функции:

boolean_function(False)(True)

По сути Not просто меняет True и False местами. Есть ли какая-то уже известная нам функция, которая делает то же самое?

Да - C- комбинатор

C(True)(1)(2) == 2
C(False)(1)(2) == 1

And

Что такое And ? Это функция, которая принимает два Boolean. Если хотя бы один из них False - тогда результат будет False. И только если оба аргумента будут True - результат будет True.

const And = p => q => p(q)(F)
// или
const And = p => q => p(q)(p)

где p, q - могут быть True или False. Почему мы можем использовать p(q)(p) вместо p(q)(F) ? Если первый аргумент (p) будет False - результатом And будет False, а как нам известно функция False возвращает второй аргумент. Но раз p == False - мы можем вернуть саму p. А если p == True - результат And будет зависеть от того, чем является q.

Проверим:

And(F)(T) == F
And(T)(F) == F
And(F)(F) == F
And(T)(T) == T

Or

Что такое Or ? Это функция, которая принимает два Boolean. Если оба из них False - тогда результат будет False. А если хотя бы один из аргументов True - результат будет True. По аналогии с And получаем:

const Or = p => q => p(T)(q)
// или
const Or = p => q => p(p)(q)

Проверим:

Or(F)(T) == T
Or(T)(F) == T
Or(T)(T) == T
Or(F)(F) == F

А если мы посмотрим внимательно на

const Or = p => q => p(p)(q)

То заметим, что это в точности тоже самое что M - комбинатор, с той лишь разницей что мы добавляем дополнительный аргумент.

Проверим:

M(F)(T) == T
M(T)(F) == T
M(T)(T) == T
M(F)(F) == F

Boolean Equal

Что такое Boolean Equal? Функция, принимающая два boolean аргумента и возвращающая True если оба аргумента True или оба аргумента False.

const Beq = p => q => p(q)(Not(q))  

Beq(F)(T) == F
Beq(T)(F) == F
Beq(T)(T) == T
Beq(F)(F) == T

Сможете реализовать функцию Xor - исключающее или ?

Имея в распоряжении написанные нами функции мы можем доказать “Законы де Моргана”:

const MorganLaw = p => q => Beq(Not(And(p)(q)))(Or(Not(p))(Not(q)))

MorganLaw(T)(T) == T
MorganLaw(T)(F) == T
MorganLaw(F)(T) == T
MorganLaw(F)(F) == T

Табличка boolean

Имя λ-запись Смысл
True λab.a = K Истина
False λab.b = KI Ложь
And λab.aba Логическое “И”
Or λab.aab = M* Логическое “ИЛИ”
Not λa.aKIK = C* Отрицание
Beq λab.ab(Cb) Логическое “равно”

Pair

Многим известна такая структура данных как Pair - т.е. пара значений. И для Pair существуют как минимум две функции - для получения первого и второго элемента: First и Second.

const Pair = x => y => f => f(x)(y)

Pair то же самое что и V-комбинатор

First

First должна принимать в качестве аргумента Pair и возвращать её первый аргумент. Учитывая, что Pair = x => y => f(x)(y) и f должна выбирать между двумя опциями и возвращать первый - какая функция так делает? Это функция K она же True.

const fst = p => p(K)

Second

Не трудно догадаться, что для Second такой функцией будет KI или False

const snd = p => p(KI)

fst(Pair(1)(2)) == 1
snd(Pair(1)(2)) == 2

Phi

Phi здесь является функцией для генерирования следующей Pair со “сдвигом” значений. Для этого нам понадобится функция succ, которую мы рассмотрим чуть ниже. Суть её в том, что она генерирует следующий элемент.

const phi = p => Pair(snd(p))(succ(snd(p)))

// в данном случае первым аргументом Pair может быть всё что угодно
next_pair = phi(Pair(I)(n1)) // == Pair(n1)(n2) 
fst(next_pair)(x=>x+1)(0) == 1
snd(next_pair)(x=>x+1)(0) == 2

На самом деле всё не ограничивается только парой элементов: можно создать и функцию “несущую” в себе три, четыре и сколь угодно большое их количество. И в конечном итоге получить связный список с функциями доступа до элементов head - эквивалентный First, возвращающий первый или головной элемент и tail - эквивалентный Second, возвращающий всё остальное.

Табличка Pair

Имя λ-запись Смысл
Pair λabf.fab = V Пара
fst λp.pK Первое значение
snd λp.pKI Второе значение
phi λp.Pair(snd p)(succ(snd p)) “Сдвиг” значений в паре

Zero, One, Two, Three…

Ок - мы реализовали Boolean логику при помощи только лишь функций без операторов и без типов, а так же Pair. А как вы думаете: можно ли реализовать примитивную числовую арифметику при помощи только лишь функций? Давайте попробуем.

Для начала нам нужны … “числа”. И числа эти будут функциями.

Что такое 1 ? Подойдём к этому не как к конкретному числу, а представим его в качестве однократного применения функции к некоторому аргументу:

const n1 = f => a => f(a)

n1(Not)(True) == False
n1(I)(2) == 2

Тогда: что такое 2 ? Двукратное применение функции:

const n2 = f => a => f(f(a))

n2(Not)(True) == True

Что такое 3 ? Трёхкратное применение функции:

const n3 = f => a => f(f(f(a)))

Последовательность прослеживается?

Вопрос: что в такой системе 0 ?

n0 = f => a => ?
n1 = f => a => f(a)
n2 = f => a => f(f(a))
n3 = f => a => f(f(f(a)))
//... и так далее

Если n2 - применение функции дважды, n1 - применение функции единожды, то n0 - применение функции ноль раз. Т.е. просто:

const n0 = f => a => a

n0, n1, n2 …. - называются “Числами Чёрча”.

И забавный факт, что n0 по сути является тем же самым что и False и KI.

Алгебра

И так мы можем вручную сделать сколь угодно много “чисел”, но это всё же просто числа - у нас нет для них алгебры.

Чтобы хотелось от алгебры? Как минимум получать следующий элемент

succ

const succ = n => f => a => f(n(f)(a))

где n - “количество” применений функции f к аргументу a. Результат n(f)(a) передаётся аргументом в f для получения “следующего значения”.

succ(n0)(x=>x+1)(0) == n1(x=>x+1)(0) == 1
succ(n1)(x=>x+1)(0) == n2(x=>x+1)(0) == 2
succ(n2)(x=>x+1)(0) == n3(x=>x+1)(0) == 3
// и тд

is0

Проверка на ноль. Фнкция должна выдавать True только в случае если аргумент ноль (n0), в остальных случаях - False

const is0 = n => n(K(False))(True)

is0(n0) == True
is0(n1) == False
is0(n2) == False
// и т.д.

Add

Попробуем реализовать сложение. Мы можем заметить, что succ является ничем иным как add n1 к некоторому n:

Add(n1)(n2) == succ(n2)
// и далее 
Add(n2)(n2) == succ(succ(n2))
// и т.д.

Тогда add будет выглядеть в общем случае следующем образом:

const Add = n => k => n(succ)(k)

Т.е. мы n раз применяем функцию succ к k.

Add(n2)(n1)(x=>x+1)(0) == succ(n2)(x=>x+1)(0) == 3
Add(n2)(n2)(x=>x+1)(0) == succ(n3)(x=>x+1)(0) == 4

Mult

Едем дальше: умножение. Что такое умножение? Что значит умножить 2 на 3 в нашей системе? Это значит применить функцию к аргументу дважды по три:

mult(n2)(n3)(f)(a) == n2(n3(f))(a)
// можем убрать 'a' и получим
mult(n2)(n3)(f) == n2(n3(f))
// что в общем виде является
mult = n => k => f => n(k(f))

Возможно ли это выражение превратить во что-то уже знакомое нам? Обратите внимание, что n(k(f)) является композицией. И поэтому мы можем вспомнить про B-комбинатор и переписать выражение так:

mult = n => k => f => B(n)(k)(f)

и здесь можно заметить, что n, k, f - и в левой и в правой чисти и в той же последовательности:

mult(n)(k)(f) == B(n)(k)(f)
// И здесь получается, что ...
mult == B

т.е. умножение является просто композицией.

mult(n0)(n0)(x=> x + 1)(0) == 0
mult(n0)(n1)(x=> x + 1)(0) == 0
mult(n1)(n1)(x=> x + 1)(0) == 1
mult(n2)(n1)(x=> x + 1)(0) == 2
mult(n2)(n2)(x=> x + 1)(0) == 4
// ...

Pow

Возведение в степень Что есть возведение n в степень k ? Это перемножить n на себя k раз:

pow(n)(k) == n * n * n ... * n // и так k раз

Т.е. в случае с функциями нужно k раз сделать n применений функции к аргументу и вспоминаем, что умножение это композиция:

pow(n)(k)(f)(a) == k(n)(f)(a)
//  и после упрощения получаем ...
pow(n)(k) == k(n)

const pow = n => k => k(n)

pow(n0)(n1)(x=> x + 1)(0) == 0
pow(n1)(n0)(x=> x + 1)(0) == 1
pow(n1)(n1)(x=> x + 1)(0) == 1
pow(n1)(n2)(x=> x + 1)(0) == 1
pow(n2)(n1)(x=> x + 1)(0) == 2
pow(n2)(n2)(x=> x + 1)(0) == 4
// и тд...

Pred

Что насчёт вычитания? В Pair после применения n раз функции phi будет находиться n-1 и n значения. Таким образом мы можем реализовать эдакое “вычитание” единицы из n.

const pred = n => fst(n(phi)(pair(n0)(n0))) 

pred(n2)(x=>x+1)(0) == n1(x=>x+1)(0) == 1

Sub

По аналогии со сложением, вычитание из n k - применением k раз к n функции pred:

const sub = n => k => k(pred)(n)

sub(n4)(n2)(x=>x+1)(0) == n2(x=>x+1)(0) == 2

Leq

Меньше или равно.

const leq = n => k => is0(sub(n)(k))

Eq

Равно. Что значит что два элемента равны? Они равны если n меньше равно k и k меньше равно n.

const eq = n => k => And(leq(n)(k))(leq(k)(n))

Gt

Больше чем. n больше k, когда n НЕ меньше или равен k

const gt = n => k => not(leq(n)(k))

Таюличка операций над числами Чёрча

Имя λ-запись Смысл
succ λnfa.f(nfa) == λnf.Bf(nf) Следующий после n элемент
add λnk.n succ k == λknf.B(nf)(kf) Сложение n и k
mult λnkf.n(kf) == B Умножение n на k
pow λnk.kn == T Возведение n в степень k
is0 λn.n(K(False))True Является ли n нулём
pred λn.fst(n(phi)(V n0 n0)) Предыдущий перед n
sub λnk.k pred n == λknf.B(nf)(kf) Вычитание из n k
leq λnk.is0 (sub n k) Проверка n меньше или равно k
eq λnk.And(leq n k)(leq k n) Проверка n равно k
qt λnk.Not(leq n k) == B1 Not leq Проверка n больше k

Послесловие

Y-комбинатор

Или Fixed-point combinator λf.(λx.f(xx))(λx.f(xx)) Наиболее известный комбинатор, при помощи которого можно организовать рекурсию с использованием анонимных функций.

const Y = f => (x => f(x(x)))(x => f(x(x)))

Если мы попробуем c помощью js посчитать факториал от любого числа то получим ошибку Maximum call stack size exceeded

const factorial = f => x => (x === 0 ? 1 : x * f(x - 1))
Y(factorial)(1) 
// `Maximum call stack size exceeded`

Это происходит, потому что js адаптирован под жадную/строгую стратегию оценки выражений.

попробуйте реализовать Y-комбинатор на “более ленивом языке”

Z-комбинатор

λg.(λx.g(λv.xxv))(λx.g(λv.xxv)) Ещё один комбинатор для рекурсии

const Z = g => (x => g(v => x(x)(v)))(x => g(v => x(x)(v)))

И вот он уже подходит для жадных языков

factorial = f => x => (x === 0 ? 1 : x * f(x - 1))
Z(factorial)(170) 
// 7.257415615307994e+306

Сколько комбинаторов нужно?

В качестве базы выделяют три комбинатора: SKI:

Но I можно выразить с помощью S и K : I == SKK

И через них можно выразить остальные и вообще написать любое выражение. Например можно выразить C:

C == S(S(K(S(KS)K))S)(KK)

Другая базовая система B, C, K, W :

Обе эти системы взаимозаменяемы, т.е. одну систему можно выразить через другую.

Универсальный комбинатор ι (Iota, jot,Zot)

ι комбинатор был придуман Крисом Баркером в 2001 году.

ι == λf.((fS)K) == λf.((fλa.λb.λc.((ac(bc)))λd.λe.d)

Тогда SKI комбинаторы будут выглядеть так:

That’s all folks!

Автор заметки надеется, что в режиме “галопом по европам” выдал хотя бы поверхностное представление о том: что такое λ-исчисление.

Ссылочки

Книги

Видео

“A Flock of Functions: Lambda Calculus and Combinatory Logic in JavaScript | Gabriel Lebec” - материал откуда автор заметки в основном брал информацию для заметки.

Прочее

Нашли ошибку?