Comments 16
Думаю, что тут уместен будет хаб Функциональное программирование.
Ээээ, если я правильно понял вот этот кусок кода
case reduce(m) { // Вычисляем функцию
Lambda(f) -> reduce(f(n)) // Бета-редукцияТо у вас внутри Lambda лежит не терм, а Rust-функция, которую вы достаёте и вызываете? Не, так не честно, это не настоящая бета-редукция, читерство какое-то. Самого главного в статье и нет.
Вы абсолютно правы, тут я немного схитрил). Статья является своего рода стартом для реализации других, более интересных исчислений, так что надеюсь это небольшое читерство не так страшно. В любом случае, спасибо за замечание!
Не, так не честно, это не настоящая бета-редукция, читерство какое-то.
Не читерство, а higher-order abstract syntax (потом можно обобщить до P(olymorphic)HOAS).
Охренительно удобная штука, на самом деле. Вам бесплатно (из метаязыка) даётся весь набор инструментов для работы с именами и байндингами, и, как следствие, отсутствие геморроя с представлением переменных (символы? de Bruijn? locally nameless? да это всё не нужно, фигачь на метаязыке!), бесплатная α-эквивалентность, процедура подстановки (это просто применение в метаязыке), и, если метаязык достаточно мощный (ну там, coq/agda/etc), то доказательства свойств вашего языка становятся сильно проще.
(P)HOAS — сила.
Как бы (страшно?) это не звучало
Если подразумевается что-то вроде макроподстановки текста, то это звучит нестрашно. Если что-то другое, то звучит не страшно, а непонятно.
заменив в нём каждое свободное вхождение переменной
Определения "свободное" не было. Что это?
Как мы помним - это применение функции M к аргументу N
Нет, мы никак не помним, потому скобочки и их значение не были введены ранее.
pub type Term { Variable(Int) // Переменная Lambda(fn(Term) -> Term) // Лямбда-функция Apply(Term, Term) // Применение}
Непонятно уже тут. То, что внутри Term, это выбор "или", или это список полей? Или ещё что-то? Далее, выше сказано, что "функция от переменной", а тут она от терма. Почему несоответствие? Аналогично с Apply.
Обратите внимание, что в конструкторе переменной указан тип Int.
Откуда мы знаем, что это конструктор? Тогда и остальные строчки - тоже конструкторы? И если это конструктор, то Variable - это тип или имя переменной? Ничего непонятно.
Далее с неба падают некие индексы и переименования переменых. Очень много недоговоренностей и умолчаний. В общем, дальше я не стал читать, потому что статья или понятна тому, кто и так в теме (тогда зачем её читать?), или непонятна остальным (тогда тоже лучше не читать, а найти другой источник).
В самом начале я сказал, что теорию объясню поверхностно и даже дал ссылку на статью, где все разжуют для тех, кто с исчислением не знаком. Тоже самое касается всех остальных ваших вопросов (например про скобки, которые проходят в начальной-средней школе на уроках математики).
Далее вы затронули интересный момент - язык, на котором пишется исчисление. Я думал, стоит ли тратить время на объяснение фишек языка gleam и пришел к выводу - нет, не стоит. Это все равно, что писать статью о создании компилятора и объяснять как в python создать переменную - абсолютно неуместно для данной темы. С языком вы можете ознакомится сами, он довольно популярный и интуитивный (возможно не для вас, потому что вы работаете с другими языками), но тратить время на его объяснение в данном статье идея так себе. Но я приму ваше замечание к сведению, и следующую статью постараюсь написать куда более простым языком. Спасибо!
Если я могу прочитать про теорию в другом месте, зачем мне эта статья?
Скобки в неком языке могут означать что угодно. Особенно, если после выражения без скобок написано такое же, но со скобок.
Ага, уже и с языком я должен сам познакомиться. Всё больше ускользает смысл этой статьи (и целой серии в будущем).
Я хочу не более простого языка, а более логичного, согласованного и по возможности строгого изложения, чтобы читатель с математическим образованием не испытывал муки недосказанности, замечания очевидных противоречий и прочего.
Далее, выше сказано, что "функция от переменной", а тут она от терма. Почему несоответствие?
Потому что это на самом деле одно и то же.
Переменная — это то, что видит тело функции. Вы пишете λx. x + 2, и вот эта вот штука справа от точки (то есть, тело функции) видит только переменную x.
Когда вы вызываете эту функцию, то передаёте вы ей полноценный терм, который подставляется на место этой переменной. Просто в данном случае за подстановку отвечает метаязык (мета- — потому, что это язык, на котором описывается язык), и в нём такие функции имеют тип Term → Term.
Ничего непонятно.
ХЗ, я gleam не знаю, но это достаточно распространённый синтаксис в языках, черпающих вдохновение в ML-семействе. При очень беглом взгляде я вообще подумал, что это раст (которого, впрочем, я тоже не знаю).
Переменная — это то, что видит тело функции.
Нет. Было сказано, что существуют 3 типа выражений/термов. То есть, существует вообще, а не один из трех - только внутри функции. И что значит Variable(Int)? Это та самая переменная или "это другое"? А ML-семейством я не занимался. Может, поэтому и нет его вдохновения.)
То есть, существует вообще
Нет смысла рассматривать существование «вообще». С подвешенным в вакууме термом x (одиноко стоящая переменная) ничего нельзя сделать, он неинтересен сам по себе.
а не один из трех - только внутри функции.
Формализация этих правил (с системами типов, отношением типизации, и так далее) раздует статью куда сильнее, и, ИМХО, оно того заслуживать не будет.
И что значит Variable(Int)?
ХЗ, в данной кодировке оно напрямую не нужно. Может, автору потом пригодится для его дальнейших замыслов, не знаю, я ж не автор. Пока оно ему нужно, только чтоб красиво печатать λ-термы.
А ML-семейством я не занимался. Может, поэтому и нет его вдохновения.)
Это, конечно, упущение!
Эта статья для меня выглядит так:
"Давайте я расскажу на пальцах, как работает память у Java, но только на китайском, он модный и очень удобный для этого, вот ссылка. Да, ну и почитайте перед этим спецификацию по работе с памятью в Java.
Не знаете, что такое вертикальная черта в китайском? Вы чего, в школе не учились? Это даже дети знают - она работает, как пайп в bash. "
Прекрасно. Спасибо большое.
А где хоть какие-нибудь тесты всего этого дела? Ни в статье примеров исполнения на произвольной лямбде, ни в тестах хоть каких-нибудь тестов, что оно действительно работает.
Спасибо, добавил тесты: https://github.com/k1ngmang/lambda-calculus/commit/bc3d7496f679936436c5fa6628c02a9177c004ce
Как то обычно бывает, нужен раздел с сопоставлениями с аналогами.
Предлагаю начать с такого: Лямбда-исчисление в 397 байтах. Тут автор не заботится о красивом представлении на метаязыке, зато размер поменьше будет.
λ-исчисление в 30 строк. Реализация лямбда-исчисления