기술 요약: 비표준 공리적 의미론 (Nonstandard Axiomatic Semantics)

문제 정의

본 논문은 호어 논리(Hoare logic)에 기반한 공리적 의미론의 근본적인 모호함을 다룬다. 스콜렘(Skolem)의 페아노 산술에 대한 비표준 모델과 유사하게, 저자는 호어 논리가 프로그래밍 언어의 의도된 연산 의미론(trace semantics)을 동형(isomorphism) 관계까지 유일하게 규정하지 못함을 입증한다.

핵심적인 문제는 **반복 규칙(Rule of Iteration)**에서 발생한다. 호어 논리는 루프에 대해 추론하기 위해 귀납적 불변량(inductive invariants)을 사용하지만, 표준 논리 이론은 다음 두 가지를 구별하지 못한다:

1. 표준 트레이스(Standard traces): 자연수($\mathbb{N}$)에 의해 인덱싱된 유한 실행 및 무한 실행.
2. 비표준 트레이스(Nonstandard traces): 비표준 자연수(예: 표준 $\omega$ 너머의 "무한한 과거" 또는 "무한한 미래"를 포함하는 스콜렘 모델)에 의해 인덱싱된 실행.

결과적으로, 표준 트레이스 모델에 대해 유효한 호어 논리 증명은 루프가 비표준 길이를 가질 수 있는(예: 비표준 과거에서 시작하거나 비표준 미래로 계속되는) 비표준 모델에서도 유효하다. 이는 전통적인 방식으로 공식화된 호어 논리가 유일하고 잘 정의된 연산 의미론을 명시하지 못함을 시사한다.

방법론

저자는 추상 해석(abstract interpretation)과 고정점 이론(fixpoint theory)의 개념을 활용하여 표준 트레이스 의미론과 비표준 트레이스 의미론 사이의 비교 분석을 수행한다.

1. 트레이스 의미론의 형식화:

   • 표준 의미론: 유한($\Sigma^*$) 및 무한($\Sigma^\infty$) 트레이스(인덱스 $\mathbb{N}$)에 대한 최소 고정점($lfp$) 및 최대 고정점($gfp$)을 통해 정의된다.
   • 비표준 의미론: 비표준 집합(예: $\mathbb{N} + \delta$인 전방 비표준 트레이스(무한한 미래 포함) 및 $\mathbb{N} - \delta$인 후방 비표준 트레이스(무한한 과거 포함), 여기서 $\delta > 0$)에 의해 인덱싱된 트레이스로 확장된다. 이러한 집합들은 스콜렘 구조를 모델링한다.

2. 추상화 및 동치성:

   • 논문은 트레이스 의미론을 유효한 호어 삼조(Hoare triples)의 집합으로 매핑하는 추상화 함수 $\alpha_S$를 정의한다.
   • **정리 1(Theorem 1)**은 표준 의미론에 대해 유효한 호어 삼조의 집합($H(L)$)이 비표준 의미론에 대해 유효한 삼조의 집합($\tilde{H}(L)$)과 동일함을 증명한다. 이는 표준 호어 증명 규칙이 비표준 해석을 배제하기에는 불충분함을 확인해 준다.

3. 제안된 해결책 (표준화, Standardisation):
   이 모호성을 해결하기 위해, 저자는 종료 증명 방법(특히 Knuth의 방법 및 서수 변형)에서 영감을 얻은 추가적인 증명 의무(proof obligations)를 통해 공리적 의미론을 풍부하게 할 것을 제안한다.

   • 비표준 전방 트레이스 방지: 트레이스 위치를 서수($\mathcal{O}$)로 매핑하는 증가 함수 $K$가 존재하고, 루프 카운터가 첫 번째 무한 극한 서수인 $\omega$에 의해 유계(bounded)되어야 한다는 조건을 추가한다. 비표준 정수 부분은 정렬된 서수와 순서 동형(order-isomorphic)이 될 수 없으므로, 이 요구 조건은 비표준 전방 무한 트레이스를 제거한다.
   • 비표준 후방 트레이스 방지: 후방 트레이스에 대한 듀얼(dual) 요구 사항이 도입되며, 이는 후방 순회(backward traversal)가 표준 범위 내에서 종료되도록 보장하는 감소 함수 $K$(반감성, antitone)를 요구한다.

주요 기여

• 비표준 모델의 식별: 본 논문은 데데킨트의 범주성 조건(Dedekind's categoricity condition)이 없는 페아노 산술과 마찬가지로 호어 논리가 비고유성 문제를 겪고 있음을 공식적으로 입증한다. 또한, 압축 정리(compactness theorem)로 인해 1차 논리에서의 루프 불변량이 표준 트레이스 모델과 비표준 트레이스 모델을 구별할 수 없음을 보여준다.
• 이론의 동치성: 표준 호어 논리와 비표준 호어 논리 이론이 동일함($H(L) = \tilde{H}(L)$)을 증명하며, 이는 기존의 증명들이 본질적으로 비표준 실행을 배제하지 못함을 의미한다.
• 서수를 통한 표준화: 서수 카운터(전방 트레이스의 경우 $\omega$로 제한됨)를 포함하는 증명 의무를 추가함으로써 공리적 의미론을 표준 모델로 제한하는 방법을 제안한다.
• 표준 증명의 보존: 이러한 추가적인 증명 의무는 항상 표준 트레이스 의미론에 의해 만족된다는 것이 핵심적인 결과이다. 따라서 표준 해석을 가정하는 경우(대부분의 호어 논리 사용에 내재된 가정), 기존의 호어 증명은 유효하며 변경되지 않는다. 새로운 의무는 표준 모델을 공식적으로 배제하면서도 표준 프로그램의 실질적인 검증을 변화시키지 않는다.

결과

• 이론적 동치성: 비표준 트레이스 모델에 대해 유효한 호어 삼조의 집합은 표준 모델에 대한 것과 정확히 일치한다.
• 모호성 해결: 서수 경계 조건을 부과함으로써 공리적 의미론을 표준 모델로 제한한다.
• 적용 가능성: 제안된 표준화는 호어 논리에 의존하는 기존의 정적 분석 및 타이핑 알고리즘과 호환된다. 단, 표준 의미론에 대한 기본 가정이 명시적이거나 새로운 의무가 검증 가능하다는 전제하에 그러하다.
• 한계점: 논문은 구체적 도메인이 요구되는 서수 함수를 정의하기에 충분히 표현력이 높지 않은 추상 도메인으로 대체되는 **추상 호어 논리(Abstract Hoare Logics)**에서는 표준화 방법이 직접 적용되지 않을 수 있다고 언급한다.

의의

본 논문은 "공리적 의미론은 논리적 단언(logical assertions)에 미치는 효과에 의해 프로그램의 의미를 정의한다"는 일반적인 주장이 기술적으로 결함이 있다고 주장한다. 그 이유는 정의된 의미가 동형 관계에 대해 유일하지 않기 때문이다. 본 연구의 의의는 다음과 같다:

1. 기초의 명확화: 호어 논리가 페아노 산술과 마찬가지로, 유일한 연산 해석을 보장하기 위해 (이 경우에는 서수 경계를 통한) "범주성" 조건이 필요함을 강조한다.
2. 암묵적 가정의 형식화: 호어 논리가 표준 계산 모델 위에서 해석된다는 암묵적인 가설을 명시적으로 만든다.
3. 논리와 의미론의 가교: 종료 증명 기법(서수를 사용)을 공리적 의미론에 통합하여 비표준 해석을 제거함으로써, 공리적 의미론을 표준 연산 트레이스 의미론과 더욱 엄격하게 일치시키는 방법을 보여준다.

저자는 표준 모델을 위한 호어 논리 증명 자체를 바꿀 필요는 없지만, 프로그램 의미의 유일한 정의를 주장하기 위해서는 이론적 프레임워크가 비표준 모델을 인식하고 이를 공식적으로 배제해야 한다고 결론짓는다.