НЕПЕРЕРВНІСТЬ ФУНКЦІЇ В ІНТЕНСІОНАЛЬНИХ МОДЕЛЯХ ЛЯМБДА-ПОДІБНИХ ЧИСЛЕНЬ : Непрерывность функции в интенсиональных МОДЕЛЯХ лямбда-ПОДОБНЫХ многочисленных

Краткое описание

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

На правах рукопису

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

УДК 004.432.42:519.766.2:515.126.2

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

01.05.01- теоретичні основи інформатики та кібернетики

Дисертація
на здобуття вченого ступеня
кандидата фізико-математичних наук

Науковий керівник - В.Н.Редько,
академик НАНУ, професор, докт. фіз.-мат.наук

Київ - 2009

З М І С Т
ВСТУП ..................... 4
1 ЗАГАЛЬНІ ЗАУВАЖЕННЯ ТА ПОПЕРЕДНІ ВІДОМОСТІ .......... 16
1.1 ДЕЯКІ НОТАТКИ ПРО ЛЯМБДА-ЧИСЛЕННЯ ТА
ЙОГО ЗАСТОСУВАННЯ .............................................................. 23
1.2 ДЕЯКІ ПОПЕРЕДНІ ПОНЯТТЯ .............. 27
1.3 ВІДНОШЕННЯ ПОРЯДКУ .......... 29
1.4. СПРЯМОВАНОСТІ, ОПЕРАТОРИ ЗАМИКАННЯ ТА
ТОПОЛОГІЧНІ ПРОСТОРИ ......................................................... 34
1.5 ЛЯМБДА-ЧИСЛЕННЯ: НЕФОРМАЛЬНИЙ ОПИС............. 40
2 ПРО ТИПИ ЗБІЖНОСТІ ПОСЛІДОВНОСТЕЙ ТА
ТОПОЛОГІЧНІ ВЛАСТИВОСТІ ЧАСТКОВО
ВПОРЯДКОВАНИХ МНОЖИН ............................. 47
2.1 СПРЯМОВАНОСТІ ТА ТИПИ ЇХ ЗБІЖНОСТІ............. 49
2.2 ТОПОЛОГІЧНІ ВЛАСТИВОСТІ ЧАСТКОВО
ВПОРЯДКОВАНИХ МНОЖИН......................... 60
2.3 ВИСНОВОК ДО РОЗДІЛ.................. 71
3 ПРО ТИПИ НЕПЕРЕРВНОСТІ ФУНКЦІЙ ТА ЇХ ВЛАСТИВОСТІ
ВІДНОСНО ЧАСТКОВО ВПОРЯДКОВАНИХ МНОЖИН.............. 72
3.1 ТИПИ НЕПЕРЕРВНОСТІ ФУНКЦІЙ ТА ЇХ
ВЛАСТИВОСТІ ...........................................................72
3.2 ГОЛОВНІ РЕЗУЛЬТАТИ ПРО НЕПЕРЕРВНІСТЬ ............. 81
3.3 ВИСНОВОК ДО РОЗДІЛУ......... 88
4 ТЕОРЕТИКО-МНОЖИННІ МОДЕЛІ ТЕОРІЇ ЛЯМБДА, ЩО
БАЗУЮТЬСЯ НА ПОНЯТТЯХ £-НЕПЕРЕРВНОЇ ФУНКЦІЇ. 89
4.1 КОРОТКИЙ ОПИС ТЕОРІЇ ЛЯМБДА............ 90
4.2 ТЕОРЕТИКО-МНОЖИННІ ІНТЕРПРЕТАЦІЇ
ТЕОРІЇ ЛЯМБДА....................................................................... 92

4.3 ТОПОЛОГІЇ СКОТТА...... 95
4.4 МЕТОД КОЙМАНСА ПОБУДОВИ МОДЕЛЕЙ
ТЕОРІЇ ЛЯМБДА: ЗАГАЛЬНІ РИСИ ...................................... 96
4.5 НОВІ МОДЕЛІ ТЕОРІЇ ЛЯМБДА.........99
4.6 ВИСНОВОК ДО РОЗДІЛУ.......................................................103
ВИСНОВКИ........ 104
СПИСОК ВИКОРИСТАНИХ ДЖЕРЕЛ .. 106

ВСТУП

Незважаючи на те, що поняття програми вже стало остенсивним як результат процесу глобальної інформатизації, теоретико- та практико-обумовлені потреби програмування потребують експлікації як самого поняття програми, так і його похідних, таких як поняття процесу виконання програми, її конструктивності, її дескриптивної визначеності і т.і. Перше, що приходить на думку, - це спробувати представити програми як деякі функції; такий підхід відомий під назвою функціональної парадигми програмування. Але на поточний час, нажаль, не існує жодної загальноприйнятої функціональної експлікації поняття програми та навіть немає жодного загальновідомого більш широкого формально описаного класу функції, що має під собою в підгрунті декілька фундаментальних причин. Ця обставина, зокрема, означає, що в загальному випадку ніхто не може бути впевненим, що довільна множина P програмних властивостей, записаних в деякій сигнатурі (наприклад, теоретико-аплікативних та/або теоретико-композиційних), співпадає з множиною всіх істинних програмних властивостей цієї сигнатури; в такій ситуації можливо тільки намагатися застосувати аксіоматичний метод, тобто перевірити, чи всі властивості з множини P є наслідками наївних або вже обгрунтованих властивостей програм, чи ні. У випадку програм (а тому також їх репрезентацій), інкапсуляція таких "наївних" властивостей зовсім не є легким завданням, навіть коли розглядаються "прості" сигнатури. Отже, наведенні аргументи вказують на те, що на поточний час одними з найважливіших задач є задачі накопичення "наївних" та обгрунтування інших істинних властивостей програм. Оскільки лямбда-подібні числення описують теоретико-аплікативні властивості програм, вивчення цих числень, що базується на побудові та дослідженні їх можливих інтенсіональних моделей, які використовують нові поняття неперервної функції обгрунтовує актуальність теми дисертаційної роботи. Також відмітимо, що запропоновані дослідження лежать на границі інформатики та математики, і можуть мати самостійну цікавість для таких математичних дисциплін, як загальна топологія, теорія частково впорядкованих множин та функціональний аналіз.
Актуальність теми. Поняття функції займає одне з самих центральних місць в тих питаннях, які стосуються побудови семантики мов програмування, оскільки кожну комп'ютерну програму можна розглядати як (часткову) функцію, що співставляє вхідним даним програми результат її роботи (якщо він існує). На відміну від класичної математики, яка оперує з екстенсіональним поняттям функції, коли кожна функція ототожнюється зі своїм графіком, з точки зору прикладних та теоретичних питань, які виникають в програмуванні, логиці, дескриптології і т.і., трактування програм як функцій природно вимагає долучити до розгляду інтенсіональні поняття функції, тобто такі, які враховують, окрім графіку функції, також й спосіб її задання. Таким чином, однією з самих важливих проблем в цих наукових галузях є задача про формалізацію інтенсіонального поняття функції, однак спроби дати таке пряме визначення не призвело, на сьогоднішній день, до жодного відповідного загально визнаного задовільного поняття. У зв'язку з цим на передній план вийшли задачі про виявлення, неформальне обгрунтування та опис таких "наївних" загальних властивостей інтенсіональних функцій, яким вони беззаперечно мають задовольняти.
Зокрема, таким чином з'явилися теорія лямбда як (нескінченна) сукупність "наївних" теоретико-аплікативних екваціональних функційних властивостей та лямбда-числення як спеціальна формальна система, яка дозволила надати опис теорії лямбда та провести неформальне обгрунтовання властивостей, що її складають.
Разом із виникненням теорії лямбда, природно постало важливе питання про можливість побудови її теоретико-множинної семантики, тобто про існування конструктивно детермінованих моделей теорії лямбда в рамках класу всіх множин. З точність до теоретико-аплікативних функційних властивостей, що складають теорію лямбда, це питання фактично запитує, чи може теорія множин служити в якості слушного базису для формалізації в ній інтенсіонального поняття функції, чи ні. Окрім вільних моделей з лямбда-термів, починаючи з 1968 р., було побудовано низку класів несинтаксичних "конкретних" теоретико-множинних лямбда-моделей. Однак вичерпної відповіді на це питання немає й досі, оскільки, по-перше, серед останніх, на сьогоднішній день, не було знайдено жодної "точної" моделі (тобто такої, теорія якої співпадає з самою теорією лямбда), та, по-друге, ці моделі мають дуже складну математичну структуру, що заважає використовувати їх на практиці, наприклад, для побудови "зрозумілої" семантики мов програмування.
Це вказує на актуальність побудови нових теоретико-множинних лямбда-моделей. Саме таке спрямування має дана дисертаційна робота; а саме, її присвячено дослідженню можливості побудови нових класів лямбда-моделей на базі підходу, що забезпечується оригінальними визначеннями неперервності функції, яка діє на частково впорядкованих множинах.
Лямбда-подібні числення є найбільш опрацьованим підходом до побудови та вивченню теорії функцій з точки зору їх теоретико-аплікативних властивостей, і вони займають одне з ключових місць в засадах інформатики з точки зору практичних їх застосувань.
Так, наприклад, добре відомо, що всі рекурсивні функції можуть бути представлені лямбда-темами, що означає, що представимість в лямбда-численні може виступати в якості визначення рекурсивної обчислюванності - результат, що має фундаментальне значення як для інформатики, так і для математики. Ця властивість теорії лямбда грає ключову роль в теорії програмування та теорії доказів з наступних причин:
- Лямбда-числення є загальноприйнятим базисом для мов функційного програмування: його можна розуміти як прототип фугкціональної мови в "чистому" вигляді. Підтвердженням цьому служать такі відомі мови програмування, як LISP [1] (1950-e), ML (1970-e) і Standart ML [2] (1980-e), Scheme [3], Miranda [4], Clean [5] і Haskell [6] (1990-е).
- Існує тісний взаємозв'язок між теорією доказів та теорією функцій, що було підтверджено інтерпретацією Колмогорова-Брауера-Гейтинга для інтуїціоністської логіки та ізоморфізмом Каррі-Говарда між натуральним виведенням та типизованим лямбда-численням. Починаючи з 1970 рр., виявилось, що лямбда-подібні числення мають значний прикладний аспект в автоматизації міркувань, особливо в тому, що стосується створення методів, засобів та систем пошуку виведення в логіках вищих порядків, таких як системи Isabelle [7], HOL [8], Nuprl [9], PVS [10] та інші.
Зв'язок роботи з науковими програмами, планами, темами. Дисертаційна робота виконувалась в рамках наукових тем "Логіко-математичні та програмологічні засоби інформаційних технологій" (державний реєстраційний номер 01БФ015-07) та "Розробка конструктивних математичних формалізмів для інтелектуальних систем прийняття рішень, обробки знань, еталонування мов сучасних СУБД та CASE-засобів" (державний реєстраційний номер 06БФ015-05) факультету кібернетики Київського національного університету імені Тараса Шевченка, де автор виконував завдання побудови та вивчення семантик функціональних мов програмування, що задаються на базі лямбда-подібних числень.
Мета і задачі дослідження. Встановити абстрактні властивості нових понять збіжності спрямованості та неперервності функції, які задано на частково впорядкованих множинах. Зробити порівняльний аналіз введених понять з класичними аналогами. Проаналізувати можливість побудови моделей теорії лямбда на базі нових понять неперервної функції. Якщо це виявиться можливим, побудувати нові класи теоретико-множинних лямбда-алгебр (лямбда-моделей), що не є ізоморфними жодній лямбда-алгебрі (лямбда-моделі) Скотта. Тим самим перевірити "повноту" класу моделей Скотта в класі всіх теоретико-множинних лямбда-моделей для потреб програмування з точки зору функціональної парадигми.
Об'єкт дослідження. Об'єктом досліджень є такі моделі лямбда-подібних числень, які базуються на спеціальних поняттях неперервної функції. Тому предметом дослідження є спрямованості над частково впорядкованими множинами, спеціальні поняття неперервності функції, яке введено автором, нові моделі лямбда-подібних числень, як в самостійному контексті, так і в контексті їх порівняння з моделями Скотта.
Методи дослідження базуються на апараті побудови семантик мов функціонального програмування, а також результатах логіко-математичних теорій, таких як теорія частково впорядкованих множин, теорії неперервних відображень спеціальних типів, теорія моделей лямбда-числення.
Наукова новизна одержаних результатів полягає в наступному:
- Проведено аналіз еволюції підходів до побудови теоретико-множинних моделей лямбда-числення та близьких питань; вказано місце одержаних результатів серед інших.
- Розглянуто нові поняття неперервної функції, що діє на частково впорядкованих множинах; сформульовано та доведено оригінальні теоретико-порядкові характеризації відповідних класів неперервних функцій; зроблено порівняльний аналіз цих понять неперервності функції з їх класичними аналогами.
- Показано, що одне з нових понять неперервності функції не призводить до нетривіальних лямбда-моделей, але інші два, що отримуються незначною, на перший погляд, модифікацією цього поняття неперервності функції, навпаки, призводять до нових класів лямбда-моделей, причому серед останніх є, зокрема, нетопологізуємі.
Наукове і практичне значення одержаних результатів. За побудовою можна розрізняти два види теоретико-множинних моделей теорії лямбда: вільні моделі, які будуються з лямбда-термів, та семантичні лямбда-моделі, які будуються за допомогою загальних теоретико-множинних конструкцій. Оскільки лямбда є екваціональною теорією, то для неї звичайним чином конструюються вільні моделі. Втім, початкові спроби побудувати "конкретні" семантичні лямбда-моделі наштовхнулись на значні труднощі, пов'язані, в основному, з тим, що (нетипізований) варіант теорії лямбда не розрізняє поняття функції та аргументу функції. Отже для того, щоб побудувати нетривіальну модель теорії лямбда, природно намагатися знайти таку множину A, яка є рівнопотужною множині AA всіх унарних операцій на A, але це неможливо за теоремою Кантора.
В 1968 р. Д.Скотт обійшов цю перешкоду та побудував перші семантичні лямбда-моделі, звузивши множину AA до множини [A ® A] всіх таких операцій на A, які є неперервними відносно деяких спеціальних топологічних просторів на повних решітках. Пізніше було представлено ще низку класів "конкретних" семантичних лямбда-моделей, але всі вони також базуються на ідеях та конструкціях, які запропонував Д.Скотт: вони будуються, відштовхуючись від класу частково впорядкованих множин і з використанням конструкції прямого або оберненого спектрів, а лямбда-терми інтерпретуються як неперервні в деяких спеціальних сенсах функції, причому неперервність розуміється як неперервність відносно монотонних топологій.
В 1982 р. К.Койманс представив свій метод побудови лямбда моделей, що узагальнює підходи, запропоновані Д.Скоттом та іншими дослідниками, до побудови семантичних теоретико-множинних моделей теорії лямбда. Метод К.Койманса має характеризаційну властивість, згідно якої за цим методом можна побудувати кожну лямбда-модель з точністю до ізоморфізму, і яка дозволяє надати достатні ознаки того, що на базі деякого поняття неперервності функції можна побудувати лямбда-модель.
Маючи на меті побудувати нові класи теоретико-множинних лямбда-моделей, в дисертаційній роботі вводяться і досліджуються нові визначення неперервності функції, яка діє на частково впорядкованих множинах з "достатньою кількістю" супремумів та інфімумів. При цьому, кожне з цих визначень індукує нетопологізуємі класи необов'язково монотонних функцій, на відміну від тих понять неперервної функції, які було застосовано у "класичних" підходах до побудови лямбда-моделей. Використовуючи метод К.Койманса, доводиться, що деякі з цих визначень дійсно індукують нові класи моделей теорії лямбда. Також проводиться загальне теоретичне дослідження одержаних класів лямбда-моделей та їх порівняння зі вже відомими. Це визначає наукове значення роботи.
Дисертація має теоретичну спрямованість. Але, з практичної точки зору, отримані результати в перспективі можуть бути застосовано в загальній теорії програм, при побудові та опису різних мов функціонального програмування, а також в теорії пошуку виведення в логіках вищих порядків.
Особистий внесок здобувача. Всі дослідження, що представлено в дисертації, отримано здобувачем особисто.
Апробація результатів дисертації. Основні результати роботи докладалися на наукових семінарах на факультеті кібернетики Київського національного університету імені Тараса Шевченка та в Інституті кібернетики НАН України, а також на:
o III Міжнародної алгебраїчної конференції в Україні, (Львів, Україна, 2003),
o Міжнародної конференції Logic Colloquium 2004” (Турін, Італія, 2004),
o Міжнародної конференції TAAPSD'06 (Київ, Україна, 2006),
o Засіданнях робочих груп Intas-проекту № 05-1000008-8144 "Practical formal verification using automated reasoning and model checking" (Західний університет м. Тімішоара, Румунія, 2006; Московський державний університет, Москва, Росія, 2007), в яких автор представляв групу Київського національного університету.
Публікації. Основні результати дисертації опубліковано у 7 роботах, з яких: 1 стаття - в фаховому журналі [15], 3 - статті у фахових збірниках наукових праць [16-18] і 3 - тези міжнародних конференцій [19-21].
Структура дисертації. Дисертаційна робота складається зі вступу, оформленого у відповідності з вимогами ВАК України, та чотирьох розділів.
В першому розділі приводиться опис виникнення та розвитку лямбда-числення, а також розповідається про його значення в тому, що стосується теоретичних засад інформатики. Надається короткий історичний опис використання лямбда-подібних числень для побудови систем програмування, що базуються на функціональній парадигмі. Також вводяться основні поняття та система позначень, що використовується в дисертаційній роботі.
В другому розділі визначаються та вивчаються властивості лімітів так званих спрямованостей; зокрема, нові поняття ліміту спрямованості порівнюється з їх топологічним аналогом, а також з поняттям (o)-ліміту спрямованості. Ці дослідження є необхідними для визначення понять неперервної функції, що діє на частково впорядкованих множинах.
Самі нові поняття неперервної функції на частково впорякованими множинами вивчаються в третьому розділі. В ньому, зокрема, ці поняття порівнюються з (o)-неперервністю, їх топологічним аналогом, і також, окремо, з неперервністю за Скоттом. Надається теоретико-порядкова характеризація кожного з цих понять. Відмітимо, що це поняття неперервності також природньо виникає в функціональному аналізі, особливо якщо розглядаються частково впорядковані структури (лінійні простори, групи і т.п.).
Четвертий розділ присвячений, головним чином, дослідженню, чи можна на базі нових понять неперервної функції побудувати теоретико-множинні моделі теорії лямбда. За допомогою теоретико-порядкових характеризацій класів неперервних (в нових сенсах) функцій в цьому розділі показується, що перше з понять неперервної функцій, а також (o)-неперервної функції не є придатними для побудови навіть лямбда-алгебр, а інші два,- навпаки, дозволяють будувати лямбда-алгебри та лямбда-моделі.

Список литературы

ВИСНОВКИ

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

СПИСОК ВИКОРИСТАНИХ ДЖЕРЕЛ

1. J.McCarthy Recursive functions of symbolic expressions and their computation by machine, part 1 // Communications of the Associations for Computing Machinery.- v. 3.- N. 4.- 1960.
2. R.Milner, M.Tofte, R.Harper. The Definition of Standard ML. - MIT Press. - 1990.
3. G.Sussman, G.Steele. SCHEME: An Interpreter for Extended Lambda Calculus. - AI Memo 349. - MIT Artificial Intelligence Laboratory.- Cambridge. - Massachusetts. - 1975.
4. А.Филд та П.Харрисон. Функциональное программирование. М.: Мир. - 1993. - 637 с.
5. http://clean.cs.ru.nl/
6. G.Hutton. Programming in Haskell. - Cambrige University Press.- 171 с.
7. L.Paulson. Isabelle: the next seven hundred theorem provers (system abstract) // У кн.: E.Lusk and R. Overbeek (редактори). 9th International Conf. on Automated Deduction (Springer LNCS 310, 1988). - C. 772773.
8. М.Gordon. From LCF to HOL: a short history // (1996).- У кн.: G. Plotkin, C. Stirling, M.Tofte (редактори). Proof, Language, and Interaction. - MIT Press.- 2000.
9. http://www.cs.cornell.edu/Info/Projects/NuPRL/
10.http://pvs.csl.sri.com/
11. A.Church. A set of postulates for the foundation of logic // Annals of Math., 33, С. 346-366 та 34, С. 839-864.- 1932/1933.
12. A.Church. The Calculi of Lambda Conversion. - Princeton University Press.- 1941.
13.D.Scott. Models for the l-calculus . - Рукопис (неопубл.).- 1969.
14.D.Scott. Data types as lattices // SIAM J. of Comp. 1976. 5(3). P. 522-587.
15.А.А.Лялецкий. О некоторых свойствах теоретико-множественных моделей теории лямбда // Математичні машини і системи. - 4. - 2008. C. 10-22.
16.A.A.Lyaletsky. On Some Logical Properties of Intentional Types of Continuity Defined with Respect to Partially Order Relations // Управляющие системы и машины.- 1.- 2004.- С. 4-9.
17.О.О.Лялецький. Про типи збіжності послідовностей та топологічні властивості частково впорядкованих множин // Вісник Київського університету.- 1.- 2008.- С. 121-126.
18.О.О.Лялецький. Про типи неперервності функцій та їх властивості відносно частково впорядкованих множин // Вісник Київського університету. - 1. - 2008. - С. 98-104.
19.A.A.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. - 4-9 August 2003. - C. 139-140.
20.A.A.Lyaletsky. 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. - С. 135.
21.А.А.Лялецкий. Об одном понятии непрерывности функции // Труды Межд. конференции TAAPSD'06. - Киев. - 2006. С. 64-66.
22.A.A.Lyaletsky. Different notions of conuity and intensional models for λ-calculus // Proceedings of the 1st Intas-meeting. Intas Nr 05-1000008-8144. - Timisoara. - 2006. - Web-site.
23.Барендрегт Х. Лямбда-исчисление. Его синтаксис и семантика. - М.: Мир.- 1985. 606 с.
24.J.Hindley, G.Longo. Lambda calculus models and extensionality // Z. Math. Logik Grundl Math. - 26. - 1980. - С. 289-310.
25.K.Koymans. Models of the lambda calculus // Information & Control. - 52. - 1982. - С. 306-332.
26.Д.А.Владимиров. Теория булевых алгебр. - Изд-во Санкт-Петербургского университетата. - 2000. - 616 с.
27.O.Danvy. A Rational Deconstruction of Landin's SECD Machine.- BRICS research report RS-04-30. - 2004.
28.P.Landin. The Next 700 Programming Languages // CACM 9(3). - 1966. - С. 15765.
29.A.Evans. PAL - a language designed for teaching programming linguistics // Proceedings of ACM National Conference. - 1968.
30.Б.З.Вулих. Введение в теорию полуупорядоченных пространств - М.: Изд. физ.-мат. лит-ры. - 1961. - 407 с.
31.H.Barendregt, K.Koymans. Comparing some classes of lambda calculus models. / У кн. J.Hindley, J.Seldin (редактори). To H.B.Curry: Essays on Combinatory Logic, Lambda-Calculus and Forlmalism. - Academic Press. - 1980. - С. 287-302.
32.П.С.Александров. Введение в теорию множеств и общую топологию 2-е вид., М.: УРСС, 2004, 367 с.
33.Г.Гретцер. Общая теория решеток. - М.: Мир. - 1982. - 454 c.
34.Р.Энгелькинг Общая топология. - М.: Мир. - 1986. - 752 с.
35.N.Funayama. Imbedding infinitely distributive lattices complеtelly isomorphically into Boollean algebras // Nagoya Math J. - 15. - С. 71-81.
36.E.Engeler Algebras and Combinators // Algebra Universalis. - 3. - С. 389 -392.
37.В.Горбунов, В.Туманов. Об одном классе решеток квазимного-образий // Алгебра и Логика.- 19.- 1980. - С. 59-80.
38.G.Birkhoff. Moore-Smith convergence in General Topology // Ann. of Math.. - 38. - 1937. - С. 39-56.
39.J.Kelley. Convergence in Topology // Duke Math. J. - 17. - 1950. - С. 277 -283.
40. Дж.Келли. Общая топология. - М.: Наука, 1980.
41.J.Kisynski. Convergence du type L // Coll. Math. - 7. - 1960.- С. 205-221.
42.P.Alexandrov та Uryson P. Une condition necessaire et suffisante pour qu'une classe (L) soit un classe (D) // C.R.Acad.Sci.- 177. - 1923. - С. 1274-1276.
43.P.Uryson. Sur le classes (L) de M.Frechet // Enseign. Math. - 25. - 1926. - С. 77-83.
44.M.Frechet. Sur quelques points du calcul fonctionnel // Rend. del Circ. Mat. di Palermo. - 22. - 1906. - С. 1-74.
45.M. Frechet. Sur la notion de voisinage dans les ensembles abstraits // Bull. Sci. Math. - 42. - 1918. - С. 138-156.
46.G.Plotkin. T as a universal domain // J. Comput.Syst. Sci. - 17. - 1978. - С. 209-236.
47.G.Plotkin. A powerdomain construction // SIAM J. Comput. - 5. - 1976. - С. 452-478.
48.G.Longo. Set theoretical models of lambda calculus: theories, expansions, and isomorphisms // Ann. Pure and Appl. Logic. - 24 - С. 153-188.
49.F.Lawvare (редактор) та інші. Toposes, Algebraic Geometry and Logic // Lecture notes in Mathematics. - 274. - Springer-Verlag. - Berlin. - 1972.
50.L.Kohen (редактор) та інші. Logic, Methotology and Philosophy of Science. - North-Holland. - Amsterdam. - 1982.
51.P.Gianinni, G.Longo. Effectively given domains and lambda calculus semantics. - Dipt. Informatica, - Pisa, Italy, - 1983.

52.J.Stoy. Denotational semantics. The Scott-Strategy approach to Programming Languages. - MIT Press. - Cambridge. - 1982.