의미론 (컴퓨터 과학)
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.
1. 개요
의미론 (컴퓨터 과학)은 컴퓨터 프로그램의 의미를 형식적으로 정의하고 연구하는 분야이다. 1960년대 후반 로버트 W. 플로이드와 토니 호어의 연구를 시작으로 지시적, 동작적, 공리적 의미론 등 다양한 접근 방식이 개발되었다. 지시적 의미론은 언어 구문을 수학적 객체로, 동작적 의미론은 프로그램 실행을 직접, 공리적 의미론은 구문에 적용되는 공리를 통해 의미를 부여한다. 이 외에도 행위, 대수적, 속성 문법, 범주적, 병행, 게임, 술어 변환기 의미론 등 다양한 형식 의미론이 존재하며, 이들 간의 관계를 증명하는 연구도 활발히 진행된다. 형식 의미론은 프로그래밍 언어 설계 및 구현, 형식 검증, 모델 검사 등 컴퓨터 과학의 여러 분야와 밀접하게 관련되어 있다.
더 읽어볼만한 페이지
- 프로그래밍 언어 의미론 - 리스코프 치환 원칙
리스코프 치환 원칙은 객체 지향 프로그래밍에서 하위 타입이 상위 타입으로 대체될 수 있어야 한다는 원칙으로, 하위 타입은 상위 타입의 조건을 준수해야 하며, 클래스 계층 구조 설계의 지침이 된다. - 프로그래밍 언어 의미론 - 표시적 의미론
표시적 의미론은 프로그램의 의미를 수학적 객체로 표현하는 방법론으로, 프로그램의 의미를 입출력 매핑 함수로 제공하며, 병행 컴퓨팅 및 예외 처리와 같은 현대 프로그래밍 언어 기능을 지원하기 위한 연구가 활발히 진행되고 있다. - 정형 기법 - 자동 정리 증명
자동 정리 증명은 논리적 진술의 타당성을 자동으로 확인하는 기술로서, 형식 논리 발전과 컴퓨터 등장 이후 다양한 논리를 지원하며 여러 분야에 응용되고, 관련 연구와 시스템 개발이 활발히 진행되고 있다. - 정형 기법 - 튜링 기계
튜링 기계는 앨런 튜링이 제시한 계산 모델로, 테이프 위에서 기계적으로 작동하며, 유한한 상태, 테이프, 헤드, 명령 표를 통해 작동하고, 계산 가능성과 알고리즘의 한계를 연구하는 데 사용된다. - 컴퓨터 과학 내 논리 - 자동화된 추론
자동화된 추론은 컴퓨터 프로그램을 사용하여 논리적 추론을 수행하는 인공지능 분야로, 수리 논리학의 발전과 초기 연구를 통해 자동 정리 증명 분야의 기틀을 마련했으며, AI 겨울을 겪었지만 소프트웨어 검증 등 다양한 분야에 활용되며 Coq, HOL Light 등의 증명 보조기가 개발되어 난제들의 형식적 증명에 기여했다. - 컴퓨터 과학 내 논리 - 혼 절
혼 절은 하나의 긍정 리터럴만을 포함하는 분리절이며, 논리 프로그래밍, 자동 정리 증명, 데이터베이스 이론 등 여러 분야에 응용된다.
| 의미론 (컴퓨터 과학) |
|---|
2. 역사
형식 의미론은 1960년대 로버트 W. 플로이드와 토니 호어의 연구에서 시작되었다. 1970년대에는 동작적 의미론 및 지시적 의미론이라는 용어가 등장했다.[5]
2. 1. 초기 연구
1967년, 로버트 W. 플로이드는 논문 ''프로그램에 의미 할당하기''를 발표했는데, 그의 주요 목표는 "정확성, 동등성 및 종료 증명을 포함하는 컴퓨터 프로그램에 대한 증명의 엄격한 표준"이었다.[2][3] 플로이드는 다음과 같이 썼다.> 우리 접근 방식에서 프로그래밍 언어의 의미론적 정의는 구문론적 정의에 기반합니다. 구문적으로 올바른 프로그램의 구문 중 어떤 구문이 명령을 나타내는지, 그리고 각 명령 근처의 해석에 어떤 조건이 적용되어야 하는지를 명시해야 합니다.
1969년, 토니 호어는 플로이드의 아이디어를 바탕으로 호어 논리에 관한 논문을 발표했으며, 이는 현재 ''공리적 의미론''이라고 불린다.[4]
2. 2. 발전
1967년, 로버트 W. 플로이드는 논문 '프로그램에 의미 할당하기'를 발표했는데, 그의 주요 목표는 "정확성, 동등성 및 종료 증명을 포함하는 컴퓨터 프로그램에 대한 증명의 엄격한 표준"이었다.[2][3] 1969년, 토니 호어는 플로이드의 아이디어를 바탕으로 호어 논리에 관한 논문을 발표했으며, 현재는 때때로 통칭하여 ''공리적 의미론''이라고 부른다.[4] 1970년대에는 ''동작적 의미론'' 및 ''지시적 의미론''이라는 용어가 등장했다.[5]3. 접근 방식
형식 의미론은 프로그래밍 언어의 의미를 정의하는 방식에 따라 크게 세 가지로 분류된다.
- '''지시적 의미론''':[6] 언어의 각 구문을 추상적인 개념적 의미인 ''지시''로 해석한다.
- '''동작적 의미론''':[7] 언어의 실행을 직접 설명한다.
- '''공리적 의미론''':[8] 구문에 적용되는 ''공리''를 설명하여 구문에 의미를 부여한다.
형식 의미론 시스템은 위 세 가지 외에도 지원되는 수학적 형식주의의 선택에 따라 다양하게 변형될 수 있다.
3. 1. 지시적 의미론 (Denotational Semantics)
지시적 의미론[6]은 언어의 각 구문에 대해 ''지시''라고 불리는 추상적인 개념적 의미를 할당하여 의미를 정의한다. 이러한 지시는 주로 수학적 공간에 존재하는 수학적 객체로 표현되지만, 반드시 그래야 하는 것은 아니다. 실질적인 필요에 따라 지시는 특정 수학적 표기법을 사용하여 설명되며, 이는 다시 지시적 메타언어로 형식화될 수 있다. 예를 들어, 함수형 프로그래밍 언어의 지시적 의미론은 종종 언어를 영역 이론으로 번역한다. 지시적 의미론적 설명은 프로그래밍 언어에서 지시적 메타언어로의 구성적 번역 역할을 할 수 있으며, 컴파일러 설계를 위한 기반으로 사용될 수 있다.3. 2. 조작적 의미론 (Operational Semantics)
동작적 의미론은 언어의 실행을 직접 설명한다.[7] 인터프리터의 작동 방식을 모델링하는 데 사용될 수 있지만, 여기서 "구현 언어"는 일반적으로 수학적 형식주의를 사용한다. 동작적 의미론은 추상 기계 (예: SECD 머신)를 정의하고, 기계의 상태를 변화시키는 과정을 설명하여 의미를 부여할 수 있다. 또는, 람다 계산법과 같이, 언어 자체의 구문 변환을 통해 정의될 수도 있다.[7]3. 3. 공리적 의미론 (Axiomatic Semantics)
공리적 의미론[8]은 프로그램 구문에 적용되는 ''공리''를 설명하여 의미를 부여한다. 공리적 의미론에서는 구문의 의미와 이를 설명하는 논리적 공식 사이를 구별하지 않는데, 이는 구문의 의미가 어떤 논리에서 증명될 수 있는 정확한 것이기 때문이다. 호어 논리는 공리적 의미론의 전형적인 예시이다.4. 다양한 형식 의미론
형식 의미론은 사용하는 수학적 도구와 관점에 따라 여러 변형이 존재한다. 주요 형식 의미론은 다음과 같다:
| 의미론 종류 | 설명 |
|---|---|
| 행위 의미론 | 의미론적 형식을 모듈화하고, 형식화 과정을 두 계층(매크로 및 마이크로 의미론)으로 나누며, 사양을 단순화하기 위해 세 가지 의미적 개체(행위, 데이터, yielders)를 미리 정의하는 접근 방식이다.[9] |
| 대수적 의미론 | 프로그램 의미론을 형식적 방법으로 설명하고 추론하기 위한 대수 법칙을 기반으로 하는 공리적 의미론의 한 형태이다.[8] 지시적 의미론과 운영 의미론도 지원한다. |
| 속성 문법 | 언어의 구문의 다양한 경우에 대해 "메타데이터"(속성이라고 함)를 체계적으로 계산하는 시스템이다.[10] 컴파일러에서 코드 생성에 사용되거나, 정규 언어 또는 문맥 자유 언어를 문맥 의존 언어 조건으로 보강하는 데에도 사용된다. |
| 범주적 의미론 | 범주론을 핵심 수학적 형식주의로 사용하는 의미론이다.[11] |
| 병행 의미론 | 병행 계산을 설명하는 모든 형식 의미론을 포괄하는 용어이다.[13] 액터 모델 및 프로세스 계산이 대표적이다. |
| 게임 의미론 | 게임 이론에서 영감을 얻은 은유를 사용하는 의미론이다.[14] |
| 술어 변환기 의미론 | 에츠허르 데이크스트라가 개발했으며, 프로그램 구문의 의미를 사후 조건을 설정하는 데 필요한 전제 조건으로 변환하는 함수로 설명한다.[15] |
4. 1. 행위 의미론 (Action Semantics)
행위 의미론[9]은 의미론적 형식을 모듈화하고, 형식화 과정을 두 계층(매크로 및 마이크로 의미론)으로 나누며, 사양을 단순화하기 위해 세 가지 의미적 개체(행위, 데이터, yielders)를 미리 정의하려는 접근 방식이다.4. 2. 대수적 의미론 (Algebraic Semantics)
대수적 의미론은 프로그램 의미론을 형식적 방법으로 설명하고 추론하기 위한 대수 법칙을 기반으로 하는 공리적 의미론의 한 형태이다.[8] 지시적 의미론과 운영 의미론도 지원한다.4. 3. 속성 문법 (Attribute Grammars)
속성 문법[10]은 언어의 구문의 다양한 경우에 대해 "메타데이터"(''속성''이라고 함)를 체계적으로 계산하는 시스템이다. 속성 문법은 대상 언어가 단순히 속성 주석으로 보강된 원래 언어인 지시적 의미론으로 이해할 수 있다. 형식 의미론 외에도, 속성 문법은 컴파일러에서 코드 생성에 사용되었으며, 정규 언어 또는 문맥 자유 언어를 문맥 의존 언어 조건으로 보강하는 데에도 사용되었다.[16]4. 4. 범주적 의미론 (Categorical Semantics)
범주론을 핵심 수학적 형식주의로 사용한다.[11] 범주적 의미론은 일반적으로 범주 구조의 구문적 표현을 제공하는 어떤 공리적 의미론에 해당하는 것으로 증명된다. 또한, 지시적 의미론은 종종 일반적인 범주적 의미론의 인스턴스이다.[12] "함수적 의미론"이라고도 한다.[11]4. 5. 병행 의미론 (Concurrency Semantics)
병행 의미론[13]은 병행 계산을 다루는 모든 형식 의미론을 통칭한다. 액터 모델과 프로세스 계산이 대표적인 병행 형식주의이다.[13]4. 6. 게임 의미론 (Game Semantics)
게임 이론에서 영감을 얻은 은유를 사용한다.[14]4. 7. 술어 변환기 의미론 (Predicate Transformer Semantics)
에츠허르 데이크스트라가 개발했으며, 프로그램 구문의 의미를 사후 조건을 설정하는 데 필요한 전제 조건으로 변환하는 함수로 설명한다.[15]5. 의미론 간의 관계
서로 다른 형식 의미론 체계 간의 관계를 증명하는 것은 중요한 연구 주제이다. 여러 이유로, 서로 다른 형식적 의미론 간의 관계를 설명하고자 할 수 있다.
예를 들어, 어떤 언어의 조작적 의미론의 결과가 그 언어의 공리적 의미론의 논리식과 모순되지 않음을 증명하거나, 고수준 추상 기계와 저수준 추상 기계에서의 조작적 의미가 쌍모방성에 의해 관련되어 있음을 증명해야 할 수도 있다. 복수의 의미론은 추상 해석 이론에 의한 추상화를 통해 연관될 수 있다.
5. 1. 건전성 증명
어떤 언어의 특정 조작적 의미론이 해당 언어의 공리적 의미론의 논리적 공식을 만족함을 증명할 수 있다. 이러한 증명은 특정 (조작적) '해석 전략'에 대해 특정 (공리적) '증명 시스템'을 사용하여 추론하는 것이 건전하다는 것을 보여준다.[1]5. 2. 시뮬레이션 증명
고수준 기계에 대한 조작적 의미론이 저수준 기계에 대한 의미론과 시뮬레이션으로 관련되어 있음을 증명할 수 있다. 여기서 저수준 추상 기계는 주어진 언어의 고수준 추상 기계 정의보다 더 원시적인 연산을 포함한다. 이러한 증명은 저수준 기계가 고수준 기계를 "충실하게 구현"한다는 것을 보여준다.5. 3. 추상 해석
추상 해석 이론을 통해 추상화를 통해 여러 의미론을 연결하는 것도 가능하다.[1]6. 관련 분야
형식 의미론은 논리, 집합론, 모형 이론, 범주론 등 수학적 구조와 계산 간의 관계를 다룬다.[1] 프로그래밍 언어 설계, 형식 이론, 컴파일러 및 인터프리터, 프로그램 검증, 모델 검사 등 컴퓨터 과학의 다른 분야와도 밀접하게 관련되어 있다.[1]
6. 1. 프로그래밍 언어 설계 및 구현
형식 의미론은 컴퓨터 과학의 프로그래밍 언어 설계, 형식 이론, 컴파일러 및 인터프리터, 프로그램 검증 및 모델 검사와 같은 다른 분야와 밀접한 관련이 있다.[1]프로그램 의미론 분야는 다음을 포함한다.[1]
- 의미론적 모델의 정의
- 서로 다른 의미론적 모델 간의 관계
- 의미에 대한 서로 다른 접근 방식 간의 관계
- 계산과 그 근본이 되는 수학적 구조(수리 논리학, 집합론, 모델 이론, 범주론)과의 관계
6. 2. 형식 검증 및 모델 검사
형식 의미론은 컴퓨터 과학의 프로그래밍 언어, 형식 이론, 컴파일러 및 인터프리터, 프로그램 검증, 모델 검사 등과 같은 분야와 밀접하게 관련되어 있다.[1] 형식 의미론은 형식적 검증 및 모델 검사를 통해 프로그램의 정확성을 검증하고 시스템 동작을 분석하는 데 사용된다.[1]6. 3. 기타
형식 의미론 분야는 다음을 포함한다.- 의미론적 모델의 정의
- 서로 다른 의미론적 모델 간의 관계
- 의미에 대한 서로 다른 접근 방식 간의 관계
- 논리, 집합론, 모형 이론, 범주론 등과 같은 분야의 수학적 구조와 계산 간의 관계
이는 컴퓨터 과학의 프로그래밍 언어 설계, 형식 이론, 컴파일러 및 인터프리터, 프로그램 검증 및 모델 검사와 같은 다른 분야와 밀접한 관련이 있다.
참조
[1]
서적
Category Theory Applied to Computation and Control
Springer
1975
[2]
서적
Mathematical Aspects of Computer Science
https://books.google[...]
American Mathematical Society
[3]
웹사이트
Memorial Resolution: Robert W. Floyd (1936–2001)
https://stacks.stanf[...]
Stanford Historical Society
[4]
간행물
An axiomatic basis for computer programming
1969-10
[5]
서적
The formal semantics of programming languages : an introduction
https://archive.org/[...]
MIT Press
1993
[6]
서적
Denotational Semantics: A Methodology for Language Development
William C. Brown Publishers
1986
[7]
보고서
A structural approach to operational semantics
Computer Science Department, Aarhus University
1981
[8]
간행물
Initial algebra semantics and continuous algebras
1977
[9]
보고서
Theory and practice of action semantics
Aarhus University
1996
[10]
서적
"Attribute Grammars: Definitions, Systems and Bibliography
Springer-Verlag
1988
[11]
간행물
Functorial semantics of algebraic theories
1963
[12]
간행물
Some fundamental algebraic tools for the semantics of computation: Part 3. Indexed categories
1991
[13]
학술회의
The problem of programming language concurrency semantics
http://kar.kent.ac.u[...]
Springer
2015
[14]
서적
Semantics and Logics of Computation
https://ora.ox.ac.uk[...]
Cambridge University Press
2009
[15]
간행물
Guarded commands, nondeterminacy and formal derivation of programs
1975
[16]
문서
[17]
서적
Category Theory Applied to Computation and Control
Springer
1975
본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.
문의하기 : help@durumis.com