합성 도메인 이론에서의 파워도메인(Powerdomains)과 비결정론(nondeterminism)

합성 도메인 이론 (Synthetic domain theory)은 도메인 사이의 모든 정의 가능한 사상 (definable maps)이 연속적 (continuous)이 되도록 하는 구성적 집합 우주 (constructive universe of sets) 내에서의 도메인 이론 (domain theory)의 공리화입니다. 본 논문에서 우리는 합성 도메인 이론의 설정 내에서 잘 알려진 하한 (lower), 상한 (upper), 그리고 볼록 (convex) 파워도메인 (powerdomains)에 대응하는 개념들을 구축하고, 이들이 비결정론 (nondeterminism)의 계산적으로 적절한 (computationally adequate) 데노테이션 모델 (denotational models)을 생성함을 증명합니다. 합성 도메인 이론에서 파워도메인 이론을 발전시킴으로써, 우리는 종속 타입 이론 (dependent type theory)에 직접 임베딩되는 비결정론적 메타언어 (nondeterministic metalanguage)를 얻으며, 여기서 종속 타입 이론은 메타언어에 대해 추론하기 위한 표현력 있는 논리 (expressive logic) 역할을 합니다. 또한, 계산적 적절성 (computational adequacy) 결과는 메타언어를 통한 데노테이션 추론 (denotational reasoning)이 실제 프로그램의 연산적 동작 (operational behaviors)을 연구하는 데 사용될 수 있음을 시사합니다.