Теория доменов — это раздел математики , который изучает особые виды частично упорядоченных множеств (частично упорядоченных множеств), обычно называемых доменами . Следовательно, теорию доменов можно рассматривать как раздел теории порядка . Эта область имеет основные приложения в информатике , где она используется для определения денотационной семантики , особенно для функциональных языков программирования . Теория доменов формализует интуитивные идеи аппроксимации и сходимости в очень общем виде и тесно связана с топологией .
Основной мотивацией для изучения доменов, которое было инициировано Даной Скотт в конце 1960-х годов, был поиск денотационной семантики лямбда -исчисления . В этом формализме рассматриваются «функции», заданные определенными терминами в языке. Чисто синтаксическим способом можно перейти от простых функций к функциям, которые принимают другие функции в качестве своих входных аргументов. Используя снова только синтаксические преобразования, доступные в этом формализме, можно получить так называемые комбинаторы с фиксированной точкой (наиболее известным из которых является комбинатор Y ); они, по определению, обладают свойством, что f ( Y ( f )) = Y ( f ) для всех функций f .
Чтобы сформулировать такую денотационную семантику, можно было бы сначала попытаться построить модель для лямбда-исчисления, в которой подлинная (общая) функция связана с каждым лямбда-термом. Такая модель формализовала бы связь между лямбда-исчислением как чисто синтаксической системой и лямбда-исчислением как системой обозначений для манипулирования конкретными математическими функциями. Комбинаторное исчисление является такой моделью. Однако элементы комбинаторного исчисления являются функциями от функций к функциям; для того, чтобы элементы модели лямбда-исчисления имели произвольную область и диапазон, они не могли бы быть истинными функциями, а только частичными функциями .
Скотт обошел эту трудность, формализовав понятие «частичной» или «неполной» информации для представления вычислений, которые еще не вернули результат. Это было смоделировано путем рассмотрения для каждой области вычислений (например, натуральных чисел) дополнительного элемента, который представляет неопределенный вывод, т. е. «результат» вычисления, которое никогда не заканчивается. Кроме того, область вычислений снабжена отношением упорядочения , в котором «неопределенный результат» является наименьшим элементом .
Важным шагом к поиску модели для лямбда-исчисления является рассмотрение только тех функций (на таком частично упорядоченном множестве), которые гарантированно имеют наименьшее количество неподвижных точек . Множество этих функций вместе с соответствующим упорядочением снова является «доменом» в смысле теории. Но ограничение подмножеством всех доступных функций имеет еще одно большое преимущество: можно получить домены, которые содержат свои собственные функциональные пространства , т. е. можно получить функции, которые можно применить к самим себе.
Помимо этих желаемых свойств, теория доменов также допускает привлекательную интуитивную интерпретацию. Как упоминалось выше, домены вычислений всегда частично упорядочены. Этот порядок представляет собой иерархию информации или знаний. Чем выше элемент в порядке, тем он конкретнее и тем больше информации он содержит. Более низкие элементы представляют собой неполные знания или промежуточные результаты.
Затем вычисление моделируется путем многократного применения монотонных функций к элементам домена для уточнения результата. Достижение фиксированной точки эквивалентно завершению вычисления. Домены обеспечивают превосходную настройку для этих идей, поскольку фиксированные точки монотонных функций могут гарантированно существовать и, при дополнительных ограничениях, могут быть аппроксимированы снизу.
В этом разделе будут представлены центральные концепции и определения теории доменов. Вышеуказанная интуиция доменов как информационных упорядочений будет подчеркнута для мотивации математической формализации теории. Точные формальные определения можно найти в специальных статьях для каждой концепции. Список общих определений теории порядка, которые включают также понятия теории доменов, можно найти в глоссарии теории порядка . Тем не менее, наиболее важные концепции теории доменов будут представлены ниже.
Как упоминалось ранее, теория доменов имеет дело с частично упорядоченными множествами для моделирования домена вычислений. Цель состоит в том, чтобы интерпретировать элементы такого порядка как фрагменты информации или (частичные) результаты вычислений , где элементы, которые находятся выше в порядке, расширяют информацию элементов, расположенных ниже, согласованным образом. Из этой простой интуиции уже ясно, что домены часто не имеют наибольшего элемента , поскольку это означало бы, что есть элемент, который содержит информацию всех других элементов — довольно неинтересная ситуация.
Важную роль в теории играет концепция направленного подмножества домена; направленное подмножество — это непустое подмножество порядка, в котором любые два элемента имеют верхнюю границу , которая является элементом этого подмножества. Ввиду нашей интуиции о доменах это означает, что любые две части информации в направленном подмножестве последовательно расширяются некоторым другим элементом в подмножестве. Следовательно, мы можем рассматривать направленные подмножества как последовательные спецификации , т. е. как наборы частичных результатов, в которых никакие два элемента не являются противоречивыми. Эту интерпретацию можно сравнить с понятием сходящейся последовательности в анализе , где каждый элемент более конкретен, чем предыдущий. Действительно, в теории метрических пространств последовательности играют роль, которая во многих аспектах аналогична роли направленных множеств в теории доменов.
Теперь, как и в случае последовательностей, нас интересует предел направленного множества. Согласно сказанному выше, это будет элемент, который является наиболее общей частью информации, которая расширяет информацию всех элементов направленного множества, т.е. уникальный элемент, который содержит ровно ту информацию, которая присутствовала в направленном множестве, и ничего больше. В формализации теории порядка это просто наименьшая верхняя граница направленного множества. Как и в случае предела последовательности, наименьшая верхняя граница направленного множества не всегда существует.
Естественно, особый интерес представляют те области вычислений, в которых сходятся все согласованные спецификации , то есть порядки, в которых все направленные множества имеют наименьшую верхнюю границу. Это свойство определяет класс направленно-полных частичных порядков , или dcpo для краткости. Действительно, большинство соображений теории доменов рассматривают только порядки, которые по крайней мере направленно полны.
Из базовой идеи частично определенных результатов как представляющих неполное знание, выводится еще одно желательное свойство: существование наименьшего элемента . Такой элемент моделирует состояние отсутствия информации — место, где начинается большинство вычислений. Его также можно рассматривать как выход вычисления, которое вообще не возвращает никакого результата.
Теперь, когда у нас есть некоторые базовые формальные описания того, какой должна быть область вычислений, мы можем обратиться к самим вычислениям. Очевидно, что это должны быть функции, принимающие входные данные из некоторой области вычислений и возвращающие выходные данные в некоторой (возможно, другой) области. Однако можно также ожидать, что выходные данные функции будут содержать больше информации, когда информационное содержание входных данных увеличивается. Формально это означает, что мы хотим, чтобы функция была монотонной .
При работе с dcpos можно также захотеть, чтобы вычисления были совместимы с формированием пределов направленного множества. Формально это означает, что для некоторой функции f образ f ( D ) направленного множества D (т. е. множество образов каждого элемента D ) снова направлен и имеет в качестве наименьшей верхней границы образ наименьшей верхней границы D . Можно также сказать, что f сохраняет направленные супремумы . Также следует отметить, что при рассмотрении направленных множеств из двух элементов такая функция также должна быть монотонной. Эти свойства приводят к понятию функции, непрерывной по Скотту . Поскольку это часто не является двусмысленным, можно также говорить о непрерывных функциях .
Теория доменов — это чисто качественный подход к моделированию структуры информационных состояний. Можно сказать, что что-то содержит больше информации, но количество дополнительной информации не указано. Тем не менее, существуют некоторые ситуации, в которых хочется говорить об элементах, которые в некотором смысле намного проще (или намного более неполны), чем заданное состояние информации. Например, в естественном порядке включения подмножеств на некотором powerset любой бесконечный элемент (т. е. множество) намного более «информативен», чем любое из его конечных подмножеств.
Если кто-то хочет смоделировать такую связь, он может сначала захотеть рассмотреть индуцированный строгий порядок < домена с порядком ≤. Однако, хотя это полезное понятие в случае полных порядков, оно не говорит нам многого в случае частично упорядоченных множеств. Рассматривая снова порядки включения множеств, множество уже строго меньше другого, возможно бесконечного, множества, если оно содержит всего на один элемент меньше. Однако вряд ли кто-то согласится, что это отражает понятие «намного проще».
Более сложный подход приводит к определению так называемого порядка аппроксимации , который более предположительно также называется отношением «путь-ниже» . Элемент x находится намного ниже элемента y , если для каждого направленного множества D с супремумом таким, что
существует некоторый элемент d в D такой, что
Тогда также говорят, что x приближает y и пишут
Это подразумевает, что
поскольку синглтон-множество { y } направлено. Например, в упорядочении множеств бесконечное множество находится намного выше любого из его конечных подмножеств. С другой стороны, рассмотрим направленное множество (фактически, цепочку ) конечных множеств
Поскольку супремум этой цепочки представляет собой множество всех натуральных чисел N , это показывает , что ни одно бесконечное множество не находится намного ниже N.
Однако, быть намного ниже некоторого элемента — это относительное понятие и не раскрывает многого об элементе в отдельности. Например, хотелось бы охарактеризовать конечные множества в порядково-теоретическом смысле, но даже бесконечные множества могут быть намного ниже некоторого другого множества. Особое свойство этих конечных элементов x заключается в том, что они намного ниже самих себя, т.е.
Элемент с этим свойством также называется компактным . Однако такие элементы не обязательно должны быть «конечными» или «компактными» в любом другом математическом использовании этих терминов. Тем не менее, обозначение мотивировано определенными параллелями с соответствующими понятиями в теории множеств и топологии . Компактные элементы домена обладают важным специальным свойством, заключающимся в том, что они не могут быть получены как предел направленного множества, в котором они уже не встречались.
Многие другие важные результаты, касающиеся отношения «путь-вниз», подтверждают утверждение, что это определение подходит для охвата многих важных аспектов предметной области.
Предыдущие мысли поднимают другой вопрос: можно ли гарантировать, что все элементы домена могут быть получены как предел гораздо более простых элементов? Это весьма актуально на практике, поскольку мы не можем вычислить бесконечные объекты, но мы все еще можем надеяться приблизить их произвольно близко.
В более общем смысле, мы хотели бы ограничиться определенным подмножеством элементов, достаточным для получения всех остальных элементов как минимальных верхних границ. Следовательно, мы определяем базу частично упорядоченного множества P как подмножество B множества P , такое, что для каждого x в P множество элементов в B , которые находятся намного ниже x , содержит направленное множество с супремумом x . Частично упорядоченное множество P является непрерывным частично упорядоченным множеством, если оно имеет некоторую базу. В частности, само P является базой в этой ситуации. Во многих приложениях мы ограничиваемся непрерывным (d)cpos как основным объектом изучения.
Наконец, еще более сильное ограничение на частично упорядоченное множество задается требованием существования базы конечных элементов. Такой посет называется алгебраическим . С точки зрения денотационной семантики алгебраические посеты ведут себя особенно хорошо, поскольку они допускают аппроксимацию всех элементов даже при ограничении конечными. Как отмечалось ранее, не каждый конечный элемент является «конечным» в классическом смысле, и вполне может быть, что конечные элементы составляют несчетное множество .
В некоторых случаях, однако, база для частично упорядоченного множества является счетной . В этом случае говорят о ω-непрерывном частично упорядоченном множестве. Соответственно, если счетная база состоит полностью из конечных элементов, мы получаем порядок, который является ω-алгебраическим .
Простой частный случай домена известен как элементарный или плоский домен . Он состоит из набора несравнимых элементов, таких как целые числа, вместе с одним «нижним» элементом, который считается меньшим, чем все остальные элементы.
Можно получить ряд других интересных специальных классов упорядоченных структур, которые могли бы быть подходящими в качестве «доменов». Мы уже упоминали непрерывные частично упорядоченные множества и алгебраические частично упорядоченные множества. Более специальные версии обоих — непрерывные и алгебраические cpos . Добавляя еще больше свойств полноты, можно получить непрерывные решетки и алгебраические решетки , которые являются просто полными решетками с соответствующими свойствами. Для алгебраического случая можно найти более широкие классы частично упорядоченных множеств, которые все еще стоит изучать: исторически домены Скотта были первыми структурами, которые изучались в теории доменов. Еще более широкие классы доменов состоят из SFP-доменов, L-доменов и биконечных доменов.
Все эти классы порядков могут быть преобразованы в различные категории dcpos, используя функции, которые являются монотонными, непрерывными по Скотту или даже более специализированными как морфизмы . Наконец, обратите внимание, что сам термин домен не является точным и, таким образом, используется только как аббревиатура, когда формальное определение было дано ранее или когда детали не имеют значения.
Посет D является dcpo тогда и только тогда, когда каждая цепь в D имеет супремум. (Направление «если» основано на аксиоме выбора .)
Если f — непрерывная функция в области D , то она имеет наименьшую неподвижную точку, заданную как наименьшая верхняя граница всех конечных итераций f на наименьшем элементе ⊥:
Это теорема Клини о неподвижной точке . Символ — направленное соединение .
Пространство непрерывности — это обобщение метрических пространств и частично упорядоченных множеств , которое можно использовать для унификации понятий метрических пространств и областей.
