Sözel anlambilim - Denotational semantics - Wikipedia

İçinde bilgisayar Bilimi, gösterimsel anlambilim (başlangıçta olarak bilinir matematiksel anlambilim veya Scott – Strachey semantiği) anlamlarını resmileştirme yaklaşımıdır Programlama dilleri matematiksel nesneler oluşturarak ( gösterimler) dillerdeki ifadelerin anlamlarını açıklayan. Diğer yaklaşımlar sağlar programlama dillerinin biçimsel anlambilim dahil olmak üzere aksiyomatik anlambilim ve operasyonel anlambilim.

Genel olarak ifade edilen anlambilim, adı verilen matematiksel nesneleri bulmakla ilgilidir. etki alanları programların ne yaptığını temsil eden. Örneğin, programlar (veya program cümleleri) şu şekilde temsil edilebilir: kısmi işlevler veya çevre ve sistem arasındaki oyunlarla.

Anlamsal anlamın önemli bir ilkesi şudur: anlambilim olmalı kompozisyon: bir program cümlesinin ifadesi, onun alt sözcükler.

Tarihsel gelişim

Denotasyonel anlambilim Christopher Strachey ve Dana Scott 1970'lerin başında yayınlandı.[1] Başlangıçta Strachey ve Scott tarafından geliştirildiği gibi, gösterime dayalı anlambilim, bir bilgisayar programının anlamını bir işlevi girdiyi çıktıya eşleyen.[2] Anlam vermek yinelemeli olarak tanımlanmış Scott ile çalışmayı önerdi sürekli fonksiyonlar arasında etki alanları özellikle kısmi siparişler. Aşağıda açıklandığı gibi, programlama dillerinin sıralılık gibi yönleri için uygun ifade semantiğinin araştırılmasına yönelik çalışmalar devam etmiştir. eşzamanlılık, belirlenimsizlik ve yerel eyalet.

Belirtisel anlambilim, aşağıdaki gibi yetenekleri kullanan modern programlama dilleri için geliştirilmiştir. eşzamanlılık ve istisnalar, Örneğin., Eşzamanlı ML,[3] CSP,[4] ve Haskell.[5] Bu dillerin anlambilimi, bir cümlenin anlamının, alt cümlelerinin anlamlarına bağlı olması bakımından bileşimseldir. Örneğin, uygulamalı ifade f (E1, E2), f, E1 ve E2 alt cümlelerinin anlambilimine göre tanımlanır. Modern bir programlama dilinde, E1 ve E2 eşzamanlı olarak değerlendirilebilir ve bunlardan birinin yürütülmesi, birbirleriyle etkileşim kurarak diğerini etkileyebilir. paylaşılan nesneler anlamlarının birbirleri açısından tanımlanmasına neden olur. Ayrıca, E1 veya E2 bir istisna oluşturabilir ve bitirmek diğerinin infazı. Aşağıdaki bölümler, bu modern programlama dillerinin anlambiliminin özel durumlarını açıklamaktadır.

Özyinelemeli programların anlamları

Gösterimsel anlambilim, bir ortamdan (serbest değişkenlerinin mevcut değerlerini tutan) gösterime kadar bir işlev olarak bir program ifadesine atfedilir. Örneğin, ifade n * m iki serbest değişkeni için bağlayıcı olan bir ortam sağlandığında bir ifade üretir: n ve m. Ortamdaysa n 3 değerine sahiptir ve m 5 değerine sahipse, ifade 15'tir.[kaynak belirtilmeli ]

Bir işlev, bir dizi olarak temsil edilebilir sıralı çiftler bağımsız değişken ve karşılık gelen sonuç değerleri. Örneğin, {(0,1), (4,3)} kümesi, bağımsız değişken 0 için sonuç 1, bağımsız değişken 4 için sonuç 3 ve aksi takdirde tanımsız olan bir işlevi belirtir.

Çözülmesi gereken sorun, özyinelemeli programların tanımlanması gibi kendi açısından tanımlanan anlamlar sağlamaktır. faktöryel işlev olarak

int faktöryel(int n) { Eğer (n == 0) sonra dönüş 1; Başka dönüş n * faktöryel(n-1); }

Bir çözüm, anlamları yaklaşık olarak oluşturmaktır. Faktöriyel işlevi bir toplam işlev ℕ ile ℕ arası (etki alanında her yerde tanımlanmıştır), ancak biz onu bir kısmi işlev. Başlangıçta, boş işlev (boş bir küme). Ardından, faktöriyel işleve daha iyi yaklaşan başka bir kısmi işlevle sonuçlanmak için sıralı çifti (0,1) işleve ekliyoruz. Daha sonra, daha da iyi bir yaklaşım oluşturmak için başka bir sıralı çifti (1,1) ekliyoruz.

Bu yineleme zincirini "kısmi faktöriyel işlev" için düşünmek öğreticidir F gibi F0, F1, F2, ... nerede Fn gösterir F uygulamalı n zamanlar.

  • F0({}), {} kümesi olarak gösterilen, tamamen tanımlanmamış kısmi işlevdir;
  • F1({}), {(0,1)} kümesi olarak temsil edilen kısmi işlevdir: 0'da 1 olarak tanımlanır ve başka yerde tanımsız;
  • F5({}), {(0,1), (1,1), (2,2), (3,6), (4,24)} kümesi olarak temsil edilen kısmi işlevdir: 0 bağımsız değişkenleri için tanımlanmıştır 1,2,3,4.

Bu yinelemeli süreç, ℕ ile ℕ arasında bir dizi kısmi işlev oluşturur. Kısmi fonksiyonlar bir zincir tamamlanmış kısmi sipariş sipariş olarak ⊆ kullanarak. Dahası, faktöriyel işlevin daha iyi yaklaşımlarının bu yinelemeli süreci, kapsamlı (ilerleyen olarak da adlandırılır) bir eşleme oluşturur çünkü her biri sipariş olarak ⊆ kullanarak. Yani bir sabit nokta teoremi (özellikle Bourbaki – Witt teoremi ), bu yinelemeli süreç için sabit bir nokta vardır.

Bu durumda, sabit nokta, bu zincirin en az üst sınırı olan faktöryel işlev olarak ifade edilebilir direkt limit

Burada "⊔" sembolü, yönlendirilmiş katılma (nın-nin yönetilen setler ), "en az üst sınır" anlamına gelir. Yönlendirilmiş birleştirme esasen katılmak yönlendirilmiş setlerin.

Belirleyici olmayan programların ifade semantiği

Kavramı güç alanları deterministik olmayan sıralı programlara tanımsal bir anlam vermek için geliştirilmiştir. yazı P bir güç alanı kurucusu için alan P(D) ile belirtilen türdeki deterministik olmayan hesaplamaların alanıdır. D.

Adaletle ilgili zorluklar var ve sınırsızlık non-determinizm alan-teorik modellerinde.[6]

Eşzamanlılığın sözel semantiği

Birçok araştırmacı, yukarıda verilen alan teorik modellerinin daha genel bir durum için yeterli olmadığını iddia etmiştir. eşzamanlı hesaplama. Bu nedenle çeşitli yeni modeller tanıtıldı. 1980'lerin başlarında, insanlar eşzamanlı diller için anlambilim vermek için ifadesel anlambilim tarzını kullanmaya başladılar. Örnekler şunları içerir: Will Clinger'in oyuncu modeli ile çalışması; Glynn Winskel'in olay yapılarıyla çalışması ve petri ağları;[7] ve Francez, Hoare, Lehmann ve de Roever'in (1979) CSP için iz semantikleri üzerine çalışmaları.[8] Tüm bu sorgulama hatları halen araştırılmaktadır (örneğin CSP için çeşitli tanım modellerine bakınız).[4]).

Son zamanlarda, Winskel ve diğerleri şu kategoriyi önerdiler: profunctors eşzamanlılık için bir alan teorisi olarak.[9][10]

Durumun sözdizimsel semantiği

Durum (bir yığın gibi) ve basit zorunlu özellikler yukarıda açıklanan tanımsal anlambilimde doğrudan modellenebilir. Hepsi ders kitapları aşağıda ayrıntıları var. Temel fikir, bir komutu bazı durumların etki alanında kısmi bir işlev olarak düşünmektir. Anlamı "x: = 3"o zaman bir durumu eyalete taşıyan işlevdir 3 atandı x. Sıralama operatörü ";", işlevlerin bileşimi ile gösterilir. Sabit noktalı yapılar daha sonra döngü yapılarına bir anlambilim vermek için kullanılır, örneğin"süre".

Yerel değişkenlerle programların modellenmesinde işler daha zor hale gelir. Bir yaklaşım, artık alanlarla çalışmak yerine türleri şu şekilde yorumlamaktır: functors bazı dünya kategorilerinden bir alan kategorisine. Programlar daha sonra şu şekilde gösterilir: doğal bu işlevler arasındaki sürekli işlevler.[11][12]

Veri türlerinin açıklamaları

Birçok programlama dili, kullanıcıların yinelemeli veri türleri. Örneğin, numara listelerinin türü şu şekilde belirtilebilir:

veri tipi liste = Eksileri nın-nin nat * liste | Boş

Bu bölüm yalnızca değiştirilemeyen işlevsel veri yapılarını ele almaktadır. Geleneksel zorunlu programlama dilleri, tipik olarak, böyle bir özyinelemeli listenin öğelerinin değiştirilmesine izin verir.

Başka bir örnek için: işaretlerin türü türlenmemiş lambda hesabı dır-dir

veri tipi D = D nın-nin (D  D)

Sorunu alan denklemlerini çözme bu tür veri türlerini modelleyen alanlar bulmakla ilgilenir. Kabaca bir yaklaşım, tüm etki alanlarının koleksiyonunu bir etki alanı olarak düşünmek ve ardından burada yinelemeli tanımı çözmektir. Aşağıdaki ders kitapları daha fazla ayrıntı verir.

Polimorfik veri türleri bir parametre ile tanımlanan veri türleridir. Örneğin, α türü listes tarafından tanımlanır

veri tipi α liste = Eksileri nın-nin α * α liste | Boş

O halde doğal sayıların listeleri türdendir nat listesidizge listeleri ise dize listesi.

Bazı araştırmacılar, polimorfizmin alan teorik modellerini geliştirdiler. Diğer araştırmacılar da modelledi parametrik polimorfizm yapıcı küme teorileri içinde. Detaylar aşağıda listelenen ders kitaplarında bulunmaktadır.

Yeni bir araştırma alanı, nesne ve sınıf tabanlı programlama dilleri için tanımsal anlambilim içermektedir.[13]

Sınırlı karmaşıklık programları için ifade anlambilim

Temel alan programlama dillerinin gelişimini takip etmek doğrusal mantık, gösterimsel anlambilim doğrusal kullanım için dillere verilmiştir (bkz. geçirmez ağlar, tutarlılık uzayları ) ve ayrıca polinom zaman karmaşıklığı.[14]

Sıralılığın sözel anlambilim

Tam sorunu soyutlama sıralı programlama dili için PCF uzun bir süre, anlamsal anlambilimde büyük ve açık bir soruydu. PCF ile ilgili zorluk, çok sıralı bir dil olmasıdır. Örneğin, tanımlamanın bir yolu yoktur. paralel veya PCF'de işlev. Bu nedenle, yukarıda anlatıldığı gibi, alanları kullanan yaklaşım, tamamen soyut olmayan bir gösterimsel anlambilim sağlar.

Bu açık soru çoğunlukla 1990'larda oyun semantiği ve ayrıca aşağıdakileri içeren tekniklerle mantıksal ilişkiler.[15] Daha fazla ayrıntı için, PCF'deki sayfaya bakın.

Kaynaktan kaynağa çeviri olarak ifade anlambilim

Bir programlama dilini diğerine çevirmek genellikle yararlıdır. Örneğin, eşzamanlı bir programlama dili bir süreç hesabı; yüksek seviyeli bir programlama dili bayt koduna çevrilebilir. (Aslında, geleneksel ifade anlambilim, programlama dillerinin iç dil alan kategorisinin.)

Bu bağlamda, tam soyutlama gibi tanımsal anlamlardan gelen kavramlar, güvenlik endişelerinin giderilmesine yardımcı olur.[16][17]

Soyutlama

Belirtisel anlambilim ile bağlantı kurmanın genellikle önemli olduğu düşünülmektedir. operasyonel anlambilim. Bu, özellikle anlamsal anlambilim oldukça matematiksel ve soyut olduğunda ve işlemsel anlambilim daha somut veya hesaplama sezgilerine daha yakın olduğunda önemlidir. Bir tanımsal semantiğin aşağıdaki özellikleri genellikle ilgi çekicidir.

  1. Sözdizimi bağımsızlığı: Programların anlamları kaynak dilin sözdizimini içermemelidir.
  2. Yeterlilik (veya sağlamlık): Herşey gözle görülür şekilde farklı programların farklı anlamları vardır;
  3. Tam soyutlama: Gözlemsel olarak eşdeğer tüm programlar eşit anlamlara sahiptir.

Geleneksel tarzdaki anlambilim için, yeterlilik ve tam soyutlama, kabaca "işlemsel eşdeğerliğin, anlamsal eşitlikle çakışması" gerekliliği olarak anlaşılabilir. Daha derinlemesine modellerde ifade anlambilim için, örneğin aktör modeli ve işlem taşı Her modelde farklı eşdeğerlik kavramları vardır ve bu nedenle yeterlilik ve tam soyutlama kavramları bir tartışma konusudur ve tespit edilmesi daha zordur. Ayrıca işlemsel semantiğin matematiksel yapısı ve tanımsal anlambilim çok yakın hale gelebilir.

Operasyonel ve gösterimsel anlamlar arasında tutmayı isteyebileceğimiz diğer arzu edilen özellikler şunlardır:

  1. Yapılandırmacılık: Yapılandırmacılık alan öğelerinin yapıcı yöntemlerle var olduğunun gösterilip gösterilemeyeceği ile ilgilenir.
  2. Gösterimsel ve işlemsel anlambilimin bağımsızlığı: Belirtisel anlam, bir programlama dilinin işlemsel anlamından bağımsız matematiksel yapılar kullanılarak biçimlendirilmelidir; Bununla birlikte, temelde yatan kavramlar yakından ilişkili olabilir. İle ilgili bölüme bakın Kompozisyonalite altında.
  3. Tam eksiksizlik veya tanımlanabilirlik: Anlamsal modelin her morfizmi, bir programın ifadesi olmalıdır.[18]

Kompozisyonalite

Programlama dillerinin tanımsal anlambiliminin önemli bir yönü, bir programın gösteriminin, parçalarının gösterimlerinden oluşturulduğu bileşimdir. Örneğin, "7 + 4" ifadesini düşünün. Bu durumda kompozisyon, "7", "4" ve "+" anlamlarına göre "7 + 4" için bir anlam sağlamaktır.

Alan teorisindeki temel bir anlamsal anlambilim, aşağıdaki gibi verildiği için bileşimseldir. Program parçalarını, yani serbest değişkenli programları dikkate alarak başlıyoruz. Bir bağlam yazmak her bir serbest değişkene bir tür atar. Örneğin, ifadede (x + y) bir yazma bağlamında düşünülebilir (x:nat,y:nat). Şimdi aşağıdaki şemayı kullanarak parçaları programlamak için tanımsal bir anlambilim veriyoruz.

  1. Dilimizin türlerinin anlamını açıklayarak başlıyoruz: her türün anlamı bir alan olmalıdır. Τ tipini belirten etki alanı için 〚τ〛 yazıyoruz. Örneğin, yazının anlamı nat doğal sayıların alanı olmalıdır: 〚nat〛 = ℕ.
  2. Türlerin anlamından bağlamları yazmak için bir anlam çıkarırız. Ayarladık [ x1: τ1,..., xn: τn〛 = 〚Τ1〛 × ... × 〚τn〛. Örneğin, [x:nat,y:nat>〛 = ℕ× ℕ. Özel bir durum olarak, değişken içermeyen boş yazma bağlamının anlamı, 1 ile gösterilen tek öğeli alandır.
  3. Son olarak, yazım bağlamındaki her program parçasına bir anlam vermeliyiz. Farz et ki P genellikle Γ⊢ yazılan bağlam context yazılırken, σ tipinde bir program parçasıdırP: σ. O zaman bu program-yazım bağlamının anlamı sürekli bir fonksiyon olmalıdır 〚Γ⊢P: σ〛: 〚Γ〛 → 〚σ〛. Örneğin, 〚⊢7:nat〛: 1 → ℕ sürekli "7" işlevi, 〚x:nat,y:natx+y:nat〛: ℕ× ℕ→ ℕ iki sayı ekleyen işlevdir.

Şimdi, bileşik ifadenin anlamı (7 + 4), üç fonksiyon 〚⊢7 oluşturularak belirlenir:nat〛: 1 → ℕ, 〚⊢4:nat〛: 1 → ℕ, ve [x:nat,y:natx+y:nat〛: ℕ× ℕ→ ℕ.

Aslında bu, kompozisyonel anlamsal anlamlar için genel bir şemadır. Burada etki alanları ve sürekli işlevler hakkında belirli hiçbir şey yoktur. Biri farklı bir kategori yerine. Örneğin, oyun anlambiliminde oyun kategorisinde oyunlar nesne olarak ve stratejiler morfizm olarak bulunur: türleri oyun olarak ve programları strateji olarak yorumlayabiliriz. Genel özyineleme içermeyen basit bir dil için, kümeler ve işlevler kategorisi. Yan etkileri olan bir dil için, Kleisli kategorisi bir monad için. Devleti olan bir dil için, bir functor kategorisi. Milner nesneler olarak arayüzlerle bir kategoride çalışarak modelleme konumu ve etkileşimi savunmuştur ve Bigraphs morfizmler olarak.[19]

Anlambilim ve uygulama

Dana Scott'a (1980) göre:[20]

Anlambilimin bir uygulamayı belirlemesi gerekli değildir, ancak bir uygulamanın doğru olduğunu göstermek için kriterler sağlamalıdır.

Clinger'a (1981) göre:[21]:79

Bununla birlikte, genellikle, geleneksel bir sıralı programlama dilinin biçimsel anlambiliminin kendisi, dilin (verimsiz) bir uygulamasını sağlamak için yorumlanabilir. Biçimsel bir anlambilimin her zaman böyle bir uygulama sağlamasına gerek yoktur ve anlambilimin bir uygulama sağlaması gerektiğine inanmak, eşzamanlı dillerin biçimsel anlambilimiyle ilgili kafa karışıklığına yol açar. Böyle bir kafa karışıklığı, bir programlama dilinin anlambilimindeki sınırsız belirsizlik varlığının, programlama dilinin uygulanamayacağını ima ettiği söylendiğinde acı bir şekilde ortaya çıkar.

Bilgisayar biliminin diğer alanlarıyla bağlantılar

Gösterimsel anlambilim alanındaki bazı çalışmalar, türleri, alan teorisi anlamında alanlar olarak yorumlamıştır; bu, bir dalı olarak görülebilir. model teorisi ile bağlantılara yol açar tip teorisi ve kategori teorisi. Bilgisayar bilimi içinde aşağıdakilerle bağlantılar vardır: soyut yorumlama, program doğrulama, ve model kontrolü.

Referanslar

  1. ^ Dana S. Scott. Matematiksel bir hesaplama teorisinin ana hatları. Technical Monograph PRG-2, Oxford University Computing Laboratory, Oxford, İngiltere, Kasım 1970.
  2. ^ Dana Scott ve Christopher Strachey. Bilgisayar dilleri için matematiksel bir semantiğe doğru Oxford Programlama Araştırma Grubu Teknik Monografı. PRG-6. 1971.
  3. ^ John Reppy Springer-Verlag'da "Eşzamanlı Makine Öğrenimi: Tasarım, Uygulama ve Anlambilim", Bilgisayar Bilimlerinde Ders Notları, Cilt. 693. 1993
  4. ^ a b A. W. Roscoe. "Eş Zamanlılık Teorisi ve Pratiği" Prentice-Hall. 2005 revize edildi.
  5. ^ Simon Peyton Jones Alastair Reid, Fergus Henderson, Tony Hoare ve Simon Marlow. "Kesin olmayan istisnalar için bir anlambilim "Programlama Dili Tasarımı ve Uygulaması Konferansı. 1999.
  6. ^ Levy, Paul Blain (2007). "Amb Sağlamlığı Bozar, Temel Amb Yapmaz". Electr. Notlar Teorisi. Bilgisayar. Sci. 173: 221–239. doi:10.1016 / j.entcs.2007.02.036.
  7. ^ CCS ve İlgili Diller için Etkinlik Yapısı Anlamları. DAIMI Araştırma Raporu, Aarhus Üniversitesi, 67 s., Nisan 1983.
  8. ^ Nissim Francez, C.A. R. Hoare, Daniel Lehmann ve Willem-Paul de Roever. "Belirsizlik, eşzamanlılık ve iletişim anlambilim ", Bilgisayar ve Sistem Bilimleri Dergisi. Aralık 1979.
  9. ^ Cattani, Gian Luca; Winskel, Glynn (2005). "Profunctors, open maps and bisimulation". Bilgisayar Bilimlerinde Matematiksel Yapılar. 15 (3): 553–614. CiteSeerX  10.1.1.111.6243. doi:10.1017 / S0960129505004718.
  10. ^ Nygaard, Mikkel; Winskel, Glynn (2004). "Eşzamanlılık için alan teorisi". Theor. Bilgisayar. Sci. 316 (1–3): 153–190. doi:10.1016 / j.tcs.2004.01.029.
  11. ^ Peter W. O'Hearn John Power, Robert D. Tennent, Makoto Takeyama. Girişimin sözdizimsel kontrolü yeniden ziyaret edildi. Electr. Notlar Teorisi. Bilgisayar. Sci. 1. 1995.
  12. ^ Frank J. Oles. Programlamanın Anlamsallığına Kategori-Teorik Bir Yaklaşım. Doktora tezi, Syracuse üniversitesi, New York, ABD. 1982.
  13. ^ Reus, Bernhard; Streicher, Thomas (2004). "Nesne taşının anlam ve mantığı". Theor. Bilgisayar. Sci. 316 (1): 191–213. doi:10.1016 / j.tcs.2004.01.030.
  14. ^ Baillot, P. (2004). "Tabakalı tutarlılık uzayları: Işık Doğrusal Mantık için bir gösterimsel anlambilim". Theor. Bilgisayar. Sci. 318 (1–2): 29–55. doi:10.1016 / j.tcs.2003.10.015.
  15. ^ O'Hearn, P.W .; Riecke, J.G. (Temmuz 1995). "Kripke Mantıksal İlişkiler ve PCF". Bilgi ve Hesaplama. 120 (1): 107–116. doi:10.1006 / inco.1995.1103.
  16. ^ Martin Abadi. "Programlama dili çevirilerinde koruma". Proc. ICALP'98. LNCS 1443. 1998.
  17. ^ Kennedy, Andrew (2006). ".NET programlama modelinin güvenliğini sağlama". Theor. Bilgisayar. Sci. 364 (3): 311–7. doi:10.1016 / j.tcs.2006.08.014.
  18. ^ Curien Pierre-Louis (2007). "Tanımlanabilirlik ve Tam Soyutlama". Teorik Bilgisayar Bilimlerinde Elektronik Notlar. 172: 301–310. doi:10.1016 / j.entcs.2007.02.011.
  19. ^ Milner, Robin (2009). İletişim Aracılarının Yeri ve Hareketi. Cambridge University Press. ISBN  978-0-521-73833-0. 2009 taslağı Arşivlendi 2012-04-02 de Wayback Makinesi.
  20. ^ "Gösterge Anlambilim Nedir?", MIT Laboratory for Computer Science Distinguished Lecture Series, 17 Nisan 1980, Clinger'da (1981) alıntılanmıştır.
  21. ^ Clinger William D. (1981). "Aktör Anlambiliminin Temelleri" (Doktora). Massachusetts Teknoloji Enstitüsü. hdl:1721.1/6935. AITR-633. Alıntı dergisi gerektirir | günlük = (Yardım)

daha fazla okuma

Ders kitapları
Ders Notları
diğer referanslar

Dış bağlantılar