Sayangnya, ada terlalu banyak hal yang terjadi di sini. Jadi, mudah untuk mencampuradukkan berbagai hal. Penggunaan "penuh" dalam "kelengkapan penuh" dan "abstraksi penuh" merujuk pada gagasan kepenuhan yang sepenuhnya berbeda. Tapi, ada juga beberapa hubungan yang tidak jelas di antara mereka. Jadi, ini akan menjadi jawaban yang rumit.
Kelengkapan lengkap : "Suara dan lengkap" adalah properti yang Anda inginkan untuk logika tradisional untuk sehubungan dengan semantiknya. Tingkat kesehatan berarti bahwa apa pun yang dapat Anda buktikan dalam logika adalah benar dalam model semantik. Kelengkapan berarti bahwa apa pun yang benar dalam model semantik dapat dibuktikan dalam logika. Kami mengatakan bahwa logika adalah suara dan lengkap untuk model semantik tertentu. Ketika kita sampai pada logika konstruktif, seperti teori tipe Martin-Lof atau logika linier, kami tidak hanya peduli tentang apakah formula dapat dibuktikan, tetapi juga apa buktinya. Formula yang dapat dibuktikan mungkin memiliki banyak bukti dan logika konstruktif ingin memisahkannya. Jadi, semantik untuk logika konstruktif melibatkan menentukan tidak hanya apakah formula itu benar, tetapi juga beberapa gagasan semantik abstrak tentang "bukti" ("bukti") untuk kebenarannya. Abramsky dan rekannya menciptakan istilah "kelengkapan penuh" yang berarti bahwa bukti dalam logika dapat mengekspresikan semua bukti semantik dalam model. Jadi, "penuh" mengacu pada bukti di sini. Logika "lengkap" dapat membuktikan semua yang dibutuhkan. Logika "sepenuhnya lengkap" memiliki semua bukti yang perlu dimiliki. Jadi "kelengkapan penuh" berarti "kelengkapan konstruktif" atau "kelengkapan bukti". Ini tidak ada hubungannya dengan abstraksi penuh.
Abstraksi penuh : "Cukup dan sepenuhnya abstrak" adalah properti yang Anda inginkan untuk model semantik bahasa pemrograman. (Perhatikan perbedaan pertama: kita sekarang berurusan dengan sifat-sifat model semantik, bukan sifat-sifat bahasa!) Kecukupan berarti bahwa, setiap kali dua istilah memiliki makna yang sama dalam model semantik, mereka secara observasi setara dalam bahasa pemrograman (sehubungan dengan beberapa gagasan eksekusi). Abstraksi penuh berarti bahwa, jika dua istilah setara secara pengamatan, mereka memiliki makna yang sama dalam model semantik. Ide-ide ini dapat dikaitkan dengan kesehatan dan kelengkapan, tetapi dengan cara yang agak dibuat-buat. Jika kita menganggap model semantik bahasa pemrograman sebagai "logika" atau "metode bukti" untuk berbicara tentang kesetaraan pengamatan, maka kecukupan berarti bahwa metode bukti ini masuk akal; abstraksi penuh berarti bahwa metode bukti ini lengkap. Tidak ada gagasan "kelengkapan penuh"metode bukti. (Tapi, hal seperti itu secara teori dimungkinkan, dan suatu hari seseorang mungkin melakukannya.)
Dalam kasus Anda, Anda lebih tertarik pada terjemahan daripada model semantik. Properti kecukupan dan abstraksi penuh dapat diperluas untuk menangani terjemahan sebagai berikut. Anda menganggap bahasa target sebagai "model semantik" Anda, yaitu formalisme yang sepenuhnya Anda pahami. Jika demikian, Anda memiliki gagasan tentang kesetaraan untuk itu. Kemudian, kami mengatakan bahwa terjemahannya memadai jika, setiap kali terjemahan dari dua program sumber setara dalam bahasa target, mereka secara observasi setara dalam bahasa sumber. Kami mengatakan bahwa itu sepenuhnya abstrak jika, setiap kali dua program sumber setara secara observasi dalam bahasa sumber, terjemahannya setara dalam bahasa target.
Pada kenyataannya, saya tidak tahu ada bahasa target yang benar-benar kami "pahami". Yang kita tahu adalah beberapa gagasan lain tentang kesetaraan pengamatan untuk bahasa target. Dalam hal itu, terjemahannya memadai jika kesetaraan pengamatan dari terjemahan dalam bahasa target menyiratkan kesetaraan pengamatan dalam bahasa sumber.
Terjemahan sepenuhnya abstrak jika kesetaraan pengamatan dari istilah-istilah dalam bahasa sumber menyiratkan kesetaraan pengamatan dari terjemahan dalam bahasa target.
M ≅ N ⟹ τ ( M )
τ(M)≅τ(N)⟹M≅N
Beberapa penulis mengambil "terjemahan sepenuhnya abstrak" yang berarti kombinasi dari dua sifat ini:
M ≅ NM≅N⟹τ(M)≅τ(N)
M≅N⟺τ(M)≅τ(N)
Egger dkk tampaknya juga memperluas gagasan kelengkapan penuh pada terjemahan. Dalam pengaturannya, rumus adalah tipe dan bukti adalah istilah. Terjemahan mereka menerjemahkan berbagai jenis dan istilah. Mereka menyebut terjemahan mereka sepenuhnya lengkap jika terjemahan dari tipe hanya memiliki istilah-istilah yang diperoleh dengan menerjemahkan istilah asli tipe A .
∀ N : τ ( A ) .AA
∀N:τ(A).∃M:A.τ(M)=N
Sekarang untuk koneksi yang samar antara kelengkapan penuh dan abstraksi penuh. Membuktikan bahwa model semantik atau terjemahan sepenuhnya abstrak sering melibatkan beberapa definisi. Ini karena bahasa kita pada umumnya lebih tinggi. Jadi, jika model semantik atau bahasa target memiliki "konteks" yang terlalu banyak, maka itu akan dapat menyodok istilah atau makna semantik kita dengan cara yang tidak diinginkan dan merusak kesetaraannya. "Cara yang tidak diinginkan" berarti dengan cara bahwa bahasa pemrograman itu sendiri tidak dapat menyodoknya. Jadi, untuk mendapatkan abstraksi penuh, kita perlu memastikan bahwa "konteks" yang tersedia dalam model semantik atau bahasa target memang berasal dari yang ada dalam bahasa sumber dalam beberapa bentuk. Perhatikan bahwa ini berkaitan dengan properti kelengkapan penuh.
Mengapa kita menginginkan properti seperti itu? Tidak ada apa-apaharus dilakukan dengan kompiler! Kami ingin properti ini untuk mengklaim bahwa bahasa sumber disematkan ke bahasa target. Jika kita senang dengan bahasa target tertentu (sebagai bahasa yang bersih, dapat dimengerti, entah bagaimana fundamental atau diberikan Tuhan) maka, jika bahasa sumber menanamkan ke dalamnya, maka kita dapat mengklaim bahwa tidak ada yang baru dalam bahasa sumber. Itu hanya bagian dari bahasa target yang kita kenal dan cintai. Ini hanya gula sintaksis. Jadi, terjemahan yang sepenuhnya abstrak diberikan oleh orang-orang untuk membuktikan bahwa bahasa target tertentu hebat. Mereka juga terkadang diberikan oleh orang-orang yang memiliki bahasa besar atau rumit untuk dihadapi. Jadi, alih-alih mendefinisikan semantik untuknya secara langsung, mereka menerjemahkannya ke beberapa bahasa inti dan kemudian memberikan semantik ke bahasa inti. Misalnya, laporan Haskell melakukan ini. Tetapi abstraksi penuh dari terjemahan-terjemahan ini jarang dibuktikan karena bahasa sumbernya besar dan rumit. Orang-orang percaya bahwa terjemahannya baik.
Sekali lagi, ini tidak ada hubungannya dengan kompiler. Kompiler jarang pernah memadai atau sepenuhnya abstrak. Dan, mereka tidak perlu seperti itu! Yang perlu dilakukan oleh kompiler adalah mempertahankan perilaku eksekusi dari program yang lengkap. Bahasa target kompilator umumnya besar, yang berarti ia memiliki banyak konteks yang dapat mengacaukan kesetaraan. Jadi, program setara dalam bahasa sumber hampir tidak pernah setara secara kontekstual saat dikompilasi.
Ringkasan: kelengkapan penuh berarti bahwa fungsi interpretasi tidak hanya lengkap, tetapi juga bersifat perkiraan pada program. Abstraksi penuh tidak memiliki persyaratan untuk surjectivity.
Detail: Arti terperinci dari abstraksi penuh dan kelengkapan penuh tergantung pada sifat apa / di mana / bagaimana Anda menafsirkan. Berikut adalah terjemahan untuk interpretasi dari satu bahasa pemrograman yang diketik ke bahasa lainnya. Anda memiliki fungsi interpretasi[[ . ]] yang memetakan tiga hal.
JenisSEBUAH dari bahasa sumber ke tipe [[ A ]] dalam bahasa target.
KonteksΓ dalam bahasa sumber ke konteks
[[ Γ ]] dalam bahasa target.
Program dalam konteksΓ ⊢ P: α untuk program dalam konteks [[ Γ ]] ⊢ [[ P]] : [[ α ]] .
Dalam interpretasi kategorikal dua peta pertama runtuh menjadi satu. Fungsi interpretasi dapat memiliki berbagai sifat, misalnya dapat bersifat komposisi, atau mempertahankan pemutusan atau ... Abstraksi penuh adalah salah satu sifat tersebut. Ingat abstraksi penuh dari[[ . ]]
maksudnya
untuk semuaP, Q . Sini≅S adalah gagasan yang dipilih dari kesetaraan program yang diketik untuk bahasa sumber sementara ≅T memainkan peran itu untuk bahasa target. Lebih tepatnya, karena kita berada dalam pengaturan yang diketik,
Now full abstraction does not imply that[[.]]
is surjective on types, contexts or programs in context.
Full completeness means that the map[[.]] is (complete and) surjective on
programs in context for all definable contexts and definable types,
i.e. any program [[Γ]]⊢Q:[[α]] in the target
language is the denotation of some Γ⊢P:α in the
source language, i.e. Q=[[P]] . Note that this does not
require [[.]] to be surjective on types and contexts, because
that property rarely holds in the interpretations we are
typically interested in.
sumber