Apakah ada CCC yang diketahui ditutup dengan operasi powerdomain probabilistik?

Secara ekuivalen, adakah semantik denotasional yang dikenal untuk bahasa pemrograman fungsional tingkat tinggi probabilistik? Secara khusus, apakah ada model domain murni -kalkulus murni yang diperluas dengan operasi pilihan biner acak simetris.$\lambda$

Motivasi

Kategori tertutup Cartesian menyediakan semantik untuk -calculi tingkat tinggi. Powerdomain probabilistik menyediakan semantik untuk program stokastik. A CCC ditutup di bawah operasi domain power probabilistik akan memberikan semantik untuk bahasa pemrograman fungsional tingkat tinggi stokastik.$\lambda$

Pekerjaan yang berhubungan

Tix, Keimel, dan Plotkin (2004) [1] memberikan konstruksi modern dari operasi domain kekuasaan bawah, atas, dan cembung, tetapi berkomentar bahwa

Ini masih menjadi masalah terbuka apakah ada kategori tertutup kartesian dari domain kontinu yang ditutup berdasarkan pembangunan domain kekuasaan probabilistik.

Mislove (2013) [2,3] memberikan semantik untuk variabel acak kontinu dalam bahasa tingkat pertama, tetapi menyatakan itu

Meskipun domain kekuatan probabilistik membuat CCC dari poset lengkap terarah (dcpos, singkatnya) dan Scott-continuous map invarian, tidak ada kategori tertutup Cartesian domain - dcpos yang memenuhi asumsi perkiraan yang biasa - yang dikenal invarian di bawah konstruksi ini. Yang terbaik yang diketahui adalah bahwa kategori domain yang koheren adalah tidak tetap di bawah monad pilihan probabilistik [4], tetapi kategori ini tidak tertutup Cartesian.

Referensi

1. Regina Tix, Klaus Keimel, dan Gordon Plotkin (2004) "Domain semantik untuk menggabungkan probabilitas dan non-determinisme" .
2. Michael Mislove (2013) "Anatomi domain variabel acak kontinu I"
3. Michael Mislove (2013) "Anatomi domain variabel acak kontinu II"
4. Jung, A. dan R. Tix (1998) "The powerdomain probabilistic merepotkan"

Berikut ini adalah komentar yang diperluas, itu tidak menjawab pertanyaan Anda dalam istilah yang Anda ajukan tetapi memberikan semantik untuk kalkulus probabilistik tingkat tinggi yang mungkin menarik bagi Anda.

Dalam beberapa tahun terakhir telah ada garis penelitian yang sangat aktif seputar apa yang disebut semantik denotasi kuantitatif logika linier, berdasarkan pada gagasan (awalnya karena Girard [1]) bahwa program tingkat tinggi dapat dimodelkan oleh rangkaian daya. Dalam kasus probabilistik, ini mengambil bentuk yang disebut ruang koherensi probabilistik (PCS), juga diperkenalkan oleh Girard [2] dan dipelajari secara mendalam oleh Danos dan Ehrhard [3]. PCS menghasilkan model kalkulus probabilistik yang diketik dan tidak diketik yang memiliki sifat yang sangat berbeda dari domain daya dan model terkait monad lainnya. Secara khusus, PCS memberikan apa yang sejauh ini merupakan satu-satunya model abstrak yang sepenuhnya abstrak dari PCF probabilistik [4], yang terkenal sulit dan tampaknya tidak mungkin dicapai dengan domain kekuasaan (lih. KaryaJean Goubault-Larrecq ).

Terlepas dari Ehrhard, semantik kuantitatif sekarang secara aktif dikembangkan oleh Michele Pagani dan rekan penulis, saya sarankan Anda melihat halaman web-nya untuk referensi tambahan.

$\lambda$

[2] Jean-Yves Girard, Antara logika dan quantic: traktat . Dalam logika Linear dalam ilmu komputer , CUP, 2004.

[3] Vincent Danos dan Thomas Ehrhard, ruang koherensi probabilistik sebagai model perhitungan probabilistik tingkat tinggi . Informasi dan Komputasi 209 (6): 966-991, 2011.

[4] Thomas Ehrhard, Michele Pagani dan Christine Tasson, ruang koherensi probabilistik sepenuhnya abstrak untuk PCF probabilistik . Dalam Prosiding POPL , hlm. 309-320, 2014.

Komentar di bawah ini benar, tetapi penting untuk memahami arti elemen "terbatas" atau "kompak" dari suatu domain. Ini adalah denotasi objek yang dapat dihitung dalam waktu yang terbatas, sehingga penampilan mereka dalam model semantik bukan untuk kenyamanan teori-bukti - mereka mewakili hubungan yang kuat antara model dan perhitungan yang sebenarnya.

Nah, kutipan Mislove sudah mengandung jawaban positif: kategori dcpos adalah carteisan ditutup dan juga ditutup di bawah domain kekuasaan probabilistik. Ini memang dapat digunakan untuk memberikan semantik denotasional untuk perhitungan probabilistik tingkat tinggi. Namun, dcpos gagal untuk memenuhi "asumsi perkiraan biasa" bahwa setiap elemen dapat didekati oleh elemen "terbatas" dalam beberapa hal, seperti halnya untuk aljabar dan terus menerus. Asumsi-asumsi ini membantu dengan argumen denotasional tertentu tetapi tidak diperlukan untuk memberikan semantik per se.