계산 가능한 함수 프로그래밍

컴퓨터 과학에서 Programming Computable Functions(PCF)는 Dana Scott가 이전에 발표하지 않은 자료를 바탕으로 1977년 Gordon Plotkin이 도입한 활자 기능 언어다.^{[note 1]}활자형 람다 미적분학의 확장판이나 ML이나 하스켈과 같은 현대식 기능언어의 단순판이라고 볼 수 있다.

PCF의 완전 추상적인 모델은 밀너(1977년)에 의해 처음 주어졌다.그러나, 밀너의 모델은 본질적으로 PCF의 구문에 기초했기 때문에 만족스럽지 못한 것으로 간주되었다(On, 1995).구문을 채택하지 않은 최초의 완전히 추상적인 두 모델은 1990년대에 공식화되었다.이러한 모델은 게임 의미론(Hyland and Ong, 2000; Abramsky, Jagadean, 2000)과 Kripke 논리적 관계(O'Hearn and Riecke, 1995)를 기반으로 한다.한동안은 이 모델들 중 어느 것도 완전히 만족스럽지 못하다는 느낌이 들었다.그러나, 랄프 로더는 PCF의 미세한 부분에서의 프로그램 동등성에 대한 문제는 해독할 수 없기 때문에 효과적으로 표현 가능한 완전 추상적인 모델은 존재할 수 없다는 것을 증명했다.

구문

PCF의 종류는 다음과 같이 귀납적으로 정의된다.

nat은 유형이다.
σ형, τ형의 경우 →형 → τ형이 있다.

컨텍스트는 pair x : σ의 목록으로, 여기서 x는 변수 이름이고 σ은 유형으로 변수 이름이 중복되지 않는다.그런 다음, 다음과 같은 구문구조에 대해 통상적인 방법으로 용어-인-콘텍스트의 타이핑 판단을 정의한다.

변수(x : σ이 컨텍스트 γ의 일부인 경우 then x : σ)
적용(유형 σ → τ형 σ형 σ형 σ형)
λ-굴절
Y 고정점 콤비네이터(타입 σ의 항을 → → σ의 항으로 함)
NAT에 대한 후속(such) 및 이전(pred) 운영 및 상수 0
타이핑 규칙을 사용하는 경우 조건부:

{\frac {\Gamma \;\vdash \;t\;:{\textbf {nat}},\quad \quad \Gamma \;\vdash \;s_{0}\;:\sigma ,\quad \quad \Gamma \;\vdash \;s_{1}\;:\sigma }{\Gamma \;\vdash \;{\textbf {if}}(t,s_{0},s_{1})\;:\sigma }}

(nats는 진리를 나타내는 제로(zero)와 같은 관습과 거짓을 나타내는 다른 숫자와 같은 관습으로 여기에서는 술꾼으로 해석될 것이다.)

의미론

변절 의미론

그 언어에 대한 비교적 간단한 의미론으로는 스콧 모델이 있다.이 모델에서는

유형은 특정 도메인으로 해석된다.
- ${\$ $[{\textbf{nat}}\!]:$ $=\mathbe{N} _{\bot }}($ 하단 원소가 결합된 자연수, 플랫 오더 포함)
- $[$ $[\sigma \to \to$ \,]\}은 $($ 는) [ $[\![\sigma ]\!]\,$ $[\![\sigma ]\!]\,$ {\ $displaystyle [\!]$ 의 스콧 연속 함수의 영역으로 해석된다 $[\![\sigma \to \tau \,]\!]$ . $[\\\!]\,}$ 에 $[\![\sigma ]\!]\,$ [ $[\![\tau ]\!]\,$ $[\![\tau ]\!]\,$ $[\![\tau ]\!]\,$ ${\$ $[\tau ]\!]\,}$ 포인트 순서 $[\![\tau ]\!]\,$
컨텍스트 $x_{1}:\sigma _{1},\;\dots ,\;x_{n}:\sigma _{n}$ $x_{1}:\sigma _{1},\;\dots ,\;x_{n}:\sigma _{n}$ : $x_{1}:\sigma _{1},\;\dots ,\;x_{n}:\sigma _{n}$ $x_{1}:\sigma _{1},\;\dots ,\;x_{n}:\sigma _{n}$ , $x_{1}:\sigma _{1},\;\dots ,\;x_{n}:\sigma _{n}$ … , $x_{1}:\sigma _{1},\;\dots ,\;x_{n}:\sigma _{n}$ n $x_{1}:\sigma _{1},\;\dots ,\;x_{n}:\sigma _{n}$ : $x_{1}:\sigma _{1},\;\dots ,\;x_{n}:\sigma _{n}$ ${\$ }\\dots $,\;x_{n}:\sigma$ $[\![\sigma _{1}]\!]\times \;\dots \;\times [\![\sigma _{n}]\!]$ ${n}}}}}$ 는 제품 $x_{1}:\sigma _{1},\;\dots ,\;x_{n}:\sigma _{n}$ $[\![\sigma _{1}]\!]\times \;\dots \;\times [\![\sigma _{n}]\!]$ [ $[\![\sigma _{1}]\!]\times \;\dots \;\times [\![\sigma _{n}]\!]$ $[\![\sigma _{1}]\!]\times \;\dots \;\times [\![\sigma _{n}]\!]$ [ $[\![\sigma _{1}]\!]\times \;\dots \;\times [\![\sigma _{n}]\!]$ [ n $[\![\sigma _{1}]\!]\times \;\dots \;\times [\![\sigma _{n}]\!]$ ${\displaystystylease [\!$ $【\\\\\】\\\nowled \\\nowled \\\\beat [\!$ $[\\probma _{n}\!]}$
컨텍스트 $\Gamma \;\vdash \;x\;:\;\sigma$ : $\Gamma \;\vdash \;x\;:\;\sigma$ $\Gamma \;\vdash \;x\;:\;\;\sigma$ 의 용어는 연속함수 $[\![\Gamma ]\!]\;\to \;[\![\sigma ]\!]$ [ $[\![\Gamma ]\!]\;\to \;[\![\sigma ]\!]$ ] → $[\![\Gamma ]\!]\;\to \;[\![\sigma ]\!]$ [ $[\![\Gamma ]\!]\;\to \;[\![\sigma ]\!]$ → [ $[\![\Gamma ]\!]\;\to \;[\![\sigma ]\!]$ $[\\Gamma ]!]$ 로 해석된다 $\Gamma \;\vdash \;x\;:\;\sigma$ . $;\to \;[\]!$ $[\\\!]}$
- 변수 항은 투영으로 해석된다.
- 람다 추상화 및 적용은 도메인 및 연속 기능 범주의 데카르트 폐쇄 구조를 이용하여 해석된다.
- Y는 인수의 가장 고정되지 않은 점을 취함으로써 해석된다.

이 모델은 PCF의 경우 완전히 추상적인 것은 아니지만 PCF에 병렬이나 연산자를 추가하여 얻은 언어에 대해서는 완전히 추상적이다(아래 하이랜드와 옹 2000 참조의 페이지 293).

메모들

^ "PCF는 LCF, Scott의 계산 가능한 함수의 논리인 계산 가능한 함수의 프로그래밍 언어" (Plotkin 1977)이다.Computable Functions 프로그래밍은 (Mitchell 1996)에 의해 사용된다.또한 Computable Functions를 이용한 Programming 또는 Computable Functions를 위한 Programming language라고도 한다.

참조

Scott, Dana S. (1969). "A type-theoretic alternative to CUCH, ISWIM, OWHY" (PDF). Unpublished Manuscript. 로 나타났다.
Plotkin, Gordon D. (1977). "LCF considered as a programming language" (PDF). Theoretical Computer Science. 5 (3): 223–255. doi:10.1016/0304-3975(77)90044-5.
Milner, Robin (1977). "Fully abstract models of typed λ-calculi" (PDF). Theoretical Computer Science. 4: 1–22. doi:10.1016/0304-3975(77)90053-6. hdl:20.500.11820/731c88c6-cdb1-4ea0-945e-f39d85de11f1.
Mitchell, John C. (1996). "The Language PCF". Foundations for Programming Languages.
Abramsky, S., Jagadeesan, R., and Malacaria, P. (2000). "Full Abstraction for PCF". Information and Computation. 163 (2): 409–470. doi:10.1006/inco.2000.2930.{{cite journal}}: CS1 maint : 복수이름 : 작성자 목록(링크)
Hyland, J. M. E. & Ong, C.-H. L. (2000). "On Full Abstraction for PCF". Information and Computation. 163 (2): 285–408. doi:10.1006/inco.2000.2917.
O'Hearn, P. W. & Riecke, J. G (1995). "Kripke Logical Relations and PCF". Information and Computation. 120 (1): 107–116. doi:10.1006/inco.1995.1103.
Loader, R. (2001). "Finitary PCF is not decidable". Theoretical Computer Science. 266 (1–2): 341–364. doi:10.1016/S0304-3975(00)00194-8.
Ong, C.-H. L. (1995). "Correspondence between Operational and Denotational Semantics: The Full Abstraction Problem for PCF". In Abramsky, S.; Gabbay, D.; Maibau, T. S. E. (eds.). Handbook of Logic in Computer Science. Oxford University Press. pp. 269–356. Archived from the original on 2006-01-07. Retrieved 2006-01-19.

외부 링크

[1] "PCF는 LCF, Scott의 계산 가능한 함수의 논리인 계산 가능한 함수의 프로그래밍 언어" (Plotkin 1977)이다.Computable Functions 프로그래밍은 (Mitchell 1996)에 의해 사용된다.또한 Computable Functions를 이용한 Programming 또는 Computable Functions를 위한 Programming language라고도 한다.

[note 1]

Search

계산 가능한 함수 프로그래밍

네임스페이스

더

목차

구문

의미론

변절 의미론

메모들

참조

외부 링크