Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic

기술 요약: 단순 유형론적 상수 영역 양상 람다 계산법 I: 거리 기반 베타 축약과 조합 논리

1. 문제 및 동기
본 논문은 양상 논리와 유형론적 람다 계산법의 형식적 통합 과정에서 나타난 공백을 다룬다. 리처드 몬태규(Richard Montague)와 다나 갈린(Dana Gallin)이 이 분야들을 통합한 체계들을 개발했으나, 그들의 작업은 (항등식과 양화론을 포함하는) 처치의 단순 유형 이론에 의존했으며 상태 변수(state variables)를 다루는 데 있어 한계가 있었다. 현대의 유형론적 람다 계산법, 특히 단순 유형 람다 계산법(STLC)은 컴퓨터 과학과 언어학의 표준적인 기초 이론이지만, 현대적 의미론 분석에 필요한 특정 양상적 특징들(예: 다중 상태 변수 및 내포적 맥락)이 결여되어 있다.

저자인 숀 월시(Sean Walsh)는 기존 프레임워크에서 두 가지 주요 결함을 식별한다:

1. 강도(Strength): 몬태규의 체계는 처치의 단순 유형 이론의 모든 자원을 가정하기 때문에 현대적 응용 분야에는 "너무 강하다". 반면 현대적 체계들은 종종 더 약한 기초 이론인 STLC를 활용한다.
2. 약점(Weakness): 몬태규의 체계는 양상적 표현력 측면에서 "너무 약하다". 즉, 2차원 의미론, 현실 연산자(actuality operators), 그리고 단일 표현식 내에서 다수의 구별되는 상태 변수를 바인딩하는 메커니즘이 부족하다.

본 논문의 목적은 양상 논리를 단순 유형 람다 계산법과 통합하는 체계인 $\lambda\theta$를 개발함으로써 이를 보완하는 것이다. 핵심적인 과제는 $\lambda\theta$의 "유한 변수(finite-variable)"적 성격이다. 이 체계는 각 상태 유형에 대해 사용 가능한 변수의 개수를 제어하는 파라미터 $\theta$를 통해 변수의 수를 제한한다. 이러한 제한은 표준적인 개방 항 모델(open term models)을 사용하여 완전성을 증명하는 것을 어렵게 만드는데, 왜냐에는 일반적인 $\alpha$-변환 기술이 변수 캡처를 피하기 위해 바인딩된 변수를 재명명할 만큼 충분한 변수를 제공하지 못하기 때문이다.

2. 방법론 및 핵심 정의
본 논문은 $\theta$에 의해 매개변수화된 $\lambda\theta$라는 일련의 체계를 도입하며, 여기서 $\theta$는 각 상태 유형에 대해 가용한 변수의 수(1에서 $\omega$까지의 카디널 수)를 매핑한다.

• 유형(Types): 상태 유형은 함수형의 공역(codomain)이 될 수 없다 (즉, $A$가 상태 유형이면 $A \to B$는 유형이 될 수 없다). 이는 상태 유형의 항이 엄격하게 변수 또는 상수임을 보장한다 (명제 2.6).
• 거리 기반 베타 축약(Distanced Beta Reduction): 새로운 기여로서 "거리 기반" $\beta$-축약을 정의한다. 인자가 람다 추상(lambda abstract)에 직접 적용되는 표준 $\beta$-축약과 달리, 거리 기반 축약은 인자 $N$이 중간 항들의 시퀀스 $\vec{M}$에 의해 추상 $\lambda v:A.L$로부터 분리될 수 있도록 허용한다:
  $$(\lambda \vec{x}: \vec{B}. \lambda v:A. L) \vec{M} N \to_\beta (\lambda \vec{x}: \vec{B}. L[v := N]) \vec{M}$$
  이 메커니즘은 시스템에 변수가 부족하여 변수 캡처를 피하기 위한 표준 $\alpha$-변환을 수행할 수 없을 때, 람다 추상 아래에서 축약을 수행하기 위해 필요하다.
• 조합 논리 기초(Combinatory Logic Basis): 본 논문은 전통적인 SKI 기초 대신 BCDKW 조합자(B, C, D, K, W)를 중심으로 하는 조합 논리 기초를 채택한다. 다디날(Dardinal)($D$) 조합자의 포함은 이 시스템에 특화된 것으로, 상수가 함수에 대입되는 경우를 처리한다.

3. 주요 기여 및 결과

• 모델의 조합론적 특징 규명 (정리 1.5):
  본 논문은 STLC에 대한 앤드류스(Andrews)의 헨킨 모델(Henkin models) 특징 규명을 양상적 설정으로 일반화한다. 모든 BCDKW-조합적 항들의 데노테이션(denotations)이 잘 정의될 때만 프레임이 $\lambda\theta$의 모델이 된다는 것을 증명한다. 이러한 특징 규명은 개방 항 모델이 존재하지 않는 경우(예: $\lambda_1$과 같이 비최대 파라미터의 경우, $\alpha$-변환을 위한 변수가 부족함)를 우회한다 (예시 3.9).

• 의미론적 보존 및 표현력 (정리 1.1 & 1.2):
  본 논문은 최대 시스템 $\lambda\omega$ ($\theta(A) = \omega$인 경우)와 제한된 시스템 $\lambda\theta$ 사이의 관계에 관한 짐머만(Zimmermann, 1989)의 질문을 해결한다.

  • 보존성(Conservation): 모든 $\lambda\theta$의 모델은 $\lambda\omega$의 모델이다. 따라서 의미론적 타당성이 보존된다: $\lambda\theta \models M = N$ iff $\lambda\omega \models M = N$.
  • 표현력(Expressibility): 자유 변수와 상수가 $\lambda\theta$에서 추출된 $\lambda\omega$의 모든 항은 동일한 데노테이션을 가진 $\lambda\theta$의 항에 의해 표현될 수 있다.
    이러한 결과들은 "유한 변수" 제한이 표준 의미론에서 시스템의 표현력을 제한하지 않음을 시사한다. 즉, 최대 시스템은 제한된 시스템들에 대해 보존적이다.

• 양상 및 비양상 시스템 간의 연역적 관계 (정리 1.3 & 1.4):
  본 논문은 양상 시스템 $\lambda\omega$와 일반적인 비양상 STLC($\lambda$) 사이의 관계를 확립한다.

  • 연역적 보존성(Deductive Conservation): $\lambda\omega$ 내의 항들에 대해, $\lambda\omega$에서 $\beta\eta$-동등성이 성립하는 것은 $\lambda$에서 성립하는 것과 같다.
  • 연역적 표현력(Deductive Expressibility): $\lambda$의 유형과 상수가 $\lambda\omega$와 호환되는 항들은 $\lambda\omega$ 내에서 표현될 수 있다.
    이러한 증명들은 STLC의 표준 도구들(Church-Rosser, 강한 정규화)에 의존하며 비교적 짧다.

• $\infty$-규칙을 통한 완전성 (정리 1.6):
  $\lambda\theta$(비최대 $\theta$의 경우)는 개방 항 모델이 결여되어 있고 표준 $\beta\eta$-축약에 대해 Church-Rosser 성질이 실패하므로(예시 2.26), 본 논문은 $\infty$-규칙을 도입한다. 이 규칙은 $M =_{\beta\eta} N$이 최대 시스템 $\lambda\omega$에서 성립할 때 $M \to_\infty N$을 허용한다. 이 규칙을 추가함으로써, $\lambda\theta$는 그 의미론에 대해 연역적으로 완전해진다.

• 약한 연역적 보존성 (정리 1.7):
  축약과 동등성이 람다 추상 하에서 보존되지 않는(no $\xi$-rule) "약한" 람다 계산법을 조사한다. BCDKW 기초를 사용하는 순수 내포적 조합 논리(CL$\theta$)를 사용하여, 저자는 $\lambda\omega$에서의 약한 $\beta$-동등성이 (시그니처가 상태 유형의 상수를 포함하지 않는 한) $\lambda\theta$에서의 $\beta\eta$-동등성으로 보존됨을 증명한다. 이 결과는 완전한 전개(complete developments)를 이용한 다카하시(Takahashi)의 방법을 사용하여 약한 조합 논리에 대한 Church-Rosser 성질을 확립하는 것에 의존한다.

4. 의의 및 주장
본 논문은 현대적 STLC의 자원을 양상 논리와 통합하는 "현대적" 단순 유형 양상 람다 계산법을 처음으로 철저히 개발했다고 주장한다. 그 의의는 다음과 같다:

1. 짐머만의 질문에 대한 답변: 이 논문은 최대 양상 시스템의 표현력이 제한된 유한 변수 설정에서도(의미론적으로, 그리고 $\infty$-규칙을 통해 연역적으로) 포착된다는 점을 입증함으로써 짐머만의 질문에 답한다.
2. 메타이론적 도구: 제한된 변수 가용성을 다루기 위한 필수적인 도구로서 "거리 기반 $\beta$-축약"과 BCDKW 기반의 조합 논리를 도입하여, 표준 개방 항 모델의 실패를 극복한다.
3. 내포적 의미론: 제한된 시스템 $\lambda\theta$가 최대 시스템 $\lambda\omega$와 의미론적으로 동등함을 보여줌으로써, $A \to B$ 유형의 항이 내포적 맥락에서도 절차(procedure)로 해석될 수 있다는 관점을 지지한다.

저자는 명시적으로 한계를 언급한다: $\lambda\theta$만을 사용하여 표준 $\beta\eta$-규칙만으로 완전성 정리를 제공하지는 않으며(질문 4.17), 시스템이 접근성 관계(accessibility relations)와 같은 해석을 외부에 드러내지 않고 특정 유형 규약을 요구한다는 점을 인정한다. 동반 논문은 이러한 결과들을 처치의 단순 유형 이론으로 확장한다.