Embeddings Dangkal versus Deep

Saat menyandikan logika menjadi asisten bukti seperti Coq atau Isabelle, pilihan perlu dibuat antara menggunakan dangkal dan penyisipan dalam . Dalam formula logis embedding dangkal ditulis langsung dalam logika prover teorema, sedangkan dalam formula logis embedding mendalam direpresentasikan sebagai tipe data.

• Apa kelebihan dan keterbatasan berbagai pendekatan?
• Apakah ada pedoman yang tersedia untuk menentukan mana yang akan digunakan?
• Apakah mungkin untuk beralih di antara dua representasi dengan cara sistematis?

Sebagai motivasi, saya ingin menyandikan berbagai logika terkait keamanan ke dalam Coq dan saya bertanya-tanya apa pro dan kontra dari berbagai pendekatan tersebut.

Apa kelebihan dan keterbatasan berbagai pendekatan?

• Kelebihan embeddings yang dalam: Anda dapat membuktikan dan mendefinisikan sesuatu dengan induksi pada struktur formula. Contoh minat adalah ukuran formula.

• Kekurangan embeddings mendalam: Anda harus berurusan secara eksplisit dengan pengikatan variabel. Itu biasanya sangat melelahkan.

Apakah ada pedoman yang tersedia untuk menentukan mana yang akan digunakan?

Embeddings dangkal sangat berguna untuk mengimpor hasil yang dibuktikan dalam logika objek. Misalnya, jika Anda telah membuktikan sesuatu dalam logika kecil (misal logika pemisahan) dangkal embeddings dapat menjadi alat pilihan untuk mengimpor hasil Anda dalam Coq.

Di sisi lain, deep embedding hampir wajib ketika Anda ingin membuktikan meta-teorema tentang logika objek (seperti misalnya cut-elimination).

Apakah mungkin untuk beralih di antara dua representasi dengan cara sistematis?

Gagasan di balik embedding dangkal adalah benar-benar bekerja secara langsung dalam model rumus objek. Biasanya orang akan memetakan rumus objek P secara langsung (menggunakan notasi atau dengan melakukan terjemahan dengan tangan) ke penghuni Prop. Tentu saja, ada penghuni Prop yang tidak dapat diperoleh dengan menyematkan rumus logika objek. Karena itu Anda kehilangan semacam kelengkapan.

Jadi dimungkinkan untuk mengirim setiap hasil yang diperoleh dalam pengaturan embedding yang mendalam melalui fungsi interpretasi.

Berikut adalah sedikit contoh coq:

Formula induktif: Set: =
    Ftrue: formula
  | Salah: rumus
  | Fand: formula -> formula -> formula
  | Untuk: formula -> formula -> formula.

Interpretasi fixpoint (F: formula): Prop: = cocok F dengan 
    Ftrue => Benar
  | Salah => Salah
  | Fand ab => (interpretasikan a) / \ (interpretasikan b)
  | Untuk ab => (interpretasikan a) \ / (interpretasikan b)
 akhir.

Derivatif induktif: rumus -> Prop: = 
    deep_axiom: Ftrue yang dapat diturunkan
  | deep_and: forall ab, derivable a -> derivable b -> derivable (Fand ab)
  | deep_or1: forall ab, derivable a -> derivable (For ab)
  | deep_or2: forall ab, derivable b -> derivable (For ab).

Dapat digunakan secara induktif: Prop -> Prop: = 
    shallow_axiom: sderivable True 
  | shallow_and: forall ab, sderivable a -> sderivable b -> sderivable (a / \ b)
  | shallow_or1: forall ab, sderivable a -> sderivable (a \ / b)
  | shallow_or2: forall ab, sderivable b -> sderivable (a \ / b).

(* Anda dapat membuktikan lemma berikut: *)
Lemma shallow_deep: 
   forall F, derivable F -> sderivable (interpretasikan F).

(* Anda TIDAK bisa membuktikan lemma berikut: *)
Akan t: 
   forall P, sderivable P -> ada F, tafsirkan F = P.

Secara kasar, dengan penyematan logika yang mendalam, Anda (1) mendefinisikan tipe data yang mewakili sintaks untuk logika Anda, dan (2) memberikan model sintaksis , dan (3) membuktikan bahwa aksioma tentang sintaks Anda adalah suara dengan hormat ke model. Dengan penyematan dangkal, Anda melewati langkah (1) dan (2), dan mulai saja dengan model, dan buktikan keterkaitan di antara rumus. Ini berarti embeddings yang dangkal biasanya lebih sulit untuk diselesaikan, karena mereka merepresentasikan pekerjaan yang biasanya Anda lakukan dengan embedding yang dalam.

Namun, jika memiliki embedding yang dalam, biasanya lebih mudah untuk menulis prosedur keputusan reflektif, karena Anda bekerja dengan formula yang sebenarnya memiliki sintaks yang dapat Anda ulangi. Juga, jika model Anda aneh atau rumit, maka Anda biasanya tidak ingin bekerja secara langsung dengan semantik. (Misalnya, jika Anda menggunakan biorthogonality untuk memaksakan penutupan yang diizinkan, atau menggunakan model gaya Kripke untuk memaksa properti bingkai dalam logika pemisahan, atau game serupa.) Namun, embedding yang dalam hampir pasti akan memaksa Anda untuk berpikir banyak tentang pengikatan dan penggantian variabel , yang akan mengisi hatimu dengan amarah, karena ini (a) sepele, dan (b) sumber kekesalan yang tidak pernah berakhir.

Urutan yang benar yang harus Anda ambil adalah: (1) mencoba bertahan dengan penanaman dangkal. (2) Ketika itu kehabisan tenaga, coba gunakan taktik dan kutipan untuk menjalankan prosedur keputusan yang ingin Anda jalankan. (3) Jika itu juga kehabisan tenaga, menyerah dan gunakan sintaks yang diketik secara dependen untuk penanaman dalam Anda.

• Rencanakan untuk mengambil beberapa bulan pada (3) jika ini adalah pertama kalinya Anda keluar. Anda akan perlu untuk mendapatkan akrab dengan mewah fitur asisten bukti untuk tinggal waras. (Tapi ini adalah investasi yang akan terbayar secara umum.)
• Jika asisten bukti Anda tidak memiliki tipe dependen, tetap di level 2.
• Jika bahasa objek Anda diketik secara dependen, tetap di level 2.

Juga, jangan mencoba naik secara bertahap. Ketika Anda memutuskan untuk naik tangga kompleksitas, ambil langkah penuh pada satu waktu. Jika Anda melakukan hal-hal sedikit demi sedikit, maka Anda akan mendapatkan banyak teorema yang aneh dan tidak dapat digunakan (misalnya, Anda akan mendapatkan beberapa sintaks setengah-berpasangan, dan teorema yang mencampur sintaksis dan semantik dengan cara yang aneh), yang akan Anda dapatkan akhirnya harus membuang.

EDIT: Berikut ini komentar yang menjelaskan mengapa naik tangga secara bertahap begitu menggoda, dan mengapa itu mengarah (secara umum) ke penderitaan.

$A \star B$$I$$A \star B \iff B \star A$$(A \star B) \star C \iff A \star (B \star C)$$(I \star A) \star (B \star C)$$A \star (B \star (C \star I))$

$\star$

Ini benar, dan berhasil! Namun, perhatikan bahwa kata hubung juga ACUI, dan demikian juga disjungsi. Jadi Anda akan melalui proses yang sama dalam bukti lain, dengan tipe data daftar yang berbeda, dan kemudian Anda akan memiliki tiga sintaks untuk fragmen logika pemisahan yang berbeda, dan Anda akan memiliki metatheorem untuk masing-masingnya, yang pasti akan berbeda, dan Anda akan mendapati diri Anda menginginkan metatheorem yang Anda buktikan karena memisahkan konjungsi untuk disjungsi, dan kemudian Anda akan ingin mencampur sintaksis, dan kemudian Anda akan menjadi gila.

Lebih baik menargetkan fragmen terbesar yang bisa Anda tangani dengan upaya yang masuk akal, dan lakukan saja.

Penting untuk dipahami bahwa ada spektrum dari dalam hingga dangkal. Anda memodelkan bagian-bagian bahasa Anda secara mendalam yang entah bagaimana harus berpartisipasi dalam beberapa argumen induktif tentang pembuatannya, sisanya lebih baik dibiarkan dalam pandangan dangkal semantik langsung dari substrat logika.

Misalnya, ketika Anda ingin memberi alasan tentang Hoare Logic, Anda bisa memodelkan bahasa ekspresi dengan cara yang dangkal, tetapi garis besar bahasa assign-if-While harus berupa tipe data konkret. Anda tidak perlu memasukkan struktur x + y atau a <b, tetapi Anda harus bekerja dengan whiledll.

Di jawaban lain ada sindiran untuk tipe dependen. Ini mengingatkan pada masalah kuno untuk merepresentasikan bahasa dengan binder dengan cara yang waras, sedemikian rupa sehingga mereka sedangkal mungkin, tetapi masih mengakui beberapa argumen induktif. Kesan saya adalah bahwa juri masih keluar menilai semua pendekatan dan makalah yang berbeda yang telah muncul dalam 10-20 tahun terakhir tentang masalah itu. "Tantangan POPLmark" untuk komunitas asisten pembuktian yang berbeda juga sampai batas tertentu.

Anehnya, dalam HOL klasik tanpa tipe dependen, pendekatan HOL-Nominal oleh C. Urban bekerja dengan baik untuk penjilidan dangkal, meskipun tidak mengikuti perubahan budaya dalam komunitas formalisasi bahasa pemrograman ini.