표기 의미론

컴퓨터 과학에서 표현적 의미론(처음에는 수학적 의미론 또는 스콧-스트레이시 의미론으로 알려짐)은 언어에서 표현의 의미를 기술하는 수학적 객체(표현이라고 함)를 구성함으로써 프로그래밍 언어의 의미를 공식화하는 접근법이다.프로그래밍 언어의 형식적 의미론을 제공하는 다른 접근법에는 자명한 의미론과 운영적 의미론이 포함된다.

일반적으로 표현적 의미론은 프로그램이 하는 일을 나타내는 도메인이라고 불리는 수학적 객체를 찾는 것과 관련이 있다.예를 들어, 프로그램(또는 프로그램 문구)은 부분 기능 또는 환경과^[1][2] 시스템 간의 게임으로^[3] 표시될 수 있습니다.

지시적 의미론의 중요한 원칙은 의미론이 구성되어야 한다는 것이다: 프로그램 구문의 표기는 하위 구문의 표기로 구축되어야 한다.

역사적 발전

표기적 의미론은 1970년대 ^[1][2]초에 출판된 크리스토퍼 스트레이시와 다나 스콧의 연구에서 비롯되었다.Stracey와 Scott에 의해 처음 개발된 것처럼, 표현적 의미론은 입력을 ^[2]출력에 매핑하는 함수로 컴퓨터 프로그램의 의미를 제공했습니다.반복적으로 정의된 프로그램에 의미를 부여하기 위해 Scott는 도메인 간에 연속적인 함수, 특히 부분 순서를 완성하는 작업을 제안했습니다.아래에 기술된 바와 같이 순차성, 동시성, 비결정성 및 로컬 상태와 같은 프로그래밍 언어의 측면에 대한 적절한 표현적 의미론을 조사하는 작업이 계속되고 있습니다.

동시성 및 예외와 같은 기능을 사용하는 최신 프로그래밍 언어(예: Concurrent ML,^{[4] [5]}CSP 및 Haskell)^[6]용으로 표현적 의미론이 개발되었습니다.이 언어들의 의미론들은 구절의 의미가 하위 구절의 의미에 달려있다는 점에서 구성적이다.예를 들면, 적용식 f(E1, E2)의 의미는, 그 서브 프레이즈 f, E1, E2의 의미에 근거해 정의된다.현대의 프로그래밍 언어에서는 E1과 E2를 동시에 평가할 수 있으며, 이들 중 하나의 실행은 공유 객체를 통해 상호 작용함으로써 다른 것에 영향을 미칠 수 있으며, 그 의미는 서로 정의된다.또한 E1 또는 E2는 다른 한쪽의 실행을 종료할 수 있는 예외를 발생시킬 수 있습니다.아래 섹션에서는 이러한 최신 프로그래밍 언어의 의미론에 대한 특별한 경우를 설명합니다.

재귀 프로그램의 의미

표현적 의미론은 환경(자유 변수의 현재 값을 유지하는 것)에서 표현까지의 함수로 프로그램 문구에 기인한다.예를 들어 다음과 같은 문구가 있습니다.n*m는 다음 2개의 자유변수에 대해 바인딩을 가진 환경을 제공할 때 표기를 생성합니다.n그리고.m환경에 있는 경우n값이 3이고m값은 5이고, 표시는 ^[2]15입니다.

함수는 인수와 대응하는 결과값의 순서가 매겨진 쌍의 집합으로 나타낼 수 있다.예를 들어, 집합 {(0,1), (4,3)}은(는) 인수가 0인 경우 결과가 1, 인수가 4인 경우 결과가 3인 함수를 나타내며, 그렇지 않으면 정의되지 않습니다.

예를 들어, 다음과 같이 재귀적으로 정의될 수 있는 요인 함수를 고려하십시오.

인트 요인(인트 n) { 한다면 (n == 0) 그리고나서 돌아가다 1; 또 다른 돌아가다 n * 요인(n-1); } 

이 재귀 정의에 대한 의미를 제공하기 위해 표현은 근사치의 한계로 구축되며, 여기서 각 근사치는 요인 호출 수를 제한합니다.처음에는 콜이 없기 때문에 아무것도 정의되어 있지 않습니다.다음 근사치에서는 순서 쌍(0,1)을 추가할 수 있습니다. 이 경우 계수를 다시 호출할 필요가 없기 때문입니다.마찬가지로 요인(n)을 계산하려면 n+1 호출이 필요하기 때문에 (1,1,2,2) 등을 더하고 연속 근사치마다 쌍을 하나씩 추가할 수 있습니다.제한에서는 영역 내 어디에서나 정의된 N$(\$ ~ $(\$의 총 함수를 얻을 수 있습니다.

공식적으로 각 근사치를 부분 ${\displaystyle \mathbb{}}$ N${\displaystyle n\mathbb{}}$ N$$\$displaystyle \mathbb {N}$ \$rightharpoonup \mathbb {N$으로 모델링합니다. 그런 다음, 우리의 근사치는 "좀 더 정의된 부분 요인 함수 만들기" $함수{\displaystyle }$F ${\displaystyle :}$ (${\displaystyle N\mathbb{}n\mathbb{}}$N )$$ (\$displaystyle$ F: {$n})$를 반복적으로 적용합니다.b${N}$ \$rightharpounup \mathbb {N$ 빈 함수(빈 집합)부터 시작합니다.F는 다음과 같이 코드로 정의할 수 있습니다(사용:Map<int,int>N${\displaystyle \mathbb{}}$ N \ $displaystyle$\ $mathbb${ $N$} \ $rightharpounup$\ $mathbb${$N }$ 의 경우:$$

인트 요인_비재귀적(지도< >인트,인트> factor_less_defined, 인트 n) {   한다면 (n == 0) 그리고나서 돌아가다 1;   또 다른 한다면 (동작하다 = 찾다(factor_less_defined, n-1)) 그리고나서     돌아가다 n * 동작하다;   또 다른     돌아가다 정의되어 있지 않다; } 지도< >인트,인트> F(지도< >인트,인트> factor_less_defined) {    지도< >인트,인트> new_displays(신규_displaces) = 지도.빈();   위해서(인트 n 에 모든.< >인트>()) {     한다면(f = 요인_비재귀적(factor_less_defined, n) != 정의되어 있지 않다)       new_displays(신규_displaces).놓다(n,f);   }   돌아가다 new_displays(신규_displaces); } 

그런 다음 F 표기법을ⁿ 도입하여 F가 n번 적용되었음을 나타낼 수 있습니다.

• F⁰({})는 완전히 정의되지 않은 부분 함수이며 집합 {}으로 표시됩니다.
• F¹({})는 집합 {(0,1)}으로 나타나는 부분 함수입니다. 0에서 정의되고 1로 정의되며 다른 곳에서는 정의되지 않습니다.
• F({})는⁵ 집합 {(0,1), (1,1), (2,2), (3,6), (4,24)로 표시되는 부분 함수입니다. 인수 0,1,2,3,4에 대해 정의됩니다.

이 반복 프로세스에서는 N$(\$부터 N$(\$까지의 부분 함수의 시퀀스를 구축합니다.부분 함수는 as를 순서로 사용하여 연쇄 완성 부분 순서를 형성합니다.또한 각 ${\displaystyle {Fi}^{}{}^{}}$ ${\displaystyle {Fi}^{}}$+ $(\$i}\$leq$ F$^{i+1})$이 순서로서 사용되기 때문에 요인 함수의 보다 나은 근사치 반복 프로세스는 확장(프로그레시브라고도 불린다) 매핑을 형성한다.그래서 고정점 정리(특히 부르바키-)에 의해위트 정리)는 이 반복 과정을 위한 고정점이 존재한다.

이 경우 고정점은 이 체인의 최소 상한이며, 이는 최대값입니다.factorial결합으로 표현될 수 있는 함수

$\displaystyle \bigcup _{i\in \mathbb {N}}F^{i}({\}).}$

반복이 도메인에서 가장 작은 요소(빈 집합)에서 시작되었기 때문에 발견된 고정점은 F의 최소 고정점입니다.이를 증명하기 위해서는 크나스터-타스키 정리처럼 더 복잡한 고정점 정리가 필요하다.

비결정론적 프로그램의 표현적 의미론

파워 도메인의 개념은 비결정론적 순차적 프로그램에 표현적 의미를 부여하기 위해 개발되었다.멱함수역 생성자를 위해 P를 쓸 때, 도메인 P(D)는 D로 나타나는 유형의 비결정론적 계산의 도메인이다.

비결정론의 ^[7]영역 이론 모델에는 공정성과 무한성의 어려움이 있다.

동시성의 표현적 의미론

많은 연구자들은 위에 제시된 영역 이론 모델은 동시 연산의 보다 일반적인 경우에 충분하지 않다고 주장해 왔다.이 때문에 다양한 신모델이 출시되고 있다.1980년대 초, 사람들은 동시 언어에 대한 의미론을 제공하기 위해 표현적 의미론의 스타일을 사용하기 시작했다.예로는 윌 클링거의 배우 모델 작업, 글린 윈스켈의 이벤트 구조 및 페트리 ^[8]네트 작업, 프랑스, 호어,^[9] 레만 및 드 로에버(1979)의 CSP 추적 의미론 연구가 있다.이러한 모든 조사 라인은 조사 중에 있습니다(예: CSP에 대한 다양한 표현^[5] 모델 참조).

최근 윈스켈 등은 동시성을 ^[10][11]위한 도메인 이론으로 교수 범주를 제안했다.

상태 표시 의미론

상태(히프 등)와 간단한 필수 기능은 위에서 설명한 지시적 의미론에서 쉽게 모델링할 수 있습니다.아래의 모든 교과서에 자세한 내용이 있습니다.주요 아이디어는 명령어를 일부 상태 도메인에서 부분 함수로 간주하는 것입니다."의 의미x:=3「」는, 다음의 상태가 되는 함수입니다.3에 할당된.x·시퀀싱 연산자 ";"는 함수의 구성으로 나타납니다.고정 소수점 구조는 다음과 같은 루프 구조에 의미를 부여하기 위해 사용됩니다.while".

지역 변수를 사용하여 프로그램을 모델링하는 것은 더 어려워진다.한 가지 방법은 도메인에서 더 이상 작업하지 않고 유형을 특정 범주의 월드에서 범주의 도메인 함수로 해석하는 것입니다.그런 다음 프로그램은 이러한 ^[12][13]함수들 사이의 자연스러운 연속 함수로 나타납니다.

데이터 유형의 표시

많은 프로그래밍 언어에서 사용자는 재귀 데이터 유형을 정의할 수 있습니다.예를 들어, 번호 목록 유형은 다음과 같이 지정할 수 있습니다.

데이터형 목록. = 단점 의 내트 * 목록.   빈 

이 섹션에서는 변경할 수 없는 기능 데이터 구조만 취급합니다.기존의 명령형 프로그래밍 언어에서는 일반적으로 이러한 재귀 목록의 요소를 변경할 수 있습니다.

또 다른 예: 유형화되지 않은 람다 미적분의 표시 유형은 다음과 같습니다.

데이터형 D = D 의 (D → D) 

영역 방정식을 푸는 문제는 이러한 데이터 유형을 모델링하는 영역을 찾는 것과 관련이 있습니다.대략적으로 말하면, 모든 도메인의 컬렉션을 도메인으로 간주하여 재귀적 정의를 해결하는 방법이 있습니다.아래 교과서는 더 자세한 내용을 알려준다.

다형 데이터 유형은 매개 변수로 정의된 데이터 유형입니다.예를 들어, α의 유형은list는 에 의해 정의됩니다.

데이터형 α 목록. = 단점 의 α * α 목록.   빈 

자연수 리스트는 다음과 같습니다.nat list단, 스트링 리스트는string list.

몇몇 연구자들은 다형성의 영역 이론 모델을 개발했다.다른 연구자들 또한 구성 집합 이론 내에서 파라메트릭 다형성을 모델링했습니다.자세한 내용은 아래 나열된 교과서에서 확인할 수 있습니다.

최근 연구 영역에서는 객체 및 클래스 기반 프로그래밍 ^[14]언어에 대한 표현적 의미론이 포함되어 있습니다.

복잡성이 제한된 프로그램에 대한 표현적 의미론

선형 논리에 기반한 프로그래밍 언어의 개발에 따라, 표현적 의미론은 선형 사용(예: 증명망, 일관성 공간 참조) 및 다항식 시간 ^[15]복잡성에 대한 언어에 주어졌다.

순차성의 표현적 의미론

순차 프로그래밍 언어 PCF의 완전한 추상화 문제는 오랫동안 표현적 의미론에서 큰 미해결 문제였습니다.PCF의 어려움은 매우 순차적인 언어라는 것입니다.예를 들어 PCF에서 병렬 또는 함수를 정의하는 방법은 없습니다.위에서 소개한 바와 같이 도메인을 사용하는 접근법이 완전히 추상적이지 않은 표현적 의미론을 생성하는 것은 이 때문이다.

이 개방형 질문은 1990년대에 게임 의미론의 개발과 논리적 ^[16]관계를 포함한 기술로 대부분 해결되었다.상세한 것에 대하여는, PCF 의 페이지를 참조해 주세요.

소스 투 소스 번역으로서의 표현적 의미론

프로그래밍 언어를 다른 언어로 번역하는 것은 종종 유용합니다.예를 들어 동시 프로그래밍 언어는 프로세스 미적분으로 변환될 수 있고, 고급 프로그래밍 언어는 바이트 코드로 변환될 수 있습니다(실제로, 기존의 표현적 의미론은 프로그래밍 언어를 도메인 카테고리의 내부 언어로 해석하는 것으로 볼 수 있습니다).

이 맥락에서, 완전한 추상화와 같은 표현적 의미론으로부터의 개념은 보안 우려를 ^[17][18]충족시키는 데 도움이 됩니다.

추상화

종종 표현적 의미론과 운영적 의미론을 연결하는 것이 중요하다고 여겨집니다.이것은 표현적 의미론이 다소 수학적이고 추상적이며, 운영적 의미론이 보다 구체적이거나 계산적 직관들에 가까울 때 특히 중요하다.표현적 의미론의 다음과 같은 특성이 종종 관심을 끈다.

1. 구문의 독립성:프로그램의 표기는 소스 언어의 구문을 포함하지 않아야 합니다.
2. 적정성(또는 건전성):눈에 띄게 구별되는 모든 프로그램에는 구별되는 의미가 있습니다.
3. 완전 추상화:관측적으로 동등한 모든 프로그램은 동일한 표시를 가집니다.

전통적인 스타일의 의미론에서, 적절성과 완전한 추상화는 대략적으로 "운영적 등가성이 표현적 평등과 일치한다"는 요구사항으로 이해될 수 있다.행위자 모델 및 프로세스 계산과 같은 보다 집중적인 모델에서의 표현적 의미론에는 각 모델 내에서 동등성에 대한 다른 개념이 있기 때문에 적절성과 완전한 추상화의 개념은 논쟁의 문제이며 정확히 밝히기가 어렵습니다.또한 연산 의미론과 표현 의미론의 수학적 구조는 매우 가까워질 수 있다.

운용 시멘틱스와 표기 시멘틱스 사이에 보유할 수 있는 기타 바람직한 속성은 다음과 같습니다.

1. 구성주의:구성주의는 도메인 요소들이 건설적인 방법으로 존재함을 보여줄 수 있는지와 관련이 있다.
2. 표현적 의미론 및 운영적 의미론의 독립성:표현적 의미론은 프로그래밍 언어의 운영 의미론과는 독립적인 수학적 구조를 사용하여 공식화해야 한다.그러나 기본 개념은 밀접하게 관련되어 있을 수 있습니다.아래 '구성' 섹션을 참조하십시오.
3. 완전성 또는 정의 가능성:의미 모델의 모든 형태론은 프로그램의 ^[19]표현이어야 한다.

구성성

프로그래밍 언어의 표현적 의미론의 중요한 측면은 프로그램의 표기가 그 부분의 표기로 구성되는 구성성이다.예를 들어, "7 + 4"라는 식을 생각해 보십시오.이 경우의 구성성은 "7"과 "4" 및 "+"의 의미 측면에서 "7 + 4"에 대한 의미를 제공하는 것이다.

도메인 이론에서 기본적인 표현적 의미론은 다음과 같이 주어지기 때문에 구성적이다.우선 프로그램 조각, 즉 자유 변수가 있는 프로그램을 고려합니다.입력 컨텍스트는 각 자유 변수에 유형을 할당합니다.예를 들어 식(x + y)에서 입력 컨텍스트(x:nat,y:nat)는, 다음의 스킴을 사용해 프로그램 fragment에 지시적 의미를 부여합니다.

1. 먼저 우리 언어 유형의 의미를 설명하는 것으로 시작합니다. 각 유형의 의미는 도메인이어야 합니다.우리는 τ형을 나타내는 도메인에는 τ을 씁니다.예를 들어, 타입의 의미는nat자연수의 영역이어야 합니다. 〚nat=$$= $N$ \$displaystyle$ \$mathbb {$N } $。$_⊥
2. 유형의 의미로부터 우리는 문맥을 입력하는 의미를 도출한다.【x₁:】【x_n:】【x:】【x:】【x:】【x:】【x₁:】【...】으로_1n 설정했습니다.예를 들어_n, x:nat,y:nat= $N(\displaystyle$ \$mathbb$ {N$})$_⊥ × $(\displaystyle$ \$mathbb$ {N$\}).$_⊥ 특별한 경우 변수가 없는 빈 입력 컨텍스트의 의미는 1로 표시된 하나의 요소를 가진 도메인입니다.
3. 마지막으로 각 프로그램 문맥에 의미를 부여해야 합니다.P가 타입 「」의 프로그램 fragment로, 컨텍스트 「」를 입력하는 경우는, 「P:」라고 하는 경우가 많다고 합니다.다음으로 이 program-in-typing-context의 의미는 연속함수 δP여야 합니다.σ : 〚〚 → 〛〛〛 。예를 들어 77:natθ:${\displaystyle \mathbb{}}$→ $N(\displaystyle$ \$mathbb$ {N$})$은_⊥ 상시 "7" 함수이며, θx:nat,y:natx+y:nat: : $N \displaystyle \mathbb$ {$}$$$_⊥×$N$ \$displaystyle \mathbb$ {N$}$_⊥→$N \displaystyle$ \$mathbb$ {N$}$은_⊥ 두 숫자를 더하는 함수이다.

여기서 복합식(7+4)의 의미는 세 가지 함수 δ7을 합성하여 구한다.nat§:${\displaystyle \mathbb{}}$→ $N(\displaystyle$ \$mathbb$ {N$}),$_⊥§4:natθ:${\displaystyle \mathbb{}}$→$N \displaystyle$ \$mathbb$ {N$}$ 및$$_⊥δx:nat,y:natx+y:nat: : $N \displaystyle$ \$mathbb$ {N$}$_⊥ × ${\displaystyle \mathbb{}}$\$displaystyle$ \$mathbb$ {N$}$_⊥→$N \displaystyle$ \$mathbb$ {N$\}$_⊥ 。

사실, 이것은 구성적 표현적 의미론을 위한 일반적인 체계이다.여기에는 도메인 및 연속 함수에 대한 구체적인 내용은 없습니다.대신 다른 카테고리로 작업할 수 있습니다.예를 들어, 게임 의미론에서, 게임의 카테고리는 게임을 개체로, 전략을 형태론으로 가지고 있다: 우리는 유형을 게임으로, 프로그램을 전략으로 해석할 수 있다.일반적인 재귀가 없는 단순한 언어에 대해서는 집합과 함수의 범주로 해결할 수 있습니다.부작용이 있는 언어는 클라이슬리 카테고리에서 모나드 작업을 할 수 있습니다.스테이트가 있는 언어의 경우 펑터 카테고리에서 작업할 수 있습니다.밀너는 인터페이스를 개체로, 빅그래프를 형태론으로 ^[20]하는 카테고리에서 작업함으로써 모델링 위치와 상호작용을 지지해 왔다.

의미론과 구현

Dana Scott(1980)^[21]에 따르면:

시멘틱스가 실장을 결정할 필요는 없지만, 실장이 올바르다는 것을 나타내는 기준을 제공해야 한다.

Clinger(1981)^{[22]: 79} 에 따르면:

그러나 보통, 전통적인 순차 프로그래밍 언어의 형식적 의미론 자체가 언어의 (비효율적인) 구현을 제공하는 것으로 해석될 수 있다.그러나 형식적 의미론은 항상 그러한 구현을 제공할 필요는 없으며, 의미론이 반드시 구현을 제공해야 한다고 믿는 것은 동시 언어의 형식적 의미론에 대한 혼란을 초래한다.이러한 혼란은 프로그래밍 언어의 의미론에서 무제한 비결정론의 존재가 프로그래밍 언어가 구현될 수 없음을 암시한다고 할 때 고통스러울 정도로 명백하다.

컴퓨터 사이언스의 다른 분야와의 연결

표현적 의미론에서 일부 연구는 유형을 모델 이론의 한 분야로 볼 수 있는 도메인 이론의 의미에서 도메인으로 해석하여 유형 이론과 범주 이론과의 연관성을 이끌어냈다.컴퓨터 과학에서는 추상 해석, 프로그램 검증, 모델 확인과 관련이 있습니다.

레퍼런스

추가 정보

교재

강의 노트

기타 참고 자료

외부 링크

Wikibook Haskell에는 다음과 같은 토픽의 페이지가 있습니다.

• 표현적 의미론.Lloyd Allison의 책 개요
• Schreiner, Wolfgang (1995). "Structure of Programming Languages I: Denotational Semantics". Course notes.