Введение

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

Мотивация и интуиция

Основной мотивацией для изучения доменов, которая была инициирована Даной Скотт в конце 1960-х годов, был поиск денотационной семантики лямбда-исчисления. В этом формализме рассматриваются «функции», задаваемые определенными термами в языке. Чисто синтаксическим образом можно перейти от простых функций к функциям, принимающим другие функции в качестве входных аргументов. Используя лишь синтаксические преобразования, доступные в этом формализме, можно получить так называемые комбинаторы фиксированной точки (наиболее известный из которых — комбинатор Y); они, по определению, обладают свойством f(Y(f)) = Y(f) для всех функций f.

Для формулирования такой денотационной семантики можно сначала попытаться построить модель для лямбда-исчисления, в которой каждой лямбда-формуле сопоставляется настоящая (полная) функция. Такая модель формализовала бы связь между лямбда-исчислением как чисто синтаксической системой и лямбда-исчислением как системой обозначений для манипулирования конкретными математическими функциями. Комбинаторное исчисление является одной из таких моделей. Однако элементы комбинаторного исчисления — это функции от функций к функциям; чтобы элементы модели лямбда-исчисления имели произвольную область определения и область значений, они не могли бы быть истинными функциями, а лишь частичными функциями. Скотт обошел эту трудность, формализовав понятие «частичной» или «неполной» информации для представления вычислений, которые еще не вернули результат. Это было смоделировано путем рассмотрения, для каждой области вычислений (например, натуральных чисел), дополнительного элемента, представляющего неопределенный результат, то есть «результат» вычисления, которое никогда не завершается. Кроме того, область вычислений снабжается отношением порядка, в котором «неопределенный результат» является наименьшим элементом. Важным шагом в поиске модели для лямбда-исчисления является рассмотрение только тех функций (на таком частично упорядоченном множестве), которые гарантированно имеют наименьшие фиксированные точки. Множество этих функций вместе с соответствующим отношением порядка снова является «доменом» в смысле теории. Но ограничение подмножеством всех доступных функций имеет еще одно значительное преимущество: можно получить домены, содержащие свои собственные функциональные пространства, то есть функции, которые могут быть применены к самим себе. Помимо этих желательных свойств, теория доменов также допускает привлекательную интуитивную интерпретацию. Как упоминалось выше, области вычислений всегда частично упорядочены. Этот порядок представляет собой иерархию информации или знаний. Чем выше элемент в порядке, тем более конкретным он является и тем больше информации содержит. Нижние элементы представляют собой неполные знания или промежуточные результаты. Вычисление моделируется путем многократного применения монотонных функций к элементам домена для уточнения результата. Достижение фиксированной точки эквивалентно завершению вычисления. Домены предоставляют более подходящую среду для этих идей, поскольку существование фиксированных точек монотонных функций можно гарантировать, и при дополнительных ограничениях их можно приближать снизу.

Руководство по формальным определениям

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

Направленные наборы как конвергентные спецификации

Как упоминалось ранее, теория доменов имеет дело с частично упорядоченными множествами для моделирования области вычислений. Цель состоит в том, чтобы интерпретировать элементы такого порядка как фрагменты информации или (частичные) результаты вычислений, где элементы, расположенные выше в порядке, расширяют информацию элементов, расположенных ниже, согласованным образом. Из этой простой интуиции уже ясно, что домены часто не имеют наибольшего элемента, поскольку это означало бы существование элемента, содержащего информацию обо всех остальных элементах — довольно неинтересная ситуация. Концепция, играющая важную роль в теории, — это направленное подмножество домена; направленное подмножество — это непустое подмножество порядка, в котором для любых двух элементов существует верхняя граница, являющаяся элементом этого подмножества. В свете нашей интуиции о доменах это означает, что любые два фрагмента информации в пределах направленного подмножества согласованно расширяются каким-либо другим элементом в этом подмножестве. Следовательно, мы можем рассматривать направленные подмножества как согласованные спецификации, то есть как множества частичных результатов, в которых никакие два элемента не противоречат друг другу. Эту интерпретацию можно сравнить с понятием сходящейся последовательности в анализе, где каждый элемент более конкретен, чем предыдущий. Действительно, в теории метрических пространств последовательности играют роль, во многих аспектах аналогичную роли направленных множеств в теории доменов. Теперь, как и в случае последовательностей, нас интересует предел направленного множества. Согласно вышесказанному, это будет элемент, являющийся наиболее общей информацией, расширяющей информацию всех элементов направленного множества, то есть уникальный элемент, содержащий ровно ту информацию, которая присутствовала в направленном множестве, и ничего больше. В формализации теории порядка это просто наименьшая верхняя граница направленного множества. Как и в случае с пределом последовательности, наименьшая верхняя граница направленного множества не всегда существует. Естественно, особый интерес представляют те области вычислений, в которых сходятся все согласованные спецификации, то есть в порядках, в которых все направленные множества имеют наименьшую верхнюю границу. Это свойство определяет класс направленно полных частичных порядков, или dcpo для краткости. Действительно, большинство рассмотрений в теории доменов касаются только порядков, которые по крайней мере направленно полны. Из базовой идеи частично заданных результатов как представления неполных знаний вытекает еще одно желательное свойство: существование наименьшего элемента. Такой элемент моделирует состояние отсутствия информации — точку, с которой начинаются большинство вычислений. Его также можно рассматривать как результат вычисления, которое вообще не возвращает никакого результата.

Вычисления и области

Теперь, когда у нас есть некоторые основные формальные описания того, что представляет собой область вычислений, мы можем перейти к самим вычислениям. Очевидно, что это должны быть функции, принимающие входные данные из некоторой вычислительной области и возвращающие выходные данные в некоторой (возможно, другой) области. Однако, естественно ожидать, что выход функции будет содержать больше информации при увеличении информационного содержания входа. Формально это означает, что мы хотим, чтобы функция была монотонной. При работе с dcpos, также желательно, чтобы вычисления были совместимы с образованием пределов направленного множества. Формально это означает, что для некоторой функции f образ f(D) направленного множества D (то есть множество образов всех элементов D) также является направленным множеством и имеет в качестве наименьшей верхней границы образ наименьшей верхней границы D. Можно также сказать, что f сохраняет направленные супремумы. Следует также отметить, что, рассматривая направленные множества из двух элементов, такая функция также должна быть монотонной. Эти свойства приводят к понятию функции Скотта, являющейся непрерывной. Поскольку это часто не вызывает неоднозначности, можно также говорить просто о непрерывных функциях.

Приближение и конечность

Теория доменов – это чисто качественный подход к моделированию структуры информационных состояний. Можно сказать, что что-то содержит больше информации, но величина этой дополнительной информации не уточняется. Тем не менее, существуют ситуации, когда возникает необходимость говорить об элементах, которые в определенном смысле значительно проще (или значительно менее полны), чем данное информационное состояние. Например, в естественном порядке включения подмножеств на некотором булеане (powerset), любой бесконечный элемент (то есть множество) гораздо более "информативен", чем любое его конечное подмножество. Если требуется смоделировать подобное отношение, можно сначала рассмотреть индуцированный строгий порядок < домена, заданного порядком ≤. Однако, хотя это полезное понятие для линейных порядков, оно мало что говорит о частично упорядоченных множествах. Рассматривая снова порядок включения множеств, множество уже строго меньше другого, возможно, бесконечного множества, если оно содержит всего на один элемент меньше. Однако вряд ли можно согласиться с тем, что это отражает понятие "значительно проще".

Базы доменов

Предыдущие размышления порождают еще один вопрос: возможно ли гарантировать, что все элементы домена могут быть получены как предел значительно более простых элементов? Это весьма актуально на практике, поскольку мы не можем вычислить бесконечные объекты, но можем надеяться приблизить их сколь угодно точно. В более общем плане, мы хотели бы ограничиться некоторым подмножеством элементов, достаточным для получения всех остальных элементов как супремумов. Таким образом, основанием частично упорядоченного множества P определяется подмножество B из P, такое что для каждого x из P множество элементов из B, строго ниже x, содержит направленное множество с супремумом x. Частично упорядоченное множество P является непрерывным, если оно имеет некоторое основание. В частности, само P является основанием в данной ситуации. Во многих приложениях в качестве основного объекта изучения рассматриваются непрерывные (d)cpos. Наконец, еще более сильное ограничение на частично упорядоченное множество задается требованием существования основания из конечных элементов. Такое множество называется алгебраическим. С точки зрения денотационной семантики, алгебраические множества особенно хорошо себя ведут, поскольку они позволяют приближать все элементы даже при ограничении конечными. Как отмечалось ранее, не каждый конечный элемент является "конечным" в классическом смысле, и вполне возможно, что конечные элементы образуют несчетное множество. Однако в некоторых случаях основание для частично упорядоченного множества счетно. В этом случае говорят о ω-непрерывном множестве. Соответственно, если счетное основание состоит исключительно из конечных элементов, мы получаем порядок, который является ω-алгебраическим.

Особые типы доменов

Простой частный случай домена известен как элементарный или плоский домен. Он состоит из множества несравнимых элементов, таких как целые числа, а также одного "нижнего" элемента, считающегося меньшим всех остальных элементов. Можно получить ряд других интересных специальных классов упорядоченных структур, которые могут подходить для использования в качестве "доменов". Мы уже упоминали непрерывные и алгебраические позиты. Более специализированными версиями обоих являются непрерывные и алгебраические cpos. Добавляя еще более сильные свойства полноты, получают непрерывные решетки и алгебраические решетки, которые являются просто полными решетками, обладающими соответствующими свойствами. Для алгебраического случая существуют более широкие классы позитов, которые также представляют интерес для изучения: исторически, домены Скотта были первыми структурами, исследованными в теории доменов. Еще более широкие классы доменов составляют домены SFP, домены L и биконечные домены. Все эти классы порядков можно представить в виде различных категорий dcpos, используя монотонные, скоттовски непрерывные или еще более специализированные функции в качестве морфизмов. Наконец, следует отметить, что сам термин "домен" не является строгим и, следовательно, используется лишь как сокращение, когда формальное определение было дано ранее или когда детали несущественны.