2 Постановка задачи: о связном предъявлении теории информатики и практики программирования в теме исполнения для теоретического мышления. 13 (стр. 10 из 25)
Определим преобразование графа для представления применения Y-комбинатора. Это нетрудно сделать. Такое определение вытекает из определения фиксированной точки, то есть для любого l-выражения X имеем YX = X (YX) = X (X (X...X (YX)...)). Таким образом, граф обеспечивает корректное представление:
3.3 Модели теорий и типовые языки (системологический аспект).
В этом пункте следовало бы “во всей красе” показать тесную связь техники неподвижной точки с денотационной семантикой лямбда-исчисления по Д. Скотт. Как уже отмечалось, на плоских доменах D’ и D’’ можно определить домен всех монотонных и непрерывных функций f : [D’ ® D’’]. В трактовке функций как абстрактных объектов нет ничего нового, также через комбинаторы (Карри, Чёрча) мы уже привыкли, что выражение f(x) определяется как вычислимая функция и от f, и от x. Но Д. Скотт решил задачу интерпретации: желательно было иметь множество A, в котором вкрадывалось бы его функциональное пространство A®A; по мощностным соображениям Кантора этого, однако, невозможно достичь; в 69 г. Д. Скотт построил модели лямбда-исчислений, урезав A®A до множества непрерывных (в надлежащей топологии; или, как мы показывали, через последовательности) функций на A.
Конечно же, следовало бы рассмотреть пространство D¥, но мы не готовы к этому. Поэтому в пункте 3.3.1 предлагается подход к рассмотрению графиковых моделей лямбда-исчисления по книге Э. Энгелера “Метаматематика элементарной математики”.
Пункт 3.3.2 затрагивает общее значение теоремы о неподвижной точке, которое также следует разработать через аппликативный стиль. Это позволит в обучении непосредственно перейти от системологического аспекта прагматика к классу универсала. Завораживают слова Х. Барендрегта в книге “Ламбда исчисление” (стр. 155): “Как геделевская конструкция рефлексивного предложения, так и теорема рекурсии могут быть истолкованы как теоремы о неподвижной точке для подходящих предполных нумерованных множеств в смысле Ершова”.
3.3.1 Î ìîäåëÿõ l-àëãåáðû èëè l-òåîðèè.
(по Э. Энглер “Метаматематика элементарной математики”, Москва “МИР”, 1987г.)
Возможности и границы эффективных методов, т.е. алгоритмов, в математике образуют столь же фундаментальный комплекс вопросов, как и возможности и границы аксиоматического описания основных математических структур.
Мы снова применим метатеоретический подход. Мы попытаемся говорить об алгоритмах как об объектах в том же смысле, как раньше говорили о вещественных числах или таких геометрических объектах, как точки или прямые. Основные связи между такими объектами будут введены в качестве элементов языка.
Язык позволяет использовать выразительные средства, во-первых, при аксиоматическом исследовании; во-вторых, при обосновании вычислимости как теории формального оперирования с вычислительными операциями.
1 Что такое вычислительное предписание?
1.1 Алгоритмика начинается с понятия функции, точнее, понятия вычислимой функции. Разумеется, всем знакомо сведение функции к понятию множества (по Дирихле): функция F: A®B - это подмножество F Í A x B, обладающее свойством
"xÎA $!yÎB (<x,y>ÎF)
В соответствии с этим реляционным определением функция расположена перед нами как единое целое во всем своем протяжении или экстенсионале. Однако вычислительное предписание не соответствует такому идеализированному теоретико-множественному пониманию; оно начинает с понятия функции, которая в применении к аргументу выдает вполне определенное значение. В школе вычислительные предписания принимают главным образом вид выражений. Например,
f1=(x+2)(x-2)
или
f2=x2-4.
Таким образом, f1 ¹ f2, хотя f1(x) = f2(x). То есть в случае вычислительных предписаний наш интерес направлен не на экстенсионал функции, совокупность ее значений, а скорее на ее интенсионал. Например, смысл функционального выражения в алгоритмике состоит в его сущности как предписания для исполнения одной или нескольких вычислительных операций.
Наша цель - обосновать алгоритмику как теорию оперирования с вычислительными предписаниями и над ними. Сравним с теорией групп - она работает с понятием умножения элементов группы. В аксиоматической алгоритмике основной операцией является применение функции к аргументу или аппликация ¦*a.
Итак, исходный пункт - понятие функции, понимаемой как вычислительное предписание. Теперь мы делаем большой скачок в неизвестное: мы мыслим вычислительные предписания собранными в одну-единственную неструктурированную совокупность. Предусмотренное нами слияние типов родственно точке зрения, принятой в теории множеств, где между множествами также нет никаких различий в уровне. (В теории множеств удается образовать на основе одного-единственного понятия “x есть элемент совокупности y” чрезвычайно многообразно структурированную совокупность математических понятий. Вспомним пару {{x}, {x,y}}. Совсем не такая точка зрения принята в анализе, где функции из R®R отличаются от функционалов (R®R)®R и т.д.)
Бестиповое понимание совокупности вычислительных предписаний делает возможным столь же экономный выбор исходных понятий при аксиоматизации, как и в аксиоматической теории множеств. Например, нам не нужно различать одноместные и многоместные вычислительные предписания (карризация; F=lx.ly.f x y, тогда F*x=ly.f x y, тогда (F*x)*y=f x y. Эта идея восходит от Фреге и была впервые систематически применена Шейнфинкелем.)
| Примеры вычислительных предписаний. Мы можем мыслить объект B, удовлетворяющий равенству Bfgx = f(gx) {звездочки, по соглашению, опускаются} или fxyzuv = z (x (zu (yv))) (y (x (zuv))) |
Теперь мы выдвинем неограниченную выполнимость этой функциональной абстракции в качестве аксиоматического требования к предметной области.
| Комбинаторные алгебры. Пусть A = <A, *, c1,¼,cm> - алгебраическая структура с непустым носителем А; выделенными в нем элементами c1, c2,¼, cm, m³0; двуместной операцией *. {Итак, А - множество имен} Пусть t(x1,¼,xn) - терм в А, (т.е. построен из констант, обозначающих выделенные элементы, и переменных x1,¼,xn с помощью скобок и знака операции *. Говорят, что элемент ¦ множества А представляет терм t в А, если "a1,¼,an (¦ a1¼an = t(a1,¼,an)). Алгебра А комбинаторно полна, если любой терм t представим в А. В этом случае А называется комбинаторной алгеброй. Она называется нетривиальной, если А содержит более одного элемента. |
| Достаточно комбинаторов S и K. Пусть A = <A, *, K, S> Sxyz = xz (yz) Kxy = x. Тогда А - комбинаторная алгебра. |
Таким образом, комбинация, заданная термом t, всегда представляется в комбинаторной алгебре (хотя бы одним) объектом. Ввиду их происхождения мы называем такие объекты комбинаторами.
Доказательство обеспечим леммой. Из доказательства следует естественность выбора комбинаторов S, K.
Лемма. Для любого n и терма tn(x1,¼,xn), построенного из S, K и x1,¼,xn, имеется терм tn-1(x1,¼,xn-1), построенный из S, K и x1,¼,xn-1, такой, что
tn-1(x1,¼,xn-1)* xn = tn(x1,¼,xn).
Доказательство: индукцией по построению
База:
Пусть tnº K | S | xi, i¹n, тогда имеем tn-1=(Ktn). Действительно, (Ktn)*xn=tn.
Пусть tnº xn, тогда имеем tn-1=I=SKK. Действительно, SKK*xn = Kxn (Kxn) = xn.
Составные термы:
, тогда имеем tn-1 = St’n-1t’’n-1.Действительно, St’n-1t’’n-1*xn = t’n-1xn (t’’n-1xn) = t’nt’’n.
Теперь комбинаторная полнота получается многократным применением леммы: tn(x1,¼,xn) = tn-1(x1,¼,xn-1)xn = tn-2(x1,¼,xn-2)xn-1xn =¼= tox1,x2¼,xn.
Применим доказательство для построения комбинаторов для выражений.
1) Bxyz = x (yz)
Итак,
t2(x,y) = S(Kx)y = t1(x)y,
Осталось t1(x) = S(Kx) = tox
t’o = S = Ksx
t’’o = Kx,
Значит tox = S(KS)Kx.
Тем самым B = S (KS) K. Действительно,
Bxyz = S(KS)Kxyz = (KSx)(Kx)yz = S(Kx)yz = (Kxz)(yz) = x(yz).
2) Cxyz = (xz)y
Итак,
Итак,
, 
Итак, C=S (1S (KS) (2S (KK) S)2)1 (KK).
Действительно, Cxyz = S()1(KK)xyz = (()1x)Kyz = (S(()2x))Kyz = S(K(Sx))Kyz = (K(Sx)y)(Ky)z = Sx(Ky)z = (xz)y.
3)
, т.к. K=KKx.2 Существование комбинаторных алгебр.
Карри и Чёрч построили системы математики (добавив логические законы и части математики), которые оказались противоречивыми. Вспомним Фреге. Исторически первым был теоретико-доказательный подход. (То есть дань времени - программы Гильберта. Вопрос о существовании таких алгебр заменяется вопросом о непротиворечивости формальной системы; комбинаторная алгебра превращается в комбинаторную логику.