Неперервність функції в інтенсіональних моделях лямбда-подібних числень

Размещено на http://www.allbest.ru/

КИЇВСЬКИЙ НАЦІОНАЛЬНИЙ УНІВЕРСИТЕТ ІМЕНІ ТАРАСА ШЕВЧЕНКА

УДК 004.432.42:519.766.2:515.126.2

НЕПЕРЕРВНІСТЬ ФУНКЦІЇ В ІНТЕНСІОНАЛЬНИХ МОДЕЛЯХ ЛЯМБДА-ПОДІБНИХ ЧИСЛЕНЬ

Спеціальність: 01.05.01- теоретичні основи інформатики та кібернетики

Автореферат дисертації на здобуття вченого ступеня

кандидата фізико-математичних наук

Лялецький Олександр Олександрович

Київ 2009

Дисертацією є рукопис.

Робота виконана в Київському національному університеті імені Тараса Шевченка

Науковий керівник: академік НАНУ, професор, доктор фізико-математичних наук Володимир Никифорович Редько Київський національний університет імені Тараса Шевченка, кафедра теорії та технології програмування, професор

Офіційні опоненти: доктор фізико-математичних наук, професор Провотар Олександр Іванович, Київський національний університет імені Тараса Шевченка, завідувач кафедрою інформаційних систем

кандидат фізико-математичних наук, доцент Володимир Васильович Бублік, Національний університет “Києво-Могилянська академія”, м. Київ, завідувач кафедрою

Захист відбудеться "17" грудня 2009 р. о "14" годині на засіданні спеціалізованої вченої ради Д 26.001.09 Київського національного університету імені Тараса Шевченка за адресою: 03127, м. Київ, проспект академіка Глушкова, 2, корпус 6, Київський національний університет імені Тараса Шевченка, факультет кібернетики, ауд.40. Тел. 259-04-24.

З дисертацією можна ознайомитися в бібліотеці Київського національного університету імені Тараса Шевченка (вул. Володимирська, 58).

Автореферат розісланий “ 16” листопада 2009 р.

Вчений секретар спеціалізованої вченої ради Шевченко В.П.

ЗАГАЛЬНА ХАРАКТЕРИСТИКА РОБОТИ

Актуальність теми. Поняття функції займає одне з самих центральних місць в тих питаннях, які стосуються побудови семантики мов програмування, оскільки кожну комп'ютерну програму можна розглядати як (часткову) функцію, що співставляє вхідним даним програми результат її роботи (якщо він існує). На відміну від класичної математики, яка оперує з екстенсіональним поняттям функції, коли кожна функція ототожнюється зі своїм графіком, з точки зору прикладних та теоретичних питань, які виникають в програмуванні, логиці, дескриптології і т.і., трактування програм як функцій природно вимагає долучити до розгляду інтенсіональні поняття функції, тобто такі, які враховують, окрім графіку функції, також й спосіб її задання. Таким чином, однією з самих важливих проблем в цих наукових галузях є задача про формалізацію інтенсіонального поняття функції, однак спроби дати таке пряме визначення не призвело, на сьогоднішній день, до жодного відповідного загально визнаного задовільного поняття. У зв'язку з цим на передній план вийшли задачі про виявлення, неформальне обгрунтування та опис таких "наївних" загальних властивостей інтенсіональних функцій, яким вони беззаперечно мають задовольняти.

Зокрема, таким чином з'явилися теорія лямбда як (нескінченна) сукупність "наївних" теоретико-аплікативних екваціональних функційних властивостей та лямбда-числення як спеціальна формальна система, яка дозволила надати опис теорії лямбда та провести неформальне обґрунтування властивостей, що її складають.

Разом із виникненням теорії лямбда, природно постало важливе питання про можливість побудови її теоретико-множинної семантики, тобто про існування конструктивно детермінованих моделей теорії лямбда в рамках класу всіх множин. З точність до теоретико-аплікативних функційних властивостей, що складають теорію лямбда, це питання фактично запитує, чи може теорія множин служити в якості слушного базису для формалізації в ній інтенсіонального поняття функції, чи ні. Окрім вільних моделей з лямбда-термів, починаючи з 1968 р., було побудовано низку класів несинтаксичних "конкретних" теоретико-множинних лямбда-моделей. Однак вичерпної відповіді на це питання немає й досі, оскільки, по-перше, серед останніх, на сьогоднішній день, не було знайдено жодної "точної" моделі (тобто такої, теорія якої співпадає з самою теорією лямбда), та, по-друге, ці моделі мають дуже складну математичну структуру, що заважає використовувати їх на практиці, наприклад, для побудови "зрозумілої" семантики мов програмування.

Це вказує на актуальність побудови нових теоретико-множинних лямбда-моделей. Саме таке спрямування має дана дисертаційна робота; а саме, її присвячено дослідженню можливості побудови нових класів лямбда-моделей на базі підходу, що забезпечується оригінальними визначеннями неперервності функції, яка діє на частково впорядкованих множинах.

З точки зору практичних застосувань, слід відмітити, що теорія лямбда має два основні напрямки її використання. З одного боку, результат С.Кліні, який стверджує, що сукупність представимих в теорії лямбда часткових натуральних функцій співпадає з класом частково рекурсивних функцій, дозволяє використовувати апарат лямбда-числення для формальної побудови та дослідження багатьох функційних мов програмування; зокрема, на базі лямбда-числення було розроблено такі мови як LISP, ML, Standart ML, Scheme, Miranda, Clean і Haskell. З іншого боку, встановлений ізоморфізм Каррі-Говарда між натуральним виведенням та типизованим варіантом лямбда-числення служить фундаментом для застосування лямбда-числення для розробки методів та для створення автоматизованих систем пошуку виведення в логіках вищих порядків, таких, наприклад, як Isabelle, HOL, Nurpl, PVS та інші.

Зв'язок роботи з науковими програмами, планами, темами. Наукові результати роботи отримані в рамках наукових тем "Логіко-математичні та програмологічні засоби інформаційних технологій" (2001-2005 рр., державний реєстраційний номер 01БФ015-07) та "Розробка конструктивних математичних формалізмів для інтелектуальних систем прийняття рішень, обробки знань, еталонування мов сучасних СУБД та CASE-засобів" (2006-2010, державний реєстраційний номер 06БФ015-05) факультету кібернетики Київського національного університету імені Тараса Шевченка.

Мета і завдання дослідження. Встановити абстрактні властивості нових понять збіжності спрямованості та неперервності функції, які задано на частково впорядкованих множинах. Зробити порівняльний аналіз введених понять з класичними аналогами. Проаналізувати можливість побудови моделей теорії лямбда за методом К.Койманса на базі нових понять неперервної функції. Побудувати нові класи теоретико-множинних моделей теорії лямбда та зробити порівняльний аналіз їх та відомих класів лямбда-моделей.

Об'єктом дослідження є такі моделі теорії лямбда, які базуються на спеціальних поняттях неперервної функції.

Предметом дослідження є спрямованості над частково впорядкованими множинами, спеціальні поняття неперервності функції, а також нові моделі теорії лямбда, як в самостійному контексті, так і в контексті їх порівняння з відомими лямбда-моделями.

Методи дослідження базуються на апараті побудови семантик мов функціонального програмування, а також результатах логіко-математичних теорій, таких як теорія частково впорядкованих множин, теорії неперервних відображень спеціальних типів, теорія моделей лямбда-числення.

Наукова новизна одержаних результатів полягає в наступному:

- Проведено аналіз еволюції підходів до побудови теоретико-множинних моделей лямбда-числення та близьких питань; вказано місце одержаних результатів серед інших.

- Розглянуто нові поняття неперервної функції, що діє на частково впорядкованих множинах; сформульовано та доведено оригінальні теоретико-порядкові характеризації відповідних класів неперервних функцій; зроблено порівняльний аналіз цих понять неперервності функції з їх класичними аналогами.

- Показано, що одне з нових понять неперервності функції не призводить до нетривіальних лямбда-моделей, але інші два, що отримуються незначною, на перший погляд, модифікацією цього поняття неперервності функції, навпаки, призводять до нових класів лямбда-моделей, причому серед останніх є, зокрема, нетопологізуємі.

Наукове та практичне значення одержаних результатів. За побудовою можна розрізняти два види теоретико-множинних моделей теорії лямбда: вільні моделі, які будуються з лямбда-термів, та семантичні лямбда-моделі, які будуються за допомогою загальних теоретико-множинних конструкцій. Оскільки лямбда є екваціональною теорією, то для неї звичайним чином конструюються вільні моделі. Втім, початкові спроби побудувати "конкретні" семантичні лямбда-моделі наштовхнулись на значні труднощі, пов'язані, в основному, з тим, що (нетипізований) варіант теорії лямбда не розрізняє поняття функції та аргументу функції. Отже для того, щоб побудувати нетривіальну модель теорії лямбда, природно намагатися знайти таку множину A, яка є рівнопотужною множині A^A всіх унарних операцій на A, але це неможливо за теоремою Кантора.

В 1968 р. Д.Скотт обійшов цю перешкоду та побудував перші семантичні лямбда-моделі, звузивши множину A^A до множини [A A] всіх таких операцій на A, які є неперервними відносно деяких спеціальних топологічних просторів на повних решітках. Пізніше було представлено ще низку класів "конкретних" семантичних лямбда-моделей, але всі вони також базуються на ідеях та конструкціях, які запропонував Д.Скотт: вони будуються, відштовхуючись від класу частково впорядкованих множин і з використанням конструкції прямого або оберненого спектрів, а лямбда-терми інтерпретуються як неперервні в деяких спеціальних сенсах функції, причому неперервність розуміється як неперервність відносно монотонних топологій. неперервність лямбда функція числення

В 1982 р. К.Койманс представив свій метод побудови лямбда моделей, що узагальнює підходи, запропоновані Д.Скоттом та іншими дослідниками, до побудови семантичних теоретико-множинних моделей теорії лямбда. Метод К.Койманса має характеризаційну властивість, згідно якої за цим методом можна побудувати кожну лямбда-модель з точністю до ізоморфізму, і яка дозволяє надати достатні ознаки того, що на базі деякого поняття неперервності функції можна побудувати лямбда-модель.

Маючи на меті побудувати нові класи теоретико-множинних лямбда-моделей, в дисертаційній роботі вводяться і досліджуються нові визначення неперервності функції, яка діє на частково впорядкованих множинах з "достатньою кількістю" супремумів та інфімумів. При цьому, кожне з цих визначень індукує нетопологізуємі класи необов'язково монотонних функцій, на відміну від тих понять неперервної функції, які було застосовано у "класичних" підходах до побудови лямбда-моделей. Використовуючи метод К.Койманса, доводиться, що деякі з цих визначень дійсно індукують нові класи моделей теорії лямбда. Також проводиться загальне теоретичне дослідження одержаних класів лямбда-моделей та їх порівняння зі вже відомими. Це визначає наукове значення роботи.

Дисертація має теоретичну спрямованість. Але, з практичної точки зору, отримані результати в перспективі можуть бути застосовано в загальній теорії програм, при побудові та опису різних мов функціонального програмування, а також в теорії пошуку виведення в логіках вищих порядків.

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

Апробація результатів дисертації. Основні положення і результати дисертаційної роботи доповідались й обговорювались на наступних конференціях та засіданнях робочих груп:

- IV International Algebraic Conference in Ukraine.- Lviv, Ukraine.- 2003;

- Logic Colloquium 2004.- Torino, Italy.- 25-31 July, 2004;

- 3rd International Conference „Theoretical and Applied Aspects of Program Systems Development”. - Kyiv. - 2006.

- 1-st Intas-meeting "Practical Formal Verification Using Automated Reasoning and Model Checking". - Timisoara, Romania.- 2006.

Публікації. За темою дисертації опубліковано 4 статті у фахових наукових журналах, 3 тези доповідей на конференціях.

Структура і обсяг дисертації. Дисертація складається зі вступу, 4-х розділів, висновку та списку використаних джерел з 52-х найменувань. Повний обсяг дисертації складає 110 сторінок.

ПЕРЕЛІК ОСНОВНИХ РЕЗУЛЬТАТІВ ДИСЕРТАЦІЇ

Згідно з результатами Е.Енгелера, Ф. Хонзелла, Д.Скотта та інших, кожний групоїд можна поповнити до (екстенсіональної) лямбда-моделі; тому клас всіх теоретико-множинних лямбда-моделей є дуже широким та різноманітним. Тим не менш, представники відомих класів "конкретних" теоретико-множинних лямбда-моделей мають багато спільних специфічних властивостей: зокрема, в них лямбда-терми інтерпретуються як неперервні функції відносно деяких монотонних топологій.

З точністю до ізоморфізму клас вичерпується тими лямбда-моделями, які можна побудувати за методом К.Койманса; тому природно було припустити, що, змінивши поняття неперервності функції, наприклад, на нетопологічне та немонотонне, вдасться, за допомогою методу К.Койманса, побудувати нові класи "конкретних" лямбда-моделей. В якості такого поняття було досліджено поняття слабкої, середньої та сильної неперервностей функції, що діє на передрешітках. В результаті виявилося, що одне з цих понять неперервності функції не призводить до нетривіальних лямбда-моделей, але інші два поняття індукують нові класи лямбда-моделей.

У вступі відображено актуальність основної задачі дисертації - побудови нових лямбда-моделей та їх дослідження. Також визначені методи дослідження, завдання, наукова новизна й практична цінність отриманих результатів. Наведено вже відомі підходи побудови теоретико-множинних моделей теорії лямбда.

У першому розділі приводяться всі необхідні визначення та попередні відомості з теорії множин, теорій частково впорядкованих множин та решіток, топології, теорій (о)-неперервності та неперервності за Скоттом і т.і., що є необхідними для подальшого викладення наукового матеріалу.

Що стосується інших 3-х розділів, то вони мають наступний причинно-наслідковий зв'язок: для побудови нових лямбда-моделей (розділ 4) вводяться спеціальні поняття неперервної функції (що вивчаються в розділі 3), які вводяться через властивість зберігати відповідні ліміти збіжних спрямованостей (які вивчаються в розділі 2).

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

Як звичайно, під спрямованістю над множиною A розуміється будь-яка функція d: I A, що діє з деякої непорожньої спрямованої частково впорядкованої множини ‹I, ?› (множини індексів) в множину A; при цьому елементи множини d(I) називаються елементами спрямованості d.

Передрешіткою називається будь-яка непорожня частково впорядкована множина, яка містять супремум кожної своєї непорожньої спрямованої підмножини та інфімум кожної своєї непорожньої ко-спрямованої підмножини.

Для зростаючої (спадаючої) спрямованості P над передрешіткою ‹A, ?› її ліміт визначається як супремум (інфімум) множини всіх її елементів. Якщо ж P - довільна спрямованість над ‹A, ?›, то кажуть, що вона слабко -збігається до елемента aA в тому і тільки тому випадку, коли множина всіх її монотонних (тобто зростаючих або спадаючих) конфінальних підспрямованостей не є порожньою, і всі вони збігаються до a.

Елемент b спрямованості P називається її нейтральним елементом, якщо він не є елементом жодної зростаючої або спадаючої конфінальної підспрямованості спрямованості P.

Кажуть, що спрямованість P середньо збігається до елемента aA, якщо P слабко збігається до a та, починаючи з деякого індекса, P не містить нейтральних елементів. Якщо ж спрямованість P слабко збігається до елемента aA та не містить нейтральних елементів взагалі, то кажуть, що P сильно збігається до елемента a.

Теорема 2.1. На R всі три поняття збіжності спрямованості (послідовності) збігаються зі звичайним поняттям збіжності спрямованості (послідовності).

Для кожної множини А через _A будемо позначати клас всіх спрямованостей над A. Для кожного топологічного простору T над множиною A через lim_T позначимо часткове відображення lim_T:_AA, яке кожній спрямованості над A ставить у відповідність топологічний ліміт відносно T. Підмножина частково впорядкованої множини ‹A, ?› називається -замкненою, якщо вона містить супремум (інфімум) кожної своєї непорожньої спрямованої (відповідно ко-спрямованої) підмножини. Нехай T позначає топологічний простір на множині A, який відповідає топологічному оператору замикання, який кожній підмножині B множини A співставляє найменшу -замкнену підмножину множини A, що містить B.

Також вводяться дві спеціальні передрешітки L₀ та L₁, які є необхідними при формулюванні наступного результату.

Теорема 2.2. Для довільної передрешітки A = ‹A, ?› в тому і тільки тому випадку існує така топологія T, що відображення lim та lim_T збігаються, якщо A не містить впорядковану підмножину, ізоморфну одній з передрешіток L₀, L₁ та L₀^-1, L₁^-1. Якщо ця умова виконується, то можна покласти T рівною T.

Підмножина B довільної передрешітки ‹A, ?› називається квазіопуклою, якщо, по-перше, для будь-яких елементів x, z B та y A з нерівностей x y z випливає y B і, по-друге, B є замкненою відносно супремумів своїх непорожніх спрямованих підмножин та інфімумів своїх непорожніх ко-спрямованих підмножин.

Через позначимо найменшу топологію, яка містить топологію Скотта S^? та топологію S^?-1, що є дуальною до останньої.

Теорема 2.3. Нехай ‹A, ?› є передрешіткою. Довільна підмножина B множини A є -замкненою в тому і тільки тому разі, якщо її можна представити як скінченне об'єднання квазіопуклих множин.

Наслідок 2.1. Топологія T є більш тонкою, ніж топологія , але, взагалі кажучи не навпаки.

В третьому розділі вводяться та досліджуються нові визначення неперервності функції.

Через K позначимо клас всіх передрешіток; функції f:‹A₀,₀›‹A₁,₁›, які розглядаються як функції, що діють на передрешітках, будемо називати K-функціями.

Нехай f:‹A₀,₀›‹A₁,₁› - K-функція. f називається слабко (середньо, сильно) неперервною в тому і тільки тому випадку, якщо f зберігає слабкі (середні, сильні) ліміти всіх збіжних спрямованостей (тобто для будь-якої спрямованості P над A₀ з того, що P збігається, випливає збіжність f(P), причому в цьому випадку f(lim P) = lim f(P)).

Теорема 3.1. На дійсній прямій R поняття слабкої, середньої та сильної неперервностей функції збігається зі звичайним поняттям неперервної функції.

Для довільної підмножини R передрешітки ‹A, ?› через R^> (через R^<) позначимо найменшу надмножнину множини R, що є замкненою відносно супремумів (інфімумів) своїх непорожніх спрямованих (ко-спрямованих) підмножин.

Для того, щоб побудувати теоретико-порядкові характеризації введених класів неперервних функцій, для довільної K-функції f: ‹A₀,₀›‹A₁,₁› розглянемо наступні властивості:

(С) кожний нескінчений ₀-ланцюг С, C A₀, має таку скінченну підмножину F, F C, що множина-образ f(C \ F) є ₁- ланцюгом;

(CW) A₀ не містить такий нескінчений антиланцюг E, всі елементи множини-образу f(E) якої є попарно ₁-зрівняними;

(CA) для кожної спрямованої чи ко-спрямованої підмножини D множини A₀ існує скінчене (можливо, порожнє) число елементів d₁, …, d_n, таких, що множина-образ f (D\{d₁,…, d_n }) є або спрямованою, або ко-спрямованою;

(CS) якщо елементи a₀, a₁ A₀ є ₀-зрівняними, то їх образи f(a₀) та f(a₁) є ₁-зрівняними;

(Sc) якщо R є областю зростання функції f, то R^> також є областю зростання функції f, і для кожної непорожньої спрямованої підмножини D множини R^>, має місце рівність f(sup D) = sup f(D), а якщо R є областю спадання функції f, то R^< також є областю спадання функції f, і для кожної непорожньої ко-спрямованої підмножини D множини R^<, має місце рівність f(inf D) = sup f(D).

Тепер ми можемо зформулювати наступний результат.

Теорема 3.2. Нехай f: ‹A₀,₀›‹A₁,₁› є довільною K-функцією. Тоді:

а) f є слабко неперервною f задовольняє властивостям (С), (СW) та (Sc);

б) f є середньо неперервною f задовольняє властивостям (СA) та (Sc);

с) f є сильно неперервною f задовольняє властивостям (СS) та (Sc).

В застосуваннях теорії решіток до аналізу особливу роль відіграє поняття (o)-неперервності. Виявилося, що на класі нескінченно дистрибутивних решіток - як раз тих решіток, які найчастіше зустрічаються аналізі, зокрема, в теорії частково впорядкованих лінійних просторів - поняття середньої неперервності та (o)-неперервності функції співпадаючі класи непрерервних функцій.

Теорема 3.3. На класі повних решіток, що задовольняють тотожностям нескінченної дистрибутивності, поняття (о)-неперервності функції збігається з поняттям середньої неперервності.

Дослідження, проведені в третьому розділі, мають самостійний інтерес; але вони також можуть мати цікаві застосування для таких галузей математики як: загальна топологія, функціональний аналіз упорядкованих лінійних просторів, теорія міри і т.і.

Четвертий розділ присвячений побудові нових лямбда-моделей за допомогою методу К.Койманса на базі нових визначень неперервності функції, а також їх порівнянню з відомими теоретико-множинними лямбда-моделями.

Існує декілька визначень лямбда-моделі; відомо, що кожне з них разом із відповідними морфізмами індукують "конструктивно" ізоморфні між собою категорії (теж саме стосується визначень лямбда-алгебр). В дисертаційній роботі було обрано поняття лямбда-алгебри та лямбда-моделі, які були визначені наступним чином.

Множину всіх змінних мови теорії лямбда позначаємо через X, а множину всіх лямбда-термів - через T. Для довільного групоїду A = < A, > через Val(A) будемо позначати сукупність всіх оцінок в A, тобто сукупність всіх відображень : X A. Лямбда-інтерпретацією в групоїд A називається будь-яке відображення I: TVal(A) A, яке задовольняє наступним умовам (де I(t, ) позначається як [t]):

1) [x] = (x);

2) [t₀t₁] = [t₀][t₁];

3) [(x.t₀)t₁] = [t₀]_[x:=b], де b = [t₁];

4) FV(t) = `FV(t) [t] = [t]<sub>`</sub>,

де FV(t) позначає множину всіх вільних змінних терму t.

Аплікативною структурою називається пара < A, I >, де A - групоїд, а I - лямбда-інтерпретація в A. Поняття істинності при оцінці та загальної істинності лямбда-рівності на аплікативній структурі вводяться звичайним чином. Аплікативна структура < A, I > називається лямбда-алгеброю, якщо сукупність всіх лямбда-рівностей, що є істинними на < A, I >, містить теорію лямбда. Аплікативна структура < A, I > називається лямбда-моделлю, якщо для будь-якої оцінки : X A з того, що для будь-яких елемента a A та змінної x виконується [t₀]_[x:=a] = [t₁]_[x:=a], випливає [x.t₀] = [x.t₁]. (Відомий результат стверджує, що кожна лямбда-алгебра є лямбда-моделлю.)

Метод, за допомогою якого автор дисертації намагався побудувати нові лямбда-моделі, був розроблений К.Коймансом в рамках теоретико-категорних формалізмів. Цей метод, по суті, є узагальненням конструкцій, які використовував Д.Скотт, Ю.Єршов та інші при побудові своїх теоретико-множинних лямбда-моделей. Наведемо необхідні визначення та основні результати цього методу.

Нехай C - декартово замкнена категорія з термінальним об'єктом T та U - її довільний об'єкт; тоді |U| позначає сукупність всіх точок об'єкта U (тобто |U| = Hom_C(T,U)). Кажуть, що U має достатньо багато точок, якщо за допомогою його точок можна розрізнити будь-яку пару різних епіморфізмів об'єкта U (тобто для для будь-яких ₀, ₁: U U з того, що _{0 1}, випливає існування такої точки x: T U, що x₀ x₁). Зауважимо, що будь-яка строго конкретна (тобто "теоретико-множинна") категорія має достатньо багато точок.

Об'єкт U називається рефлексивним, якщо існують морфізми : U U^U та :U^U U, такі, що виконується рівність = id_U^U, де id_U^U позначає тотожній епімофізм об'єкта U^U.

Теорема (К. Койманс). 1. Нехай C - довільна декартово замкнена категорія, яка містить деякий рефлексивний об'єкт U з відповідними морфізмами : U U^U та :U^UU. Тоді на множині |U| можна (деяким спеціальним чином) так визначити операцію та лямбда-інтерпретацію I в групоїд U = < |U|, >, що аплікативна структура <U, I > є лямбда-алгеброю. Якщо при цьому U має достатньо багато точок, то, по-перше, < U, I > є лямбда-моделлю, і, по-друге, групоїд < |U|, > в тому і тільки тому випадку є екстенсіональним, коли виконується рівність = id_U.

2. Кожна лямбда-алгебра може бути отримана таким чином (з точністю до ізоморфізму).

Для цілей дисертації більш зручним є інший, теоретико-множинний варіант методу К.Койманса, який формулюється на базі напів-формального поняття "структури" (у разі необхідності опис, що приводиться нижче, може бути повністю формалізовано за допомогою поняття строго конкретної категорії).

Опис теоретико-множинного варіанту методу К.Койманса.

Нехай K - клас деяких теоретико-множинних структур, замкнений відносно прямих добутків, і P - деяке поняття неперервної функції, що діє на структурах з K, і яке співставляє кожній парі <A₀,A₁> K-структур K-структуру [A₀A₁]_P = [A₀A₁] P-неперервних функцій, що діють з A₀вA₁, причому виконуються наступні умови:

довільна функція f:A₀A₁B P-неперервна тоді і тільки тоді, коли f неперервна за кожним аргументом;

"операція" аплікації _A:[AA]AA є неперервною для кожної K-структури A;

K містить деяку рефлексивну структуру M (тобто існують такі неперервні відображення :[MM]M та :[MM]M, що =id_[MM], де id_[MM] - тотожнє відображення).

На рефлексивній структурі M визначимо бінарну операцію , поклавши для кожних m₀,m₁M m₀m₁=(m₀)(m₁). Індуктивно визначимо лямбда-інтерпретацію I:TVal(M) M в групоїд A = < M, >, поклавши для довільної оцінки в A:

[x] = (x), де x - змінна;

[t₀t₁] = [t₀][t₁];

[x.t] = f_t,

де f_t: M M - функція, що співставляє кожному m M значення [t]_[x:=m].

Тоді мають місце наступні твердження:

аплікативна структура < A,I > є лямбда-моделлю;

групоїд A є екстенсіональним в тому і тільки тому випадку, якщо виконується =id_M.

За допомогою теореми 3.2 неважко перевірити, чи задовільняє кожне з введених понять неперервності функції умовам 1 та 2 методу К.Койманса.

Теорема 4.1. а) Поняття середньо та сильно неперервної функції задовільняє умовам:

довільна функція f:A₀A₁B неперервна тоді і тільки тоді, коли f є неперервною за кожним аргументом,

"операція" аплікації _A: [AB]AB є неперервною для кожних передрешіток A та B.

б) Поняття слабко неперервної функції задовільняє умові 1 попередньої теореми, але не задовільняє умові 2.

Зокрема, з цієї теореми випливає, що на базі поняття слабко неперервної функції не можна будувати нетрівіальні моделі теорії лямбда за допомогою методу К.Койманса. Щодо інших двох понять неперервності функцій, то вони-таки індукують нетривіальні лямбда-моделі. На це вказує наступний результат.

Для кожних передрешіток A і B через [AB]_A та [AB]_S будемо позначати сукупності всіх середньо та сильно неперервних функцій, які діють з A в B.

Теорема 4.2. Кожну передрешітку A можна поповнити до рефлексивної передрешітки B, що є лімітом прямого експоненційного спектру, який складається з передрешіток B₀, B₁,..., B_i,..., де B₀ = A, B_i+1 = [B_iB_i]_A та гомоморфізмів-експонент _i: B_i B_i+1, причому при цьому A можна підібрати таким чином, що B є нетопологізуємою лямбда-моделлю. Аналогічне твердження має місце, якщо в визначенні спектру покласти B_i+1 = [B_iB_i]_S.

ВИСНОВКИ

Для дослідження можливостей побудови теоретико-множинних моделей лямбда-подібних числень, які задовільняють тим чи іншим спеціальним властивостям, в дисертаційної роботі було виконано відповідні дослідження та отримано наступні головні результати.

- Запропоновано та досліджено нові визначення збіжності спрямованості (послідовності) на частково впорядкованих множинах з "достатньою кількістю" супремумів та інфімумів.

- Надано нові природні означення поняття неперервної функції, яка діє на частково впорядкованих множинах. За домогою встановлених властивостей лімітів спрямованостей, наведено абстрактні теоретико-порядкові характеризації таких функцій.

- На базі цих характеризаційних властивостей лімітів спрямованостей зроблено вивчення та порівняльний аналіз відповідних класів неперервних (в новому сенсі) функцій з добре відомими класами неперервних функцій, таких як класи топологічно- та (o)-неперервні функції, а також класи функцій, що є неперервними за Скоттом.

- Досягнуто головну мету дисертації: на базі нових визначень неперервних функцій побудовано нові класи моделей теорії лямбда за методом К.Койманса. Зокрема, показано, що одне з нових понять неперервної функції взагалі не придатне для побудови нетривіальних лямбда-моделей, але інші два, навпаки, призводять до нових класів неперервних лямбда-моделей, причому серед останніх є, зокрема, нетопологізуємі.

СПИСОК ОПУБЛІКОВАНИХ РОБІТ ЗА ТЕМОЮ ДИСЕРТАЦІЇ

1. Lyaletsky A. On Some Logical Properties of Intentional Types of Continuity Defined with Respect to Partially Order Relations // Управляющие системы и машины. Киів. 2004. № 1. C. 4-9.

2. Лялецький О.О. Про типи збіжності послідовностей та топологічні властивості частково впорядкованих множин // Вісник Київського університету. Сер.: фіз.мат. науки. 2008. Вип. 1. С. 121-126.

3. Лялецький О.О. Про типи неперервності функцій та їх властивості відносно частково впорядкованих множин // Вісник Київського університету. Сер.: фіз.мат. науки. 2008. Вип. 2. C. 98-104.

4. Лялецкий А.А. О некоторых свойствах теоретико-множественных моделей теории лямбда // Математичні машини і системи. Киів. 2008. № 4. C. 10-21.

5. Lyaletsky А. On notions of continuity and embeddings of theories of topological algebras into the theories of partially ordered algebras // Abstracts of the IV International Algebraic Conference in Ukraine. Lviv, Ukraine. 2003. P. 139-140.

6. Lyaletsky A. On types of continuity defined by partially ordered sets and their interconnection with usual topological continuity // TIMETABLE and ABSTRACTS of the Logic Colloquium 2004. Torino, Italy. 25-31 July, 2004. P. 135.

7. Лялецкий А.А. Об одном понятии непрерывности функции // Abstracts of the 3rd International Conference „Theoretical and Applied Aspects of Program Systems Development”. Kyiv. 2006. P. 64-66.

АНОТАЦІЯ

Лялецький О.О. Неперервність функції в інтенсіональних моделях лямбда-подібних числень. - Рукопис.

Дисертація на здобуття наукового ступеня кандидата фізико-математичних наук за спеціальністю 01.05.01 - теоретичні основи інформатики та кібернетики. - Київський національний університет імені Тараса Шевченка, м. Київ, 2009.

Головним чином, дисертацію присвячено дослідженню деяких спеціальних понять неперервності функції в контексті побудови на їх базі моделей лямбда-числення за допомогою методу К.Койманса. А саме:

В роботі пропонуються три нові природні визначення збіжності спрямованості над частково впорядкованою множиною з "достатньою кількістю" супремумів та інімумів.

На базі цих трьох визначень вводяться три поріднені, але різні поняття неперервної функції через властивість функції зберігати відповідні ліміти спрямованостей. Зроблено порівняльний аналіз цих понять з їх загально відомими аналогами, такими як неперервність за Скоттом, (о)-неперервність та топологічна неперервність. Наведено абстрактні теоретико-порядкові характеризації властивості функції "бути неперервною" в сенсі кожного з цих трьох нових понять.

На базі нових понять неперервної функції, за допомогою характеризаційних теорем, досліджено можливість побудови за методом К.Койманса нових моделей теорії лямбда. Показано, що одне з цих понять призводить лише до тривіальних лямбда-моделей, в той час як інші 2 нові поняття індукують нові "неперервні" лямбда-моделі. Побудовано приклади "неперервної", але нетопологізуємих моделей теорії лямбда.

Ключові слова: лямбда-числення, лямбда-модель, теорія лямбда, неперервність функції, збіжність спрямованості, топологія, частково впорядкована множина.

АННОТАЦИЯ

Лялецкий А.А. Непрерывность функции в интенсиональных моделях лямбда-подобных исчислений. Рукопись.

Диссертация на соискание ученой степени кандидата физико-математических наук по специальности 01.05.01 - теоретические основы информатики и кибернетики. Национальный университет имени Тараса Шевченко, г. Киев, 2009.

По построению можно различать два вида теоретико-множественных моделей теории лямбда: свободные модели, которые строятся из термов, и семантические лямбда-модели, которые строятся с помощью общих теоретико-множественных конструкций. Поскольку лямбда является эквациональной теорией, то для неё обычным способом строятся свободные модели. Однако ранние попытки построить "конкретные" теоретико-множественные семантические лямбда-модели натолкнулись на значительные трудности, связанные, в основном, со следующим. Нетипизированный вариант теории лямбда не различает понятий функции и аргумента функции; поэтому для того, чтобы построить нетривиальную модель теории лямбда, естественно пытаться найти множество A, равномощное множеству A^A всех унарных операций на A. Но из теоремы Кантора следует, что такого множества A не существует.

В 1968 г. Д. Скотт обошел эту трудность и построил первые семантические лямбда-модели, урезав A^A до множества [A A] всех таких операций на A, которые являются непрерывными относительно некоторых специальных топологических пространств на полных решетках. Позднее были построены другие классы "конкретных" семантических лямбда-моделей, но они также конструировались на базе идей и конструкций, предложенных Д.Скотом: они строятся, отталкиваясь от класса частично упорядоченных множеств и с использованием конструкции прямого или обратного спектров, а лямбда-термы интерпретируются в них как непрерывные, в некоторых специальных смыслах, функции, причем непрерывность понимается как непрерывность относительно тех или иных монотонных топологий.

Следует также отметить, что в соответствии с результатами Э.Энгелера, Ф.Хонзелла, Д.Скотта и других, каждый группоид можно пополнить до (экстенсиональной) лямбда-модели; следовательно, класс всех лямбда-моделей является очень широким и разнообразным. Кроме того, известно, что класс исчерпывается теми лямбда-моделями, которые можно построить с помощью метода К.Койманса, который, формулируясь в теоретико-категорных терминах, унифицирует методы построения "конкретных" лямбда-моделей, использованных Д.Скоттом, Ю.Ершовым и др. Поэтому естественно предположить что, изменив понятие непрерывности функции, например, на нетопологическое и немонотонное, также можно построить новые нетривиальные классы "конкретных" семантических лямбда-моделей (на базе соответствующей релятивизации метода К.Койманса к рассматриваемым теоретико-множественным конструкциям).

Исследования, представленные в диссертации, являются подтверждением этого предположения в случае, когда под неперерывной функцией понимается средне или сильно непрерывная функция, оригинальные определения которых предложены автором. Более точно:

В работе предлагаются три новые естественные определения сходимости направленности над частично упорядоченным множеством с "достаточным количеством" супремумов и инфимумов.

На базе этих трех определений вводятся три родственные, но различные понятия непрерывной функции через свойство функции сохранять соответствующие пределы направленностей. Проводится сравнительный анализ этих понятий непрерывности с такими общепринятыми, как непрерывность по Скотту, (о)-непрерывность и топологическая непрерывность. Приводятся абстрактные теоретико-порядковые характеризации свойства функции "быть непрерывной" в смысле каждого из этих трех новых понятий.

На базе новых понятий непрерывности функции, с помощью характеризационных теорем, исследуется возможность построения по методу К.Койманса новых моделей теории лямбда. Показывается, что одно из этих понятий приводит лишь к тривиальным лямбда-моделям, в то время как остальные два новых понятия приводят к новым "непрерывным" лямбда-моделям. Построены примеры "непрерывных", но нетопологизируемых моделей теории лямбда.

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

THE SUMMARY

Lyaletkyy O.O. Continuity of a function in intensional models of lambda-like calculi. The manuscript.

The dissertation for a scientific degree of the candidate of Physics and Mathematics on the speciality 01.05.01 - the foundations of Informatics and Cybernetics; Kiev National Taras Shevchenko university, Kiev, 2009.

Mainly, the dissertation is devoted to investigations of some special notions of continuity of a function in the view of constructing, on their base, new models for the theory lambda. More precisely:

In the paper, 3 new natural notions of convergence of a direction on a partially ordered set with "enough number" of supremums and infimums are introduced.

Further, on the base of these 3 new notions, 3 new similar notions of continuity of a function are introduced as the property to preserve the corresponding limits of the directions. There was made the comparative analysis of these 3 notions with their well-known analogues, such as Scott continuity, (o)-continuity, and topological continuity of a function. Abstract order-theoretical characterization of these 3 notions is constructed.

By means of these characterization theorems, the new notions of continuity of a function were tested on possibility of the construction of new lambda-models in accordance with the K.Koymans method. It appeared that one of these notions induct no lambda-models except the trivial one, but 2 other notions lead to the constriction of new "continuous" lambda-models. Examples of "continuous" but non-topologizable lambda-models were constructed.

Key words: lambda-calculus, lambda-models, theory lambda, continuity of a function, convergence of a net, topology, partially ordered set.

Размещено на Allbest.ru

...