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

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

13.6. ФОРМАЛИЗАЦИЯ НЕФОРМАЛИЗУЕМЫХ ПОНЯТИЙ

381

Содержательно данный результат означает, что основание, являю-

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

держательных утверждений. Если мы вывели имеющее смысл в данной

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

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

Понятие псевдопроблемы появилось в работах Венской школы по-

зитивизма в 20-х годах. Псевдопроблемами называли пышно звучащие

философские вопросы типа

Что первично: материя или сознание?

теряющие смысл при переводе на научный язык. Мы идем дальше, счи-

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

но опора на них является порочным методом.

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

вестному в логике примеру логической ошибки.В жизни слишком часто

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

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

изначальном равенстве способностей всех людей, мы отвергаем целесо-

образность равенства их прав. Это еще со времен Аристотеля квалифи-

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

предложение — временно принять его. Критика оснований может лишь

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

ли, что в реальной ситуации критика оснований может быть еще более

сильным аргументом, если мы обнаруживаем в основаниях не ложное

утверждение,а псевдопроблему.Допустим, опора на существование Бо-

га в научном исследовании полностью уничтожает силу приводимых

аргументов. На любое утверждение нужно опираться в своем месте и

по соответствующему поводу. Религии и так нанесли слишком большой

ущерб излишне благонамеренные ученые, очень хотевшие научно дока-

зать существование Бога и делавшие при этом легко обнаруживаемые

ошибки.

Системы формализаций неформализуемых понятий позволяют вы-

разить и еще одну важнейшую сторону знания, впервые затронутую в

неклассических логиках. Поскольку незнание всеобъемлюще и неис-

требимо, порою один из самых мощных видов знания — знание о не-

знании. Конкретные классические теории не позволяют этого исполь-

зовать, а вот в их системах постулирование и использование незнания

вполне возможно.

382

ГЛАВА 13. НЕПОЛНОТА И НЕФОРМАЛИЗУЕМОСТЬ

И наконец, можно заметить, что соотношения между неформали-

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

данным их ипостасям. Чтобы выразить более глобальные утверждения

(например, что A содержательно следует из B в том смысле, что при-

няв при формализации

, мы вынуждены принимать и

во избежание

распада системы понятий), необходимо рассматривать целые системы

теорий, а тут уже вступает в права неклассическая логика.

Подытожим

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

него самого.

Не все вычислимые функции могут быть продолжены до

всюду определенных.

Ни одна достаточно богатая теория не может быть полна.

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

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

верку.

Неразрешимые утверждения бывают разных типов, в том

числе и такие, которые не зависят не только от теории, но

и друг от друга.

Пополнение теории правилом, позволяющим переходить от

доказуемости

A(n) при произвольном n к истинно-

сти ∀x A(x) весьма сильно расширяет возможности теории.

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

да

∀x P (x) с разрешимым P , для доказательства которых

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

Можно заниматься формализацией и неформализуемых по-

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

дидат на звание подходящей для теорий, описывающих со-

стояние понятий в данный момент, для данной цели и с дан-

ной точки зрения.

Классическая логика перестает работать, если мы интере-

суемся не истинностью в случае неизменной фиксирован-

ной точки зрения,а развитием понятий. Она может подвести

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

13.6. ФОРМАЛИЗАЦИЯ НЕФОРМАЛИЗУЕМЫХ ПОНЯТИЙ

383

утверждения вида ∃x A(x) как основу для алгоритмических

построений.

Классическая логика практически бессильна, когда нужно

формализовывать незнание.

Выражаясь несколько метафорически, классическая логи-

ка —логика конкретного знания и веры,а неклассическая —

логика построения, изменения знания и сомнения.

384

ГЛАВА 13. НЕПОЛНОТА И НЕФОРМАЛИЗУЕМОСТЬ

Часть III

Введение в неклассические

логики

385

Глава 14. Основы

-исчисления

Язык λ-конверсий является сейчас одним из важнейших выразитель-

ных средств в логике, информатике, математической лингвистике, ис-

кусственном интеллекте и когнитивной науке.Начнем с синтаксических

аспектов λ-конверсий и их использования как формального языка.

§ 14.1. ОСНОВЫ

-ЯЗЫКА

В математике укоренились некоторые т. н. “вольности речи”, часто при-

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

облегчая взамен. Одна из таких традиционных неаккуратностей — сме-

шение значения выражения с функцией, вычисляющей это выражение.

Например, в уравнении x

= 1 x

есть выражение, в тождестве

= 2x (14.1)

есть функция,а относительно 2x этот вопрос может быть решен лишь

из контекста (а порою и из него возникают лишь двусмысленности). Для

обозначения функций используются записи типа x → x

, и этого хвата-

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

Но уже запись

x → x

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

чиняет все больше и больше неприятностей.

Американский логик Черч (A. Church) предложил обозначения, по-

зволяющие трактовать функциональные и смешанные выражения столь

же последовательно, как и обычные математические. Квантор функци-

ональности λx. t(x), где t(x) — терм, образует выражение, интерпрети-

руемое как функция, аргументом которой является x, а результатом —

388

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

-ИСЧИСЛЕНИЯ

значение t(x). Это выражение само рассматривается как терм, к которо-

му можно применять преобразования и о свойствах которого можно го-

ворить, x становится связанной переменной, подстановки производятся

по тем же правилам, что и обычно, чтобы избежать коллизий. Так что с

точки зрения

-языка утверждение, что производная

в точке

есть

записывается четко и ясно:

D(λx. e

)(0) = 1 (14.2)

Здесь

D — оператор дифференцирования, применяемый к функции

λx. e

(заметим, что традиционное dx становится просто ненужным; ар-

гумент функции однозначно определяет, по какой переменной берется

производная). D применяется к функции действительной переменной и

в результате дает также функцию действительной переменной. Видно,

что результат применения оператора D к функции λx. e

применяется

далее к числу 0.

Рассмотрим несколько более сложный пример: формулу для произ-

водной суммы.

Dλx. (f(x) + g(x)) = λx. (D(f)(x) + D(g)(x)) (14.3)

Здесь строго различается применение операций к функциям и к значе-

ниям этих функций. Сложение обрабатывает числа, а дифференцирова-

ние — операции над числами.

То, что математику можно построить не на базе чисел и множеств, а

на базе понятия функции, если разрешить свободно использовать функ-

ции как аргументы и результаты

других функций, заметили практиче-

ски одновременно великий венгерский математик Я. фон Нейман и рос-

сийский логик М. И. Шейнфинкель. Фон Нейман стремился в тот мо-

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

орию, которая выглядит как перевод теории множеств на язык функций,

и, как недостаточно безумная, она оказалась забыта. Зато Шейнфин-

кель выделил минимальный базис колоссальной общности и необычно-

сти, который был развит другими. Операции, применяемые к функциям,

осознанно использовались в математике и до Шейнфинкеля. Они назы-

вались операторами (если результат — функция) либо функционалами

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

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

приводит к безнадежной неэффективности вычислений.

14.1. ОСНОВЫ

-ЯЗЫКА

389

(если результат — объект). Сейчас они чаще всего называются функци-

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

ются просто функциями. Но лишь М. И. Шейнфинкель и Х. Б. Карри

(H. B. Curry) начали разработку их систематической теории. И сразу же

они натолкнулись на важное преобразование, позволяющее уменьшить

количество сущностей.

Для описания функций многих переменных хочется ввести много-

местный квантор типа

λx

. . . x

. t(x

, . . . , x

). Карри

подметил ис-

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

функции систематически трактуются как значения. Вместо f(x, y) он

рассмотрел функционал f, перерабатывающий x в функцию от y:

f(x)(y) = f(x, y). Таким образом, без ограничения общности доста-

точно рассматривать функции от одного аргумента. Такое преобразова-

ние называется преобразованием Карри (Currying). Оно соответствует

также представлению λx

. . . x

в форме λx

. . . λx

. (Проверьте!)

Преобразование Карри имеет важные аналогии в программирова-

нии.Оно соответствует частичной параметризации процедур.Если име-

ется процедура P(x1, x2, . . . , xn), а известно лишь значение x1 = a, мож-

но тем не менее проделать внутри P вычисления, зависящие лишь от

x1, и получить частичную процедуру P1(x2, . . . , xn) = P(a, x2, . . . , xn).

Если не требовать оптимизации частичной процедуры, то частичная па-

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

эффективность программ методом программирования, который, к не-

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

ление наиболее популярных языков программирования —

Pascal

. У

себя в примерах будем обозначать частичную параметризацию P

∗

(a, . . . , z).

Отметим один тонкий момент. Пусть дана процедура P(x, y). Произ-

ведя частичную параметризацию P

∗

(a, b), мы с точки зрения програм-

мирования получаем не значение P(a, b), а процедуру без параметров,

вычисляющую это значение.

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

14.1.1. Пусть

f(x, y) — функция, вычисляющая расстояние между дву-

мя действительными числами. Что такое λx. f(0, x)?

14.1.2. Запишите определенный интеграл

f(x) dx на λ-языке.

На самом деле это преобразование рассматривалось еще Шейнфинкелем и фон Ней-

маном.

390

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

-ИСЧИСЛЕНИЯ

14.1.3. Если f(x, y) = e

∙ sin(y), то что такое λxy. f (y, π/2 −x)?

14.1.4. Вычислить

λx. Dλy (y

∙ x + y)(1)(3).

14.1.5. Студентка Тупицына спросила: « А зачем вообще все многочи-

сленные кванторы?Почему не писать, например,

∃λx A(x) вместо

∃x A(x), где ∃ понимается как логическая операция над функция-

ми с логическими значениями, и обходиться одним квантором λ?»

Ваше отношение к этому предложению: приносит ли оно какие-то

удобства либо неудобства, либо совсем некорректно, и почему?

14.1.6. Студентка Примерная записала утверждение

λx. x

+ 1 > λx.

2+x

. Что Вы скажете по этому поводу?

14.1.7. Прокомментируйте запись

∀x Max(a, b, f(x)) > f(x), где

Max — функционал нахождения максимума функции на от-

резке [a, b].

14.1.8. Студент Чудаков предложил по аналогии с распространенным

в математике обозначением множеств в стиле

{f(x, y) | A(x, y)}

использовать λ-обозначения типа λ(x

). {sin(x)∙cos(y)}. Что

можно сказать по данному поводу?

§ 14.2.

-КОНВЕРСИИ

Пожалуй, впервые общие свойства и преобразования пространств неко-

торых частных видов операторов и функционалов начали исследовать-

ся в линейной алгебре. Матрицы были введены как представления про-

странства линейных преобразований; еще более фундаментальное на-

блюдение было сделано при рассмотрении пространств линейных функ-

ционалов из конечномерного пространства в скаляры. Это пространство

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

странства могут рассматриваться как линейные функционалы на этом

сопряженном пространстве. В выражении fx = c возникает двойствен-

ность между функциями и аргументами, которая является краеуголь-

ным камнем при развитии λ-языка: можно считать функцией f, а x —

ее аргументом, можно и наоборот

Двойственность не означает возможность путать аргументы и функции. Она озна-

чает лишь право сделать глобальную замену функций и аргументов друг на друга. А уж