강력한 정규화 증거에 대해 논의하는 동안 이 의견 은 “정상적인 형식 모델”과 “순전히 구문론적인 방법”을 대조합니다.
이것은 구문에 기초한 모델에 직면하여 구문과 의미 론적 구조를 엄격하게 구별 할 수 있는가? 대수학에 대한 용어 모델, 1 차 논리에 대한 Henkin 모델은 어떻습니까? 구조적 작동 의미론은 어떻습니까? 용어 모델은 구문에 대해 동형이 될 수 있으므로 확고한 구별을하기가 어렵습니다.
논리에서 증명 이론과 모델 이론의 차이점을 연구 할 때까지는 “정적 유형 시스템은 구문 분석법”이라는 아이디어에 당황했습니다. 결국, 유형 시스템은 프로그램 동작의 추상화 (및 종속 유형의 경우 임의로 정확한 유형) 인 유형에 대한 이유를 제시합니다.
답변
구문론과 의미 론적 방법을 엄격하게 구별 할 수는 없지만, 그 구별은 여전히 의미가 있습니다.
-
구조적 작동 의미론은 의미 론적이지 않습니다. 이는 의미론을 프로그래밍 언어에 제공하는 구성 방법이 아니기 때문입니다.
-
그러나 실현 가능성 또는 논리적 관계 방법을 사용하여 구조적 작동 의미론에서 denotational 모델을 작성할 수 있습니다. 예를 들어 Robert Harper의 연산 시맨틱에 대한 유형 시스템 구성을 참조하십시오 .
-
용어 모델은 부정적이지만 일반적으로 의미 론자들은 만족하지 않습니다. 일반적으로 원하는 것은 모델이라는 용어가 초기 인 모델 범주로, 견고성과 완전성 결과를 증명하는 데 사용할 수 있습니다. (직교 닫힌 범주에 대한 입력 된 람다 미적분의 건전성과 완성도는 패러다임의 예입니다. 자세한 내용 은 Simply-Typed -calculus에
λ대한 Alex Simpson의 범주 완전성 결과를 참조하십시오.)
-
반대로, 의미 의미론이있는 경우 그 구문이 무엇인지 파악할 수 있습니다. 그런 다음 모델이라는 용어가 적합한 모델 범주에서 intitial 객체 역할을 할 수있는 구문 및 추상 시스템을 찾고 싶습니다.
예를 들어, 게임의 의미는 순수한 의미 구조로서의 생활을 시작했고, 결국 운영 게임의 의미에 대한 작업을 주도 — 최근의 예는 어느 알렉시스 Goyet의입니다 람다 바 미적분 람다 : 구속 전략 듀얼 미적분학 .
-
전반적으로, 구조적 운영 의미론은 구현하기 쉬운 추상 기계를 지정하는 방법으로 생각할 수 있습니다. 명칭 의미론은 추론하기 쉬운 언어의 구성 모델을 제공합니다. 둘 다 가지고 있다면 언어를 구현하고 추론 할 수 있습니다.
-
정규화 정리는 흥미로운 모호한 경우입니다. 일반적으로 정규화를 증명하려면 시맨틱 모델 (일반적으로 논리 관계)이 필요합니다. 그러나 정규화가 유지되는 것을 알면 이제는 순전히 구문론적인 논거 인 정규 형식에 대한 유도를 통해 많은 속성을 증명할 수 있습니다.
약한 논리 (유도없는 1 차 논리까지)의 경우 유전 대체 기법을 사용하여 구문 적으로 정규화를 증명할 수 있습니다 . 이러한 논리에서 하위 수식 속성이 유지되므로 유형을 유도하여 정규화를 증명할 수 있습니다. 이것이 어떻게 작동하는지에 대한 설명은 Frank Pfenning의 Structural Cut Elimination 을 참조하십시오 .