Непейвода Н.Н. Прикладная логика

Подождите немного. Документ загружается.

14.2.

-КОНВЕРСИИ

391

Шейнфинкель предложил подчеркнуть двойственность следующей

системой обозначений. Операция применения функции к аргументу за-

писывается (fx), а не f(x), как обычно. Здесь важно то, что при помощи

преобразования Карри все функции могут быть сделаны одноместными

функционалами. Черч предложил важное упрощение языка Карри, ко-

торое сейчас и принято называть языком

λ-исчисления.

Определение 14.2.1.

-сигнатура — множество констант.

-термы сиг-

натуры

задаются следующим индуктивным определением:

1. Константа сигнатуры

есть

-терм.

2. Переменная есть

-терм.

3. Если

—

-термы, то

(tu)

—

-терм.

4. Если

— переменная,

—

-терм, то

λx. t

—

-терм.

Пример 14.2.1.

Если

— константы, изображающие оператор

дифференцирования, функцию одной переменной и ноль, то значение

(0)

изображается

((Df)0)

Так же, как в логике предикатов, для λ-термов определяются поня-

тия свободной и связанной переменной и подстановки. Через подста-

новку определяется важнейшее из преобразований над λ-термами — β-

конверсия. Оно состоит в символьном вычислении результата вызова

функции λx. t(x). Одинарная стрелка → читается “за один шаг перехо-

дит в”. Большая стрелка ⇒ читается “преобразуется в”.

(λx. t r) → Subst(t, x, r) (14.4)

Это преобразование называется

β-конверсией.

Пример 14.2.2.

λx. x

есть тождественная функция. В самом деле,

(λx. x t) ⇒ t

для любого

. Обозначив терм

λx. x

через

, можем записать это как

(I t) ⇒ t

. В частности,

(I I) ⇒ I

насколько она будет странно выглядеть, другое дело.

392

ГЛАВА 14. ОСНОВЫ

-ИСЧИСЛЕНИЯ

λ-термы позволяют определить предельно общее

исчисление сим-

вольных вычислений функциональных выражений. Оно называется ис-

числением λ-конверсий. В этом исчислении выводятся выражения вида

r ⇒ t. Аксиомы его — (14.4), переписанная через ⇒:

(λx. t r) ⇒ Subst(t, x, r) (14.5)

t ⇒ t.

Правила вывода следующие.

t ⇒ u u ⇒ r

t ⇒ r

(транзитивность) (14.6)

t ⇒ u

(t r) ⇒ (u r)

(преобразование функции) (14.7)

t ⇒ u

(r t) ⇒ (r u)

(преобразование аргумента) (14.8)

t ⇒ u

λx. t ⇒ λx. u

(правило ξ) (14.9)

Названия “

β-конверсия” и “правило ξ” традиционны для обозначе-

ния этих характерных преобразований λ-термов. Правда, их суть лучше

отражали бы названия типа “символьное вычисление” и “преобразова-

ние определения”. Чаще всего ⇒не ставят, а просто выписывают после-

довательность преобразуемых (конвертируемых) друг в друга термов.

Пример 14.2.3.

Рассмотрим

-термы

Ψ = λx. (x x); Ω = (Ψ Ψ) = (λx. (x x) λx. (x x)).

По

-конверсии

преобразуется в

Subst(λx. (x x), x, Ψ) = (Ψ Ψ) = Ω.

Итак,

конвертируется сам в себя.

Отметим взаимосвязь

с парадоксом Расселла. Рассмотрим множе-

ство всех множеств,

являющихся

собственными элементами:

Z = {x|x ∈

Общее не значит, что туда запихали все, что можно и нельзя. Это означает предельно

простое выражение широко применимой идеи, которое может быть легко конкретизи-

ровано для частных случаев.

14.2.

-КОНВЕРСИИ

393

. Тогда

Z ∈ Z ⇔ Z ∈ {x|x ∈ x} ⇔ Z ∈ Z

. Хотя здесь мы и не

получили грубого противоречия, мы высветили логическую основу па-

радокса Расселла, парадокса лжеца и многих других парадоксов: ударя-

ясь в абстракции, слишком легко определить понятия, не содержащие

ничего, кроме самих себя

. Карри дал интересную переформулировку

таких “рефлексивных парадоксов”. Пусть

A = {x|x ∈ x ⇒ A}

. Тогда

A ∈ A ⇔ (A ∈ A ⇒ A)

. Пусть

A ∈ A

. Тогда

A ∈ A ⇒ A

. Значит, из

A ∈ A

следует

. Но

(A ∈ A ⇒ A) ⇔ A ∈ A

. Следовательно,

A ∈ A

Но

A ∈ A ⇒ A

. Значит,

. Итак, имея неограниченные абстракции

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

конверсиях объекты, подобные

, относительно безобидны (в точности

в той же степени, что “зацикливание” в программах).

Подробней проанализируем роль различных правил в λ-конверсиях.

β-конверсия является определением вызова процедуры, принятым в

большинстве языков программирования. Транзитивность означает воз-

можность выполнить целую последовательность вычислений. Един-

ственное разумное ограничение на нее — исчерпание ресурсов, которое

обычно игнорируется в семантике алгоритмического языка. Практиче-

ски нечего возразить и на правило преобразования аргумента. А вот пре-

образование функции уже несколько более сомнительно. Оно чаще все-

го просто избегается в языках программирования за счет того, что функ-

ция не является полноправным значением. Правило ξ не может быть

просто проигнорировано, поскольку любой приличный язык включает

описания процедур, но такое преобразование чаще всего прямо запре-

щается в семантике языков программирования. В самом деле, чаще все-

го процедура содержит операторы, рассчитанные на разные значения

аргумента, и при конкретном значении аргумента выполняются (за счет

операторов типа

case

while

repeat

) лишь некоторые из них. Попытка

же вычислять, не разобравшись со значением аргумента, вполне может

привести к ошибке. Например, если процедура для положительного x

вычисляет его квадратный корень, а для отрицательного действует по-

другому, то попытка слишком рано вычислить

√

приведет к ошибке.

Таким образом, анализ правила ξ привел нас к выявлению ограничений

на частичные вычисления в обычных языках программирования. Даже

Некоторые философы и богословы определяли Бога как “то, что является причиной

самого себя”. Анализ парадоксов показывает, что это довольно плоско: причина самой

себя скорее ничто, чем Бог.

394

ГЛАВА 14. ОСНОВЫ

-ИСЧИСЛЕНИЯ

если известны значения всех переменных, входящих в выражение, но

выражение находится внутри описания процедуры либо внутри услов-

ного оператора, вычислять его нельзя. А вот в λ-конверсиях можно про-

изводить вычисление любого подтерма, где бы он ни стоял. Докажем

это.

Определение 14.2.2. λ

-терм с дырой. Пусть символ



обозначает дыру.



—

-терм с дырой.

2. Если

—

-терм,

—

-терм с дырой, то

(t r)

(r t)

—

-термы

с дырой.

3. Если

— переменная,

—

-терм с дырой, то

λx. r

—

-терм с

дырой.

Через

t[r]

обозначим результат замены дыры в

-терме

с дырой на

терм

Предложение 14.2.1. 1. В λ-терме с дырой ровно одна дыра.

2. Если

t — λ-терм с дырой, r — λ-терм, то t[r] — λ-терм.

3. Если

r — подтерм λ-терма s, то найдется терм с дырой t, такой,

что s ≡ t[r]

4. Если

t — λ-терм с дырой, r и s — λ-термы, r ⇒ s, то t[r] ⇒ t[s].

Доказательство. Пункты 1 и 2 тривиально доказываются индукцией

по построению терма с дырой. Пункт 3 опирается на единственность

дерева построения

λ-терма и усиливает ее до следующей леммы.

Лемма о подтермах. Если r — вхождение подтерма в λ-терм t, то

дерево порождения r является поддеревом дерева t.

И, наконец, пункт 4. Действуем индукцией по длине терма с дырой,

используя пункт 1. Если терм состоит из одной дыры, то все очевидно.

В противном случае дыра находится в одном из его подтермов, который

сам, согласно 3, является λ-термом с дырой.Рассмотрим три возможных

случая. Если t имеет вид λx t

, то, по предположению индукции, t

[r] ⇒

[s]. Но тогда по правилу ξ t[r] ⇒ t[s].

Остальные случаи также разбираются прямым применением правил

конверсии.

≡ означает графическое равенство выражений.

14.2.

-КОНВЕРСИИ

395

Рассмотрим некоторые конструкции λ-языка. Пусть f и g — функ-

ции. Тогда (f(gx)) применяет f к результату вычисления g на x, и терм

λx. (f(gx)) выражает функцию, являющуюся композицией f и g. С дру-

гой стороны, ((fx)y), если принять во внимание преобразование Карри,

выражает применение функции

к двум аргументам, а, соответственно,

((fg)y) — применение функционала f к функциональному аргументу

g и обычному x

Исходя из содержательного смысла конверсий как символьных вы-

числений, можно определить равенство

λ-термов t и r как существова-

ние такого s, что t ⇒ s, r ⇒ s. Но обосновать такое определение не

слишком просто: ведь прежде всего отношение равенства должно быть

отношением эквивалентности; рефлексивность и симметричность на-

шего определения очевидны, но с транзитивностью дело обстоит не так

просто. Если t

⇒ s

, t

⇒ s

, t

⇒ s

, t

⇒ s

, то откуда следу-

ет, что найдется такое s, что t

⇒ s, t

⇒ s? Тем не менее временно

примем такое сомнительное определение, которое обосновывается тео-

ремой Черча-Россера, доказываемой в следующей главе.

Теперь рассмотрим преобразование, впервые введенное явно в

λ-

исчислении и ставшее краеугольным камнем современной теории про-

граммирования.

Предложение 14.2.2. (Лемма о неподвижной точке) Для любого

λ-

терма F найдется такой λ-терм X, что X = (F X).

Доказательство. Определим

W как λx. (F (xx)),и пусть X есть (W W ).

Тогда легко показать самим, что X конвертируется в (F X)

Данное предложение служит ярким примером важной и нетривиаль-

ной теоремы, доказывающейся в три строчки, но такой, до которой не-

легко было додуматься, и такой, которая имеет множество применений.

В самом деле, поскольку создатели λ-языка с самого начала отдавали

себе отчет в его универсальности (он годится для выражения любого

функционала, встречающегося в математике, естественно, при подхо-

На самом деле нигде не сказано, что g — функция, а x — предмет. Занимаясь λ-

исчислением, необходимо помнить, что функция может быть подставлена в любом ме-

сте.

Здесь есть единственная, но ехидная тонкость: не (F X) преобразуется в X, а X в

него!

396

ГЛАВА 14. ОСНОВЫ

-ИСЧИСЛЕНИЯ

дящем подборе исходных констант), то их не могло не смущать, в част-

ности, следующее рассуждение:

Рассмотрим функцию натуральных чисел

ϕ =

λn n + 1

. Она не имеет неподвижной точки, посколь-

ку, если

— таковая, то

m = m + 1

(14.10)

Здесь на помощь приходит то, что в

λ-исчислении имеется, в частности,

терм Ω, конвертирующийся сам в себя и не имеющий значения. (ϕ Ω)

просто не имеет значения, так же как и само Ω, и как Ω + 1. И, соответ-

ственно, нет ничего удивительного в том, что (ϕ Ω) = Ω = Ω + 1.

Поскольку приведенное нами преобразование, очевидно, само вы-

ражается в λ-языке, то имеется комбинатор неподвижной точки Y, ко-

торый можно определить, например, как

λF (λx (F (x x)) λx (F (x x))).

не является ни единственным, ни даже наилучшим из комбинаторов

неподвижной точки, но используется он чаще всего. В частности,

Yf → f(Yf)

не имеет места (почему?).

Поэтому часто рассматривается комбинатор

Θ ≡ (λxy. y(xyy) λxy. y(xyy)).

Красивые примеры еще нескольких комбинаторов неподвижной точ-

ки см. в упражнениях.

Упражнения к § 14.2

14.2.1. Покажите, что

(ΘF ) → (F (θF )).

14.2.2.

(Klop)

Пусть

= λabcdefghijklmnopqstuvwxyzr.

(r(thisisafixedpointcombinator)),

$ = (

ЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪ)

Показать, что $ — комбинатор неподвижной точки.

14.2.3. Перевести пример Клопа на русский язык (так, чтобы в терме

читалась русская фраза с аналогичным значением, а алфавит, в от-

личие от латинского, присутствовал бы в неизмененном порядке).

14.2.4. Построить комбинатор A, такой, что (Afx) = (fx).

14.3. ТЕОРЕМА ЧЕРЧА-РОССЕРА

397

§ 14.3. ТЕОРЕМА ЧЕРЧА-РОССЕРА

Важнейшим из известных приятных свойств систем преобразований явля-

ется свойство конфлюэнтности, либо свойство квадрата: если a пре-

образуется как в b, так и в c, то имеется такое d, что b преобразуется в d и

c преобразуется в d. Это означает, что, какими путями ни вести преобра-

зование, придем к одному и тому же результату. Докажем это свойство

для λ-конверсий.

Теорема Черча-Россера. Если

t ⇒ r, t ⇒ s, то найдется такое q, что

s ⇒ q, r ⇒ q.

Доказательство. Пользуясь идеей Мартин-Лефа, определим вспомога-

тельное отношение конверсии

→,в котором β-конверсия к каждому под-

терму применяется не более одного раза.

t → t;

t →

λx. t → λx. r

;

t → r s →

(t r) → (s q)

;

t → r s →

λx. (t s) → r[x|q]

(14.11)

Лемма 14.3.1. Если

t → r, то t ⇒ r.

Лемма 14.3.2.

⇒ является транзитивным замыканием →.

Лемма 14.3.3. Если

λx t ⇒ r, то r также начинается с λx.

Лемма 14.3.4. Если

(t r) → s, то либо s есть (qv), где t → q, r → v,

либо t есть λx. q, s есть q1[s|r1], где q → q1, r → r1.

Все эти леммы очевидны.

Лемма 14.3.5. Если

t → r, s → q, то t[x|s] → r[x|q].

Доказывается индукцией по построению

t, аналогично предложе-

нию 3.2.1.

Лемма 14.3.6. Отношение

→ обладает свойством конфлюэнтности.

Доказательство леммы. Индукцией по длине преобразования

t в r.

Если

t есть само r, то достаточно взять s в качестве q.

Если

t есть λx. (t

), a r есть r

[x|r

], где t

→ r

, t

→ r

, то s

есть одно из двух.

398

ГЛАВА 14. ОСНОВЫ

-ИСЧИСЛЕНИЯ

1. λx (s

), где t

→ s

, t

→ s

. Тогда, по предположению индук-

ции, для r

, s

можно найти q

и, соответственно, для r

, s

общее

. По лемме 14.3.5 в качестве q можно взять q

[x|q

2. s

[x|s

]. Непосредственно применяем предположение индукции и

лемму 14.3.5.

Если теперь

есть

)

, а

есть

)

, то опять возникают два

подслучая.

). Непосредственно применяем предположение индукции.

2. t есть λx. (t

), s есть s

[x|s

], где t

→ s

, t

→ s

. Тогда по

предположению индукции, t

и r

, t

и r

попарно приводятся к

общему терму. Применяем лемму 14.3.5.

А теперь, поскольку конверсия — транзитивное замыкание →, а → кон-

флюэнтно, теорема доказана.

Конец доказательства теоремы.

Упражнения к § 14.3

14.3.1. Студент Талантов предложил следующее расширение

λ-конвер-

сий. Ввести термы вида [x y z] со следующими правилами конвер-

сии: [faa] ⇒ (fa)(fa); [fga] ⇒ (fa)(ga). Прокомментируйте это

предложение.

14.3.2. Студентка Невинная предложила следующий вариант λ-конвер-

сий для кортежей. Вводятся термы вида [t

. . . t

] вместе со следу-

ющими правилами конверсии:

([t

. . . t

] r) ⇒ [(t

r) . . . (t

r)]

(t[r

. . . r

]) ⇒ [(t r

) . . . (t r

)]

Ваше мнение об этом предложении: разумно ли оно с точки зрения

истолкования и сохраняет ли оно свойство локальности конверсий

и свойство конфлюэнтности?

14.4.

-ИСЧИСЛЕНИЕ

399

§ 14.4.

-ИСЧИСЛЕНИЕ

Исчислению λ-конверсий соответствует исчисление равенств термов,

конвертируемых в одно и то же выражение, которое обычно называется

λ-исчислением либо комбинаторной логикой. Языком этого исчисления

служат равенства λ-термов t = u. Аксиомы и правила вывода — следу-

ющие семь.

t = t аксиома равенства

λx. (t r) = Subst(t, x, r) (аксиома β-конверсии)

t =

u = t

t = u u = r

t = r

t =

(t r) = (u r)

t = u

(r t) = (r u)

t =

λx. t = λx. u

(

правило ξ)

(14.12)

Теорема 14.1. Формула

t = u выводима в комбинаторной логике тогда

и только тогда, когда существует такой терм v,что t ⇒ v, u ⇒ v.

Доказательство. Индукцией по построению вывода. Аксиома равен-

ства порождает диаграмму

t t

(14.13)

Во второй аксиоме левая часть равенства просто конвертируется в пра-

вую. Транзитивность равенства соответствует диаграмме

u r

(14.14)

Остальные случаи разбираются еще легче

400

ГЛАВА 14. ОСНОВЫ

-ИСЧИСЛЕНИЯ

Следствие 14.4.1. Отношение выводимости t = u является отноше-

нием эквивалентности на множестве термов. Если t = u, то термы

(ts) и (rs) одновременно либо имеют нормальную форму, либо не имеют

ее, и в случае нормализуемости их значения равны.

Обратное свойство — если

ts = rs при всех s, то t = r, — не все-

гда выполнено. Чтобы обеспечить его, достаточно добавить еще одну

аксиому равенства λx (f x) = f, но тогда разрушается теорема 14.1.