Лямбда-мю-исчисление

В математической логике и информатике лямбда -мю-исчисление является расширением лямбда-исчисления, введенного Мишелем Париго. Он вводит два новых оператора: оператор µ (который полностью отличается как от оператора µ, найденного в теории вычислимости , так и от оператора µ модального µ-исчисления ) и оператора скобки. С точки зрения теории доказательства это обеспечивает правильную формулировку классической естественной дедукции .

Одна из основных целей этого расширенного исчисления — дать возможность описывать выражения, соответствующие теоремам классической логики . Согласно изоморфизму Карри-Говарда , лямбда-исчисление само по себе может выражать теоремы только в интуиционистской логике , а некоторые классические логические теоремы вообще не могут быть написаны. Однако с помощью этих новых операторов можно писать термины типа, например, закона Пирса .

Семантически эти операторы соответствуют продолжениям , встречающимся в некоторых функциональных языках программирования .

Формальное определение

Мы можем расширить определение лямбда-выражения, чтобы получить его в контексте лямбда-мю-исчисления. Три основных выражения, встречающихся в лямбда-исчислении, следующие:

1. V — переменная , где V — любой идентификатор .
2. λVE.E — абстракция , где V — любой идентификатор, а E — любое лямбда-выражение.
3. (EE') , приложение , где E и E' ; любые лямбда-выражения.

Подробности смотрите в соответствующей статье .

В дополнение к традиционным λ-переменным лямбда-мю-исчисление включает в себя отдельный набор μ-переменных. Эти μ-переменные можно использовать для именования или фиксации произвольных подтерминов, что позволяет нам позже абстрагироваться от этих имен. Набор термов содержит безымянные (к таким относятся все традиционные лямбда-выражения) и именованные термы. Члены, добавляемые в результате лямбда-мю-исчисления, имеют вид:

1. [α]t — именованный терм, где α — µ-переменная, а t — безымянный терм.
2. (μ α. E) — безымянный терм, где α — µ-переменная, а E — именованный терм.

Сокращение

Основные правила редукции, используемые в лямбда-мю-исчислении, следующие:

логическое сокращение

$(\lambda x.u)v\;\triangleright _{c}\;u[v/x]$

структурное сокращение

$(\mu \beta .u)v\;\triangleright _{c}\;\mu \beta .u\left[[\beta ](wv)/[\beta ]w\right]$, где замены должны быть сделаны для всех подчленов $u$ формы $[\beta ]w$.

переименование

$[\alpha ]\mu \beta .u\;\triangleright _{c}\;u[\alpha /\beta ]$

эквивалент η-редукции

$\mu \alpha .[\alpha ]u\;\triangleright _{c}\;u$, для α, не встречающегося свободно в u

Эти правила приводят к тому, что исчисление становится сливным . Можно было бы добавить дополнительные правила редукции, чтобы дать нам более четкое представление о нормальной форме, хотя это будет происходить за счет слияния.

См. также

• Классические системы чистых типов для типизированных обобщений лямбда-исчислений с управлением

Внешние ссылки

• Lambda-mu Соответствующее обсуждение Lambda the Ultimate.