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

Краткое содержание

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

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

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

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

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

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

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

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

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

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

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

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

            Для кожної множини А через D_A будемо позначати клас всіх спрямованостей над A. Для кожного топологічного простору T над множиною A через lim_T позначимо часткове відображення lim_T: D_A ® A, яке кожній спрямованості над 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^≤ та топологію S^≤-1, що є дуальною до останньої.

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

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

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

            Через 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, тобто сукупність всіх відображень r: X ® A. Лямбда-інтерпретацією в групоїд A називається будь-яке відображення I: T´Val(A) ® A, яке задовольняє наступним умовам (де I(t, r) позначається як [t]_r):

1)     [x]_r = r(x);

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

ii)      [t₀t₁]_r = [t₀]_r·[t₁]_r;

iii)    [lx.t]_r = f_ty,

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

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

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

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

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

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

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

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

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

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

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

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

ВИСНОВКИ

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

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

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

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

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