Кривошипная машина
-
Определение и применение машины Кривина
- Машина Кривина — это абстрактная машина для вычисления нормальных форм в лямбда-исчислении.
- Она была разработана для решения проблемы сокращения терминов в нормальной форме головы.
-
Процесс сокращения
- Сокращение нормальной формы головы начинается с термина и заканчивается в нормальной форме головы.
- Сокращение включает в себя вызов по имени, который уменьшает объем приложения.
-
Описание машины Кривина
- Машина основана на лямбда-термах с индексами де Брейна и предполагает, что термины являются замкнутыми.
- Она изменяет состояние до тех пор, пока не сможет сделать это, и в этом случае она получает нормальную форму головы.
-
Состояние машины
- Состояние состоит из трех компонентов: термина, стека и окружающей среды.
- Стек и среда представляют собой списки пар <термин, окружающая среда>, называемых замыканиями.
-
Правила работы машины
- Машина имеет четыре перехода: App, Abs, Zero, Succ.
- Каждый переход соответствует определенному действию, например, удалению параметра приложения или удалению λ из термина.
-
Примеры работы машины
- Приведены примеры оценки членов лямбда-исчисления с использованием машины Кривина.
-
Взаимосвязи с другими теориями
- Машина Кривина функционально соответствует метоциклическому вычислителю и математическому анализу.
- Она также синтаксически соответствует λ
- ρ
- ^
- {\displaystyle \lambda {\widehat {\rho }}}
- Вычислениям явных подстановок и абстрактной машине ZINC Ксавье Леруа.
Полный текст статьи: