Hesaplanabilir Fonksiyonları Programlama - Programming Computable Functions

Gelen bilgisayar bilimleri , hesaplanabilir fonksiyonlar Programlama (PCF) bir olduğunu yazdınız işlevsel dil tarafından tanıtılan Gordon Plotkin önceki yayımlanmamış malzemeye dayanan 1977 yılında, Dana Scott . Yazılan lambda hesabının genişletilmiş bir versiyonu veya ML veya Haskell gibi modern yazılan fonksiyonel dillerin basitleştirilmiş bir versiyonu olarak düşünülebilir .

Bir tam arka PCF modeli, ilk olarak verildi Milner (1977). Bununla birlikte, Milner'ın modeli esas olarak PCF sözdizimine dayandığından, yetersiz olarak kabul edildi (Ong, 1995). Sözdizimi kullanmayan ilk iki tamamen soyut model 1990'larda formüle edildi. Bu modeller oyun semantiğine (Hyland ve Ong, 2000; Abramsky, Jagadeesan ve Malacaria, 2000) ve Kripke mantıksal ilişkilerine (O'Hearn ve Riecke, 1995) dayanmaktadır . Bir süre, bu modellerin hiçbirinin tam olarak tatmin edici olmadığı hissedildi, çünkü bunlar etkili bir şekilde sunulabilir değildi. Bununla birlikte, Ralph Loader , PCF'nin sonlu parçasındaki program denkliği sorunu kararlaştırılamaz olduğundan, etkin bir şekilde sunulabilir tamamen soyut bir modelin var olamayacağını gösterdi.

Sözdizimi

Türleri PCF indüktif olarak tanımlanmaktadır

• nat bir türdür
• σ ve τ türleri için bir σ → τ türü vardır.

Bir içerik çiftlerin bir listesi x şu şekilde hesaplanır: , X değişken adım ve σ bir değişken adı iki kez, örneğin bir türüdür. Daha sonra, aşağıdaki sözdizimsel yapılar için bağlam içindeki terimlerin yazım yargılarını olağan şekilde tanımlar:

• Değişkenler (eğer x : σ Γ bağlamının bir parçasıysa , o zaman Γ ⊢ x  : σ )
• Uygulama ( σ → τ türündeki bir terimden σ türündeki bir terime )
• λ-soyutlama
• Y, sabit nokta combinator (tip koşullarını yapma σ türü açısından üzerinden σ → σ )
• nat ve 0 sabitinde ardıl ( succ ) ve öncül ( pred ) işlemleri
• Yazma kuralıyla koşullu if :

${\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 burada sıfır gerçeği ifade eden ve diğer herhangi bir sayı yanlışlığı ifade eden bir kuralla boolean olarak yorumlanacaktır)

anlambilim

düz anlambilim

Dil için nispeten basit bir anlambilim, Scott modelidir . Bu modelde,

• Türler belirli etki alanları olarak yorumlanır .
  • ${\displaystyle [\![{\textbf {nat}}]\!]:=\mathbb {N} _{\bot }}$ (düz sıralama ile bitişik bir alt elemanlı doğal sayılar)
  • ${\displaystyle [\![\sigma \to \tau \,]\!]}$etki olarak yorumlanır Scott-sürekli gelen fonksiyonlara göre noktasal sipariş ile.${\görüntüleme stili [\![\sigma ]\!]\,}$${\görüntüleme stili [\![\tau ]\!]\,}$
• Bir bağlam ürün olarak yorumlanır${\displaystyle x_{1}:\sigma _{1},\;\dots ,\;x_{n}:\sigma _{n}}$${\displaystyle [\![\sigma _{1}]\!]\times \;\dots \;\times [\![\sigma _{n}]\!]}$
• Bağlamdaki terimler sürekli işlevler olarak yorumlanır${\displaystyle \Gamma \;\vdash \;x\;:\;\sigma }$${\displaystyle [\![\Gamma ]\!]\;\to \;[\![\sigma ]\!]}$
  • Değişken terimler projeksiyon olarak yorumlanır
  • Lambda soyutlaması ve uygulaması, alanlar ve sürekli fonksiyonlar kategorisinin kartezyen kapalı yapısından yararlanılarak yorumlanmıştır.
  • Y , argümanın en az sabit noktası alınarak yorumlanır

Bu model PCF için tamamen soyut değildir; ancak PCF'ye bir paralel veya operatör eklenerek elde edilen dil için tamamen soyuttur (aşağıdaki Hyland ve Ong 2000 referansında s. 293).

Notlar

Referanslar

• Scott, Dana S. (1969). "CUCH, ISWIM, OWHY'ye teorik bir alternatif" (PDF) . Yayınlanmamış El Yazması .Scott, Dana S. (1993) olarak göründü . "CUCH, ISWIM, OWHY'ye teorik bir alternatif" . Teorik Bilgisayar Bilimi . 121 : 411–440. doi : 10.1016/0304-3975(93)90095-b .
• Plotkin, Gordon D. (1977). "LCF bir programlama dili olarak kabul edilir" (PDF) . Teorik Bilgisayar Bilimi . 5 (3): 223–255. doi : 10.1016/0304-3975(77)90044-5 .
• Milner, Robin (1977). "Yazılan λ-hesaplarının tamamen soyut modelleri" (PDF) . Teorik Bilgisayar Bilimi . 4 : 1–22. doi : 10.1016/0304-3975(77)90053-6 . hdl : 20.500.11820/731c88c6-cdb1-4ea0-945e-f39d85de11f1 .
• Mitchell, John C. (1996). "Dil PCF". Programlama Dillerinin Temelleri .
• Abramsky, S., Jagadeesan, R. ve Malacaria, P. (2000). "PCF için Tam Soyutlama" . Bilgi ve Hesaplama . 163 (2): 409-470. doi : 10.1006/inco.2000.2930 .CS1 bakımı: birden çok ad: yazar listesi ( bağlantı )
• Hyland, JME & Ong, C.-HL (2000). "PCF için Tam Soyutlama Üzerine" . Bilgi ve Hesaplama . 163 (2): 285–408. doi : 10.1006/inco.2000.2917 .
• O'Hearn, PW & Riecke, J.G (1995). "Kripke Mantıksal İlişkiler ve PCF" . Bilgi ve Hesaplama . 120 (1): 107–116. doi : 10.1006/inco.1995.1103 .
• Yükleyici, R. (2001). "Finter PCF kararlaştırılamaz" . Teorik Bilgisayar Bilimi . 266 (1–2): 341–364. doi : 10.1016/S0304-3975(00)00194-8 .
• Ong, C.-HL (1995). "İşlemsel ve Denotasyonel Semantik Arasındaki Uyum: PCF için Tam Soyutlama Problemi" . Abramsky'de, S.; Gabbay, D.; Maibau, TSE (ed.). Bilgisayar Biliminde Mantık El Kitabı . Oxford Üniversitesi Yayınları. s. 269-356. Arşivlenmiş orijinal 2006-01-07 tarihinde . 2006-01-19 alındı .

Dış bağlantılar

• RealPCF'ye Giriş
• SML ile yazılmış PCF için Lexer ve Ayrıştırıcı