Error: Incorrect password!
Шпаргалка по λ-исчислению (теория) — codedot — Сохраненная запись в кэше | Ljrate.ru
2012/03/26 14:50:32
История λ-исчисления уходит в начало прошлого века. Этимология названия данного раздела математической логики, который служит основой для «computer science», следующая. Сам значек «λ» используется для одной из двух основных конструкций в созданной Черчем системе — абстракции. Оказывается, что выбор обозначения абстракции не был совершенно случайным, а сделан в противопоставление другой более ранней конструкции, которую использовали Whitehead и Russell и обозначали как «xˆ». Для новой конструкции, чтобы отличать ее от прежней, Черч сначала заменил обозначение сначала на «∧x», а затем — на «λx», очевидно, интерпретировав первый символ как заглавную букву «Λ», для упрощения набора.

Опишем кратко систему λβη, то есть классическое бестиповое экстенсиональное λ-исчисление, вывернув наизнанку монографию Барендрегта.

Множество λ-выражений Λ строится индуктивно из переменных

x, y, z… ∈ Λ

с помощью абстракций

M ∈ Λ ⇒ λx.M ∈ Λ

и аппликаций

M, N ∈ Λ ⇒ M N ∈ Λ,

при этом аппликация лево-ассоциативна:

(M) ≣ M, M N P ≣ (M N) P.

Рефлективное транзитивное отношение Μ ⊂ N означает, что M является подвыражением выражения N:

M ⊂ M ⊂ λx.M;
M ⊂ M N ⊃ N;
M ⊂ N ∧ N ⊂ P ⇒ M ⊂ P.

FV(M) — это множество свободных переменных в выражении M:

FV(x) ≣ {x};
FV(λx.M) ≣ FV(M) ∖ {x};
FV(M N) ≣ FV(M) ∪ FV(N).

Переменные, которые не являются свободными, называются связанными и могут быть заменены другой переменной (такое преобразование называют α-конверсией):

y ∉ FV(M) ⇒ λx.M ≣ λy.M[x := y], где M[x := N] — результат подстановки:

x[x := P] ≣ P;
y[x := P] ≣ y;
(λx.M)[x := P] ≣ λx.M;
(λy.M)[x := P] ≣ λy.M[x := P];
(M N)[x := P] ≣ M[x := P] N[x := P].

В четвертом пункте не нужно специально оговаривать условие «x ≢ y и y ∉ FV(P)», так как оно выполняется в силу соглашения о переменных: если в определенном математическом контексте встречаются термы M1,…, Mn, то подразумевается, что связанные переменные в них выбраны так, чтобы они были отличны от свободных переменных.

Если множество FV(M) пусто, то M называют комбинатором. Множество всех комбинаторов обозначают Λ0:

Λ0 ≣ {M ∈ Λ | FV(M) = ∅}.

Следующие отношения β, η и βη являются редукциями:

β ≣ {((λx.M) N, M[x := N]) | M, N ∈ Λ};
η ≣ {(λx.M x, M) | M ∈ Λ, x ∉ FV(M)};
βη ≣ β ∪ η.

Выражение, подвыражением которого является дырка, называется контекстом и обозначается C[ ], при этом C[M] — результат подстановки выражения M вместо дырки в контексте C[ ].

Если σ — редукция, то выражение M — σ-редекс, если ∃N: (M, N) ∈ σ. Токже можно говорить и о σ-конверсии «=σ»:

(M, N) ∈ σ ⇒ C[Μ] →σ C[N];
M →σ N ∧ N →σ P ⇒ M ↠σ P;
M ↠σ M;
∃P: M ↠σ P ∧ N ↠σ P ⇒ M =σ N.

σ-нормальной формой называют выражение Μ, если ∄Ν: M →σ Ν. В экстенсиональном λ-исчислении под редексом имеют в виду βη-редекс, а под нормальной формой — βη-нормальную форму. Говорят, что M имеет нормальную форму N, если M ↠ N. При этом βη-конверсию обычно обозначают просто «=», и это неслучайно: формально система λβη является эквациональной теорией. Так как такие теории свободны от логики, непротиворечивость в них определяется несколько иначе.

Равенством будем считать формулу вида M = N, где M, N — λ-выражения; такое равенство замкнуто, если M и N — комбинаторы. Пусть T — формальная теория, формулами которой являются равенства. Тогда говорят, что T непротиворечива (и пишут Con(T)), если в T доказуемо не любое замкнутое равенство. В противном случае говорят, что T противоречива. Одна из причин рассмотрения λβη состоит в том, что эта теория обладает определенным свойством полноты. Эквациональная теория T называется полной по Гильберту-Посту (сокращенно HP-полной), если для любого равенства M = N в языке теории T или M = N доказуемо, или T + (M = N) противоречива. HP-полные теории соответствуют максимальным непротиворечивым теориям в теории моделей для логики первого порядка.

Стратегия — это такое отображение F: Λ → Λ, что ∀M: M ↠ F(M). Для одношаговой стратегии выполняется ∀M: M → F(M). Стратегия называется нормализующей, если для любого выражения M, имеющего нормальную форму N, для некоторого числа n выполняется Fn(M) ≣ N. Левая редукция Fl — одна из самых простых одношаговых нормализующих стратегий: она заключается в выборе редекса, значек «λ» в котором стоит текстуально левее, чем у других редексов. Таким образом, если два терма имеют общую нормальную форму, то с помощью левой редукции доказательство соответствующей формулы можно получить за конечное число простых шагов. Если же формула недоказуема, то либо процесс не завершается вовсе, либо он завершается на разных нормальных формах.
100 посетителей, 12 комментариев, 3 ссылки, за 24 часа