의미론(컴퓨터 과학)

Semantics (computer science)
계산 의미론과 혼동하지 마십시오.

프로그래밍 언어 이론에서 의미론은 프로그래밍 [1]언어의 의미에 대한 엄격한 수학적 연구입니다.의미론은 프로그래밍 언어 구문에서 유효한 문자열에 계산적 의미를 할당합니다.

의미론은 특정 언어로 프로그램을 실행할 때 컴퓨터가 수행하는 프로세스를 설명합니다.이것은 프로그램의 입력과 출력의 관계를 설명하거나 프로그램이 특정 플랫폼에서 어떻게 실행될지에 대한 설명을 통해 계산 모델을 생성함으로써 나타낼 수 있습니다.

개요

형식 의미론 필드에는 다음 항목이 모두 포함됩니다.

  • 의미 모델의 정의
  • 서로 다른 의미 모델 간의 관계
  • 의미에 대한 다른 접근법 간의 관계
  • 연산과 논리, 집합론, 모델론, 범주론 등과 같은 분야의 기초 수학 구조 사이의 관계.

프로그래밍 언어 설계, 유형 이론, 컴파일러 및 인터프리터, 프로그램 검증 및 모델 확인과 같은 컴퓨터 과학의 다른 분야와 밀접하게 연계되어 있습니다.

접근

형식 의미론에는 많은 접근법이 있습니다.이러한 접근법은, 다음의 3개의 주요한 클래스에 속합니다.

  • 표현적 의미론,[2] 언어의 각 문구가 표현, 즉 추상적으로 생각할 수 있는 개념적 의미로 해석됩니다.이러한 표현은 종종 수학적 공간에 존재하는 수학적 객체이지만, 그렇게 해야 하는 것은 아니다.실용적 필요성으로서, 표기는 수학 표기법의 어떤 형태로든 설명되며, 이것은 다시 표제 메타언어로서 공식화될 수 있다.예를 들어, 기능 언어의 표현적 의미론은 종종 언어를 도메인 이론으로 변환합니다.지시적 의미 기술은 프로그래밍 언어에서 지시적 메타언어로의 구성적 번역으로서도 사용할 수 있으며 컴파일러를 설계하기 위한 기초로 사용됩니다.
  • 언어 실행이 (번역이 아닌) 직접 기술되는 운영 [3]의미론입니다.해석자의 "실장 언어"는 일반적으로 수학적 형식주의이지만, 연산 의미론은 해석과 느슨하게 일치한다.운영 의미론에서는 추상 머신(SECD 머신 등)을 정의하고 머신 상태에 대해 유도하는 전이를 설명함으로써 구에 의미를 부여할 수 있습니다.또는 순수한 람다 미적분과 마찬가지로 언어 자체의 구문에 대한 구문 변환을 통해 운영적 의미를 정의할 수 있다.
  • 공리적인 의미론,[4] 구에 적용되는 공리를 설명함으로써 구에 의미를 부여합니다.공리적인 의미론은 구절의 의미와 그것을 설명하는 논리식을 구분하지 않는다; 그 의미는 정확히 어떤 논리학에서 증명될 수 있는 것이다.공리적인 의미론의 표준적인 예는 Hoare 논리이다.

표현적, 운영적 또는 자명한 접근법 사이의 선택과는 별도로, 형식적 의미 체계에서의 대부분의 변화는 수학적 형식주의를 뒷받침하는 선택에서 비롯된다.

바리에이션

형식 의미론에는 다음과 같은 종류가 있습니다.

  • 행동[5] 의미론은 표현적 의미론을 모듈화하려는 접근법으로, 형식화 프로세스를 두 개의 계층(매크로 및 마이크로 의미론)으로 나누고 세 개의 의미 실체(행동, 데이터 및 산출자)를 미리 정의하여 규격을 단순화한다.
  • 대수적[4] 의미론은 형식적인 방식으로 프로그램 의미론에 대해 기술하고 추론하기 위한 대수적 법칙에 기초한 자명한 의미론의 한 형태이다.또한 표현 의미론 및 운영 의미론도 지원합니다.
  • 속성 문법은[6] 언어 구문의 다양한 경우에 대해 체계적으로 "메타데이터"(속성이라고 함)를 계산하는 시스템을 정의합니다.속성 문법은 대상 언어가 단순히 속성 주석이 풍부한 원래 언어인 표현적 의미론으로서 이해될 수 있다.형식적인 의미론 이외에도 속성 문법은 컴파일러의 코드 생성 및 컨텍스트에 민감한 조건에서의 규칙적인 또는 컨텍스트 없는 문법을 증가시키기 위해 사용되어 왔습니다.
  • 범주적 의미론(또는 "함수적")은[7] 범주 이론을 핵심적인 수학적 형식주의로 사용한다.범주적 의미론은 보통 범주적 구조의 통사적 표시를 제공하는 몇 가지 공리적 의미론에 대응하는 것으로 증명된다.또한 표현적 의미론은 흔히 일반적인 범주적 [8]의미론의 예이다.
  • 동시성[9] 시멘틱스는 동시 연산을 설명하는 모든 형식 시멘틱스의 포괄적인 용어입니다.역사적으로 중요한 동시 형식에는 행위자 모델과 프로세스 계산이 포함되어 있다.
  • 게임 의미론에서는[10] 게임 이론에서 영감을 얻은 은유를 사용합니다.
  • Edsger W. Dijkstra에 의해 개발된 술어 변압기 [11]의미론은 프로그램 조각의 의미를 사후 조건을 확립하는 데 필요한 전제 조건으로 변환하는 함수로서 설명한다.

관계 설명

여러 가지 이유로 다른 형식 의미론 간의 관계를 기술하고 싶을 수 있습니다.예를 들어 다음과 같습니다.

  • 언어에 대한 특정 운영 의미론이 해당 언어에 대한 자명한 의미론의 논리 공식을 충족함을 증명하는 것.이러한 증거는 특정(자동) 증명 시스템을 사용하여 특정(운영) 해석 전략을 추론하는 것이 "건전하다"는 것을 보여준다.
  • 높은 수준의 기계에 대한 운영 시멘틱스가 낮은 수준의 기계에 대한 시멘틱스와의 시뮬레이션에 의해 관련된다는 것을 증명하기 위해, 낮은 수준의 추상 기계는 주어진 언어의 높은 수준의 추상 기계 정의보다 더 원시적인 연산을 포함한다.이러한 증거는 하위 수준의 기계가 상위 수준의 기계를 "충실히 구현"한다는 것을 보여줍니다.

추상 해석 이론을 통해 추상화를 통해 여러 의미론을 연관시키는 것도 가능하다.

역사

로버트 W. Floyd는 Floyd(1967)[12]에서 프로그래밍 언어 의미론 분야를 설립한 것으로 인정받고 있습니다.

「 」를 참조해 주세요.

레퍼런스

  1. ^ Joseph A. Goguen (1975). "Semantics of computation". Category Theory Applied to Computation and Control. Lecture Notes in Computer Science. Vol. 25. Springer. pp. 151–163. doi:10.1007/3-540-07142-3_75. ISBN 978-3-540-07142-6.
  2. ^ David A. Schmidt (1986). Denotational Semantics: A Methodology for Language Development. William C. Brown Publishers. ISBN 9780205104505.
  3. ^ Gordon D. Plotkin (1981). "A structural approach to operational semantics". Technical Report DAIMI FN-19. Computer Science Department, Aarhus University. {{cite journal}}:Cite 저널 요구 사항 journal=(도움말)
  4. ^ a b Joseph A. Goguen; James W. Thatcher; Eric G. Wagner; Jesse B. Wright (1977). "Initial algebra semantics and continuous algebras". Journal of the ACM. 24 (1): 68–95. doi:10.1145/321992.321997. S2CID 11060837.
  5. ^ Peter D. Mosses (1996). "Theory and practice of action semantics". BRICS Report RS9653. Aarhus University. {{cite journal}}:Cite 저널 요구 사항 journal=(도움말)
  6. ^ Pierre Deransart; Martin Jourdan; Bernard Lorho (1988). "Attribute Grammars: Definitions, Systems and Bibliography. Lecture Notes in Computer Science 323. Springer-Verlag. ISBN 9780387500560.
  7. ^ F. William Lawvere (1963). "Functorial semantics of algebraic theories". Proceedings of the National Academy of Sciences of the United States of America. 50 (5): 869–872. doi:10.1073/pnas.50.5.869. PMC 221940. PMID 16591125.
  8. ^ Andrzej Tarlecki; Rod M. Burstall; Joseph A. Goguen (1991). "Some fundamental algebraic tools for the semantics of computation: Part 3. Indexed categories". Theoretical Computer Science. 91 (2): 239–264. doi:10.1016/0304-3975(91)90085-G.
  9. ^ Mark Batty; Kayvan Memarian; Kyndylan Nienhuis; Jean Pichon-Pharabod; Peter Sewell (2015). "The problem of programming language concurrency semantics". Proceedings of the European Symposium on Programming Languages and Systems. Springer. pp. 283–307. doi:10.1007/978-3-662-46669-8_12.
  10. ^ Samson Abramsky (2009). "Semantics of interaction: An introduction to game semantics". In Andrew M. Pitts; P. Dybjer (eds.). Semantics and Logics of Computation. Cambridge University Press. pp. 1–32. doi:10.1017/CBO9780511526619.002. ISBN 9780521580571.
  11. ^ Edsger W. Dijkstra (1975). "Guarded commands, nondeterminacy and formal derivation of programs". Communications of the ACM. 18 (8): 453–457. doi:10.1145/360933.360975. S2CID 1679242.
  12. ^ Donald E. Knuth. "Memorial Resolution: Robert W. Floyd (1936–2001)" (PDF). Stanford University Faculty Memorials. Stanford Historical Society.

추가 정보

교재
강의 노트

외부 링크