Programmering af beregningsfunktioner - Programming Computable Functions

Inden for datalogi er Programming Computable Functions (PCF) et maskinskrevet funktionssprog, der blev introduceret af Gordon Plotkin i 1977, baseret på tidligere upubliceret materiale af Dana Scott . Det kan betragtes som en udvidet version af den typede lambda -beregning eller en forenklet version af moderne typede funktionssprog som ML eller Haskell .

En fuldstændig abstrakt model for PCF blev først givet af Milner (1977). Men da Milners model i det væsentlige var baseret på PCF -syntaksen, blev den betragtet som mindre end tilfredsstillende (Ong, 1995). De to første fuldt abstrakte modeller, der ikke anvender syntaks, blev formuleret i løbet af 1990'erne. Disse modeller er baseret på spil semantik (Hyland og Ong, 2000; Abramsky, Jagadeesan og Malacaria, 2000) og Kripke logiske relationer (O'Hearn og Riecke, 1995). For en tid føltes det, at ingen af ​​disse modeller var helt tilfredsstillende, da de ikke var effektivt præsentable. Imidlertid demonstrerede Ralph Loader , at der ikke kunne eksistere en effektivt præsentabel fuldstændig abstrakt model, da spørgsmålet om programækvivalens i det endelige fragment af PCF ikke kan afgøres.

Syntaks

De typer af PCF er induktivt defineret som

• nat er en type
• For typerne σ og τ er der en type σ → τ

En kontekst er en liste over par x: σ , hvor x er et variabelnavn og σ er en type, således at intet variabelnavn duplikeres. Man definerer derefter at skrive bedømmelser af udtryk-i-kontekst på den sædvanlige måde for følgende syntaktiske konstruktioner:

• Variabler (hvis x: σ er en del af en kontekst Γ , så Γ ⊢ x  : σ )
• Anvendelse (af et udtryk af typen σ → τ til et udtryk af typen σ )
• λ-abstraktion
• The Y faste punkt combinator (gør udtryk af typen o ud af udtryk af typen cr → cr )
• Efterfølgeren ( succ ) og forgængeren ( forud ) operationer på nat og den konstante 0
• Den betingede hvis med typebestemmelsen:

${\ 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 s vil blive fortolket som booleanske her med en konvention som nul angiver sandhed og ethvert andet tal, der angiver falskhed)

Semantik

Denotationssemantik

En relativt ligetil semantik for sproget er Scott -modellen . I denne model,

• Typer tolkes som bestemte domæner .
  • ${\ displaystyle [\! [{\ textbf {nat}}] \!]: = \ mathbb {N} _ {\ bot}}$ (de naturlige tal med et bundelement ved siden af, med den flade rækkefølge)
  • ${\ displaystyle [\! [\ sigma \ to \ tau \,] \!]}$fortolkes som domænet for Scott-kontinuerlige funktioner fra til , med den punktvise rækkefølge.${\ displaystyle [\! [\ sigma] \!] \,}$${\ displaystyle [\! [\ tau] \!] \,}$
• En kontekst fortolkes som produktet${\ displaystyle x_ {1}: \ sigma _ {1}, \; \ dots, \; x_ {n}: \ sigma _ {n}}$${\ displaystyle [\! [\ sigma _ {1}] \!] \ times \; \ dots \; \ times [\! [\ sigma _ {n}] \!]}$
• Termer i kontekst fortolkes som kontinuerlige funktioner${\ displaystyle \ Gamma \; \ vdash \; x \;: \; \ sigma}$${\ displaystyle [\! [\ Gamma] \!] \; \ to \; [\! [\ sigma] \!]}$
  • Variable udtryk tolkes som fremskrivninger
  • Lambda -abstraktion og anvendelse fortolkes ved at gøre brug af den kartesiske lukkede struktur i kategorien domæner og kontinuerlige funktioner
  • Y fortolkes ved at tage det mindst faste punkt i argumentet

Denne model er ikke fuldstændig abstrakt for PCF; men det er fuldstændigt abstrakt for sproget opnået ved at tilføje en parallel eller operator til PCF (s. 293 i Hyland og Ong 2000 -referencen nedenfor).

Noter

Referencer

• Scott, Dana S. (1969). "Et typeteoretisk alternativ til CUCH, ISWIM, OWHY" (PDF) . Upubliceret manuskript .Fremkom som Scott, Dana S. (1993). "Et typeteoretisk alternativ til CUCH, ISWIM, OWHY" . Teoretisk datalogi . 121 : 411–440. doi : 10.1016/0304-3975 (93) 90095-b .
• Plotkin, Gordon D. (1977). "LCF betragtes som et programmeringssprog" (PDF) . Teoretisk datalogi . 5 (3): 223–255. doi : 10.1016/0304-3975 (77) 90044-5 .
• Milner, Robin (1977). "Fuldt abstrakte modeller af typede λ-calculi" (PDF) . Teoretisk datalogi . 4 : 1–22. doi : 10.1016/0304-3975 (77) 90053-6 . HDL : 20.500.11820 / 731c88c6-cdb1-4ea0-945e-f39d85de11f1 .
• Mitchell, John C. (1996). "Sprog -PCF". Fundamenter til programmeringssprog .
• Abramsky, S., Jagadeesan, R. og Malacaria, P. (2000). "Fuld abstraktion til PCF" . Information og beregning . 163 (2): 409–470. doi : 10.1006/inco.2000.2930 .CS1 maint: flere navne: forfatterliste ( link )
• Hyland, JME & Ong, C.-HL (2000). "På fuld abstraktion til PCF" . Information og beregning . 163 (2): 285–408. doi : 10.1006/inco.2000.2917 .
• O'Hearn, PW & Riecke, J. G (1995). "Kripke logiske relationer og PCF" . Information og beregning . 120 (1): 107–116. doi : 10.1006/inco.1995.1103 .
• Loader, R. (2001). "Finitær PCF kan ikke vælges" . Teoretisk datalogi . 266 (1–2): 341–364. doi : 10.1016/S0304-3975 (00) 00194-8 .
• Ong, C.-HL (1995). "Korrespondance mellem operationel og denotational semantik: Det fulde abstraktionsproblem for PCF" . I Abramsky, S .; Gabbay, D .; Maibau, TSE (red.). Håndbog i logik i datalogi . Oxford University Press. s. 269–356. Arkiveret fra originalen 2006-01-07 . Hentet 2006-01-19 .

eksterne links

• Introduktion til RealPCF
• Lexer og Parser til PCF skrevet i SML