Programmering av beräkningsbara funktioner - Programming Computable Functions

Inom datavetenskap är Programming Computable Functions (PCF) ett maskinskrivet funktionellt språk som introducerades av Gordon Plotkin 1977, baserat på tidigare opublicerat material av Dana Scott . Det kan anses vara en utökad version av den typade lambda -kalkylen eller en förenklad version av moderna maskinskrivna funktionella språk som ML eller Haskell .

En helt abstrakt modell för PCF gavs först av Milner (1977). Eftersom Milners modell i huvudsak baserades på syntaxen för PCF ansågs den dock vara mindre än tillfredsställande (Ong, 1995). De två första helt abstrakta modellerna som inte använder syntax formulerades under 1990 -talet. Dessa modeller är baserade på spelsemantik (Hyland och Ong, 2000; Abramsky, Jagadeesan och Malacaria, 2000) och Kripkes logiska relationer (O'Hearn och Riecke, 1995). För en tid ansågs det att ingen av dessa modeller var helt tillfredsställande, eftersom de inte var effektivt presenterbara. Men Ralph Loader visade att ingen effektivt presentabel helt abstrakt modell skulle kunna existera, eftersom frågan om program likvärdighet i finitary fragment av PCF inte avgörbara.

Syntax

De typer av PCF är induktivt definieras som

• nat är en typ
• För typerna σ och τ finns det en typ σ → τ

Ett sammanhang är en lista med par x: σ , där x är ett variabelnamn och σ är en typ, så att inget variabelnamn dupliceras. Man definierar sedan att skriva bedömningar av termer-i-sammanhang på vanligt sätt för följande syntaktiska konstruktioner:

• Variabler (om x: σ är en del av ett sammanhang Γ , då Γ ⊢ x  : σ )
• Tillämpning (av en term av typen σ → τ på en term av typen σ )
• λ-abstraktion
• Den Y fasta punkten Combinator (gör termer av typen o ur termer av typen o → o )
• Efterträdaren ( succ ) och föregångaren ( pred ) operationer på nat och konstant 0
• Villkoren om med skrivregeln:

${\ displaystyle {\ 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}}}$

( nat kommer att tolkas som booleaner här med en konvention som noll som anger sanning och alla andra siffror som anger falskhet)

Semantik

Denotationssemantik

En relativt enkel semantik för språket är Scott -modellen . I denna modell,

• Typer tolkas som vissa domäner .
  • ${\ displaystyle [\! [{\ textbf {nat}}] \!]: = \ mathbb {N} _ {\ bot}}$ (de naturliga siffrorna med ett bottenelement intill, med den platta ordningen)
  • ${\ displaystyle [\! [\ sigma \ to \ tau \,] \!]}$tolkas som domänen för Scott-kontinuerliga funktioner från till , med den punktvisa ordningen.${\ displaystyle [\! [\ sigma] \!] \,}$${\ displaystyle [\! [\ tau] \!] \,}$
• Ett sammanhang tolkas som produkten${\ displaystyle x_ {1}: \ sigma _ {1}, \; \ dots, \; x_ {n}: \ sigma _ {n}}$${\ displaystyle [\! [\ sigma _ {1}] \!] \ times \; \ dots \; \ times [\! [\ sigma _ {n}] \!]}$
• Termer i sammanhang tolkas som kontinuerliga funktioner${\ displaystyle \ Gamma \; \ vdash \; x \;: \; \ sigma}$${\ displaystyle [\! [\ Gamma] \!] \; \ to \; [\! [\ sigma] \!]}$
  • Variabla termer tolkas som prognoser
  • Lambda -abstraktion och tillämpning tolkas genom att använda den kartesiska slutna strukturen för kategorin domäner och kontinuerliga funktioner
  • Y tolkas genom att ta den minst fasta punkten i argumentet

Denna modell är inte helt abstrakt för PCF; men det är helt abstrakt för språket som erhålls genom att lägga till en parallell eller operator till PCF (s. 293 i Hyland och Ong 2000 -referensen nedan).

Anteckningar

Referenser

• Scott, Dana S. (1969). "Ett typteoretiskt alternativ till CUCH, ISWIM, OWHY" (PDF) . Opublicerat manuskript .Föddes som Scott, Dana S. (1993). "Ett typteoretiskt alternativ till CUCH, ISWIM, OWHY" . Teoretisk datavetenskap . 121 : 411–440. doi : 10.1016/0304-3975 (93) 90095-b .
• Plotkin, Gordon D. (1977). "LCF betraktas som ett programmeringsspråk" (PDF) . Teoretisk datavetenskap . 5 (3): 223–255. doi : 10.1016/0304-3975 (77) 90044-5 .
• Milner, Robin (1977). "Helt abstrakta modeller av typade λ-kalkyler" (PDF) . Teoretisk datavetenskap . 4 : 1–22. doi : 10.1016/0304-3975 (77) 90053-6 . hdl : 20.500.11820/731c88c6-cdb1-4ea0-945e-f39d85de11f1 .
• Mitchell, John C. (1996). "Språket PCF". Grunder för programmeringsspråk .
• Abramsky, S., Jagadeesan, R. och Malacaria, P. (2000). "Full abstraktion för PCF" . Information och beräkning . 163 (2): 409–470. doi : 10.1006/inco.2000.2930 .CS1 -underhåll: flera namn: författarlista ( länk )
• Hyland, JME & Ong, C.-HL (2000). "På fullständig abstraktion för PCF" . Information och beräkning . 163 (2): 285–408. doi : 10.1006/inco.2000.2917 .
• O'Hearn, PW & Riecke, J. G (1995). "Kripke logiska relationer och PCF" . Information och beräkning . 120 (1): 107–116. doi : 10.1006/inco.1995.1103 .
• Loader, R. (2001). "Slutlig PCF går inte att bestämma" . Teoretisk datavetenskap . 266 (1–2): 341–364. doi : 10.1016/S0304-3975 (00) 00194-8 .
• Ong, C.-HL (1995). "Korrespondens mellan operativ och denotationell semantik: Det fullständiga abstraktionsproblemet för PCF" . I Abramsky, S .; Gabbay, D .; Maibau, TSE (red.). Handbook of Logic in Computer Science . Oxford University Press. s. 269–356. Arkiverad från originalet 2006-01-07 . Hämtad 2006-01-19 .

externa länkar

• Introduktion till RealPCF
• Lexer och Parser för PCF skriven i SML