표시적 의미론

"오늘의AI위키"는 AI 기술로 일관성 있고 체계적인 최신 지식을 제공하는 혁신 플랫폼입니다.
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.

1. 개요

표시적 의미론은 1970년대 초 크리스토퍼 스트레이치와 데이나 스콧의 연구에서 시작된 컴퓨터 프로그램의 의미를 수학적으로 정의하는 방법이다. 프로그램의 의미를 입력을 출력으로 매핑하는 함수로 표현하며, 재귀 프로그램의 의미를 부여하기 위해 스콧 연속 함수를 사용한다. 구성성, 추상화, 다양한 프로그래밍 기능의 의미론을 다루며, 프로그램 분석, 검증, 프로그래밍 언어 번역 등 다양한 분야에 응용된다. 타입 이론, 범주론, 추상 해석, 프로그램 검증, 함수형 프로그래밍 등과 연관되어 있으며, 한국 프로그래밍 언어 연구에도 기여하고 있다.

더 읽어볼만한 페이지

1970년 컴퓨팅 - 커누스-모리스-프랫 알고리즘
커누스-모리스-프랫 알고리즘은 문자열 검색 알고리즘으로, 부분 일치 테이블을 이용하여 불필요한 비교를 줄여 효율적으로 특정 검색어의 위치를 찾으며 시간 복잡도는 O(n + k)이다.
프로그래밍 언어 의미론 - 리스코프 치환 원칙
리스코프 치환 원칙은 객체 지향 프로그래밍에서 하위 타입이 상위 타입으로 대체될 수 있어야 한다는 원칙으로, 하위 타입은 상위 타입의 조건을 준수해야 하며, 클래스 계층 구조 설계의 지침이 된다.
프로그래밍 언어 의미론 - 의미론 (컴퓨터 과학)
의미론 (컴퓨터 과학)은 프로그램의 동작을 수학적 모델로 표현하여 정확성 검증, 컴파일러 최적화, 프로그래밍 언어 설계 등에 활용하는, 프로그램의 의미를 형식적으로 정의하고 분석하는 분야이다.
컴퓨터 과학 내 논리 - 자동화된 추론
자동화된 추론은 컴퓨터 프로그램을 사용하여 논리적 추론을 수행하는 인공지능 분야로, 수리 논리학의 발전과 초기 연구를 통해 자동 정리 증명 분야의 기틀을 마련했으며, AI 겨울을 겪었지만 소프트웨어 검증 등 다양한 분야에 활용되며 Coq, HOL Light 등의 증명 보조기가 개발되어 난제들의 형식적 증명에 기여했다.
컴퓨터 과학 내 논리 - 혼 절
혼 절은 하나의 긍정 리터럴만을 포함하는 분리절이며, 논리 프로그래밍, 자동 정리 증명, 데이터베이스 이론 등 여러 분야에 응용된다.

표시적 의미론

2. 역사적 발전

표시적 의미론은 1970년대 초 크리스토퍼 스트레이치와 데이나 스콧의 연구에서 시작되었다.^[1]^[2] 스트레이치와 스콧은 컴퓨터 프로그램의 의미를 입력을 출력으로 매핑하는 함수로 제공하고, 재귀적으로 정의된 프로그램에 의미를 부여하기 위해 영역 이론의 완전 부분 순서인 연속 함수를 사용하는 것을 제안했다.

표시적 의미론은 병행 컴퓨팅 및 예외 처리와 같은 기능을 사용하는 최신 프로그래밍 언어, 예를 들어 병렬 ML,^[4] CSP,^[5] 및 하스켈에 대해 개발되었다.^[6] 이러한 언어의 의미는 구문의 의미가 하위 구문의 의미에 의존한다는 점에서 구성적이다. 예를 들어, 응용 프로그래밍 언어의 `f(E1,E2)` 표현식의 의미는 하위 구문 f, E1 및 E2의 의미에 따라 정의된다. 최신 프로그래밍 언어에서 E1과 E2는 동시에 평가될 수 있으며, 그 중 하나의 실행은 공유 객체를 통해 상호 작용하여 서로의 의미가 정의되도록 하여 다른 하나에 영향을 미칠 수 있다. 또한 E1 또는 E2는 다른 하나의 실행을 종료할 수 있는 예외를 발생시킬 수 있다.

1964년 크리스토퍼 스트레이치는 형식 언어 기술 언어(formal language description language)에 관한 IFIP 작업부회를 위해 "Towards a formal semantics"라는 논문을 작성했다. 이 논문에서 스트레이치는 추상 구문을 함수에 사상시키고, 함수의 합성으로 정의된 의미 함수를 도입하여, 고정점 조합 연산자 Y를 사용하여 루프의 의미를 표시했다. 그러나 프로그램 요소의 표시적 의미(denotation)는 무형 람다 계산(type-free lambda calculus)에 사상되는 형태였지만, 무형 람다 계산의 수학적 모델이 밝혀지지 않았다는 문제가 있었다. 즉, 고정점 조합 연산자 Y는 조작적으로 규칙으로 해석할 수 있었지만, 표시적 의미로서 어떤 함수를 나타낸다고 생각할 수 없었다.^[26]

1969년, 데이나 스콧은 크리스토퍼 스트레이치와의 공동 연구를 통해 무형 람다 계산이 수학적 모델을 가진다는 것을 발견하고, 의미 기술법의 기초가 되는 영역 이론을 구축했다.

2. 1. 초기 연구

표시적 의미론은 1970년대 초 크리스토퍼 스트레이치와 데이나 스콧의 연구에서 시작되었다.^[1]^[2] 스트레이치와 스콧이 처음 개발한 표시적 의미론은 컴퓨터 프로그램의 의미를 입력을 출력으로 매핑하는 함수로 제공했다.^[2] 재귀적으로 정의된 프로그램에 의미를 부여하기 위해 스콧은 영역 이론의 완전 부분 순서인 연속 함수를 사용하는 것을 제안했다.

1964년 크리스토퍼 스트레이치는 형식 언어 기술 언어(formal language description language)에 관한 IFIP 작업부회를 위해 "Towards a formal semantics"라는 논문을 작성했다. 이 논문은 추상 구문을 함수(편의상 함수는 무형 람다 계산으로 표현되었다)에 사상시키고, 함수의 합성으로 정의된 의미 함수를 도입하여, 고정점 조합 연산자 Y를 사용하여 루프의 의미를 표시했다. 여기서 이론적으로 문제였던 것은, 프로그램 요소의 표시적 의미(denotation)는, 형식적으로는, 무형 람다 계산(type-free lambda calculus)에 사상되는 형태였지만, 그 핵심인 무형 람다 계산의 수학적 모델이 밝혀지지 않았다는 것이었다. 즉, 고정점 조합 연산자 Y는 조작적으로 규칙으로 해석할 수 있었지만, 표시적 의미로서 어떤 함수를 나타낸다고 생각할 수 없었다.^[26]

1969년, 스트레이치의 이론에 흥미를 느낀 데이나 스콧은 스트레이치와의 공동 연구 끝에 무형 람다 계산이 수학적 모델을 가진다는 것을 발견했다. (처음에는 기대하지 않았던 결과였다.) 그 후 스콧은 의미 기술법의 기초가 되는 영역 이론을 구축했다.

2. 2. 영역 이론 발전

1969년, 데이나 스콧은 크리스토퍼 스트레이치의 이론에 관심을 갖고 공동 연구를 진행하여, 무형 람다 계산에 대한 수학적 모델을 발견하였다. 그 결과, 스콧은 의미 기술법의 기초가 되는 영역 이론을 구축했다.^[26]

3. 핵심 개념

표시적 의미론은 1970년대 초 크리스토퍼 스트레이치와 데이나 스콧의 연구에서 시작되었다.^[1]^[2] 병행 컴퓨팅 및 예외 처리와 같은 기능을 사용하는 최신 프로그래밍 언어(예: 병렬 ML,^[4] CSP,^[5] 하스켈)^[6]의 의미를 표현하기 위해 개발되었다.

표시적 의미론의 핵심 개념은 다음과 같다.

표시(Denotation): 프로그램의 의미를 함수로 표현한다. 예를 들어, "n*m" 구문은 n과 m의 값에 따라 결과값을 생성하는 함수로 볼 수 있다.^[2]
영역(Domain): 계산의 의미를 나타내는 수학적 구조로, 완전 부분 순서 집합 등이 있다.
부동점 의미론(Fixed-Point Semantics): 재귀적 정의를 갖는 프로그램(예: 팩토리얼 함수)의 의미를 최소 고정점을 이용하여 설명한다.

3. 1. 표시 (Denotation)

크리스토퍼 스트레이치와 데이나 스콧이 1970년대 초에 개발한 표시적 의미론에서, 컴퓨터 프로그램의 의미는 입력을 출력으로 매핑하는 함수로 표현된다.^[2] 예를 들어, "n*m" 구문은 두 개의 자유 변수 "n"과 "m"에 대한 바인딩이 있는 환경에서 "n"의 값이 3이고 "m"의 값이 5이면 15를 생성하는 함수로 볼 수 있다.^[2]

함수는 인수와 결과 값의 순서쌍 집합으로 표현될 수 있다. 예를 들어, {(0,1), (4,3)} 집합은 인수 0에 대해 결과 1, 인수 4에 대해 결과 3을 반환하고, 그렇지 않은 경우 정의되지 않은 함수를 나타낸다.

재귀적으로 정의된 프로그램에 의미를 부여하기 위해 스콧은 영역 이론의 완전 부분 순서인 연속 함수를 사용하는 것을 제안했다. 예를 들어, 팩토리얼 함수는 다음과 같이 재귀적으로 정의될 수 있다.

```c

int factorial(int n) {

if (n == 0) then return 1;

else return n * factorial(n-1);

}

```

이 재귀적 정의의 의미는 각 근사가 팩토리얼 호출 횟수를 제한하는 근사의 극한으로 구축된다.

`F`⁰({})은 완전히 정의되지 않은 부분 함수로, {} 집합으로 표현된다.
`F`¹({})은 집합 {(0,1)}로 표현되는 부분 함수이다. 0에서 1로 정의되고 다른 곳에서는 정의되지 않는다.
`F`⁵({})은 집합 {(0,1), (1,1), (2,2), (3,6), (4,24)}로 표현되는 부분 함수이다. 인수 0, 1, 2, 3, 4에 대해 정의된다.

이 반복 프로세스는 최소 고정점을 가지며, 이는 전체 factorial 함수이다.

다음은 factorial 함수의 표시에 대한 또 다른 예시이다.

함수 `factorial`이 다음과 같이 정의되어 있다고 가정한다.

```

factorial ≡ λ(n)if (n==0)then 1 else n*factorial(n-1)

```

`factorial`의 '''`graph`'''는 인자와 값의 쌍으로 이루어진 순서 집합이며, 다음과 같다.

: `graph`(factorial) = {|n∈ω} = {<0,1>,<1,1>,<2,2>,<3,6>,<4,24>…}

`factorial` 프로그램의 표시(의미) `Denote`_factorial는 다음과 같이 구성된다.

```

Denote_factorial = graph(factorial) = ∪_i∈ω progression_factorialⁱ({})

```

여기서

```

progression_factorial(g) ≡ λ(n)if (n==0)then 1 else n*g(n-1)

```

단, `progression`_factorial은 고정점 연산자이며, 최소 고정점 `Denote`_factorial는 다음과 같다.

```

Denote_factorial = progression_factorial(Denote_factorial)

```

또한, `progression`_factorial은 ω-연속이다.

3. 2. 영역 (Domain)

영역(Domain)은 계산의 의미를 표현하는 데 사용되는 수학적 구조이다. 대표적인 예로 완전 부분 순서 집합(CPO)이 있다.

관계 `x≤y`는 `x`가 `y`로 계산적으로 발전할 수 있음을 의미한다. 표시가 완전 부분 순서 집합의 요소라면, 예를 들어 `f≤g`는 `f`가 정의된 모든 값에 대해 `g`와 같음을 의미한다.

계산 영역은 다음과 같은 특징을 갖는다.

특징	설명
하한의 존재	영역에는 반드시 `⊥`로 표시되는 요소가 포함되어 있으며, 영역 내의 임의의 요소 `x`에 대해 `⊥≤x`가 성립한다.
상한의 존재	계산을 계속하면 표시는 정제되지만, 한계를 가져야 한다. 그러므로, $\forall i \in \omega$ $x_i \le x_{i+1}$ 일 때, 상한 $\vee_{i \in \omega} x_i$ 가 존재한다. 이것을 $\omega$ -완전이라고 부른다.
유한 요소는 가산	유향 집합 `A`에 대해 `∨A`가 존재하고 $x \le \vee A$ 일 때, $x \le a$ 인 $a \in A$ 가 존재한다. 그럴 때, 요소 `x`는 유한이라고 한다(영역 이론적으로 말하면, isolated). 바꿔 말하면, `x`에 도달하거나 `x`를 넘어서는 것이 유한의 프로세스로 가능하다면, `x`는 유한이다.
모든 요소는 유한 요소의 순차열의 상한이다	임의의 요소에 유한의 계산 절차로 도달할 수 있음을 의미한다.
영역은 downward closed이다

시스템 `S`에 관한 수학적 표시는, 초기 빈 표시 `⊥_S`에서 시작하여, 표시 근사 함수 `'''progression'''_S`를 사용하여 `S`의 표시(의미)를 구축해 나감으로써 더 나은 근사를 만드는 것으로 구축된다.

`'''Denote'''_S ≡ ∨_i∈ω '''progression'''_Sⁱ(⊥_S)`

여기서, `'''progression'''_S`는 "단조"여야 하며, `x≤y`일 때 `'''progression'''_S(x)≤'''progression'''_S(y)`이다. 더 일반적으로 표현하면 다음과 같다.

`'''progression'''_S(∨_i∈ω x_i) = ∨_i∈ω '''progression'''_S(x_i)` (단,`∀i∈ω x_i≤x_i+1`)

이러한 `'''progression'''_S`의 특징을 ω-연속이라고 부른다.

표시적 의미론에서는, `'''Denote'''_S`의 방정식에 따라 표시(의미)를 생성 가능한지 여부를 주제로 한다. 계산 영역 이론의 기본적인 정리는, `'''progression'''_S`가 ω-연속이라면, `'''Denote'''_S`가 존재한다는 것이다.

`'''progression'''_S`가 ω-연속이기 때문에 다음이 성립한다.

`'''progression'''_S('''Denote'''_S) = '''Denote'''_S`

이것은 `'''Denote'''_S`가 `'''progression'''_S`의 "부동점; fixed point"임을 의미한다.

이 부동점은 `'''progression'''_S`의 부동점 중에서 극소이다.

3. 3. 부동점 의미론 (Fixed-Point Semantics)

Fixed-point semantics^영어는 재귀적 정의를 갖는 프로그램(예: 팩토리얼 함수)의 의미를 최소 고정점을 이용하여 설명한다.

예를 들어, 다음과 같이 재귀적으로 정의될 수 있는 팩토리얼 함수를 고려해 보자.^[2]

```c

int factorial(int n) {

if (n == 0) then return 1;

else return n * factorial(n-1);

}

```

이 재귀적 정의에 대한 의미를 제공하기 위해, 각 근사가 팩토리얼 호출 횟수를 제한하는 근사의 극한으로 지시 사항이 구축된다. 처음에 우리는 호출이 없으므로 아무것도 정의되지 않는다. 다음 근사에서는 팩토리얼을 다시 호출할 필요가 없으므로 순서쌍 (0,1)을 추가할 수 있다. 마찬가지로 (1,1), (2,2) 등을 추가할 수 있으며, ''factorial(n)''을 계산하려면 ''n+1''번 호출해야 하므로 각 연속적인 근사에 한 쌍씩 추가할 수 있다. 극한에서는

\mathbb{N}

에서

\mathbb{N}

으로의 전체 함수를 도메인의 모든 곳에서 정의한다.^[2]

공식적으로 각 근사를 부분 함수

\N \rightharpoonup \N

으로 모델링한다. 그러면 "더 정의된 부분 팩토리얼 함수 만들기"를 구현하는 함수, 즉

F : (\N \rightharpoonup \N) \to (\N \rightharpoonup \N)

을 반복적으로 적용하여 근사치를 구한다. 시작은 빈 함수(빈 집합)으로 한다. ''F''는 다음과 같이 코드로 정의할 수 있다.(

\N \rightharpoonup \N

에 Map 사용):^[2]

```cpp

int factorial_nonrecursive(Map factorial_less_defined, int n)

{

if (n == 0) then return 1;

else if (fprev = lookup(factorial_less_defined, n-1)) then

return n * fprev;

else

return NOT_DEFINED;

}

Map F(Map factorial_less_defined)

{

Map new_factorial = Map.empty();

for (int n in all()) {

if (f = factorial_nonrecursive(factorial_less_defined, n) != NOT_DEFINED)

new_factorial.put(n, f);

}

return new_factorial;

}

```

그런 다음 ''Fⁿ'' 표기법을 도입하여 ''F''가 ''n''번 적용됨을 나타낼 수 있다.^[2]

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

이 반복 프로세스는

\mathbb{N}

에서

\mathbb{N}

으로의 부분 함수의 시퀀스를 구축한다. 부분 함수는 순서가 ⊆를 사용하여 사슬 완비 부분 순서를 형성한다. 또한 팩토리얼 함수의 더 나은 근사의 이 반복 프로세스는 각

F^i\le F^{i+1}

가 ⊆를 순서로 사용하여 확장(진보적이라고도 함) 매핑을 형성한다. 따라서 고정점 정리 (특히 부르바키-비트 정리)에 의해, 이 반복 프로세스에 대한 고정점이 존재한다.^[2]

이 경우, 고정점은 이 사슬의 최소 상한이며, 이는 전체 factorial^영어 함수이며, 합집합으로 표현할 수 있다.^[2]

:

\bigcup_{i \in \mathbb N} F^i(\{\}).

우리가 찾은 고정점은 ''F''의 최소 고정점이다. 왜냐하면 우리의 반복은 도메인의 가장 작은 요소(빈 집합)으로 시작했기 때문이다. 이것을 증명하기 위해서는 크나스터-타르스키 정리와 같은 더 복잡한 고정점 정리가 필요하다.^[2]

함수 factorial이 다음과 같이 정의되어 있다고 가정한다.^[2]

:factorial \equiv \lambda(n)if (n==0)then 1 else n*factorial(n-1)

factorial의 '''graph'''는 인자와 값의 쌍으로 이루어진 순서 집합이며, 다음과 같다.^[2]

: '''graph'''(factorial) = {|n∈ω} = {<0,1>,<1,1>,<2,2>,<3,6>,<4,24>…}

factorial 프로그램의 표시(의미) '''Denote'''_factorial는 다음과 같이 구성된다.^[2]

: '''Denote'''_factorial = '''graph'''(factorial) = \cup_{i\in\omega} '''progression'''_factorialⁱ({})

여기서

:'''progression'''_factorial(g) \equiv \lambda(n)if (n==0)then 1 else n*g(n-1)

단, '''progression'''_factorial은 고정점 연산자이며, 최소 고정점 '''Denote'''_factorial는 다음과 같다.^[2]

:'''Denote'''_factorial = '''progression'''_factorial('''Denote'''_factorial)

또한, '''progression'''_factorial은 ω-연속이다.^[2]

4. 주요 특징

표시적 의미론은 크리스토퍼 스트레이치와 데이나 스콧의 연구에서 시작되었으며, 컴퓨터 프로그램의 의미를 입력과 출력을 매핑하는 함수로 제공한다.^[1]^[2] 재귀적으로 정의된 프로그램에 의미를 부여하기 위해 스콧은 영역 이론에서 완전 부분 순서인 연속 함수를 사용하는 것을 제안했다. 이후 순차성, 병행성, 비결정성, 지역 상태와 같은 프로그래밍 언어 측면에 대한 연구가 계속 진행되었다.

표시적 의미론은 병행 컴퓨팅 및 예외 처리 기능을 사용하는 병렬 ML,^[4] CSP,^[5] 하스켈^[6]과 같은 최신 프로그래밍 언어에 대해 개발되었다.

많은 연구자들은 영역 이론적 모델이 동시적 계산에 충분하지 않다고 주장하여, 새로운 모델들이 도입되었다. 1980년대 초에는 동시 언어의 의미를 부여하기 위해 표시적 의미론 방식을 사용하기 시작했는데, 윌 클링거의 액터 모델 연구, 글린 윈스켈의 이벤트 구조와 페트리넷 연구,^[8] 프랑스, 호어, 레만, 드 로버(1979)의 CSP에 대한 트레이스 의미론 연구^[9] 등이 그 예이다.

최근 윈스켈 등은 동시성을 위한 영역 이론으로 프로펀터 범주를 제안했다.^[10]^[11]

표시적 의미론과 관련하여 중요하게 여겨지는 속성은 다음과 같다.

속성	설명
구문 독립성	프로그램의 지시적 의미는 소스 언어의 구문을 포함하지 않아야 한다.
적절성 (또는 건전성)	관찰적으로 구별되는 프로그램은 서로 다른 지시적 의미를 가진다.
완전 추상화	관찰적으로 동일한 프로그램은 동일한 지시적 의미를 가진다.

그 외에 표시적 의미론과 동작적 의미론에서 유지하는 것이 바람직한 특징으로는 '''구축 가능성''', '''진보성''', '''완전 완전성'''(또는 '''정의 가능성''')^[19] 등이 있다.

4. 1. 구성성 (Compositionality)

Compositionality|구성성^영어은 프로그램의 의미가 각 부분의 의미로부터 구성되는 방식을 의미한다. 예를 들어, "7 + 4"라는 표현식을 생각해 보면, 이 표현식의 의미는 "7", "4", 그리고 "+" 각 부분의 의미를 조합하여 구성된다.^[2]

도메인 이론에서 기본적인 표시적 의미론은 다음과 같이 구성된다. 우선 자유 변수를 가진 프로그램 조각을 생각해 보자. 여기서 ''타이핑 컨텍스트''는 각 자유 변수에 타입을 할당한다. 예를 들어, (''x'' + ''y'')라는 표현식은 (''x'':,''y'':) 라는 타이핑 컨텍스트에서 생각해 볼 수 있다.

이제 다음 체계를 사용하여 프로그램 조각에 표시적 의미론을 제공한다.

# 먼저 언어 타입의 의미를 설명한다. 각 타입의 의미는 도메인이어야 한다. 〚τ〛를 타입 τ를 나타내는 도메인으로 표기한다. 예를 들어, 타입의 의미는 자연수의 도메인이어야 한다. 즉, 〚〛=

\mathbb{N}

_⊥이다.

# 타입의 의미로부터 타이핑 컨텍스트의 의미를 도출한다. 〚 ''x''₁:τ₁,..., ''x''_n:τ_n〛 = 〚 τ₁〛× ... ×〚τ_n〛로 정의한다. 예를 들어, 〚''x'':,''y'':〛=

\mathbb{N}

_⊥×

\mathbb{N}

_⊥이다. 변수가 없는 빈 타이핑 컨텍스트의 의미는 1로 표기되는 하나의 요소를 가진 도메인이다.

# 마지막으로, 각 프로그램 조각에 의미를 부여한다. ''P''가 타이핑 컨텍스트 Γ에서 타입 σ를 가지는 프로그램 조각이라고 할 때 (Γ⊢''P'':σ로 표기), 이 프로그램의 의미는 연속 함수 〚Γ⊢''P'':σ〛:〚Γ〛→〚σ〛여야 한다. 예를 들어, 〚⊢7:〛:1→

\mathbb{N}

_⊥는 항상 "7"을 나타내는 함수이고, 〚''x'':,''y'':⊢''x''+''y'':〛:

\mathbb{N}

_⊥×

\mathbb{N}

_⊥→

\mathbb{N}

_⊥는 두 숫자를 더하는 함수이다.

복합 표현식 (7+4)의 의미는 세 함수 〚⊢7:〛:1→

\mathbb{N}

_⊥, 〚⊢4:〛:1→

\mathbb{N}

_⊥, 그리고 〚''x'':,''y'':⊢''x''+''y'':〛:

\mathbb{N}

_⊥×

\mathbb{N}

_⊥→

\mathbb{N}

_⊥를 구성하여 결정된다.

이것은 구성적 표시적 의미론을 위한 일반적인 체계이며, 도메인과 연속 함수에 대한 구체적인 내용은 포함하지 않는다. 대신 다른 범주를 사용할 수 있다. 예를 들어, 게임 의미론에서 게임 범주는 게임을 객체로, 전략을 사상으로 갖는데, 타입을 게임으로, 프로그램을 전략으로 해석할 수 있다. 일반적인 재귀가 없는 단순한 언어의 경우, 집합과 함수의 범주로 충분하다. 모나드를 사용하는 클라이슬리 범주는 부작용이 있는 언어에 사용할수 있다. 상태가 있는 언어의 경우, 함자 범주에서 작업할 수 있다. 밀너는 인터페이스를 객체로, ''bigraphs''를 사상으로 하는 범주에서 작업하여 위치와 상호 작용을 모델링하는 것을 옹호했다.^[20]

4. 2. 추상화 (Abstraction)

표시적 의미론은 크리스토퍼 스트레이치와 데이나 스콧의 연구에서 시작되었으며, 컴퓨터 프로그램의 의미를 입력과 출력을 매핑하는 함수로 제공한다.^[1]^[2] 재귀적으로 정의된 프로그램에 의미를 부여하기 위해 스콧은 영역 이론의 완전 부분 순서인 연속 함수를 사용하는 것을 제안했다.

표시적 의미론과 관련하여 중요하게 여겨지는 속성은 다음과 같다.

속성	설명
구문 독립성	프로그램의 지시적 의미는 소스 언어의 구문을 포함하지 않아야 한다.
적절성 (또는 건전성)	모든 관찰적으로 구별되는 프로그램은 서로 다른 지시적 의미를 가진다.
완전 추상화	모든 관찰적으로 동일한 프로그램은 동일한 지시적 의미를 가진다.

특히, 완전 추상화의 특징은 다음과 같다.

'''추상성''': 표시적 의미론은 프로그래밍 언어의 조작적 의미론이나 표현과는 독립적인 수학적 구조에 의해 형식화된다.
'''정당성''': 관찰되는 동작이 다른 프로그램은 표시도 다르다.
'''완전성''': 표시가 다른 프로그램은 관찰되는 동작도 달라야 한다.

표시적 의미론에서 오랫동안 해결되지 않은 과제는 재귀적 자료형이 있는 경우, 특히 재귀에 이용 가능한 자연수형의 완전 추상화였다. 이 문제는 1990년대에 게임 의미론에 의해 완전 추상 모델이 구축되면서 해결되었다.

5. 다양한 프로그래밍 기능의 의미론

표시적 의미론은 병렬 ML,^[4] CSP,^[5] 하스켈^[6]과 같이 병행 컴퓨팅 및 예외 처리 기능을 사용하는 최신 프로그래밍 언어에 대해 개발되었다. 이러한 언어의 의미는 구문의 의미가 하위 구문의 의미에 의존한다는 점에서 구성적이다. 예를 들어, 응용 프로그래밍 언어의 `f(E1,E2)` 표현식의 의미는 하위 구문 f, E1 및 E2의 의미에 따라 정의된다. 최신 프로그래밍 언어에서 E1과 E2는 동시에 평가될 수 있으며, 이들 중 하나의 실행은 공유 객체를 통해 상호 작용하여 서로의 의미가 정의되도록 하여 다른 하나에 영향을 미칠 수 있다. 또한 E1 또는 E2는 다른 하나의 실행을 종료할 수 있는 예외를 발생시킬 수 있다.

5. 1. 비결정적 프로그램 (Non-deterministic Programs)

멱영역 개념은 비결정적 순차 프로그램에 대한 표시적 의미론을 제공하기 위해 개발되었다. 멱영역 생성자를 ''P''로 표기하면, 도메인 ''P''(''D'')는 ''D''로 표시되는 유형의 비결정적 계산 도메인이 된다.

도메인 이론적인 비결정성 모델에서는 공정성과 무제한적 비결정성에 어려움이 있다.^[7]

5. 2. 병행성 (Concurrency)

많은 연구자들이 영역 이론적 모델이 동시적 계산의 일반적인 경우에 충분하지 않다고 주장해 왔다. 이러한 이유로 다양한 새로운 모델이 도입되었다. 1980년대 초, 사람들은 동시 언어의 의미를 부여하기 위해 표시적 의미론 방식을 사용하기 시작했다. 예로는 윌 클링거의 액터 모델 연구, 글린 윈스켈의 이벤트 구조와 페트리넷 연구,^[8] 프랑스, 호어, 레만, 드 로버(1979)의 CSP에 대한 트레이스 의미론 연구가 있다.^[9] 이러한 모든 연구는 지속적으로 연구되고 있다(예: CSP에 대한 다양한 표시적 모델 참조^[5]).

최근 윈스켈 등은 동시성을 위한 영역 이론으로 프로펀터 범주를 제안했다.^[10]^[11] 프로세스 대수에 기반한 표시적 의미론도 병행성에 관한 표시적 의미론으로 연구되었다. 표시적 의미론의 병행성으로의 확장은 어렵다는 것이 증명되었다. (무제한 비결정성 참조)

5. 3. 상태 (State)

상태(힙과 같은) 및 단순한 명령형 기능은 위에서 설명한 표시적 의미론에서 간단하게 모델링할 수 있다. 핵심 아이디어는 명령을 어떤 상태 도메인에 대한 부분 함수로 간주하는 것이다. "x:=3"의 의미는 상태를 x에 3을 할당한 상태로 바꾸는 함수이다. 시퀀스 연산자 ";"는 함수의 합성에 의해 표시된다. 그런 다음 고정점 구성을 사용하여 "while"과 같은 루핑 구문에 대한 의미론을 제공한다.^[12]^[13]

지역 변수가 있는 프로그램을 모델링하는 것은 더 어려워진다. 한 가지 접근 방식은 더 이상 도메인을 사용하지 않고, 대신 형식을 일부 세계 범주에서 도메인 범주로의 함자로 해석하는 것이다. 그런 다음 프로그램은 이러한 함자 간의 자연적인 연속 함수로 표시된다.^[12]^[13]

5. 4. 자료형 (Data Types)

sml

datatype list = Cons of nat * list | Empty

```

이 섹션에서는 변경할 수 없는 함수형 데이터 구조만 다룬다. 일반적인 명령형 프로그래밍 언어는 보통 이러한 재귀 목록의 요소를 변경할 수 있도록 허용한다.

또 다른 예로, 무형 람다 계산법의 지시적 의미의 유형은 다음과 같다.

```sml

datatype D = D of (D → D)

```

'도메인 방정식 풀기' 문제는 이러한 종류의 데이터 유형을 모델링하는 도메인을 찾는 것과 관련이 있다. 대략적으로 말하면, 한 가지 접근 방식은 모든 도메인의 집합을 도메인 자체로 간주한 다음 거기에서 재귀적 정의를 푸는 것이다.

다형성 자료형은 매개변수로 정의되는 자료형이다. 예를 들어, α 의 유형은 다음과 같이 정의된다.

```sml

datatype α list = Cons of α * α list | Empty

```

따라서 자연수 리스트는 유형이고 문자열 리스트는 유형이다.

일부 연구자들은 다형성의 도메인 이론적 모델을 개발했다. 다른 연구자들은 또한 구성적 집합 이론 내에서 매개변수 다형성을 모델링해 왔다.

5. 5. 순차성 (Sequentiality)

추상화 문제는 PCF 언어의 완전한 표시적 의미론에서 오랫동안 해결되지 않은 중요한 문제였다. PCF가 어려운 이유는 이 언어가 매우 순차적이기 때문이다. 예를 들어, PCF에서는 병렬 OR 함수를 정의할 수 없다. 이러한 이유로, 앞에서 소개된 도메인 기반 접근 방식은 완전 추상적이지 않은 표시적 의미론을 제공한다.^[16]

1990년대에 게임 의미론의 개발과 논리 관계를 포함하는 기술을 통해 이 문제는 대부분 해결되었다.^[16] 더 자세한 내용은 PCF 페이지에서 확인할 수 있다.

6. 응용 및 다른 분야와의 연관성

표시적 의미론은 유형 이론 및 범주론과 연결된다. 영역 이론을 사용하여 타입을 영역으로 해석하는데, 이는 모형 이론의 한 분야로 간주될 수 있다. 컴퓨터 과학 내에서는 추상 해석, 프로그램 검증, 모형 검증과 연결된다.^[1]

다나 스콧(Dana Scott, 1980)은 의미론이 구현을 결정할 필요는 없지만, 구현이 올바르다는 것을 보여주는 기준을 제공해야 한다고 말했다.^[21] 클린저(Clinger, 1981)는 기존 순차적 프로그래밍 언어의 형식적 의미론은 그 언어의 비효율적인 구현을 제공하는 것으로 해석될 수 있지만, 형식적 의미론이 항상 구현을 제공할 필요는 없다고 언급했다.^[22]

6. 1. 프로그래밍 언어 번역

표시적 의미론은 한 프로그래밍 언어를 다른 언어로 번역하는 데 사용될 수 있다. 예를 들어, 병행 프로그래밍 언어는 프로세스 대수로 번역될 수 있고, 고급 프로그래밍 언어는 바이트 코드로 번역될 수 있다.^[17]^[18] (실제로, 전통적인 표시적 의미론은 프로그래밍 언어를 범주론의 내부 언어로 해석하는 것으로 볼 수 있다.)

이러한 맥락에서, 완전 추상화 같은 표시적 의미론의 개념은 보안 문제를 해결하는 데 도움이 된다.

6. 2. 기타 관련 분야

표시적 의미론은 영역 이론을 사용하여 타입을 영역으로 해석한다. 영역 이론은 모델 이론에서 파생된 것으로 볼 수 있으며, 타입 이론이나 범주론과도 관련된다. 컴퓨터 과학에서는 추상 해석, 프로그램 검증, 함수형 프로그래밍과 밀접한 관련이 있으며, 모나드 개념 등과도 관련이 있다. 또한, 지속 개념은 역사적으로 절차적 프로그램의 제어 흐름(goto 문) 등의 의미론을 제공하기 위해 발견되었다.

참조

_[1] 논문 Outline of a mathematical theory of computation https://ropas.snu.ac[...] Oxford University Computing Laboratory 1970-11
_[2] 간행물 Toward a mathematical semantics for computer languages Oxford Programming Research Group Technical Monograph. 1971
_[3] 논문 J. Games In The Semantics Of Programming Languages – An Elementary Introduction https://doi.org/10.1[...] 2002
_[4] 서적 Concurrent ML: Design, Application and Semantics Springer-Verlag 1993
_[5] 서적 The Theory and Practice of Concurrency Prentice-Hall 2005
_[6] 논문 A semantics for imprecise exceptions http://citeseerx.ist[...] 1999
_[7] 논문 Amb Breaks Well-Pointedness, Ground Amb Doesn't
_[8] 간행물 Event Structure Semantics for CCS and Related Languages https://www.cl.cam.a[...] DAIMI Research Report, University of Aarhus 1983-04
_[9] 논문 Semantics of nondeterminism, concurrency, and communication https://dspace.libra[...] 1979-12
_[10] 논문 Profunctors, open maps and bisimulation
_[11] 논문 Domain theory for concurrency
_[12] 논문 Syntactic control of interference revisited 1995
_[13] 학위논문 A Category-Theoretic Approach to the Semantics of Programming Syracuse University 1982
_[14] 논문 Semantics and logic of object calculi
_[15] 논문 Stratified coherence spaces: a denotational semantics for Light Linear Logic
_[16] 논문 Kripke Logical Relations and PCF https://surface.syr.[...] 1995-07
_[17] 논문 Protection in programming-language translations 1998
_[18] 논문 Securing the .NET programmingmodel
_[19] 논문 Definability and Full Abstraction
_[20] 서적 The Space and Motion of Communicating Agents https://blog.itu.dk/[...] Cambridge University Press
_[21] 강연 What is Denotational Semantics? 1980-04-17
_[22] 학위논문 Foundations of Actor Semantics Massachusetts Institute of Technology 1981-05
_[23] 문서 Mosses(1990) p.563
_[24] 서적 Domain theory http://www.cs.bham.a[...] Oxford University Press 1994
_[25] 논문 A powerdomain construction 1976-09
_[26] 문서 Mosses(1990) pp.609-610
_[27] 웹사이트 The discoveries of continuations https://www.cs.cmu.e[...] 1993-11-01

본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.

문의하기 : help@durumis.com