Apa perbedaan antara hubungan logis dan simulasi?

Saya seorang pemula yang bekerja pada metode yang membuktikan kesetaraan program. Saya telah membaca beberapa makalah tentang mendefinisikan hubungan logis atau simulasi untuk membuktikan bahwa dua program setara. Tetapi saya cukup bingung tentang dua teknik ini.

Saya hanya tahu hubungan logis didefinisikan secara induktif sementara simulasi didasarkan pada coinduction. Mengapa mereka didefinisikan sedemikian rupa? Apa pro dan kontra mereka masing-masing? Yang mana yang harus saya pilih dalam situasi yang berbeda?

Saya punya jawaban untuk pertanyaan ini yang mungkin novel. Bahkan, saya masih memikirkannya selama 6 bulan terakhir, dan itu belum ditulis di surat kabar.

Tesis umum adalah bahwa prinsip-prinsip penalaran relasional seperti "hubungan logis", "simulasi", dan bahkan "invarian" adalah manifestasi dari abstraksi data atau penyembunyian informasi. Di mana pun ada informasi yang disembunyikan, prinsip-prinsip ini akan muncul.

Orang pertama yang menemukannya adalah ahli teori automata. Automata memiliki status tersembunyi. Jadi, Anda perlu alasan relasional untuk berbicara tentang kesetaraan mereka. Ahli teori Automata berjuang dengan homomorfisme untuk sementara waktu, menyerah, dan muncul dengan gagasan yang disebut "penutup relasional", yang merupakan bentuk hubungan simulasi.

Milner mengambil gagasan itu dalam sebuah makalah yang sedikit diketahui tetapi sangat mendasar yang disebut " Gagasan aljabar simulasi antar program " pada tahun 1971. Hoare mengetahuinya dan menggunakannya untuk menghasilkan " Bukti kebenaran representasi data " pada tahun 1972 (tetapi digunakan fungsi abstraksi bukan hubungan karena dia pikir itu "lebih sederhana"). Dia kemudian mencabut klaim kesederhanaan dan kembali menggunakan hubungan dalam " Penyempitan data yang disempurnakan ". Reynolds menggunakan penalaran relasional dalam " Craft of Programming", Bab 5 (1981). Dia pikir hubungan lebih alami dan umum daripada fungsi abstraksi. Jika Anda kembali dan membaca bab ini, Anda akan menemukan ide-ide parametrisitas relasional yang mengintai, menunggu untuk ditemukan. Tentu saja, dua tahun kemudian, Reynolds menerbitkan "Jenis, abstraksi dan polimorfisme parametrik" (1983).

Sepertinya semua ide ini tidak ada hubungannya dengan tipe, tetapi mereka benar-benar melakukannya. Bahasa Stateful dan model telah built-in abstraksi data. Anda tidak perlu mendefinisikan "tipe data abstrak" untuk menyembunyikan informasi. Anda cukup mendeklarasikan variabel lokal dan menyembunyikannya. Kita bisa mengajarkannya kepada siswa tahun pertama di kelas-kelas Jawa dalam beberapa minggu pertama. Tanpa keringat.

Bahasa dan model fungsional, di sisi lain, harus menyembunyikan informasinya melalui tipe . Model fungsional tidak memiliki abstraksi data bawaan. Kita harus menambahkannya secara eksplisit, menggunakan atau . Jadi, jika Anda menerjemahkan bahasa stateful ke bahasa fungsional, Anda akan melihat semua keadaan lokal diterjemahkan ke dalam variabel tipe. Untuk deskripsi eksplisit tentang cara kerjanya, lihat makalah saya " Objek dan kelas dalam bahasa seperti Algol ", tetapi ide-ide itu benar-benar berasal dari Reynolds 1981 ("The Essence of Algol"). Kami hanya memahami ide-ide klasik yang lebih baik sekarang.$\forall$$\exists$

Ambil dua mesin dan yang ingin Anda buktikan setara. Milner 1971 mengatakan, mendefinisikan hubungan antara keadaan dan dan menunjukkan bahwa kedua mesin mempertahankan hubungan. Reynolds parametricity mengatakan, anggap keadaan mesin sebagai milik tipe dan . Tentukan hubungan antara mereka. Jika mesin-mesin dari tipe dan , parameter oleh jenis negara mereka, kemudian periksa bahwa dua mesin terkait oleh hubungan . M ′ M M ′ X X ′ R F ( X ) F ( X ′ ) F ( R $M$$M'$$M$$M'$$X$$X'$$R$$F(X)$$F(X')$$F(R)$

Jadi, simulasi dan parametrisitas relasional pada dasarnya adalah ide yang sama . Ini bukan hanya kemiripan yang dangkal. Yang pertama dibuat untuk bahasa stateful di mana ada abstraksi data bawaan. Yang terakhir dibuat untuk bahasa stateless di mana abstraksi data diperoleh melalui variabel tipe.

Lalu bagaimana dengan hubungan logis? Di permukaan, hubungan logis tampaknya menjadi ide yang lebih umum. Sedangkan parametrikitas berbicara tentang bagaimana menghubungkan variabel tipe dalam model yang sama, hubungan logis tampaknya menghubungkan tipe di berbagai model. (Dave Clarke menulis eksposisi yang brilian tentang ini sebelumnya.) Tetapi perasaan saya (dan masih perlu diperagakan) bahwa ini adalah contoh dari beberapa bentuk parametrikitas tipe yang lebih tinggi yang belum dirumuskan. Tetap disini untuk kemajuan lebih lanjut di bagian depan itu.

[Catatan ditambahkan] Koneksi antara hubungan logis dan simulasi dibahas dalam makalah kami baru-baru ini Hubungan logis dan parametrik: Program Reynolds untuk Teori Kategori dan Bahasa Pemrograman .

Salah satu perbedaan utama adalah bahwa hubungan logis digunakan sebagai teknik untuk menunjukkan bahwa kelas program (misalnya, input ke kompiler) sesuai dengan kelas program lain (misalnya, output dari kompiler), sedangkan hubungan simulasi digunakan untuk menunjukkan korespondensi antara dua program.

Kesamaan antara dua gagasan adalah bahwa keduanya mendefinisikan hubungan yang digunakan untuk menunjukkan korespondensi antara dua entitas yang berbeda. Dalam beberapa hal, orang dapat menganggap relasi logis sebagai relasi simulasi yang didefinisikan secara induktif pada sintaks tipe. Tetapi berbagai jenis hubungan simulasi ada.

Hubungan logis dapat digunakan untuk menunjukkan korespondensi antara bahasa seperti ML dan terjemahannya ke dalam bahasa assembly, seperti dalam makalah yang Anda baca. Relasi logis didefinisikan secara induktif pada struktur tipe. Relasi logis menyediakan sarana komposisional untuk menunjukkan, misalnya, bahwa terjemahan benar, dengan menunjukkan bahwa terjemahan itu benar untuk setiap konstruktor tipe. Pada tipe fungsi kondisi kondisi kebenaran akan mengatakan sesuatu seperti, terjemahan fungsi ini mengambil input yang diterjemahkan dengan baik ke output yang diterjemahkan dengan baik.

Hubungan logis adalah teknik serbaguna untuk bahasa berdasarkan kalkulus lambda. Aplikasi lain dari hubungan logis termasuk (dari sini ): mengkarakterisasi kemampuan lambda, menghubungkan definisi semantik denotasional, mengkarakterisasi polimorfisme parametrik, memodelkan interpretasi abstrak, memverifikasi representasi data, mendefinisikan semantik abstrak sepenuhnya dan memodelkan keadaan lokal dalam bahasa tingkat tinggi.

Hubungan simulasi umumnya digunakan untuk menunjukkan kesetaraan dua program. Biasanya program semacam itu menghasilkan semacam pengamatan, seperti mengirim pesan di saluran. Satu program P mensimulasikan Q lain jika P dapat melakukan semua yang dapat dilakukan Q, meskipun mungkin lebih.

Bisimulasi, secara kasar, adalah dua hubungan simulasi yang disatukan. Anda menunjukkan bahwa program P dan mensimulasikan program Q dan program Q dapat mensimulasikan program P dan Anda memiliki bisimulasi, meskipun kondisi tambahan umumnya ada. Entri Wikipedia tentang bisimulasi adalah titik awal yang baik (lebih tepat). Ada ribuan varian gagasan, tetapi ini adalah gagasan mendasar yang telah diciptakan kembali dalam kurang lebih bentuk ilmu komputer, logika modal, dan teori model yang sama. Artikel Sangiorgi memberikan sejarah ide yang indah.

Satu makalah yang membangun hubungan antara dua gagasan adalah Catatan tentang Hubungan Logika Antara Semantik dan Sintaksis oleh Andy Pitts yang menggunakan hubungan logis, akhirnya gagasan semantik yang didefinisikan secara sintaksis, untuk membuktikan sifat tertentu tentang bisimulasi aplikatif , yang merupakan gagasan sintaksis murni.

Dua jenis hubungan tampaknya digunakan dalam konteks yang berbeda. Simulasi logis untuk bahasa yang diketik dan hubungan simulasi ketika berhadapan dengan proses kalkulus atau modal logika ditafsirkan melalui sistem transisi. Dave Clarke telah memberikan banyak penjelasan intuitif, jadi saya hanya akan menambahkan beberapa petunjuk yang dapat membantu.

Telah ada upaya untuk mengkarakterisasi kedua konsep menggunakan interpretasi abstrak. Mungkin bukan yang Anda inginkan, tetapi setidaknya kedua gagasan diperlakukan dalam kerangka matematika yang sama.

Samson Abramsky menggunakan hubungan logis untuk membuktikan kesehatan dan penghentian analisis ketelitian untuk kalkulus Lambda malas ( Abstrak Interpretasi, Hubungan Logis, dan Ekstensi Kan ). Dia juga menunjukkan bahwa hubungan logis mendefinisikan fungsi abstraksi dalam pengertian koneksi Galois dari interpretasi abstrak. Baru-baru ini, Backhouse dan Backhouse menunjukkan bagaimana membangun koneksi Galois untuk tipe orde tinggi dari koneksi Galois untuk tipe dasar dan bahwa konstruksi ini dapat dijelaskan secara setara menggunakan hubungan logis ( Logical Relations dan Galois Connections ). Dengan demikian, dalam konteks spesifik bahasa fungsional yang diketik, kedua gagasan itu setara.

Hubungan simulasi menandai pelestarian properti antara struktur Kripke untuk berbagai modal dan logika temporal. Alih-alih tipe, kami memiliki modalitas dalam logika. Hubungan simulasi juga mendefinisikan koneksi Galois dan karenanya, abstraksi. Orang dapat bertanya apakah abstraksi ini memiliki sifat khusus. Jawabannya adalah bahwa abstraksi standar adalah suara dan abstraksi berbasis hubungan simulasi selesai. Gagasan kelengkapan adalah sehubungan dengan koneksi Galois, yang mungkin tidak sependapat dengan interpretasi yang intuitif. Lini pekerjaan ini telah dikembangkan oleh David Schmidt ( Hubungan Biner Struktur-Melestarikan untuk Abstraksi Program ), dan Francesco Ranzato dan Francesco Tapparo ( Pelestarian Kuat Umum dengan Interpretasi Abstrak ).

Saya akan mengatakan bahwa kedua konsep ini agak kabur. Keduanya tentang hubungan biner dari mekanisme komputasi yang entah bagaimana mewujudkan gagasan kesetaraan. Relasi logis didefinisikan oleh induksi tipe-struktur, sementara simulasi dapat didefinisikan sesuka Anda, tetapi istilah ini merujuk pada koinduksi.

$\pi$