Programarea funcțiilor calculabile - Programming Computable Functions

În informatică , Programming Computable Functions (PCF) este un limbaj funcțional introdus de Gordon Plotkin în 1977, bazat pe materialul anterior nepublicat de Dana Scott . Poate fi considerat a fi o versiune extinsă a calculului lambda tastat sau o versiune simplificată a limbajelor funcționale moderne tastate, cum ar fi ML sau Haskell .

Un model complet abstract pentru PCF a fost dat pentru prima dată de Milner (1977). Cu toate acestea, deoarece modelul lui Milner se bazează în esență pe sintaxa PCF, a fost considerat mai puțin satisfăcător (Ong, 1995). Primele două modele complet abstracte care nu utilizează sintaxă au fost formulate în anii 1990. Aceste modele se bazează pe semantica jocului (Hyland și Ong, 2000; Abramsky, Jagadeesan și Malacaria, 2000) și pe relațiile logice Kripke (O'Hearn și Riecke, 1995). Pentru o vreme s-a simțit că niciunul dintre aceste modele nu a fost complet satisfăcător, deoarece nu erau prezentabile în mod eficient. Cu toate acestea, Ralph Loader a demonstrat că nu poate exista un model complet abstract prezentabil în mod eficient, deoarece problema echivalenței programului în fragmentul finitar al PCF nu este decisă.

Sintaxă

Cele Tipurile de PCF sunt definite ca inductiv

• nat este un tip
• Pentru tipurile σ și τ , există un tip σ → τ

Un context este o listă de perechi x: σ , unde x este un nume de variabilă și σ este un tip, astfel încât niciun nume de variabilă să nu fie duplicat. Se definește apoi judecățile de tastare a termenilor în context în mod obișnuit pentru următoarele constructe sintactice:

• Variabile (dacă x: σ face parte dintr-un context Γ , atunci Γ ⊢ x  : σ )
• Aplicare (a unui termen de tip σ → τ la un termen de tip σ )
• λ-abstractizare
• Y Combinator punct fix (făcând termeni de tip sigma din termeni de tip sigma → sigma )
• Operațiile succesor ( succ ) și predecesor ( pred ) pe nat și constanta 0
• Condiționalul if cu regula de tastare:

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

( naturile vor fi interpretate ca booleeni aici cu o convenție precum zero care denotă adevăr și orice alt număr care denotă falsitate)

Semantică

Semantica denotațională

O semantică relativ simplă pentru limbă este modelul Scott . În acest model,

• Tipurile sunt interpretate ca anumite domenii .
  • ${\ displaystyle [\! [{\ textbf {nat}}] \!]: = \ mathbb {N} _ {\ bot}}$ (numerele naturale cu un element inferior alăturat, cu ordonarea plată)
  • ${\ displaystyle [\! [\ sigma \ to \ tau \,] \!]}$este interpretat ca domeniul funcțiilor continue Scott de la la , cu ordonarea punctuală.${\ displaystyle [\! [\ sigma] \!] \,}$${\ displaystyle [\! [\ tau] \!] \,}$
• Un context este interpretat ca produs${\ displaystyle x_ {1}: \ sigma _ {1}, \; \ dots, \; x_ {n}: \ sigma _ {n}}$${\ displaystyle [\! [\ sigma _ {1}] \!] \ times \; \ dots \; \ times [\! [\ sigma _ {n}] \!]}$
• Termenii din context sunt interpretați ca funcții continue${\ displaystyle \ Gamma \; \ vdash \; x \;: \; \ sigma}$${\ displaystyle [\! [\ Gamma] \!] \; \ to \; [\! [\ sigma] \!]}$
  • Termenii variabili sunt interpretați ca proiecții
  • Abstracția și aplicația Lambda sunt interpretate prin utilizarea structurii închise carteziene a categoriei de domenii și funcții continue
  • Y este interpretat luând punctul cel mai puțin fix al argumentului

Acest model nu este pe deplin abstract pentru PCF; dar este complet abstract pentru limbajul obținut prin adăugarea unei paralele sau a unui operator la PCF (p. 293 în referința Hyland și Ong 2000 de mai jos).

Note

Referințe

• Scott, Dana S. (1969). „O alternativă teoretică de tip la CUCH, ISWIM, OWHY” (PDF) . Manuscris nepublicat .A apărut ca Scott, Dana S. (1993). „O alternativă teoretică de tip la CUCH, ISWIM, OWHY” . Informatică teoretică . 121 : 411–440. doi : 10.1016 / 0304-3975 (93) 90095-b .
• Plotkin, Gordon D. (1977). „LCF considerat ca un limbaj de programare” (PDF) . Informatică teoretică . 5 (3): 223–255. doi : 10.1016 / 0304-3975 (77) 90044-5 .
• Milner, Robin (1977). „Modele complet abstracte de tip λ-calculi” (PDF) . Informatică teoretică . 4 : 1–22. doi : 10.1016 / 0304-3975 (77) 90053-6 . hdl : 20.500.11820 / 731c88c6-cdb1-4ea0-945e-f39d85de11f1 .
• Mitchell, John C. (1996). „Limbajul PCF”. Fundamente pentru limbaje de programare .
• Abramsky, S., Jagadeesan, R. și Malacaria, P. (2000). "Abstracție completă pentru PCF" . Informații și calcule . 163 (2): 409–470. doi : 10.1006 / inco.2000.2930 .CS1 maint: nume multiple: lista autorilor ( link )
• Hyland, JME & Ong, C.-HL (2000). "Pe abstractizare completă pentru PCF" . Informații și calcule . 163 (2): 285-408. doi : 10.1006 / inco.2000.2917 .
• O'Hearn, PW și Riecke, J. G (1995). „Relații logice Kripke și PCF” . Informații și calcule . 120 (1): 107-116. doi : 10.1006 / inco.1995.1103 .
• Loader, R. (2001). „PCF-ul finitar nu este decis” . Informatică teoretică . 266 (1-2): 341-364. doi : 10.1016 / S0304-3975 (00) 00194-8 .
• Ong, C.-HL (1995). „Corespondența dintre semantica operațională și denotațională: problema completă de abstractizare pentru PCF” . În Abramsky, S .; Gabbay, D .; Maibau, TSE (eds.). Manual de logică în informatică . Presa Universitatii Oxford. pp. 269-356. Arhivat din original la 07.01.2006 . Adus 19.01.2006 .

linkuri externe

• Introducere în RealPCF
• Lexer și Parser pentru PCF scrise în SML