Definability of Functional Properties in the Basic Modal-Temporal Language over Ordered Frames

기술 요약: 순서 프레임 상의 기본 양상-시간 언어에서의 함수적 속성의 정의 가능성

문제 제기
본 논문은 기본 양상 언어 $\Box$(모든 기능적 이미지 내에서)에 Prior의 시간 연산자 $G$(미래에 항상)와 $H$(과거에 항상)를 추가하여 형성된 기본 양상-시간 언어 $LT \times W$의 표현력을 조사한다. 본 연구는 다섯 가지 구별된 순서 유형(전순서(PRE), 엄격 전순서(sPRE), 부분 순서(PO), 선형 순서(LO), 엄격 선형 순서(sLO))에 걸쳐 아홉 가지 특정 함수적 속성인 전사성(totality), 비전사성(non-totality), 단사성(injectivity), 전사성(surjectivity), 단조성(monotonicity), 엄격 단조성(strict monotonicity), 반단조성(antitonicity), 엄격 반단조성(strict antitonicity), 그리고 상수성(constancy)의 정의 가능성에 초점을 맞춘다.

이 연구가 다루는 핵심 과제는 여러 접근성 함수가 공존하며 양상 연산자가 이들의 결합된 이미지에 대해 무차별적으로 양화하는 "멀티플로우(multiflow)" 설정이다. 이전 연구(예: [1, 3])는 엄격 선형 순서와 유니폼 도메인(U-Dom) 속성과 같은 전역적 제약에 분석을 제한했다. 본 논문은 이러한 속성들이 고립되어 정의 가능한지, 그리고 두 가지 의미론적 해석(현재의 순간을 포함하는 표준 해석과 현재의 순간을 제외하는 엄격한 해석)의 영향을 받아 정의 가능성이 어떻게 변하는지를 조사함으로써, 더 넓은 스펙트럼의 순서 구조에서 정의 가능성을 결정하는 것을 목표로 한다.

방법론
저자들은 $LT \times W$의 표현적 경계를 매핑하기 위해 두 단계의 분석적 접근 방식을 채택한다:

1. 임의의 순서ed 멀티플로우 설정: 연구는 프레임이 임의의 함수족으로 구성된 일반적인 설정에서 정의 가능성의 한계를 먼저 확립한다. 여기서 양상 연산자는 모든 함수의 합집합에 대한 2차 양화사로 작용한다. 저자들은 함수적 비동형성(functional bisimulation)을 유도하는 전사적 p-모르피즘(surjective p-morphism)을 사용하여 정의 불가능성을 증명한다. 만약 p-모르피즘이 특정 속성을 만족하는 프레임을 만족하지 않는 프레임으로 매핑한다면, 해당 속성은 정의 불가능하다.
2. 구조적 정교화 (최소 프레임): 표현력의 한계 원인을 격리하기 위해, 저자들은 프레임을 최대 두 개의 흐름과 하나의 접근성 함수로 제한하는 "최소 함수 프레임"($O_2$ 패밀리)을 도입한다. 이러한 축소는 멀티플로우 설정의 2차 복잡성을 1차 관계적 읽기로 붕괴시킨다.
3. 비교 분석: 저자들은 최소 프레임을 다음의 두 가지 다른 프레임워크와 비교한다:
   • 인덱스화된 언어(Indexed Languages): 연산자가 특정 함수를 구별하기 위해 명시적으로 라벨링된 경우.
   • 유니폼 도메인(U-Dom) 프레임: 프레임 내의 모든 함수가 공통된 도메인을 공유하는 경우.
4. 의미론적 변형: 분석은 표준($G, H$) 및 엄격($G^*, H^*$) 해석 하에서 모두 수행되어, 현재의 순간을 제외하는 것이 정의 가능성 지형을 변화시키는지 결정한다.

주요 기여 및 결과

• 멀티플로우 설정에서의 표현력 한계:
  일반적인 멀티플로우 설정에서 이 언어는 상당히 약하다. 연구는 오직 전사성(totality)과 전사성(surjectivity)만이 정의 가능하며, 이는 선형 순서(LO 및 sLO) 내에서만 가능하다는 것을 증명한다. 그 외의 모든 속성(단사성, 단조성, 상수성 등)은 선형 순서를 포함한 모든 순서 유형에서 정의 불가능하다. 이는 여러 함수에 대한 "무차별적 양화"가 개별 함수의 행동을 가리기 때문이다.

• 최소 프레임의 영향:
  의미론을 최소 프레임(단일 함수)으로 제한함으로써, 정의 가능성의 지형은 극적으로 확장된다:

  • 단조성 및 반단조성: 이들은 모든 순서 유형(PRE, sPRE, PO, LO, sLO)에서 정의 가능하다.
  • 단사성: 표준 해석 하에서 엄격 선형 순서(sLO)에서 정의 가능해진다.
  • 엄격 단조성/반단조성: 엄격 전순서 및 엄격 선형 순서에서 정의 가능하다.
  • 상수성: 최소 프레임에서도 비선형 순서(PRE, sPRE, PO)에서는 여전히 정의 불가능하며, 이는 p-모르피즘에 의해 보존되는 독특한 의미론적 동치 논증을 필요로 한다.

• 엄격한 해석의 역할:
  일반적인 멀티플로우 설정에서 표준 해석과 엄격한 해석 사이의 선택은 동일한 결과를 낳는다. 그러나 최소 프레임에서 엄격한 해석($G^*, H^*$)은 결정적인 이득을 제공한다:

  • 표준 해석이 실패하는 선형 순서(LO)에서 단사성의 정의를 가능하게 한다.
  • 비선형적 유형을 엄격한 대응물로 효과적으로 처리함으로써, 모든 순서 유형(PRE, PO, LO 포함)에서 엄격 단조성 및 엄격 반단조성의 정의를 가능하게 한다.

• 프레임워크의 동등성:
  본 논문은 최소 프레임에서 얻은 정의 가능성 패턴이 함수가 구문적으로 구별되는 인덱스화된 언어 및 U-Dom 프레임과 동일함을 보여준다. 이는 원래 프레임워크의 표현력 한계가 연산자 자체의 약함 때문이 아니라, 서로 다른 도메인을 가진 함수의 통제되지 않은 다중성 때문임을 나타낸다. 함수적 다중성이 제어되면(구조적 단순화, 도메인 균일성 또는 구문적 인덱싱을 통해), 기본 연산자들은 그 완전한 능력을 회복한다.

• 근본적인 장애물:
  함수적 다중성을 제어한 후에도, 전사성, 비전사성, 단사성, 전사성, 상수성과 같은 "핵심 속성"들은 모든 비선형 순서(PRE, sPRE, PO)에서 정의 불가능한 상태로 남는다. 저자들은 연결성의 결여(점들 간의 비교 불가능성)가 시간적 양상론이 극복할 수 없는 근본적인 장애물이라고 결론짓는다.

의의
본 논문은 순서 프레임 상의 기본 양상-시간 언어의 표현적 한계에 대한 체계적인 분류를 제공한다. 본 연구의 주요 의의는 원래의 멀티플로우 설정에서 근본적인 함수적 속성을 정의할 수 없는 이유가 시간 연산자 자체의 내재적 결함이 아니라, 통제되지 않은 함수적 다중성의 구조적 결과물임을 밝혀낸 데 있다.

최소 프레임, 인덱스화된 언어, U-Dom 프레임이 동일한 정의 가능성 패턴을 생성함을 보여줌으로써, 본 연구는 함수적 속성이 정의 가능해지는 정확한 조건을 명확히 한다. 구조적 단순화를 통해 모든 순서에서 단조성과 반단조성의 정의 가능성을 회복할 수 있지만, 전사성이나 단사성과 같이 전역적 도메인 비교를 요구하는 속성들에 있어서는 선형적 연결성의 결여가 지속적인 장벽으로 남는다는 점을 입증한다. 또한, p-모르피즘을 통한 표준적인 정의 불가능성 증명을 거부하고 독특한 의미론적 동치 논증을 요구하는 상수성의 특수한 지위를 강조한다.