핵심 개념
dBang 계산법에서 의미성은 타입화 가능성과 거주성을 통해 특성화될 수 있다. 또한 의미 없는 항들은 의미 있는 항들의 중요성에 영향을 미치지 않는다는 일반성 속성이 성립한다.
초록
이 논문은 dBang 계산법에서 의미성의 개념을 정의하고 이를 타입화 가능성과 거주성을 통해 특성화한다. 또한 이 개념에 대한 두 가지 속성을 검증한다:
- 의미 없는 항들을 동일시하는 이론 H의 일관성
- 의미 없는 부항들이 의미 있는 항들의 중요성에 영향을 미치지 않는다는 일반성
논문은 또한 dCBN과 dCBV에서의 의미성 및 일반성 개념이 dBang에서 제안된 개념에 의해 포괄된다는 것을 보여준다.
통계
의미 있는 항 t는 어떤 테스트 컨텍스트 T와 u∈Λ!가 존재하여 T⟨t⟩→∗
S !u를 만족한다.
타입화 가능성과 거주성을 만족하는 항 t는 dBang-의미 있는 항이다.
의미 없는 항들을 동일시하는 이론 H는 일관적이다.
H는 유일한 최대 일관적 확장을 가진다.
인용구
"의미성 = 타입화 가능성 + 거주성"
"의미 없는 부항들은 의미 있는 항들의 중요성에 영향을 미치지 않는다."