Kesetaraan analisis aliran data, interpretasi abstrak dan inferensi tipe?

@ Babou menjawab pertanyaan terakhir mengingatkan saya bahwa pada suatu waktu saya pikir saya membaca makalah tentang kesetaraan (dalam hal kedua fakta yang dapat disimpulkan atau dibuktikan dan kompleksitas waktu menjalankan algoritma inferensi) dari analisis aliran data , interpretasi abstrak , dan tipe inferensi .

Dalam beberapa sub-kasus (seperti antara analisis aliran data interprocedural sensitif konteks maju dan interpretasi abstrak) kesetaraan relatif jelas bagi saya, tetapi pertanyaannya tampaknya lebih halus untuk perbandingan lainnya. Sebagai contoh, saya tidak tahu bagaimana inferensi tipe Hindley-Milner dapat digunakan untuk membuktikan beberapa properti yang dapat dibuktikan dengan analisis aliran data sensitif aliran.

Apa referensi seminal membahas kesetaraan (atau perbedaan) antara analisis aliran data, interpretasi abstrak dan inferensi tipe?

Analisis aliran data dan inferensi tipe adalah contoh spesifik dari interpretasi abstrak.

Analisis aliran data dan interpretasi abstrak terlihat serupa karena keduanya tentang menghitung titik perbaikan. Analisis aliran data biasanya memiliki domain abstrak hingga tinggi yang memastikan penghentian. Secara umum, interpretasi abstrak tidak mengasumsikan domain abstrak tersebut; untuk menangani domain tinggi infinite, interpretasi abstrak menggunakan teknik pelebaran dan penyempitan.

Ternyata inferensi tipe juga tentang perhitungan fix-point, meskipun itu jauh dari jelas, imo. Berikut adalah makalah yang secara eksplisit menunjukkan bahwa jenis adalah interpretasi abstrak: kertas . Pada dasarnya, jenis dipandang sebagai abstraksi semantik konkret program. Dalam sistem tipe Hindley-Milner, misalnya, domain abstrak dari tipe memiliki ketinggian tak hingga dan menghitung tipe (paling umum) menggunakan unifikasi pada dasarnya melakukan operasi pelebaran (sangat tidak tepat).

Tempat yang baik untuk belajar tentang tiga pendekatan ini dan bagaimana hubungannya adalah buku Principles of Program Analysis oleh Nielson, Nielson dan Hankin.

Saya tidak berpikir itu benar untuk mengatakan bahwa analisis aliran data, interpretasi abstrak dan inferensi tipe adalah hal yang sama. Meskipun ada banyak kesamaan, dan mungkin lebih dari yang diharapkan, mengingat ketiganya berasal dari komunitas yang berbeda, ada juga banyak perbedaan.

Saya menganggap mereka pada dasarnya sama. Mereka awalnya memiliki tujuan yang berbeda dan diciptakan oleh faksi ilmu komputer yang berbeda.

Analisis aliran data berasal dari faksi teknik kompiler, mencoba untuk berbicara tentang algoritma pengoptimalan mereka dan membuktikan batas atas pada kompleksitas mereka dll.

Interpretasi abstrak berasal dari formal, bidang matematika dari ilmu komputer. Ini adalah versi yang bahkan lebih formal dengan lebih tertarik pada kebenaran dan kurang membangun kompiler nyata.

Jenis inferensi berasal dari bidang akademik pemrograman fungsional di mana ia awalnya merupakan alat untuk melakukan hal-hal keren dengan kompiler. Kemudian muncul ide, bahwa suatu tipe bisa lebih dari sekadar "int" atau "float" tetapi juga hal-hal lain seperti dalam analisis aliran data klasik.