Programmieren berechenbarer Funktionen - Programming Computable Functions

In der Informatik ist Programming Computable Functions (PCF) eine typisierte funktionale Sprache, die 1977 von Gordon Plotkin eingeführt wurde und auf früherem unveröffentlichtem Material von Dana Scott basiert . Es kann als erweiterte Version des typisierten Lambda-Kalküls oder als vereinfachte Version moderner typisierter funktionaler Sprachen wie ML oder Haskell angesehen werden .

Ein vollständig abstraktes Modell für PCF wurde zuerst von Milner (1977) gegeben. Da Milners Modell jedoch im Wesentlichen auf der Syntax von PCF basierte, wurde es als wenig zufriedenstellend angesehen (Ong, 1995). Die ersten beiden vollständig abstrakten Modelle ohne Syntax wurden in den 1990er Jahren formuliert. Diese Modelle basieren auf Spiel Semantik (Hyland und Ong, 2000; Abramsky, Jagadeesan und Malacaria, 2000) und Kripke logische Beziehungen (O'Hearn und Riecke, 1995). Eine Zeit lang war man der Meinung, dass keines dieser Modelle völlig zufriedenstellend war, da sie nicht effektiv vorzeigbar waren. Allerdings Ralph Loader gezeigt , dass kein wirksamer vorzeigbar voll abstraktes Modell existieren könnte, da die Frage der Programm Gleichwertigkeit im finitäre Fragment von PCF ist nicht entscheidbar.

Syntax

Die PCF- Typen werden induktiv definiert als

• nat ist ein Typ
• Für die Typen σ und τ gibt es einen Typ σ → τ

Ein Kontext ist eine Liste von Paaren x : σ , wobei x ein Variablenname und σ ein Typ ist, sodass kein Variablenname dupliziert wird. Typisierungsurteile von Begriffen im Kontext definiert man dann in üblicher Weise für die folgenden syntaktischen Konstrukte:

• Variablen (wenn x : σ Teil eines Kontextes Γ ist , dann Γ ⊢ x  : σ )
• Anwendung (eines Termes vom Typ σ → τ auf einen Term vom Typ σ )
• λ-Abstraktion
• Der Y- Festpunktkombinator (Terme vom Typ σ aus Termen vom Typ σ → σ machen )
• Die Nachfolger ( succ ) und Vorgänger ( pred ) Operationen auf nat und die Konstante 0
• Das bedingte if mit der Typisierungsregel:

${\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 wird hier als Boolean interpretiert, mit einer Konvention wie Null für Wahrheit und jede andere Zahl für Falschheit)

Semantik

Denotationale Semantik

Eine relativ einfache Semantik für die Sprache ist das Scott-Modell . Bei diesem Modell,

• Typen werden als bestimmte Domänen interpretiert .
  • ${\displaystyle [\![{\textbf {nat}}]\!]:=\mathbb {N} _{\bot }}$ (die natürlichen Zahlen mit einem daran anschließenden unteren Element, mit der flachen Ordnung)
  • ${\displaystyle [\![\sigma\to\tau\,]\!]}$wird als Bereich der Scott-stetigen Funktionen von bis interpretiert , mit der punktweisen Ordnung.${\displaystyle [\![\sigma ]\!]\,}$${\displaystyle [\![\tau ]\!]\,}$
• Ein Kontext wird als Produkt interpretiert${\displaystyle x_{1}:\sigma_{1},\;\dots ,\;x_{n}:\sigma_{n}}$${\displaystyle [\![\sigma_{1}]\!]\times \;\dots \;\times [\![\sigma_{n}]\!]}$
• Begriffe im Kontext werden als stetige Funktionen interpretiert${\displaystyle \Gamma\;\vdash\;x\;:\;\sigma}$${\displaystyle [\![\Gamma ]\!]\;\to \;[\![\sigma ]\!]}$
  • Variable Terme werden als Projektionen interpretiert
  • Lambda-Abstraktion und -Anwendung werden interpretiert, indem die kartesische geschlossene Struktur der Kategorie der Domänen und stetigen Funktionen verwendet wird
  • Y wird interpretiert, indem man den kleinsten Fixpunkt des Arguments nimmt

Dieses Modell ist für PCF nicht vollständig abstrakt; sie ist jedoch für die Sprache, die durch Hinzufügen eines Parallel- oder Operators zu PCF erhalten wird, vollständig abstrakt (S. 293 in der folgenden Referenz von Hyland und Ong 2000).

Anmerkungen

Verweise

• Scott, Dana S. (1969). "Eine typtheoretische Alternative zu CUCH, ISWIM, OWHY" (PDF) . Unveröffentlichtes Manuskript .Erschien als Scott, Dana S. (1993). "Eine typtheoretische Alternative zu CUCH, ISWIM, OWHY" . Theoretische Informatik . 121 : 411–440. doi : 10.1016/0304-3975(93)90095-b .
• Plotkin, Gordon D. (1977). "LCF gilt als Programmiersprache" (PDF) . Theoretische Informatik . 5 (3): 223–255. doi : 10.1016/0304-3975(77)90044-5 .
• Milner, Robin (1977). "Voll abstrakte Modelle typisierter λ-Kalküle" (PDF) . Theoretische Informatik . 4 : 1–22. doi : 10.1016/0304-3975(77)90053-6 . hdl : 20.500.11820/731c88c6-cdb1-4ea0-945e-f39d85de11f1 .
• Mitchell, John C. (1996). "Die Sprache PCF". Grundlagen für Programmiersprachen .
• Abramsky, S., Jagadeesan, R. und Malacaria, P. (2000). "Vollständige Abstraktion für PCF" . Informationen und Berechnung . 163 (2): 409–470. doi : 10.1006/inco.2000.2930 .CS1-Wartung: mehrere Namen: Autorenliste ( Link )
• Hyland, JME & Ong, C.-HL (2000). "Über die vollständige Abstraktion für PCF" . Informationen und Berechnung . 163 (2): 285–408. doi : 10.1006/inco.2000.2917 .
• O'Hearn, PW & Riecke, J.G. (1995). "Kripke Logische Beziehungen und PCF" . Informationen und Berechnung . 120 (1): 107–116. doi : 10.1006/inco.1995.1103 .
• Lader, R. (2001). "Finitärer PCF ist nicht entscheidbar" . Theoretische Informatik . 266 (1–2): 341–364. doi : 10.1016/S0304-3975(00)00194-8 .
• Ong, C.-HL (1995). "Korrespondenz zwischen operativer und denotationaler Semantik: Das vollständige Abstraktionsproblem für PCF" . In Abramsky, S.; Gabbay, D.; Maibau, TSE (Hrsg.). Handbuch der Logik in der Informatik . Oxford University Press. S. 269–356. Archiviert vom Original am 07.01.2006 . Abgerufen 2006-01-19 .

Externe Links

• Einführung in RealPCF
• Lexer und Parser für PCF in SML geschrieben