Книги
чёрным по белому
Главное меню
Главная О нас Добавить материал Поиск по сайту Карта книг Карта сайта
Книги
Археология Архитектура Бизнес Биология Ветеринария Военная промышленность География Геология Гороскоп Дизайн Журналы Инженерия Информационные ресурсы Искусство История Компьютерная литература Криптология Кулинария Культура Лингвистика Математика Медицина Менеджмент Металлургия Минералогия Музыка Научная литература Нумизматика Образование Охота Педагогика Политика Промышленные производства Психология Путеводители Религия Рыбалка Садоводство Саморазвитие Семиотика Социология Спорт Столярное дело Строительство Техника Туризм Фантастика Физика Футурология Химия Художественная литература Экология Экономика Электроника Энергетика Этика Юриспруденция
Новые книги
Цуканов Б.И. "Время в психике человека" (Медицина)

Суворов С. "Танк Т-64. Первенец танков 2-го поколения " (Военная промышленность)

Нестеров В.А. "Основы проэктирования ракет класса воздух- воздух и авиационных катапульных установок для них" (Военная промышленность)

Фогль Б. "101 вопрос, который задала бы ваша кошка своему ветеринару если бы умела говорить" (Ветеринария)

Яблоков Н.П. "Криминалистика" (Юриспруденция)
Реклама

Математика элементарной математики - Энглер Э.

Энглер Э. Математика элементарной математики — М.: Мир , 1987. — 130 c.
Скачать (прямая ссылка): matematikaelementarnoymatematiki1987.djvu
Предыдущая << 1 .. 32 33 34 35 36 37 < 38 > 39 40 41 42 .. 43 >> Следующая

Для доказательства последнего требования из определения L-алгебры допустим, что ЬМуф ЬМ2, например (а->6)є LM\\ (а-^Ь)ф LM2. Из (a-^b)^LMi следует существование некоторого р ^ а, такого, что (р->6)єМь Для этого Р верно беМіР. Так как, с другой стороны, (а-+Ь)фЬМ2, то невозможно у ^ а, такое, что (у-+Ь)^М2, в частности (Р->Ь)фМ2у и, следовательно, Ь ф.М2р. Поэтому неверно, что M\N = M2N для всех N. ?
Как мы только что видели, в L-алгебре можно конкретизировать любое вычислительное предписание t(x) в однозначно определенный объект LT, для которого верно ЬТх — t(x) при всех х. В силу комбинаторной полноты Т можно построить в виде выражения, составленного из S и К. Однако этот способ построения и особенно его описание оказывается довольно громоздким; с другой стороны, само понятие функциональной абстракции столь важно, что буквально вынуждает ввести короткий и выразительный метод записи. В отличие от теоретико-множественной абстракции, т. е. перехода от свойства Е(х) к его экстенсионалу {х\Е(х)}, функциональная абстракция пока еще не проникла в повседневную математику, хотя она могла бы внести большой вклад в прояснение понятий.
Для иллюстрации ламбда-записи, вводимой ниже, мы приведем два примера из повседневной практики математиков.
Что значит «функция Зх2+1»? Если кто-то хочет быть точным, он вводит по этому поводу функциональный символ, например /, и говорит: «функция /: R -> R, определенная со-
112
Г л. 111. Ллгоритмика
отношением f(x) = Зх2 + 1»- При этом очевидно, что переменную х можно здесь, не меняя смысла, заменить на другую переменную у, так что х — связанная переменная. Ламбда-запись устраняет произвольность в выборе / в качестве функционального символа. Она предлагает вместо / выражение «Хх.Зх2 + 1>>. Поэтохму значение выражения (Хх.Зх2 + 1)2 равно 13. Таким образом, ламбда-запись преодолевает нерегулярность обозначений при обычном функциональном способе выражения.
Пусть Р — оператор, т. е. сопоставление функций функциями. У малообразованного математика можно встретить обороты вроде «пусть f(x) — функция, и положим gr(jt) = P(f(x))». Это в общем случае ведет к недоразумениям. Например, что такое P(f(x— 1))? То ли это P(f) (х— 1), то ли P(g)(x)> гДе §(х) — f(x~ 1) ? А эго не одно и то же, как показывает следующий пример. Пусть Р определен соотношением
О для х О,
/ (я) в противном случае.
P(f)(x) = {
Тогда
( 0 для д: 1,
Р (/) (х — 1)Н п п
I }(х— 1) в противном случае,
( 0 для х ^ О,
Р (g) (Х) — 1 і / 14
I I (х ~ 1) в противном случае.
Математики, не получившие формалистической выучки, вводят в нужных случаях символы и соглашения, устраняющие такие недоразумения; стоит только вспомнить о введении оператора дифференцирования! И снова ламбда-запись дает равномерный и экономный метод достижения той же цели.
Здесь мы займемся одним и только одним полезным приложением ламбда-записи — в качестве способа обозначения терма LTy который строится для t(x), чтобы гарантировать равенство LTx = t{x) для всех х. Этот терм будет также обозначаться через Xx.t(x).
Определение. Пусть /(*1, ..., хп, х) — терм комбинаторной логики, построенный из 5, К, L и переменных Х\, ...,хп,х. Пусть Т — терм, который построен из S, К, L и х\, ..., хПу согласно лемме из § 1, и для которого верно Т>х =
t( х\, ..., хп, х) для всех хи хп. Тогда XxJ(x ь хп,х) обозначает терм LT,
§ 4. Ламбда-исчисление
113
Для работы с этим способом обозначений имеются свои правила. В рассматриваемом случае они принимают форму исчисления. Исторически это исчисление было создано Чёрчем независимо от комбинаторной логики и сначала было чисто формальным, т. е. вообще не ставился вопрос о конкретизации элементов в каких бы то ни было иных, например, теоретико-множественных терминах.
Принятая нами обратная последовательность — рассмотрение ламбда-алгебр до ламбда-исчисления — была избрана по педагогическим причинам. (См. также введение к § 2.)
Соглашение. Для термов tu t2 и переменной х обозначим через tx |? результат замены всех свободных вхождений переменной х в t\ на t2. При этом следует сделать переименования переменных, чтобы свободные вхождения переменных в t2 не попали в область действия X по тем же переменным В t\.
Исчисление ламбда-конверсии
Язык:
Термы строятся из атомарных термов, т. е. переменных и, возможно, констант, с помощью двуместной операции * и ламбда-абстракции: если / — терм и л; — переменная, то (ХхЛ) — снова терм.
Формулы — это равенства термов.
Аксиомы:
t = t для атомарных термов,
Xx.t = (ky.t ?) (переименование),
(Kx.ii) t2 = t\ I*2 (0-редукция).
Правила вывода:
*1 ~ *2 *1 = *2 *1 == *2
*1*3 = *2*3 * *3*1 ~ *3*2 * *2 = *1 *
*1 ~ *2 *2 == *3 *1 ~ *2
Предыдущая << 1 .. 32 33 34 35 36 37 < 38 > 39 40 41 42 .. 43 >> Следующая