Interpreting Lambda Calculus in Domain-Valued Random Variables

기술 요약: 도메인 값을 갖는 확률 변수에서의 람다 계산법 해석

문제 정의
본 논문은 고차 타입(higher-order types)과 확률적 선택(probabilistic choice)을 포함하는 확률적 프로그래밍 언어의 의미론적 기초를 제공하는 과제를 다룬다. 이전의 접근 방식들은 확률적 코히어런스 공간(probabilistic coherence spaces), 콘(cones), 또는 준 보렐 공간(quasi-Borel spaces)을 활용해 왔으나, 저자들은 데이나 스콧(Dana Scott)이 시작한 불리언 값 모델(Boolean-valued model) 접근법에 초점을 맞춘다. 기존 연구(예: [BFK+18])에서 식별된 특정 한계는 도메인 이론적 개념(예: 방향 집합 및 연속성)의 해석이 확률성을 다룰 때 종종 "외부적"이거나 인위적인 제한에 의존했다는 점이다. 또한, 도메인 값 확률 변수의 집합은 표준적인 의미에서 자연스럽게 연속적 방향 완비 부분 순서 집합(continuous directed-complete partial order, dcpo)을 형성하지 않으며, 이는 비타입 람다 계산법(untyped $\lambda$-calculus)의 해석을 어렵게 만든다.

방법론
저자들은 "완전한 불리언 값(completely Boolean-valued)" 관점을 채택하여, 불리언 대수 $A$ 내에서 도메인 이론을 밑바닥부터 재구성한다.

1. 불리언 값 집합론: 본 논문은 등치(equality)와 멤버십(membership)을 이진 진릿값이 아닌 불리언 대수 $A$의 값으로 해석함으로써 필요한 집합론적 기제들을 전개한다. 이를 위해 $A$-값 집합(A-valued sets)을 누적 계층을 통해 정의하고, 이 유니버스 내에서 ZFC 정리들이 불리언 값 1로 성립함을 확립한다.
2. 불리언 값 도메인 이론: 저자들은 $A$-세트오이드($A$-setoids, $A$-값 동치 관계가 부여된 집합)와 $A$-포셋($A$-posets)을 정의한다. 결정적으로, 이들은 "외부적" 정의와 내부적 해석을 구분한다. 예를 들어, "연속적 dcpo"는 내부적으로 정의된다. 본 논문은 확률 변수의 집합 $L^0(X; P(Y))$가 고전적인 의미에서는 연속적 dcpo가 아니지만, 연속성의 개념이 불리언 값 논리를 통해 내부적으로 해석될 때는 연속적 dcpo가 됨을 입증한다.
3. 재귀적 도메인 구축: 방법론의 핵심은 불리언 값 유니버스 내에서 재귀적 dcpo(자신의 함수 공간 $[D \to D]$의 은닉(retract)과 동형인 도메인 $D$)를 구축하는 것이다. 저자들은 $A$로 적응된 엔글러 모델(Engeler model)을 활용하며, 여기서 도메인은 가산 집합 $E$의 멱집합으로부터 구축된다.
4. 확률 변수와의 동형 관계: 본 논문은 불리언 값 멱집합 $P_A(\check{Y})$(여기서 $\check{Y}$는 집합 $Y$의 정준 이름)와 영집합(null ideal)에 의한 가측 함수 공간 $L^0(X; P(Y))$ 사이의 동형 관계를 확립하여, 추상적인 불리언 값 모델과 구체적인 도메인 값 확률 변수를 효과적으로 연결한다.

주요 기여

• 도메인 이론의 내부적 재구성: 주요 기여는 등치, 순서, 연속성과 같은 기본 개념이 내부적으로 해석되는 불리언 값 도메인 이론을 개발한 것이다. 이 접근법은 일반적인 논리로부터 불리언 값 논리로 정리들을 전이함으로써, 기존의 "맨손(bare-handed)" 방식보다 더 단순하고 견고한 이론을 제공한다.
• 연속성 문제의 해결: 본 논문은 확률 변수들이 표준적인 집합론적 의미에서는 연속적 dcpo를 형성하지 않지만, "연속적 dc포"가 불리언 값 의미에서 해석될 때는 그러하다는 것을 증명한다. 이를 통해 비타입 람다 계산법의 표준적인 해석이 가능해진다.
• 동형 정리: 저자들은 $A$-집합의 범주가 $A$-세트오이드의 범주와 동치임을 증명하며, 불리언 값 멱집합 $P_A(\check{Y})$가 확률 변수의 공간 $L^0(X; P(Y))$(무시 가능한 공간에 의한 모듈로 관계)와 엄격하게 동형임을 증명한다.
• 비교 불가능한 차수(Incomparable Degrees)에 대한 적용: 본 논문은 람다 정의 가능한 함수에 의해 서로를 매핑할 수 없는 두 정수 집합이 존재함을 증명함으로써 구체적인 응용 사례를 제공한다. 이 결과는 일반 재귀와 람다 정의 가능성 사이의 동치성이나 클레이니-포스트(Kleene-Post) 정리를 호출하지 않고, 순수하게 람다 계산법과 확률 프레임워크 내에서 도출된다.

결과

• 모델 구축: 저자들은 $V^A$ 내에서 해석된 엔글러 모델 내에서 비타입 람달 계산법의 모델을 성공적으로 구축한다. 이들은 임의의 재귀적 dcpo $D$가 $V^A$ 내에 존재할 때, 증명 가능한 방정식들을 존중하는 람다 항(term)들의 해석 함수가 존재함을 보여준다.
• 확률적 비교 불가능성: 구축된 모델을 사용하여, 저자들은 $\lambda$-정의 가능한 함수에 의한 many-one 환원($\leq_m$)에 대해 $T_1 \not\leq_m T_2$ 및 $T_2 \not\leq_m T_1$을 만족하는 두 정수 집합 $T_1, T_2 \subseteq \mathbb{N}$의 존재를 입증한다. 이는 불리언 값 1을 갖는 "비교 불가능한" 집합 $S_1, S_2$를 불리언 값 유니버스 내에서 정의하고, 기초 확률 공간의 특정 지점으로부터 고전적 집합 $T_1, T_2$를 추출함으로써 달성된다.
• 고전적 연속성의 한계: 본 논문은 기초 불리언 대수가 원자적(atomic)이지 않은 경우 $L^0(X; P(Y))$가 고전적인 의미에서 연속적 dcpo가 아님을 명시적으로 보여줌으로써, 내부적 불리언 값 해석의 필요성을 강조한다.

의의 및 주장
본 논문은 자사의 완전한 불리언 값 재구성이 람다 계산법을 위한 집합론적 모델을 사용하려는 데이나 스콧의 비전에 충실하면서도 "훨씬 단순한 이론"을 제공한다고 주장한다. "내부적으로" 작업함으로써, 저자들은 초기 불리언 값 도메인 이론에서 발견된 인위적인 제한들을 피한다.

본 연구의 의의는 고차 확률 프로세스를 구성적으로 다룰 수 있는 능력에 있다. 저자들은 이 프레임워크가 확률적 선택이 확장된 람다 계산법의 해석을 허용함을 언급한다. 나아가, 비교 불가능한 집합의 예시는 이 모델이 확률적 추론에 의존하면서도 확률을 명시적으로 언급하지 않는 계산 이론 및 재귀 이론의 사실들을 증명할 만큼 강력하다는 것을 보여준다. 논문은 조건화(conditioning)를 원시 개념으로 정의하고 불리언 값 프레임워크 내에서 운영 의미론(operational semantics)을 탐구하는 등의 향후 방향을 제시하며 마무리하지만, 아직 이 문제들을 해결했다고 주장하지는 않는다.