Исправление quasimoto, (текущая версия) :
Термы языка образую простое множество порождённое грамматикой по индукции, а чистые редукции — просто определённое отношение на этом множестве (см. «The Lambda Calculus, Its Syntax and Semantics»).
Нужен какой-то вычислитель или абстрактная машина которая будет производить эти редукции и кодировать эти термы? Например, TAPL после того как вводит понятие отношения редукции поясняет так:
Оно записывается в виде t -> t' и читается «t за один шаг вычисляется в t'». Интуитивно ясно, что если в какой-то момент абстрактная машина находится в состоянии t, то она может произвести шаг вычисления и перейти в состояние t'.
Ещё см. «Abstract Computing Machines: A Lambda Calculus Perspective».
Исходная версия quasimoto, :
Термы языка образую простое множество порождённое грамматикой по индукции, а чистые редукции — просто определённое отношение на этом множестве (http://www.amazon.com/Lambda-Calculus-Studies-Foundations-Mathematics/dp/0444...).
Нужен какой-то вычислитель или абстрактная машина которая будет производить эти редукции и кодировать эти термы? Например, TAPL после того как вводит понятие отношения редукции поясняет так:
Оно записывается в виде t -> t' и читается «t за один шаг вычисляется в t'». Интуитивно ясно, что если в какой-то момент абстрактная машина находится в состоянии t, то она может произвести шаг вычисления и перейти в состояние t'.
Ещё — http://www.amazon.com/Abstract-Computing-Machines-Perspective-Theoretical-ebo....