О некоторых свойствах теоретико-множественных моделей теории лямбда
Данная работа посвящена исследованию возможности построения теоретико-множественных моделей теории лямбда на базе понятий слабо и сильно непрерывной функции, предложенных автором. В статье доказывается, что, отталкиваясь от понятия слабо непрерывной функции, нельзя строить модели теории лямбда с пом...
Gespeichert in:
| Veröffentlicht in: | Математичні машини і системи |
|---|---|
| Datum: | 2008 |
| 1. Verfasser: | |
| Format: | Artikel |
| Sprache: | Russisch |
| Veröffentlicht: |
Інститут проблем математичних машин і систем НАН України
2008
|
| Schlagworte: | |
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/46821 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Zitieren: | О некоторых свойствах теоретико-множественных моделей теории лямбда / А.А. Лялецкий // Мат. машини і системи. — 2008. — № 4. — С. 10-22. — Бібліогр.: 8 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1860159504992174080 |
|---|---|
| author | Лялецкий, А.А. |
| author_facet | Лялецкий, А.А. |
| citation_txt | О некоторых свойствах теоретико-множественных моделей теории лямбда / А.А. Лялецкий // Мат. машини і системи. — 2008. — № 4. — С. 10-22. — Бібліогр.: 8 назв. — рос. |
| collection | DSpace DC |
| container_title | Математичні машини і системи |
| description | Данная работа посвящена исследованию возможности построения теоретико-множественных моделей теории лямбда на базе понятий слабо и сильно непрерывной функции, предложенных автором. В статье доказывается, что, отталкиваясь от понятия слабо непрерывной функции, нельзя строить модели теории лямбда с помощью метода Скотта, однако родственное ему понятие сильно непрерывной функции ведет к построению новых лямбда-алгебр и лямбда-моделей.
Роботу присвячено дослідженню можливості побудови теоретико-множинних моделей теорії лямбда на базі понять слабкої та сильно неперервної функції, запропонованих автором. В статті доводиться, що, відштовхуючись від поняття слабко неперервної функції, не можна будувати моделі за методом Скотта, але поняття сильно неперервної функції, що є дуже близьким до попереднього, призводить до побудови нових лямбда-алгебр та лямбда-моделей.
The paper is devoted to investigating the possibility of set-theoretical models of theory lambda on the base of the author's notions of weak and strong continuities of a function. The author proofs that starting with the notion of a weekly continuous function, one cannot construct models by means of the Scott method; nevertheless, the close notion of a strongly continuous function leads to new lambda-algebras and lambda-models.
|
| first_indexed | 2025-12-07T17:54:11Z |
| format | Article |
| fulltext |
10 © Лялецкий А.А., 2008
ISSN 1028-9763. Математичні машини і системи, 2008, № 4
ОБЧИСЛЮВАЛЬНІ СИСТЕМИ
УДК 510.67:512.562:515.126.2:519.767
А.А. ЛЯЛЕЦКИЙ
О НЕКОТОРЫХ СВОЙСТВАХ ТЕОРЕТИКО-МНОЖЕСТВЕННЫХ МОДЕЛЕЙ
ТЕОРИИ ЛЯМБДА
Abstract: The paper is devoted to investigating the possibility of constucting set-theoretical models of theory lambda
on the base of the author's notions of weak and strong continuities of a function. The author proofs that having started
with the notion of a weekly continuous function, one cannot obtain, by means of the Scott method, non-trivial lmodels
of theory lambda; nevertheless, the close notion of a strongly continuous function leads to new lambda-algebras and
lambda-models.
Key words: lambda theory, continuity of a function, lambda-calculus, lambda-algebra, lambda-model, Scott's
topology.
Анотація: Роботу присвячено дослідженню можливості побудови теоретико-множинних моделей теорії
лямбда на базі понять слабкої та сильно неперервної функції, запропонованих автором. В статті
доводиться, що, відштовхуючись від поняття слабко неперервної функції, не можна будувати моделі за
методом Скотта, але поняття сильно неперервної функції, що є дуже близьким до попереднього, навпаки,
призводить до побудови нових лямбда-алгебр та лямбда-моделей.
Ключові слова: теорія лямбда, неперервність функції, лямбда-числення, лямбда-алгебра, лямбда-модель,
топологія Скотта.
Аннотация: Данная работа посвящена исследованию возможности построения теоретико-
множественных моделей теории лямбда на базе понятий слабо и сильно непрерывной функции,
предложенных автором. В статье доказывается, что, отталкиваясь от понятия слабо непрерывной
функции, нельзя построить модели теории лямбда с помощью метода Скотта, однако родственное ему
понятие сильно непрерывной функции, наоборот, ведет к построению новых лямбда-алгебр и лямбда-
моделей.
Ключевые слова: теория лямбда, непрерывность функции, лямбда-алгебра, лямбда-модель, лямбда-
исчисление, топология Скотта.
1. Введение
Лямбда-подобные исчисления представляют собой наиболее теоретически проработанный подход
к построению и изучению теории функций с точки зрения их теоретико-аппликативных свойств и по
праву занимают одно из ключевых мест в математических основаниях математики и информатики.
Так, например, хорошо известно, что все рекурсивные функции представимы лямбда-термами, что
означает, что определимость в лямбда-исчислении может выступать в качестве определения
рекурсивной вычислимости – результат, лежащий в основах как компьютерных наук, так и
математики. Это свойство лямбда-подобных исчислений играет ключевую роль в теории
программирования и теории доказательств по следующим причинам:
Лямбда-исчисление является общепринятым базисом для языков функционального
программирования: оно может рассматриваться как прототип функционального языка в "чистом"
виде. На его базе, в частности, построены такие широко используемые языки программирования,
как LISP (1950-e) , ML (1970-e) , SML (1980-e), Scheme, Hope, Miranda, Clean и Haskell (1990-е).
Существует тесная взаимосвязь между теорией доказательств и теорией функций, что
было подтверждено интерпретацией Колмогорова-Брауэра-Гейтинга для интуиционистской логики
и изоморфизмом Карри-Говарда между натуральным выводом и типизированным лямбда-
исчислением. Начиная с 1970-х годов, оказалось, что лямбда-подобные исчисления имеют
ISSN 1028-9763. Математичні машини і системи, 2008, № 4
11
глубокий прикладной аспект в автоматизации рассуждений в той ее части, которая касается
создания средств, методов и систем поиска вывода в логиках высших порядков, таких, как системы
Isabelle, HOL, Nuprl, PVS и др.
Изначально построенная Черчем как определенная синтаксическая система в 1930-х годах
[1], лямбда-исчисление более 35 лет не имело никакой своей разумной семантики в теоретико-
множественных терминах. Только в 1969 г. Дана Скотт [3] предложил ограничиться рассмотрением
так называемых топологических моделей, построенных на его определении непрерывной функции,
которая действует на полных решетках, и приведших к определенному соответствию между
синтаксисом лямбда-подобных исчислений и семантикой Скотта. Модели Скотта были приняты за
"канонические" для лямбда-исчисления; также были построены другие модели лямбда-подобных
исчислений, базирующихся на конструкциях, которые использовал Скотт. Однако вне поля зрения
исследователей остался следующий вопрос: можно ли ввести такие понятия непрерывной
функции, которые, с одной стороны, определяют классы функций, отличные от классов функций,
непрерывных по Скотту, а, с другой стороны, также приводят к теоретико-множественным моделям
лямбда-подобных исчислений. В данной работе описан возможный подход к решению этой
проблемы.
2. Общие замечания и предварительные сведения
Несмотря на то, что понятие программы уже давно стало интерсубъективным как в
программировании (информатике), так и в обыденной жизни, теоретически и практически
обусловленные потребности программирования нуждаются в экспликации как самого понятия
программы, так и его производных, таких как понятие процесса выполнения программы, ее
конструктивности, ее дескриптивной определенности и т.д. Первое, что приходит на ум,- это
попробовать представить программы как некоторые специальные функции; такой подход известен
как функциональная парадигма программирования. Но, к сожалению, на современном этапе нет ни
одной широко известной функциональной экспликации понятия программы, что имеет под собой в
основании несколько фундаментальных причин (см. ниже). Это, в частности, означает, что в общем
случае нельзя быть уверенным, что произвольное множество P программных свойств, записанных
в некоторой сигнатуре (например, теоретико-аппликативных и/или теоретико-композиционных),
совпадает с множеством всех истинных программных свойств этой сигнатуры; в такой ситуации
возможно только пытаться применить так называемый аксиоматический метод, т.е. пытаться
проверить, верно ли, что все свойства из множества P являются следствиями наивных или уже
обоснованных свойств программ, или нет. А в случае программ (а поэтому и их репрезентаций,
представлений) инкапсуляция таких "наивных" свойств отнюдь не является простой задачей, даже
в случаях, когда рассматриваются бедные сигнатуры. Итак, приведенные аргументы указывают на
то, что на сегодняшний день одной из самых важных задач программирования являются задачи
накопления "наивных" и обоснование других истинных свойств программ.
В связи с этим следует отметить, что представления программ в функциональном виде
должны удовлетворять следующим двум условиям, которые отражают соответствующие свойства
программ. Во-первых, при прикладном анализе программ, как правило, существенными
ISSN 1028-9763. Математичні машини і системи, 2008, № 4
12
оказываются не только функции-графики типа "входные данные – выходные данные", которые они
задают, но и сам способ задания (определения) этих функций, причем иногда случается, что для
некоторой задачи математически существует функция, представляющая ее решение, но
неизвестно, возможно ли написать программу, реализующую эту функцию (а иногда даже удается
доказать, что такой программы не существует); поэтому функции, которые претендуют на то, чтобы
выступать в качестве репрезентаций программ, должны иметь интенсиональную природу (т.е. их
определения должны вводить в рассмотрение не только их графики, но и способ их задания). Во-
вторых, на практике встречаются программы, которые могут быть применены сами к себе; поэтому
функции, которые их представляют, должны допускать самоприменение, и, более того, вроде бы не
видно значимых причин отличать такие функции и их аргументы. С точки зрения инкапсуляции
теоретико-аппликативных свойств функций (и их представлений), эти два условия неявно
определяют некоторый соответствующий язык (состоящий из так называемых лямбда-термов)
дескрипций функций, причём второе условие вместе с наивными свойствами аппликации
определяет эквациональную теорию, известную как теория лямбда. Эта теория описывается и
неформально обосновывается с помощью специального исчисления, предложенного А. Черчем в
начале 30-х годов [1, 2], которое и называется лямбда-исчислением.
Сразу после возникновения теории лямбда встал следующий естественный вопрос:
существует ли ее модель в рамках теории множеств, и, вообще, что следует понимать под
теоретико-множественной моделью теории лямбда? Этот вопрос оказался очень сложным и был
открыт более 35-ти лет, что имеет своей причиной следующее. На синтаксическом уровне теория
лямбда не различает понятия функции и аргумента функции. Поэтому для того, чтобы построить
модель теории лямбда, естественно пытаться построить такое множество A , которое равномощно
множеству AA всех (обычных теоретико-множественных) унарных операций на A , что невозможно
по теореме Кантора о мощности множеств. Поэтому может сложиться ложное мнение, что теория
лямбда не может быть интерпретирована в классе всех множеств.
Но в 1969 г. Д.Скотт смог обойти эту трудность и построить лямбда-модель, урезав AA до
множества [ ]AA → непрерывных операций на некоторых специально подобранных
топологических пространствах [3]. Более точно, он показал, как можно произвольную решетку A
пополнить до такой полной решетки B, которая полно изоморфна [ ]BB → . При этом такая
решетка B по построению является пределом линейного прямого спектра, который состоит из
решеток 0B , ,...,...,1 iBB ( )Ni ∈ , где AB =0 , [ ]iii BBB →=+1 , и гомоморфизмов-экспонент
1: +→ iii BBϕ , сопоставляющих каждому элементу iBb ∈ операцию ibϕ на iB , которая
тождественно равна ibϕ . В этом построении центральное место занимают следующие
наблюдения:
а) результирующая решетка B является пределом прямого спектра, состоящего из
решеток ,...,...,, 21 iBBB и тех же гомоморфизмов iϕ { }( )0\Ni ∈ ;
ISSN 1028-9763. Математичні машини і системи, 2008, № 4
13
б) если обычным образом отождествить каждую из решеток iB ( )Ni ∈ с соответствующей
подрешеткой решетки B , то операция "аппликации" на B по построению является, для каждого i ,
продолжением операции аппликации элементов-операций решетки [ ]iii BBB →=+1 к элементам
iB .
Также отметим, что аналогичную конструкцию можно провести, исходя из произвольного
множества A и положив [ ]AA → равным множеству AA всех унарных операций на A (т.е. все
унарные операции непрерывны). Это действительно так, но, как мы уже убедились выше, это не
приведет к моделям лямбда-исчисления. Грубо говоря, причину этого можно усмотреть в том, что
мощность множества AA всех операций на A слишком "велика" по сравнению с мощностью A .
Поэтому возникает вопрос: а можно ли естественно расширить понятие непрерывной
функции, в сравнении с непрерывностью по Скотту, таким образом, чтобы существовали
множества B , изоморфные (равномощные) множеству [ ]BB → всех непрерывных операций на
B ?
Решению этого вопроса как раз и посвящена данная работа. А именно, показано, что на
некотором специальном классе Κ частично упорядоченных множеств можно естественным
образом ввести понятие непрерывной функции, действующей на Κ , так, что для произвольного
частично упорядоченного множества < A , ≤> каждая непрерывная (в новом смысле) операция на
A является непрерывной по Скотту, но не наоборот в случае нетривиального < A , ≤>; однако при
применении этого нового понятия непрерывной функции также удается, используя ту же
конструкцию предела прямого спектра, построить модели теории лямбда. Кроме того, оказывается,
что таким образом можно, в частности, получить такие модели теории лямбда, которые как
алгебраические структуры не изоморфны ни одной модели Скотта.
3. Краткое описание теории лямбда
Совокупность T всех лямбда-термов – это совокупность слов в алфавите, состоящем из символов:
,..., 10 xx – переменные,
λ – абстрактор,
( ), – скобки,
которая индуктивно определяется правилами:
Tx ∈ (где x – односимвольное слово),
( ) TxtTt ∈⇒∈ λ ,
( ) TttTtt ∈⇒∈ 1010 , .
Для произвольных Ttt ∈10 , и переменной x через [ ]10 : txt = будем обозначать лямбда-
терм, который является результатом подстановки терма 1t в терм 0t вместо переменной x .
ISSN 1028-9763. Математичні машини і системи, 2008, № 4
14
По определению, лямбда-равенство – это выражение (слово) вида 10 tt = , где 0t , 1t –
лямбда-термы, =a – символ равенства. Теория лямбда – это совокупность лямбда-равенств,
которая определяется с помощью следующих аксиом и правил вывода (вместе образующие так
называемое лямбда-исчисление):
аксиомы:
tt = ,
( )( ) [ ]1010 : txttxt ==λ ( β -конверсия);
правила вывода:
0110 tttt =⇒= ,
10 tt = & 2021 tttt =⇒= ,
10 tt = ( ) ( )10 tttt =⇒ ,
10 tt = ( ) ( )tttt 10 =⇒ ,
10 tt = ( ) ( )10 xtxt λλ =⇒ (правило ξ ),
причем аксиома β -конверсии ограничивается условием, что терм 0t является свободным для
подстановки терма 1t вместо переменной x (т.е. каждая из переменных, которая свободно входит
в терм 1t , не становится связанной в терме [ ]10 : txt = ).
По техническим соображениям и для удобства многие авторы рассматривают каждый терм
с точностью до замены в нем свободных и связанных переменных на новые, т.е. если y –
переменная, которая не входит в запись терма t , то термы t и [ ]yxt =: отождествляются. Легко
видеть, что в лямбда-исчислении утверждение о выводимости равенства 10 tt = эквивалентно
утверждению о выводимости равенства [ ]yxtt == :10 , где y – произвольная переменная, которая
не входит в запись терма 1t . (Некоторые авторы предпочитают формально отличать термы t
[ ]yxt =: ; в таком случае к лямбда-исчислению добавляют еще одну аксиому:
[ ]yxtt == : , где y – произвольная переменная, которая не входит в запись терма t .)
Тот факт, что равенство 10 tt = можно вывести в лямбда-исчислении, мы будем обозначать
следующим образом: λ ⊢ 10 tt = .
4. Теоретико-множественные интерпретации теории лямбда
Через { },..., 10 xxX = обозначим совокупность всех переменных.
Пусть Α = A< •> – группоид, т.е. произвольная алгебраическая система с основным
множеством-носителем A и единственной главной бинарной операцией •. Группоид Α
ISSN 1028-9763. Математичні машини і системи, 2008, № 4
15
называется экстенсиональным, если для любых его элементов 0a и 1a из того, что для каждого
элемента b выполняется 0a • b = 1a • b , следует 10 aa = .
Через Val( Α ) = Val( A ) обозначим совокупность всех оценок переменных из X в группоиде
Α , т.е. совокупность всех отображений из X в A . Если ρ – такая оценка и Aa ∈ , то через
[ ]ax =:ρ будем обозначать оценку, которая совпадает с ρ на все элементах, кроме, возможно,
переменной x , на которой она принимает значение a .
По определению, интерпретация в группоид Α – это такое отображение I: T×Val( Α ) → A ,
которое удовлетворяет следующим условиям (где I ( )ρ,t обозначается как [ ]ρt :
1) [ ] ( )xx ρρ = ,
2) ( )[ ] [ ]ρρ 010 ttt = • [ ]ρ1t ,
3) ( )( )[ ] [ ] [ ]bxttxt == :010 ρρλ , где [ ]ρ1tb = ,
4) ρ↓FV ( ) =t ρ`↓FV ( ) [ ] [ ] 'ρρ ttt =⇒ ,
где FV ( )t – множество всех свободных переменных в терме t .
При этом [ ]ρt называется интерпретацией терма t при оценке ρ (и при интерпретации I ).
Отметим, что каждая интерпретация удовлетворяет условию:
3`) ( )[ ]ρλxt • [ ] [ ]axta == :ρ для каждого элемента Aa ∈ ,
и в действительности условие 3) в определении интерпретации может быть равноценно заменено
на условие 3`).
Аппликативной системой называется пара < Α , I >, где Α – группоид и I – интерпретация
в Α ; аппликативные системы мы будем, как правило, обозначать тем же символом Α .
Говорят, что лямбда-равенство 10 tt = выполняется в аппликативной системе Α = >Α< I,
(или в группоиде Α при интерпретации I ) при оценке ρ, в том и только том случае, если
[ ] [ ]ρρ 10 tt = , и тогда пишут Α , ρ ⊨ 10 tt = . Если же отношение Α , ρ ⊨ 10 tt = имеет место при
любой оценке ρ в Α , то тогда просто говорят, что равенство 10 tt = выполняется в аппликативной
системе Α , и пишут Α ⊨ 10 tt = .
Аппликативная система Α называется лямбда-алгеброй, если выполняется импликация
λ ⊢ 10 tt = ⇒ A ⊨ 10 tt = .
Аппликативная система Α называется лямбда-моделью, если для любой оценки ρ в Α
из того, что для любых элемента Aa ∈ и переменной x выполняется [ ] [ ] [ ] [ ]axax tt == = :1:0 ρρ ,
следует, что ( )[ ] ( )[ ]ρρ λλ 10 xtxt = .
ISSN 1028-9763. Математичні машини і системи, 2008, № 4
16
Оказывается, что последнее условие является достаточным для того, чтобы Α была
лямбда-алгеброй.
Теорема 1. Каждая лямбда-модель является лямбда-алгеброй [4].
Приведенная терминология хотя и устоялась на сегодняшний день, но является несколько
неудачной, поскольку, когда говорят о теоретико-множественных интерпретациях (т.е. "моделях")
теории лямбда, под ними, как правило, понимают лямбда-алгебры; кроме того, с точки зрения
абстрактных теорий моделей, как раз понятие лямбда-алгебры является уточнением понятия
модели в контексте теории лямбда.
Приведем другие центральные определения и результаты, которые устанавливают
взаимосвязь между лямбда-алгебрами и лямбда-моделями.
Морфизмом одной лямбда-алгебры 0Α в другую 1Α называется любое отображение
10: AA →ϕ , такое, что для любых терма t и оценки ρ в 0Α выполняется [ ]( ) [ ]ρϕϕ tt p = . Заметим,
что из того, что ϕ – морфизм 0Α в 1Α как лямбда-алгебр, следует, что ϕ – гомоморфизм 0Α в
1Α как группоидов, но, вообще говоря, не наоборот.
Теорема 2. Аппликативная система Α является лямбда-алгеброй в том и только том
случае, когда она вкладывается в лямбда-модель [5].
Теорема 3. Существует лямбда-модель, которая не вкладывается ни в одну
экстенсиональную лямбда-модель [5].
Отметим, что исторически вначале было дано другое определение понятий лямбда-
алгебры (как группоида, сигнатура которого пополнена двумя специальными константными
символами и который удовлетворяет двум специальным тождествам) и лямбда-модели (как такого
группоида с двумя константами, который, кроме равенств для лямбда-алгебр, также удовлетворяет
одному специальному квазитождеству), а понятие морфизма таких лямбда-алгебр (лямбда-
моделей) было определено как обычный алгебраический гомоморфизм этих структур [6].
Наши же определения, правда, с некоторыми незначительными изменениями,
придерживаются работы [4], где, в частности, доказано, что каждое из понятий лямбда-алгебры
вместе с соответствующими морфизмами индуцируют изоморфные между собой категории; то же
самое касается лямбда-моделей.
5. Топологии Скотта
Как уже отмечалось выше, при построении своих лямбда-моделей Д. Скотт ограничил, для каждой
полной решетки Α , множество AA всех операций на A до множества [ ]SAA → всех таких и
только таких операций, которые непрерывны в подходящей топологии на Α , и затем установил
равномощность (изоморфизм между) A и [ ]SAA → [3]. На основании этого свойства, а также
некоторых других, ему удалось построить теоретико-множественные модели теории лямбда (см.
следующий разд.). Позже его результаты были обобщены на так называемые полные частично
упорядоченные множества [6]. Здесь мы приведем только базовые определения и самые основные
свойства введенных им топологических пространств.
ISSN 1028-9763. Математичні машини і системи, 2008, № 4
17
Непустое частично упорядоченное множество < A , ≤> называется полным (сокращенно –
п.ч.у.м.) в том и только том случае, когда оно содержит супремум каждой своей непустой цепи
(некоторые авторы дополнительно требуют, чтобы < A , ≤> содержало наименьший элемент; мы от
этого отказываемся).
Для каждого п.ч.у.м. Α = < A , ≤> через AT обозначим топологию на A , в которой
подмножество AB ⊆ является открытым в том и только том случае, когда оно удовлетворяет
условиям:
1) AC ⊆∀ ( C – направленное & sup ≠∩⇒∈ BCBC ∅);
2) 1010 (, aaAaa ≤∈∀ & )10 BaBa ∈⇒∈ .
AT называется топологией Скотта на Α .
Заметим, что для каждого элемента Ab ∈ множество ( ){ }baAaX b ≤¬∈= | является
открытым, и поэтому топологии Скотта являются 0T -пространствами и в невырожденных случаях
не являются 1T -пространствами.
Теорема 4. Пусть 0Α и 1Α – п.ч.у.м. Произвольная функция f : 10 AA → в том и только
том случае является непрерывной функцией из топологии Скотта на 0Α в топологию Скотта на
1Α , когда для любой цепи 0AC ⊆ выполняется равенство (sup C) = sup f(C) [3, 6].
Теорема 5. Пусть 0Α , 1Α и Β – п.ч.у.м. Тогда f : 0Α × 1Α → B является непрерывной
функцией из топологии Скотта на 0Α × 1Α в топологию Скотта на B в том и только том случае,
когда f непрерывна по каждому аргументу [3, 6].
Для каждых п.ч.у.м. 0Α и 1Α через [ ]S10 Α→Α обозначим п.ч.у.м., состоящее из
непрерывных функций из 0A в 1A относительно соответствующих топологий Скотта с
покоординатным упорядочением.
Теорема 6. Для каждого п.ч.у.м. Α "операция" аппликации [ ] Α→Α×Α→ΑΑ S:α ,
которая сопоставляет каждым [ ]Sf Α→Α∈ и Aa ∈ элемент ( )af , является непрерывной
функцией из топологии Скотта на [ ] Α×Α→Α S в топологию Скотта на Α [3, 6].
6. Метод Скотта построения моделей теории лямбда: общие черты
При построении теоретико-множественных моделей теории лямбда, как правило, используется
следующий метод (или его модификации), при формулировке которого мы будем считать
зафиксированным некоторое выбранное понятие непрерывной функции; он, в частности,
применим, если под непрерывной функцией понимать функцию, которая действует на полных
частично упорядоченных множествах и которая непрерывна по Скотту. Позднее будет введено
новое понятие непрерывности функции, которое будет удовлетворять всем условиям метода, но
приводить к новым лямбда-алгебрам.
ISSN 1028-9763. Математичні машини і системи, 2008, № 4
18
Описание метода. Пусть Κ – класс некоторых теоретико-множественных структур,
замкнутый относительно прямых произведений, и P – некоторое понятие непрерывной функции,
которая действует на структурах из Κ и сопоставляет каждой паре >ΑΑ< 10 , Κ -структур Κ -
структуру [ ] [ ]1010 Α→Α=Α→Α P P -непрерывных функций, причем выполняются условия:
i) произвольная функция Β→Α×Α 10:f P – непрерывна тогда и только тогда, когда f
непрерывна по каждому аргументу;
ii) «операция» аппликации [ ] Α→Α×Α→ΑΑ :α непрерывна для каждой Κ -структуры
Α ;
iii) Κ содержит некоторую рефлексивную структуру Μ (т.е. существуют такие
непрерывные отображения [ ]Μ→Μ→Μ:π и [ ] Μ→Μ→Μ:ψ , что [ ]Μ→Μ= idψπ , где
[ ]Μ→Μid – тождественное отображение на [ ]Μ→Μ ).
На рефлексивной структуре Μ определим бинарную операцию •, полагая для каждых
0m , Μ∈1m ( )( )1010 mmmm π=• . Индуктивно определим интерпретацию I: T×Val Μ→Μ)( в
группоид >•=<Μ ,M , полагая для каждой оценки ρ в Μ :
a) [ ] ( )xx ρρ = , где x – переменная,
b) [ ] [ ] [ ]ρρρ 1010 tttt •= ,
c) ( )[ ] ψλ ρ tfxt = , где MMf t →: – функция, которая сопоставляет каждому Μ∈m
значение [ ] [ ]mxt =:ρ .
Тогда имеют место следующие утверждения:
1) аппликативная система < Μ , I > является лямбда-алгеброй;
2) Μ – лямбда-модель в том и только том случае, когда Μ= idπψ .
Заметим, что К. Койманс сформулировал этот метод на чисто теоретико-категорном языке
и доказал его корректность; а именно, он показал, как в каждой декартово замкнутой категории с
рефлексивным объектом R на совокупности | R | всех морфизмов из R в терминальный объект
этой категории можно так определить группоидную операцию • и интерпретацию I , что
аппликативная система < Λ , I >, где Λ = <| R |, •>, становится лямбда-алгеброй, и что каждую
лямбда-алгебру, с точностью до изоморфизма, можно построить таким способом [7]. Таким
образом, мы по существу переформулировали метод К. Койманса для случая так называемых
конкретных категорий.
7. Новые понятие сходимости последовательности и непрерывности функции
Теперь мы введем новые понятия сходимости направленности и непрерывной функции, которые
заданы на частично упорядоченном множестве (удовлетворяющем некоторым специальным
условиям). Забегая вперед, отметим следующие свойства вводимых понятий непрерывной
функции:
ISSN 1028-9763. Математичні машини і системи, 2008, № 4
19
a) эти понятия вводятся как свойства функции сохранять (соответствующие) пределы
сходящихся последовательностей;
b) на расширенной действительной прямой эти понятия непрерывной функции совпадают с
обычным понятием непрерывной действительной функции (принимающей, возможно, бесконечные
значения);
c) они отличаются от понятия (o) непрерывной функции;
d) каждая функция, непрерывная в новых смыслах, непрерывна по Скотту, но в общем
случае не наоборот.
Под направленностью над множеством A будем понимать функцию, которая действует из
произвольного непустого направленного частично упорядоченного множества во множество A .
Понятия поднаправленности и конфинальной поднаправленности будем понимать обычным
образом. Под монотонной направленностью будем понимать направленность, которая является
либо возрастающей, либо убывающей.
Через Κ обозначим класс всех таких и только таких частично упорядоченных множеств,
которые содержат супремумы всех своих непустых направленных подмножеств и инфимумы всех
своих непустых ко-направленных подмножеств. Элементы класса Κ будем для краткости называть
Κ -ч.у.м. Пусть < A , ≤> – частично упорядоченное множество из Κ . Вначале определим понятие
слабого предела направленности для случая монотонных, а затем – для всех направленностей на
A . Итак, если D – возрастающая (убывающая) направленность, то ее пределом (относительно ≤)
будем считать элемент, равный супремуму (соответственно инфимуму) множества всех элементов
D . Если же D – произвольная направленность на A , то будем говорить, что D слабо сходится к
элементу b в том и только том случае, когда множество всех монотонных конфинальных
поднаправленностей направленности D не пусто, и все они сходятся к элементу b ; в этом случае
будем писать bDw =lim .
Заметим, что если Κ -ч.у.м. < A , ≤> не является линейным, нетрудно построить такую
направленность D , которая содержит элементы, не принимающие участия в определении слабого
предела (т.е. не входящие в состав ни одной монотонной конфинальной поднаправленности
направленности D ); такие элементы мы будем называть нейтральными.
Направленность D на множестве A называется сильно сходящейся к элементу b , если
D слабо сходится к элементу b и не содержит нейтральных элементов. Произвольная функция
10: Α→Αf , действующая из Κ -ч.у.м. < 0A , ≤0> в Κ -ч.у.м. < 1A , ≤1>, называется слабо (≤0,≤1)-
непрерывной, если f сохраняет пределы всех слабо сходящихся направленностей на 0A (т.е. для
любой направленности D на 0A , если существует ≤0- Dwlim , то существует ≤1- )(lim Dfw и
f (≤0- Dwlim ) = ≤1- )(lim Dfw ). Функция f называется сильно непрерывной, если она сохраняет
пределы всех сильно сходящихся направленностей.
Следующие две теоремы устанавливают взаимосвязь введенного понятия непрерывности
функции с понятием функции, которая непрерывна по Скотту.
ISSN 1028-9763. Математичні машини і системи, 2008, № 4
20
Теорема 7.1. Произвольная функция 10: Α→Αf , действующая из Κ -ч.у.м. <A0, ≤0> в Κ -
ч.у.м. < 1A , ≤1>, тогда и только тогда является слабо (≤0,≤1)-непрерывной, когда выполняются
следующие условия:
1) f удовлетворяет условию Скотта, т.е. для любой непустой цепи C , 0AC ⊆
выполняется равенство f (sup С) = sup f (С);
2) каждая бесконечная ≤0-цепь C , 0AC ⊆ имеет такое конечное множество F , CF ⊆ ,
что множество-образ f ( )FC \ является ≤1-цепью;
3) 0A не содержит такую бесконечную ≤0-антицепь E , все элементы множества-образа
)(Ef которой являются попарно ≤1-сравнимыми [8].
Теорема 7.2. В обозначениях предыдущей теоремы f в том и только том случае является
сильно непрерывной, когда выполняется условие (1) предыдущей теоремы, а также условие
3`. Если элементы 0a , 01 Aa ∈ ≤0-сравнимы, то элементы ( )0af и ( )1af ≤1-сравнимы [8].
8. Новые модели теории лямбда
Этот раздел посвящен, в основном, проверке, можно ли использовать понятия непрерывной
функции, введенные и охарактеризованные в предыдущем разделе, для построения лямбда-
алгебр и лямбда-моделей. Из изложенного в предыдущих разделах следует, что нужно, в первую
очередь, проверить истинность свойств i) и ii) из метода Скотта построения моделей теории
лямбда. Что касается свойства i), то все обстоит очень просто.
Теорема 8. Пусть 0Α , 1Α и Β – Κ -ч.у.м. Тогда f : 0Α × 1Α Β→ в том и только том
случае является слабо непрерывной (сильно непрерывной) функцией из Κ -ч.у.м. 0Α × 1Α в Β ,
если f слабо непрерывна (сильно непрерывна) по каждому аргументу.
Для каждых Κ -ч.у.м. 0Α =< 0A , ≤0> и 1Α = < 1A , ≤1> через [ ]w10 Α→Α обозначим Κ -
ч.у.м., состоящее из слабо (≤0,≤1)-непрерывных функций из A0 в A1 с покоординатным
упорядочением.
Теорема 9.1. Для каждого бесконечного Κ -ч.у.м. Α = < A , ≤> "операция" аппликации
[ ] Α→Α×Α→Α wA :α , сопоставляющая каждым [ ]wf Α→Α∈ и Aa ∈ элемент ( )af , не
является непрерывной функцией из Κ -ч.у.м. [ ] Α×Α→Α w в Α .
Через [ ]s10 Α→Α обозначим Κ -ч.у.м., состоящее из сильно непрерывных функций из 0A
в 1A с покоординатным упорядочением.
Теорема 9.2. Для каждого Κ -ч.у.м. Α = < A , ≤> "операция" аппликации
[ ] Α→Α×Α→Α sA :α , сопоставляющая каждым [ ]sf Α→Α∈ и Aa ∈ элемент ( )af ,
является непрерывной функцией из Κ -ч.у.м. [ ] Α×Α→Α s в Α .
ISSN 1028-9763. Математичні машини і системи, 2008, № 4
21
Отметим, что все теоремы 8, 9.1 и 9.2 являются несложными следствиями теорем 7.1 и 7.2.
Таким образом, в силу теоремы 9.1 понятие слабо непрерывной функции не подходит для
построения моделей теории лямбда методом Скотта, в отличие от понятия сильно непрерывной
функции, которое, наоборот, в соответствии с теоремами 8 и 9.2, имеет все первичные признаки в
пользу того, что на его базе удастся построить лямбда-алгебры и лямбда-модели.
Теорема 10. Каждое Κ -ч.у.м. Α можно пополнить до Κ -ч.у.м. Β , которое является
рефлексивным объектом категории, в которой элементы класса K являются объектами, а сильно
непрерывные функции - морфизмами (т.е. существуют такие непрерывные отображения
[ ]sΒ→Β→Β:π и [ ] Β→Β→Β s:ψ , что [ ]BBid →=ψπ . При этом Β является пределом
линейного прямого спектра, который состоит из Κ -ч.у.м. 0Β , ,...,...,1 iΒΒ ( )Ni ∈ , где Α=Β0 ,
[ ]iii Β→Β=Β +1 , и гомоморфизмов-экспонент 1: +Β→Β iiiϕ , которые сопоставляют каждому
элементу ib Β∈ операцию ibϕ на iΒ , тождественно равную этому элементу b .
Приведем схему доказательства теоремы 10. Строим Β так, как указано в условии
теоремы, т.е. B является фактор-множеством [ ]{ }iii aia Β∈>< ≡ |, . На B определяем операцию •,
полагая для каждой пары элементов [ ]≡>< iai , и [ ]≡>< '' , iai множества B значение
[ ] [ ]≡≡ ><•>< '' ,, iaia ii равным классу эквивалентности ≡, содержащему элемент ( )'
1 kk bb +< , >k ,
где i , ki ≤' , >>≡<>>≡<+< +
'''
1 ,,,,1, iakbiakb ikik , и доказываем, что эта операция • сильно
непрерывна по второму аргументу. Вводим сильно непрерывное отображение [ ]sΒ→Β→Β:π ,
для каждого элемента Β∈b полагая bπ равным операции bf , которая каждому
Β∈a сопоставляет значение ab • . Далее, доказываем, что каждый элемент f Κ -ч.у.м.
[ ]Β→Β можно представить в виде сильного предела Dslim направленности D, состоящей из
элементов Κ -ч.у.м. Β (если отождествить каждый элемент b из Β с унарной операцией bc на
Β , тождественно равной b ), а потому f "по непрерывности" однозначно определяется
совокупностью своих значений вида af • , где Β∈a . Последнее свойство дает ключ к
построению искомого отображения [ ] Β→Β→Β s:ψ . Для завершения доказательства остается
лишь доказать сильную непрерывность ψ .
Итак, понятие сильной непрерывности удовлетворяет всем условиям i), ii), iii) метода Скотта
построения моделей теории лямбда. Поэтому имеет место следующее утверждение.
Следствие. Для каждого Κ -ч.у.м. Α через >•=<ΒΑ ,B обозначим группоид, где •
определяется, как в схеме доказательства теоремы 10. Индуктивно определим интерпретацию I в
группоид ΑΒ в соответствии с пунктами 1), 2), 3) метода Скотта построения моделей теории
лямбда. Тогда аппликативная система < ΑΒ , >I является лямбда-алгеброй.
ISSN 1028-9763. Математичні машини і системи, 2008, № 4
22
В дополнение к следствию из теоремы 10 приведем без доказательства еще один
результат, который, по-существу, постулирует, что на базе понятия сильно непрерывной функции
можно строить новые лямбда-модели.
Теорема 11. Существует такое Κ -ч.у.м. Α , что соответствующий группоид >•=<ΒΑ ,B
индуцирует, по методу Скотта, аппликативную систему >Β< Α I, , которая является лямбда-
моделью. При этом Α можно подобрать таким образом, что группоид < B , •> алгебраически не
изоморфен ни одному группоиду Скотта (т.е. группоиду, построенному с помощью метода Скотта
на базе понятия функции, непрерывной по Скотту).
9. Заключение
Приведенные результаты показывают, что даже незначительные изменения понятия непрерывной
функции ведут к существенным изменениям в контексте построения моделей теории лямбда. Так,
на базе одного из введенных понятий непрерывности функции удалось построить такие лямбда-
модели, которые не изоморфны ни одной лямбда-модели Скотта, откуда, в частности, следует, что
семантика Скотта не является исчерпывающей с точностью до алгебраического изоморфизма. Для
другого понятия непрерывной функции удалось доказать, что оно, наоборот, не дает возможность
строить нетривиальные лямбда-алгебры и лямбда-модели.
СПИСОК ЛИТЕРАТУРЫ
1. Church А. A set of postulates for the foundation of logic // Annals of Math. – 1932. – N 33. – P. 346 – 366; 1933. –
N 34. – P. 839 – 864.
2. Church A. The Calculi of Lambda Conversion // Princeton University Press. – 1941. – 68 с.
3. Scott D. Models for the λ-calculus [Рукопись (неопубл.)]. – 1969. – 53 c.
4. Hindley J., Longo G. Lambda calculus models and extensionality // Z Math. Logik Grundl Math. – 1980. – N 26. –
P. 289 – 310.
5. Barendregt H., Koymans K. Comparing some classes of lambda calculus models // To H.B. Curry: Essays on
Combinatory Logic, Lambda-Calculus and Forlmalism / J.Hindley, J.Seldin (eds.). – Academic Press, 1980. – P. 287 –
302.
6. Barendregt H. The Lambda Calculus. Its Syntax and Semantics // North-Holland Publishing Co. – 1981. – 606 с.
7. Koymans K. Models of the lambda calculus // Information & Control. – 1983. – N 52. – P. 306 – 332.
8. Лялецький O. Про типи неперервності функції та їх властивості відносно частково впорядкованих множин //
Вісник КНУ. – 2008. – № 2. – C. 98 – 105.
Стаття надійшла до редакції 15.10.2008
|
| id | nasplib_isofts_kiev_ua-123456789-46821 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1028-9763 |
| language | Russian |
| last_indexed | 2025-12-07T17:54:11Z |
| publishDate | 2008 |
| publisher | Інститут проблем математичних машин і систем НАН України |
| record_format | dspace |
| spelling | Лялецкий, А.А. 2013-07-07T12:25:18Z 2013-07-07T12:25:18Z 2008 О некоторых свойствах теоретико-множественных моделей теории лямбда / А.А. Лялецкий // Мат. машини і системи. — 2008. — № 4. — С. 10-22. — Бібліогр.: 8 назв. — рос. 1028-9763 https://nasplib.isofts.kiev.ua/handle/123456789/46821 510.67:512.562:515.126.2:519.767 Данная работа посвящена исследованию возможности построения теоретико-множественных моделей теории лямбда на базе понятий слабо и сильно непрерывной функции, предложенных автором. В статье доказывается, что, отталкиваясь от понятия слабо непрерывной функции, нельзя строить модели теории лямбда с помощью метода Скотта, однако родственное ему понятие сильно непрерывной функции ведет к построению новых лямбда-алгебр и лямбда-моделей. Роботу присвячено дослідженню можливості побудови теоретико-множинних моделей теорії лямбда на базі понять слабкої та сильно неперервної функції, запропонованих автором. В статті доводиться, що, відштовхуючись від поняття слабко неперервної функції, не можна будувати моделі за методом Скотта, але поняття сильно неперервної функції, що є дуже близьким до попереднього, призводить до побудови нових лямбда-алгебр та лямбда-моделей. The paper is devoted to investigating the possibility of set-theoretical models of theory lambda on the base of the author's notions of weak and strong continuities of a function. The author proofs that starting with the notion of a weekly continuous function, one cannot construct models by means of the Scott method; nevertheless, the close notion of a strongly continuous function leads to new lambda-algebras and lambda-models. ru Інститут проблем математичних машин і систем НАН України Математичні машини і системи Обчислювальні системи О некоторых свойствах теоретико-множественных моделей теории лямбда Про деякі властивості теоретико-множинних моделей теорії лямбда On some properties of set-theory models of lambda theory Article published earlier |
| spellingShingle | О некоторых свойствах теоретико-множественных моделей теории лямбда Лялецкий, А.А. Обчислювальні системи |
| title | О некоторых свойствах теоретико-множественных моделей теории лямбда |
| title_alt | Про деякі властивості теоретико-множинних моделей теорії лямбда On some properties of set-theory models of lambda theory |
| title_full | О некоторых свойствах теоретико-множественных моделей теории лямбда |
| title_fullStr | О некоторых свойствах теоретико-множественных моделей теории лямбда |
| title_full_unstemmed | О некоторых свойствах теоретико-множественных моделей теории лямбда |
| title_short | О некоторых свойствах теоретико-множественных моделей теории лямбда |
| title_sort | о некоторых свойствах теоретико-множественных моделей теории лямбда |
| topic | Обчислювальні системи |
| topic_facet | Обчислювальні системи |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/46821 |
| work_keys_str_mv | AT lâleckiiaa onekotoryhsvoistvahteoretikomnožestvennyhmodeleiteoriilâmbda AT lâleckiiaa prodeâkívlastivostíteoretikomnožinnihmodeleiteoríílâmbda AT lâleckiiaa onsomepropertiesofsettheorymodelsoflambdatheory |