Логика

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

Ну вы поняли

Основной синтаксический объект в l-исчислении это l-терм.

Алфавит для построения l -термов состоит из

· символа l, называемого l-абстрактором,

· счетного набора символов, называемых переменными,

· пары круглых скобок и точки.

В качестве переменных будем использовать малые латинские буквы, возможно с индексами.

Определение. Лямбда-термом называется

· выражение, состоящее из одной переменной,

· выражение вида (MN), называемое аппликацией, где M и N - l-термы,

· выражение вида (l x. N), называемое l-абстракцией, где N - l-терм, x - переменная.

В терме вида (l x. N) терм N называется областью действия l-абстрактора по переменной х. Вхождение переменной x в терм называется связанным, если оно находится в области действия l-абстрактора по этой переменной; в противном случае такое вхождение называется свободным в рассматриваемом терме.

FV (M) - это множество переменных, имеющих свободные вхождения в l-терм M.

Правила упрощения записи:

1) Внешние скобки опускаются

2) Скобки в записи аппликаций, если можно восстановить группировкой влево N1N2N3=((N1N2)N3)

3) l x ₁ x ₂ x ₃… x_n. M º (l x ₁.(l x ₂.(l x ₃ … (l x_n. M)…)))

M_x [ N ] - результат подстановки терма N в терм M вместо всех свободных в M вхождений переменной x.

Отношение a = {((l x. M), (l y. M_x [ y ]))| y Ï FV (M)} порождает отношение a-конверсии.

Отношение b = {((l x. M) N, M_x [ N ])| x Ï FV (N)} порождает одношаговую b-редукцию.

(l x. M) N - b-редекс.

Левым редексом называется редекс, символ l которого расположен левее символов l, соответствующих всем другим редексам. Аналогично определяется правый редекс.

Внутренним редексом называется редекс, не содержащий внутри себя других редексов.

Внешним редексом называется редекс, который не содержится внутри никакого другого редекса. Ясно, что самый левый редекс всегда является внешним. Однако не любой внешний редекс будет и самым левым.

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

Выражение P ®_b* Q означает, что терм P b-редуцируется к терму Q. Выражение P =_b Q означает, что термы P и Q взаимно b-конвертируемы.

Терм назовем b-нормальным (или b-пассивным) термом если в нем нет b-редексов. Терм Q назовем b-нормальной формой терма P, если Q – b-нормальный терми P =_b Q.

Пример. (l x. xx)(l x. xx) – не имеет b-нормальной формы.

Аппликативный порядок редукций предписывает всегда выбирать самый левый из внутренних редексов. Нормальный порядок редукций предписывает всегда выбирать самый левый из внешних редексов. (Гарантирует достижение бета-нормальной формы, если она существует)

Теорема Черча-Россера (о ромбическом св-ве бета-редукции)

Если терм Р может быть редуцирован к разным термам M и N, то существует терм Q, такой что M и N редуцируются в Q.

Следствие: Если бета-нормальная форма существует, то она единственна.

Комбинатором называется терм без свободных переменных.

Определение. Терм X называется неподвижной точкой терма F, если выполняется соотношение X =_b FX.

Теорема (о существовании неподвижной точки). (" F Î L)($ X Î L) (X =_b FX).

Действительно, в качестве X возьмем терм (l x. F (xx))(l x. F (xx)), где x Ï FV (F) и убедимся в том, что он конвертируется в FX. Действительно,

X º (l x. F (xx))(l x. F (xx)) =_b F ((l x. F (xx))(l x. F (xx))) º FX.

Определение. Комбинатор M называется комбинатором неподвижной точки, если для любого терма F выполняется соотношение MF =_b F (MF). Другими словами: применяя комбинатор M к произвольному терму F, получаем неподвижную точку терма F.

Теорема (о существовании комбинатора неподвижной точки). Одним из возможных комбинаторов неподвижной точки является так называемый парадоксальный комбинатор Карри

Y º l f. (l x. f (xx))(l x. f (xx)).

Действительно, для любого терма F имеем

Y F º (l f. (l x. F (xx))(l x. F (xx))) F =_b (l x. F (xx))(l x. F (xx))=

_b F ((l x. F (xx))(l x. F (xx)))=_b F ((l f. (l x. f (xx))(l x. f (xx))) F)º F (Y F).

Комбинатор неподв. точки Тьюринга: T º (l xy. y (xxy))(l xy. y (xxy)).

Докажем, что для любого терма F выполняется соотношение T F ®_b* F (T F). Рассмотрим терм A º (l xy. y (xxy)), тогда T º AA º (l xy. y (xxy)) (l xy. y (xxy)) ®_b*l y. y (AA y) º l y. y (T y) и, следовательно, T F ®_b* (l y. y (T y)) F ®_b* F (T F), что и требовалось.

Комбинатором называется терм без свободных переменных.

I º l x. x тождественный I X ®_b* X

B º l xyz. x (yz) композитор B XYZ ®_b* X (YZ)

C º l xyz. xzy пермутатор C XYZ ®_b* XZY

K º l xy. x канцелятор K XY ®_b* X

S º l xyz. xz (yz) коннектор S XYZ ®_b* XZ (YZ)

W º l xy. xyy дупликатор W XY ®_b* XYY

Арифметика.

Существует различные способы представления натуральных чисел и арифметических операций l-термами. Для представления чисел 0, 1, 2, …, n … будем использовать соответственно комбинаторы, называемые нумералами Черча, которые будем обозначать так же как и числа но полужирным шрифтом:

0 ≡ λ fx. x 1 ≡ λ fx. fx 2 ≡ λ fx. f (fx) …… n ≡ λ fx. f ⁿ x

Succ ≡ λ nfx. f (nfx).

Add ≡ λ mnfx. nf (mfx)

Mult = λ mnf. m (nf)

Задача заключается в том, чтобы сконструировать комбинаторы для представления логических констант TRUE и FALSE и для представления базисных логических функций. Для представления констант выбираем комбинаторы:

True ≡ λ xy. x

False ≡ λ xy. y

Заметим, что комбинатор False совпадает с чёрчевским нумералом 0 «ноль». Для представления конъюнкции, дизъюнкции и отрицания выбираем соответственно комбинаторы:

And ≡ λ pq. pq False

Or ≡ λ pq. p True q

Not ≡ λ p. p False True

Ifthenelse ≡ λ pxy. pxy.

Любой комбинатор выражается через базисные комбинаторы S и K.

K º l xy. x канцелятор

S º l xyz. xz (yz) коннектор

Алгоритм элиминации основан на Т-преоброзовании.

1) T[ x ] => x, если x – переменная или принадлежит {S,K}

2) T[ E ₁ E ₂] => T[ E ₁] T[ E ₂]

3) T[λ x. E ] => K T[ E ], если x Ï FV (E)

4) T[λ x. x ] => I

5) T[λ x. λ y. E ] => T[λ x. T[λ y. E ]], если x Î FV (E)

6) T[λ x. E ₁ E ₂] => S T[λ x. E ₁] T[λ x. E ₂]

Сделаем некоторые разъяснения. Правила 3 и 4 тривиальны, так как λ x. x экстенсионально эквивалентно I и λ x. E экстенсионально эквивалентно K E, если x не свободно в E. Первые два правила тоже простые. Правило 5 говорит, что сначала надо конвертировать тело абстрактора, а затем с помощью правила 6 элиминировать сам абстрактор. Терм λ x. E ₁ E ₂ получает аргумент, скажем, a и подставляет его в терм (E ₁ E ₂) вместо x, но это равносильно подстановке в каждый из термов E ₁ и E ₂, так что

(λ x. E ₁ E ₂) a = ((λ x. E ₁) a)((λ x. E ₂) a) = S (λ x. E ₁) (λ x. E ₂) a

и по свойству экстенсиональности получаем λ x. E ₁ E ₂ = S(λ x. E ₁)(λ x. E ₂).

Для примера элиминируем абстрактор из l-термаλ x. λ y. yx:

T[λ x. λ y. yx ]

=> T[λ x. T[λ y. yx ]] (по 5)

=> T[λ x. S T[λ y. y ] T[λ y. x ]] (по 6)

=> T[λ x. S I T[λ y. x ]] (по 4)

=> T[λ x. S I (K T[ x ])] (по 3)

=> T[λ x. S I (K x)] (по 1)

=> S T[λ x. S I ] T[λ x. K x ] (по 6)

=> S (K (S I)) T[λ x. K x ] (по 3)

=> S (K (S I))(S T[λ x. K ] T[λ x. x ]) (по 6)

=> S (K (S I))(S (K K) T[λ x. x ]) (по 3)

=> S (K (S I))(S (K K) I) (по 4)

Если применим, полученный комбинатор (S (K (S I))(S (K K) I)) к термам a и b получим следующее:

S (K (S I))(S (K K) I) a b

=_b K (S I) a (S (K K) I a) b

=_b S I (S (K K) I a) b

=_b I b (S (K K) I a b)

=_b b (S (K K) I a b)

=_b b (K K a (I a) b)

=_b b (K (I a) b)

=_b b (I a)

=_b b a

Дата добавления: 2015-08-31