Insights
AI가 자동으로 큐레이션·번역·정리하는 기술 동향 피드입니다.
본 논문은 직관주의 양상 논리(IML)의 의미론적 문제를 다루며, 기존 Kripke 스타일 관계 의미론의 한계를 극복하는 새로운 접근법을 제시합니다. 특히 Goldblatt의 '관계 커버' 의미론을 기반으로, 모델 구성의 복잡성을 줄이고 표준적인 기법에 적용 가능한 보수적 확장을 제안했습니다.
AI 자동 생성 콘텐츠
본 콘텐츠는 arXiv cs.PL (Programming Languages)의 원문을 AI가 자동으로 요약·번역·분석한 것입니다. 원 저작권은 원저작자에게 있으며, 정확한 내용은 반드시 원문을 확인해 주세요.
원문 바로가기직관주의 양상 논리(Intuitionistic modal logic, IML)는 스테이징을 위한 양상 타입 시스템, 계산 효과(computational effects), 언어 기반 보안 등 프로그래밍 언어의 여러 발전을 촉발했습니다. IML은 일반적으로 Kripke 스타일 관계 의미론(Kripke-style relational semantics)을 사용하여 연구되는데, 이는 모델을 쉽게 구성할 수 있게 함으로써 완전성(completeness) 및 일관성(consistency)과 같은 메타 이론적 속성의 증명을 단순화합니다. 하지만 Kripke 스타일 관계 의미론은 고전적 추론 원리(classical reasoning principles)에 의존하기 때문에 계산적인 관점에서는 매력적이지 않고 구성적 타입 이론(constructive type theory)에서의 형식화에 부적합합니다. Goldblatt은 직관주의 명제 논리(intuitionistic propositional logic)의 Beth-Kripke-Joyal 스타일 '커버' 의미론을 관계(relations)로 확장하여 IML을 위한 대안적인 의미론을 제공합니다. Goldblatt의 '관계 커버'(relational cover) 의미론은 고전적 추론을 극복하지만, 새로운 제한 사항을 도입합니다: 이는 모델의 범위를 제한하고 모델 구성을 복잡하게 만드는 '양상 국소화(modal localization)' 조건에 의존한다는 것입니다. Goldblatt은 정교한 순서 이론적 완성 논증(order-theoretic completion arguments)을 사용하여 완전성을 증명함으로써 이 제한 사항을 우회합니다. 본 논문에서는 이러한 제한 사항을 완화하고 더 간단하며 표준적인 모델 구성 기법에 적용 가능한 관계 커버 의미론의 보수적 확장(conservative extension)을 제시합니다. 우리는 Agda에서 우리의 의미론을 형식화하고, 독립적인 박스($ox$) 및 다이아몬드 ($ riangle$) 양상을 특징으로 하는 다양한 IML에 대해 정상화 대 평가(Normalization by Evaluation) 스타일로 구성적으로 완전성을 증명합니다.