iportnov.ru

pyLambda - это интерпретатор языка, основанного на нетипизированном λ-исчислении.

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

ОПИСАНИЕ ЯЗЫКА

Язык состоит из следующих «частей»:

Собственно λ-термы. λ-выражение записывается как λx.f(x) или как \x.f(x) (символы λ и \ взаимозаменяемы). Функцию многих переменных можно записывать как λx y.f x y. Применение (аппликация) записывается через пробел, например f x. Пробел обязателен. Имена переменных могут состоять из букв английского алфавита, цифр и некоторых спецсимволов.

Остальные части являются расширениями λ-исчисления:

Целочисленные константы. Они не выражаются автоматически через нумералы Чёрча или какую-либо другую абстракцию.

Арифметические выражения, такие как 2*x+3, 4+9. Интерпретатор производит только простейшие арифметические вычисления, например, 1+2*3 будет вычислено в 1+6. Никаких упрощений не производится.

Арифметические операции в некоторых случаях применимы и к λ-выражениям, например, 3+λx.3*x будет вычислено в λx.3+3*x.

Специальная операция возведения функции в степень. Если f - это λ-выражение, а n - целочисленная константа, то f!n = f (f!(n-1)), причем f!0 = λx.x. Эту операцию можно использовать, например, для введения нумералов Чёрча.

Присваивания, или, точнее, связывания переменных. Записываются как x = F. Присваивание не может быть частью выражения. Если переменной не было ничего присвоено, то ее значение - она сама. Определяемая переменная может встречаться и справа от знака присваивания, таким образом можно писать простейшие рекурсивные определения. Однако таким образом легко по ошибке написать бесконечно вычисляющееся определение, поэтому в таких случаях интерпретатор выдает предупреждение. Переменные можно переопределять.

Выражения с запятой, например так: 7*x, x=2. Справа от запятой должно быть присваивание. При этом сначала выполняется присваивание, а затем вычисляется значение выражения.

Кроме того, интерпретатор понимает несколько специальных команд (они должны быть записаны в отдельной строке):

exit (или, что то же самое, конец входного файла или Ctrl-D) - выход;

vars - показать все текущие определения переменных;

save - сохранить текущие определения в файл ~/.config/pylambda.vars;

load - загрузить определения из этого файла.

Вычисление выражения происходит в два этапа. На первом совершаются все возможные β-редукции (с предварительной α-конверсией) и η-редукци, в нормальном, или «ленивом» порядке, то есть слева направо. При этом не делается попытки привести выражение к нормальной форме, во-первых потому, что это могло бы привести к зацикливанию, во-вторых с тем, чтобы можно было проследить все стадии вычисления. На втором этапе вместо имен переменных подставляются их значения и производятся арифметические операции. На втором этапе возможно зацикливание из-за бесконечно рекурсивных определений. Прервать вычисление можно нажатием Ctrl-C.

Специальная переменная % ссылается на результат предыдущего вычисления. Таким образом, не до конца вычисленное выражение можно заставить вычисляться дальше, просто введя %. Однако это обычная переменная, правило ленивости применимо и к ней, поэтому с присваиваниями вроде z=% следует быть очень осторожным.

Переменные не имеют типов (реализовано бестиповое λ-исчисление). Выражения же имеют тип, то есть могут быть нескольких разновидностей. Именно, тип выражения может быть:

Expr - выражение, подлежащее вычислению;

Lambda - λ-выражение, которое можно к чему-нибудь применить;

UnboundVar - переменная, с которой не связано значение;

Const - целочисленная константа

Assignment - присваивание.

Интерпретатор показывает тип вычисленного выражения (через ::) в основном для того, чтобы можно было сориентироваться, что из себя представляет длинное выражение.

БАГИ

На этапе α-конверсии существует неотловленный баг, приводящий к тому, что в некоторых сложных выражениях подтерм λx.λy.x превращается в λx.λy.x'. Если кому-нибудь удастся хотя бы выявить точные условия проявления бага, а еще лучше - исправить его, буду очень благода ;)

ЛИЦЕНЗИЯ

GNU GPL v3 or any later.