도메인 이론

이 문서에는 참고 자료, 관련 읽기 또는 외부 링크가 포함되어 있지만 인라인 인용이 부족하여 출처가 불분명합니다. 좀 더 정밀한 인용문을 도입하여 이 글의 개선에 도움을 주시기 바랍니다.(2022년 6월) (이 템플릿메시지를 삭제하는 방법과 타이밍에 대해 설명합니다)

도메인 이론은 일반적으로 도메인이라고 불리는 부분 순서 집합의 특별한 종류를 연구하는 수학의 한 분야이다.따라서 도메인 이론은 순서론의 한 분야로 간주할 수 있다.이 분야는 컴퓨터 과학에서 주요 응용 분야를 가지고 있으며, 여기서 특히 기능적 프로그래밍 언어에 대한 표현적 의미론을 규정하는 데 사용됩니다.영역 이론은 매우 일반적인 방법으로 근사와 수렴에 대한 직관적인 아이디어를 공식화하며 위상학과 밀접하게 관련되어 있습니다.

동기부여와 직관

1960년대 후반에 다나 스콧에 의해 시작된 도메인 연구의 주된 동기는 람다 미적분의 표현적 의미론을 찾는 것이었다.이 형식주의에서는 언어의 특정 용어에 의해 특정된 "기능"을 고려한다.순수하게 통사적인 방법으로, 단순한 함수에서 다른 함수를 입력 인수로 삼는 함수로 이동할 수 있다.다시 이 형식론에서 사용할 수 있는 구문 변환만을 사용하여, 소위 고정점 결합자(그 중 가장 잘 알려진 것은 Y 결합자)를 얻을 수 있다; 정의상, 이것들은 모든 함수 f에 대해 f(Y(f) = Y(f)의 특성을 가진다.

이러한 지시적 의미론을 공식화하기 위해 먼저 람다 미적분 모형을 구축하려고 시도할 수 있다. 람다 미적분에서는 순함수가 각 람다 항과 관련지어진다.그러한 모형은 람다 미적분과 구체적인 수학 함수를 조작하기 위한 통지 체계로서의 람다 미적분 사이의 연결을 공식화할 것이다.콤비네이터 미적분은 그런 모형이다.그러나, 조합 미적분의 요소들은 함수에서 함수로의 함수이다; 람다 미적분의 모형 요소들이 임의의 영역과 범위를 가지기 위해서는, 그것들은 진정한 함수가 될 수 없고, 부분 함수일 뿐이다.

스콧은 아직 결과를 반환하지 않은 계산을 나타내기 위해 "부분적" 또는 "불완전한" 정보의 개념을 공식화함으로써 이러한 어려움을 극복했습니다.이것은 계산의 각 영역(예: 자연수)에 대해 정의되지 않은 출력을 나타내는 추가 요소, 즉 끝나지 않는 계산의 "결과"를 고려하여 모델링되었다.또, 연산 영역은, 「미정의 결과」가 최소의 요소인 순서 관계를 갖춘다.

람다 미적분의 모형을 찾는 중요한 단계는 최소 고정점을 보장받는 함수(부분 순서 집합에서)만 고려하는 것입니다.이러한 기능의 집합은 적절한 순서와 함께 이론의 의미에서 다시 "도메인"이 됩니다.그러나 사용 가능한 모든 기능의 서브셋에 대한 제한에는 또 다른 큰 이점이 있습니다. 즉, 자체 기능 공간을 포함하는 도메인을 얻을 수 있습니다. 즉, 자신에게 적용할 수 있는 기능을 얻을 수 있습니다.

이러한 바람직한 특성 외에도, 영역 이론은 또한 매력적인 직관적 해석을 가능하게 한다.위에서 설명한 바와 같이 계산 영역은 항상 부분적으로 정렬됩니다.이 순서는 정보 또는 지식의 계층을 나타냅니다.순서내의 요소가 높을수록, 보다 구체적이고, 보다 많은 정보를 포함하고 있습니다.하위 요소는 불완전한 지식 또는 중간 결과를 나타냅니다.

그런 다음 결과를 개선하기 위해 영역의 요소에 단조 함수를 반복적으로 적용하여 계산을 모델링한다.고정점에 도달하는 것은 계산을 끝내는 것과 같습니다.도메인은 단조 함수의 고정점이 존재함을 보장할 수 있고 추가적인 제한 하에서 아래에서 근사할 수 있기 때문에 이러한 아이디어에 대한 우수한 설정을 제공합니다.

정식 정의 가이드

이 섹션에서는 도메인 이론의 중심 개념과 정의를 소개합니다.도메인이 정보 순서라는 위의 직관은 이론의 수학적 형식화에 동기를 부여하기 위해 강조될 것이다.정확한 공식 정의는 각 개념에 대한 전용 문서에서 확인할 수 있습니다.영역 이론 개념도 포함하는 일반적인 질서 이론 정의의 목록은 순서 이론 용어집에서 찾을 수 있습니다.그럼에도 불구하고 도메인 이론의 가장 중요한 개념은 아래에 소개될 것이다.

수렴 사양으로 지정된 세트

앞서 언급한 바와 같이, 영역 이론은 계산 영역을 모델링하기 위해 부분적으로 순서가 매겨진 집합을 다룬다.그 목적은 정보 조각이나 계산의 (부분적인) 결과와 같은 순서의 요소를 해석하는 것이다. 여기서 순서의 상위 요소는 그 아래 요소의 정보를 일관된 방식으로 확장한다.이 단순한 직감으로부터 도메인이 종종 가장 큰 요소를 가지고 있지 않다는 것은 이미 명백하다. 왜냐하면 이것은 다른 모든 요소의 정보를 포함하는 요소가 있다는 것을 의미하기 때문이다. 즉, 다소 흥미롭지 않은 상황이다.

이론에서 중요한 역할을 하는 개념은 도메인의 유도 부분 집합이다. 유도 부분 집합은 두 요소가 이 부분 집합의 요소인 상한을 갖는 순서의 비어 있지 않은 부분 집합이다.도메인에 대한 우리의 직관적인 관점에서, 이것은 지시된 서브셋 내의 어떤 두 가지 정보라도 서브셋 내의 다른 요소에 의해 일관되게 확장된다는 것을 의미합니다.따라서 우리는 지시된 하위 집합을 일관된 사양으로 볼 수 있다. 즉, 어떤 두 요소도 모순되지 않는 부분 결과의 집합으로 볼 수 있다.이 해석은 분석에서 수렴 시퀀스의 개념과 비교할 수 있으며, 각 요소는 앞의 것보다 더 구체적입니다.실제로, 미터법 공간 이론에서, 시퀀스는 도메인 이론에서 지시 집합의 역할과 많은 면에서 유사한 역할을 한다.

시퀀스의 경우와 마찬가지로 유도 집합의 한계에도 관심이 있습니다.위에서 설명한 내용에 따르면, 이것은 유도 집합의 모든 요소, 즉 유도 집합에 존재하는 정보를 정확히 포함하는 고유 요소의 정보를 확장하는 가장 일반적인 정보 요소가 될 것입니다.순서론의 공식화에서, 이것은 지시 집합의 최소 상한일 뿐이다.시퀀스의 한계와 마찬가지로 유도 집합의 최소 상한이 항상 존재하는 것은 아닙니다.

당연히, 모든 일관된 규격이 수렴되는 계산 영역, 즉 모든 지시 집합이 최소 상한을 갖는 순서에 특별한 관심을 갖는다.이 속성은 directed-complete 부분 순서(dcpo)의 클래스를 정의합니다.사실, 도메인 이론의 대부분의 고려사항들은 최소한 지시된 완전한 명령만을 고려한다.

불완전한 지식을 나타내는 부분적인 특정 결과의 기본적인 생각으로부터, 또 하나의 바람직한 속성, 즉 최소 요소의 존재를 도출한다.이러한 요소는 정보가 없는 상태(대부분의 계산이 시작되는 위치)를 모델링합니다.또한 결과를 전혀 반환하지 않는 계산의 출력으로 간주할 수도 있습니다.

계산 및 도메인

이제 계산의 영역이 무엇이어야 하는지에 대한 기본적인 공식적인 설명을 몇 가지 얻었으므로 계산 자체를 살펴볼 수 있습니다.분명히 이것들은 함수여야 하며, 어떤 계산 영역으로부터 입력을 받아 어떤 (가능성이 있는) 영역에서 출력을 반환해야 한다.그러나 입력의 정보 내용이 증가하면 함수의 출력에 더 많은 정보가 포함될 것으로 예상할 수도 있다.형식적으로 이것은 함수가 단조롭기를 원한다는 것을 의미합니다.

dcpos를 취급할 때는 다이렉트세트의 한계 형성과 호환성이 있는 계산이 필요할 수도 있습니다.형식적으로 이것은, 어떤 함수 f에 대해서, 유향 집합 D(즉, D의 각 요소의 화상의 집합)의 화상 f(D)가 다시 방향지어져 D의 최소 상한의 화상을 가지는 것을 의미한다.또한 f는 지시된 우월성을 보존한다고 말할 수 있다.또한 두 요소의 유도 세트를 고려함으로써 이러한 함수도 단조롭게 해야 한다는 점에 유의하십시오.이러한 성질은 스콧 연속 함수의 개념을 일으킨다.이것은 종종 모호하지 않기 때문에 연속 기능에 대해서도 언급할 수 있다.

근사치 및 정밀도

도메인 이론은 정보 상태의 구조를 모델링하기 위한 순수한 질적 접근법입니다.어떤 것이 더 많은 정보를 포함하고 있다고 말할 수 있지만, 추가 정보의 양은 명시되어 있지 않다.그러나, 주어진 정보 상태보다 훨씬 단순한(또는 훨씬 불완전한) 요소에 대해 말하고 싶은 상황이 있습니다.예를 들어, 일부 거듭제곱 집합의 자연 부분 집합-포함 순서에서, 무한 요소(즉, 집합)는 유한 부분 집합보다 훨씬 더 "정보적"이다.

이러한 관계를 모델화하고 싶다면 우선 차수가 θ인 도메인의 유도된 엄밀한 순서 <를 고려할 수 있다.단, 전체 주문의 경우 유용한 개념이지만, 부분 주문 세트의 경우 많은 것을 알 수 없습니다.다시 한 번 집합의 포함 순서를 고려할 때, 한 집합이 하나 적은 요소를 포함할 경우 다른 집합보다 훨씬 작으며, 무한할 수도 있습니다.그러나 이것이 "훨씬 더 단순하다"는 개념을 포착한다는 것에는 동의하지 않을 것이다.

웨이-하위 관계

좀 더 정교한 접근방식은 소위 근사 순서의 정의로 이어지며, 더 암시적으로도 방법-아래 관계라고 불린다.x 요소는 y 요소보다 훨씬 낮다. 예를 들어, 다음과 같이 최상위를 갖는 모든 유도 집합 D에 대해

${\displaystyle yd}$ sup$$D \ $displaystyle$y \ $sq subseteq$\$sup$D$$,

D에는 다음과 같은 요소 d가 있다.

${\displaystyle x}$"$displaystyle$ x$\subseteq$ d$"$ 입니다$.$

그리고 하나는 x가 y에 가깝다고 말하고 쓰기도 한다.

$x$ $스타일x\ll$y$$。

이것은, 을 의미합니다.

${\displaystyle x}$x ${\displaystyle x}$ x\$displaystyle$ x$\subseteq$ y$,$

싱글톤 집합 {y}이(가) 방향이기 때문입니다.예를 들어 집합의 순서에서 무한 집합은 유한 부분 집합보다 훨씬 높습니다.한편, 유한 집합의 유도 집합(사실, 체인)을 고려합니다.

$\displaystyle \{0\},\{0,1\},\{0,1,2\},\ldots }$

이 사슬의 최상위는 모든 자연수 N의 집합이기 때문에, 이것은 어떤 무한 집합도 N보다 훨씬 낮다는 것을 보여준다.

그러나 일부 요소보다 훨씬 아래에 있는 것은 상대적인 개념이며 요소에만 대해 많은 것을 드러내지 않습니다.예를 들어 유한 집합의 특성을 순서론적인 방법으로 나타내려고 하지만 무한 집합도 다른 집합보다 훨씬 낮을 수 있습니다.이러한 유한 요소 x의 특별한 특성은 그들이 그들 자신보다 훨씬 낮다는 것이다.

${\displaystyle \mathrm{x4}}$x$\displaystyle$ x$\ll$x$.$

이 속성을 가진 요소를 압축이라고도 합니다.그러나, 이러한 요소들은 용어의 다른 수학적 용법에서 "확정" 또는 "콤팩트"일 필요는 없습니다.그럼에도 불구하고 이 표기법은 집합론과 위상학의 각각의 개념과 특정한 유사성에 의해 동기 부여된다.도메인의 콤팩트 요소에는 아직 발생하지 않은 다이렉트 집합의 한계로 얻을 수 없는 중요한 특수 속성이 있습니다.

방법-아래 관계에 대한 다른 많은 중요한 결과들은 이 정의가 도메인의 많은 중요한 측면을 포착하는 데 적절하다는 주장을 뒷받침한다.

도메인의 베이스

이전 생각들은 또 다른 의문을 제기한다: 도메인의 모든 요소를 훨씬 더 단순한 요소의 한계로 얻을 수 있다는 것을 보장하는 것이 가능한가?무한대 개체를 계산할 수는 없지만 임의적으로 근접하게 근사하기를 바랄 수 있기 때문에 이것은 실제로 상당히 관련이 있습니다.

보다 일반적으로는 다른 모든 요소를 최소 상한으로 가져오는 데 충분한 것으로서 특정 요소의 하위 집합으로 제한하려고 합니다.따라서 포셋 P의 기저를 P의 서브셋 B로 정의함으로써 각 x in P에 대해 x보다 훨씬 아래인 B의 원소 세트는 슈프림 x를 갖는 유도 세트를 포함한다.poset P는 베이스가 있는 경우 연속 포셋입니다.특히 이 경우 P 자체가 기반이 됩니다.많은 응용 프로그램에서는 주요 연구 대상으로 연속적인 (d)cpos를 제한한다.

마지막으로 유한요소의 기저가 존재하도록 요구함으로써 부분 순서집합에 대한 보다 강력한 제한이 주어진다.이러한 포셋을 대수적이라 한다.표현적 의미론의 관점에서, 대수적 포셋은 유한한 것으로 제한될 때에도 모든 요소의 근사치를 허용하기 때문에 특히 잘 동작한다.앞에서 언급했듯이, 모든 유한 요소가 고전적인 의미에서 "유한" 것은 아니며, 유한 요소가 셀 수 없는 집합을 구성하는 것일 수도 있다.

단, 경우에 따라서는 poset의 베이스는 카운트할 수 있습니다.이 경우, --연속 포셋을 말합니다.따라서 카운트 가능 기저가 모두 유한 요소로 구성되어 있으면 우리는 θ-대수의 차수를 구한다.

특정 유형의 도메인

도메인의 단순한 특수한 경우를 기본 또는 플랫 도메인으로 알려져 있습니다.이는 정수와 같이 비교할 수 없는 요소 집합과 다른 모든 요소보다 작은 것으로 간주되는 단일 "하단" 요소로 구성됩니다.

"도메인"으로 적합할 수 있는 질서 있는 구조의 다른 많은 흥미로운 특수 클래스를 얻을 수 있다.우리는 이미 연속 포셋과 대수 포셋에 대해 언급했다.둘 다 더 특별한 버전은 연속형 및 대수형 cpos입니다.한층 더 완전성 특성을 더하면 연속 격자와 대수 격자를 얻을 수 있는데, 이러한 격자는 각각의 성질을 가진 완전한 격자에 불과하다.대수적인 경우, 사람들은 여전히 연구할 가치가 있는 더 넓은 종류의 포지셋을 발견한다: 역사적으로, 스콧 도메인은 도메인 이론에서 연구된 첫 번째 구조였다.보다 넓은 클래스의 도메인은 SFP 도메인, L 도메인 및 2중 도메인으로 구성됩니다.

이러한 모든 순서 클래스는 단조, Scott-continuous 또는 형태론으로 더욱 특화된 함수를 사용하여 다양한 범주의 dcpos로 주조할 수 있습니다.마지막으로 도메인이라는 용어 자체는 정확하지 않기 때문에 공식 정의가 제공되거나 세부 사항이 관련이 없는 경우에만 약어로 사용됩니다.

중요한 결과

포셋 D는 D의 각 체인이 슈프림을 가지고 있는 경우에만 dcpo입니다.('if' 방향은 선택 공리에 의존합니다.)

f가 도메인 D의 연속 함수인 경우, f는 최소 요소 θ의 모든 유한 반복의 최소 상한으로 주어진 최소 고정점을 가진다.

${\displaystyle \mathrm{fix}}$ ${\displaystyle (}$ (${\displaystyle }$f ) ${\displaystyle \underset{}{}}$ = ${\displaystyle \underset{}{n}}$ ${\displaystyle \underset{}{\in }}$ ${\displaystyle \underset{}{N\mathbb{}}}$ ${\displaystyle \underset{}{f}{}^{}{n}^{}}$ ( ${\displaystyle )}$ $){$ $displaystyle \operatorname {fix$} ( f ) = \ $bigsqcup$_ {$n$\ in \ $mathbb${ $N } f^$ { $n$} ( \ $bot$ )$\}$

이것이 클린 고정점 정리입니다.$"\displaystyle$ \$sqcup"$ 기호는$$ 다이렉트 조인입니다.

일반화

• "Synthetic domain theory". CiteSeerX 10.1.1.55.903. {{cite journal}}:Cite 저널 요구 사항 journal=(도움말)
• 위상 영역 이론
• 연속성 공간은 메트릭 공간 및 포셋의 일반화로 메트릭 공간 및 도메인의 개념을 통합하는 데 사용할 수 있습니다.

「 」를 참조해 주세요.

• 범주론
• 코도메인
• 표기 의미론
• 스콧 도메인
• 스콧 정보 시스템
• 유형 이론

추가 정보

• G. Gierz; K. H. Hofmann; K. Keimel; J. D. Lawson; M. Mislove; D. S. Scott (2003). "Continuous Lattices and Domains". Encyclopedia of Mathematics and its Applications. Vol. 93. Cambridge University Press. ISBN 0-521-80338-1.
• Samson Abramsky, Achim Jung (1994). "Domain theory" (PDF). In S. Abramsky; D. M. Gabbay; T. S. E. Maibaum (eds.). Handbook of Logic in Computer Science. Vol. III. Oxford University Press. pp. 1–168. ISBN 0-19-853762-X. Retrieved 2007-10-13.
• Alex Simpson (2001–2002). "Part III: Topological Spaces from a Computational Perspective". Mathematical Structures for Semantics. Archived from the original on 2005-04-27. Retrieved 2007-10-13.
• D. S. Scott (1975). "Data types as lattices". Proceedings of the International Summer Institute and Logic Colloquium, Kiel, in Lecture Notes in Mathematics. Springer-Verlag. 499: 579–651.
• Carl A. Gunter (1992). Semantics of Programming Languages. MIT Press. ISBN 9780262570954.
• B. A. Davey; H. A. Priestley (2002). Introduction to Lattices and Order (2nd ed.). Cambridge University Press. ISBN 0-521-78451-4.
• Carl Hewitt; Henry Baker (August 1977). "Actors and Continuous Functionals" (PDF). Proceedings of IFIP Working Conference on Formal Description of Programming Concepts. Archived (PDF) from the original on April 12, 2019.
• V. Stoltenberg-Hansen; I. Lindstrom; E. R. Griffor (1994). Mathematical Theory of Domains. Cambridge University Press. ISBN 0-521-38344-7.

외부 링크

• Graham Hutton의 도메인 이론 입문, 노팅엄 대학교