순서형 수반 논리 (Ordered Adjoint Logic) (확장 버전)

순서형 논리 (Ordered logics)와 타입 시스템 (type systems)은 계산 언어학 (computational linguistics), 메모리 할당 (memory allocation), 스트림 처리 (stream processing), 논리적 프레임워크 (logical frameworks), 매개변수성 (parametricity), 그리고 보안 프로토콜 (security protocols) 강제 등 다양한 응용 분야에서 사용되어 왔습니다. 대부분의 공식화에서 순서형 타입 (ordered types)은 선형 (linear)이기도 하여, 각 리소스를 정확히 한 번씩 사용하도록 요구합니다. Kanovich 등이 수행한 이전 연구는 선형 순서형 논리 (linear ordered logic) 내에서 서브엑스포넨셜 (subexponentials)을 통해 이러한 제약을 완화하는 계산법 (calculi)을 조사했습니다. 본 연구에서는 수반 양상 (adjoint modalities)을 사용하여 약화 (weakening), 좌측 축약 (left contraction), 우측 축약 (right contraction), 좌측 이동성 (left mobility), 그리고 우측 이동성 (right mobility)을 포함하여 서로 다른 미세한 구조적 속성 (structural properties)을 가진 논리들을 결합함으로써 그들의 연구를 일반화합니다. 우리는 결과적으로 도출된 시퀀트 계산법 (sequent calculus)이 컷 제거 (cut elimination)를 허용함을 보여줍니다. 나아가 우리는 구조 규칙 (structural rules)이 암시적인 자연 연역 (natural deduction) 공식화를 제공하며, 이 시스템에 대한 증명 검사 (proof checking)가 결정 가능하다는 것을 보여줍니다. 이는 표현력이 풍부한 수반 프로그래밍 언어 (adjoint programming language) 또는 논리적 프레임워크 (logical framework)를 위한 적절한 토대가 됩니다.