Кто такой Окасаки и за что его надо почитать?
2016, Окасаки Крис, Чисто функциональные структуры данных
1996, Chris Okasaki, Purely Functional Data Structures, 162 страницы
Википедия совсем другое пишет:
Денотационная семантика (англ. denotational semantics) выражениям в программе ставит в соответствие настоящие математические объекты, то есть, выражения обозначают (англ. to denote — откуда «денотационная») их величины)
Важнейшие, в том числе пионерские, результаты построения денотационных семантик получены в работах Д. Скотта (Dana Scott) и К. Страчей (Christopher Strachey) в конце 1960-х — начале 1970-х в Оксфордском университете
Бестиповое λ-исчисление
1557, Роберт Рекорд (Recorde Robert), The Whetstone of Witte, 332 страницы (Оксфордский университет)
ввёл знак (символ) для обозначения равенства = в 1557 году (в 16-м (XVI) веке).
«В континентальной Европе знак = был введён Лейбницем только на рубеже XVII—XVIII веков, то есть более чем через 100 лет после смерти Роберта Рекорда.»
1936, Алонзо Чёрч, An Unsolvable Problem of Elementary Number Theory (Принстонский университет)
представил безтиповое лямбда-исчисление в статье «Унифицированная теория формальных систем», опубликованной в апреле 1936 года в журнале American Journal of Mathematics.
Переменные: x, y, z, … являются λ-термами.
Абстракция: Если M λ-терм и x — переменная, то (λx.M) — λ-терм (называется абстракцией).
Аппликация: Если M и N λ-термы, то (M N) — λ-терм (называется аппликацией).
само по себе λ-исчисление — это лишь синтаксис, набор правил для работы с символами.
Чтобы оно «обрело смысл» или «семантику», нужно связать эти символы с чем-то осмысленным, например, с математическими объектами.
Смысл (семантика) в данном контексте означает, что каждый термин λ-исчисления будет интерпретироваться как некоторый математический объект, а операции над терминами будут соответствовать операциям над этими объектами.
Двоичное и десятичное
Можно определить функции:
- добавления единицы
- удвоения
- удесятирения
Числа можно записать не только как нумералы, но и как применение таких функций к нумералам, что позволяет говорить о двоичной и десятичной формах записи.
Аппликативный синтаксис
Аппликативный синтаксис эволюционировал из работ Шёнфинкеля, Карри и Чёрча. Функции обозначаются переменными или лямбда-абстракциями. Именование функций в аппликативном синтаксисе безтипового лямбда-исчисления осуществляется через присвоение переменным абстракций. Алонзо Чёрч (Alonzo Church), хотя и известен своей нотацией с лямбда-абстракцией и явными скобками, в некоторых своих работах также использовал более компактные формы записи, близкие к аппликативному синтаксису, особенно при работе с комбинаторами. Например, вместо того чтобы постоянно писать λx.x+1, он мог ввести сокращение f для этой функции, это записывалось в духе:
f≡λx.x+1
Таким образом, Чёрч ввёл операцию именования как связь между лямбда-выражением и символическим именем. Однако он ещё не привязал это к конкретному синтаксису, так как его работа была сосредоточена на чистой теории. Именование как операция — это идея Чёрча, использование для неё знака равенства закрепилось благодаря разработчикам функциональных языков, создатель MetaLanguage (ML) - Робин Милнер (1970-е годы).
Лямбда-абстракция (определение анонимной функции) записывается как λx.t, где x — аргумент, а t — тело функции.
Определим переменную f и присвоим ей лямбда-выражение (имеющее в безтиповом λ-исчислении единственный возможный для переменных тип «функция») в качестве значения, например функцию, которая возвращает переданный аргумент:
f=(λx.x)
f=λx.x
Теперь мы можем использовать переменную f в выражениях. Применим f к другому лямбда-выражению, например, (λy.y):
((λx.x) (λy.y))
((f) (λy.y))
В аппликативном синтаксисе приложение функции f к аргументу x записывается как
f λy.y
без скобок, a применение функции g к двум аргументам w и z — как
g w z
Бесскобочность достигается за счёт соглашения о левоассоциативности (см. также Каррирование). Выражение g w z интерпретируется как (g w) z, то есть сначала g применяется к w, а затем результат применяется к z.
Семантика
Теоретико-множественный подход
Категорный подход
В λ-исчислении любая функция может быть применена к самой себе. Это ключевая особенность, которая позволяет выражать рекурсию и другие сложные вычислительные конструкции.
нужно:
- Определить множество D, элементы которого будут значениями λ-выражений
Без такого множества D мы не можем корректно описать, что означают выражения λ-исчисления. Мы не можем сказать, какие у них значения. А без возможности приписать выражениям значения нельзя говорить об их смысле. Без подходящего D мы не можем задать интерпретацию термов и операций λ-исчисления. - Интерпретировать функции как элементы этого множества
(D должно содержать все функции из D в D, то есть D должно содержать множество всех функций D → D)
построение такого множества D - нетривиальная математическая задача (из-за парадокса Кантора). Ее решение привело к развитию теории доменов и других разделов математики.
идея фиксированной точки, когда D строится как фиксированное множество, удовлетворяющее
D≅D→D
И вот в этом месте я не осилил. Разъясните, бегом пожалуйста, люди злые добрые.
Как мне этим вашим лямбда-исчислением описать байт, его значения, и операции с ним? Нумералы Чёрча (функции с двумя параметрами) я могу написать, но дальше дело не идёт.
