Apakah mungkin untuk menghitung apakah dua fungsi sama ekstensional?

9

Jika Anda memiliki dua fungsi yang menerapkan algoritma penyortiran yang berbeda, apakah mungkin menyimpulkan dengan kode sumber bahwa keduanya memiliki properti eksternal yang sama? Berarti mereka berdua akan memiliki urutan yang mungkin tidak disortir sebagai input dan memiliki urutan yang diurutkan sebagai output? Dengan cara apa properti eksternal ini dapat ditentukan oleh kode sumber? Dan bagaimana Anda menggambarkan properti eksternal ini? Notasi apa yang akan digunakan?

Properti eksternal dapat diketahui dengan mendefinisikannya secara eksplisit, misalnya dalam sistem tipe, tetapi saya bertanya-tanya apakah ini dapat dilakukan secara implisit. Atau apakah secara teoretis tidak mungkin menyimpulkan semantik semacam ini? Saya tertarik pada apakah ini mungkin untuk fungsi sewenang-wenang, bukan hanya untuk menyortir algoritma, dengan asumsi hal-hal seperti fungsi akan selalu berhenti dan tidak memiliki efek samping.

Haruskah saya melihat semantik denotasional, atau tidak terkait?

Saya tertarik pada petunjuk untuk meneliti bidang ini dan istilah-istilah berbeda yang digunakan untuk menggambarkan subjek yang mungkin membantu pencarian literatur saya.

pl.programming-languages decidability formal-methods extensionality Matthijs Steen
sumber

Jawaban:

8

Iya. Jika Anda dapat memverifikasi bahwa mereka sama, maka komputer juga dapat sama.

Berikut adalah spesifikasi cepat untuk jenis integer di Coq:

Inductive natlist : Type :=
| nil : natlist
| cons : nat → natlist → natlist.

Fixpoint is_sorted (l : natlist ) : bool :=
    match l with
    |  nil => true
    |  (cons x nil) => true
    |  (cons x (cons y r)) => if x <= y then is_sorted (cons y r) else false
    end.

...

Theorem sort_spec : forall l, is_sorted (sort_list l).

Spesifikasi dapat langsung disandikan ke dalam deklarasi sortir menggunakan tipe dependen.

Untuk masalah khusus ini, John Darlington menunjukkan di tahun 70-an bahwa 6 keluarga algoritma penyortiran dapat diturunkan dengan secara mekanis mengubah spesifikasi semacam menjadi implementasi; Saya percaya ini berjalan di bawah nama "derivasi program berbasis semantik."

Dalam dunia rekayasa perangkat lunak, menemukan fungsi yang setara secara ekstensi dikenal sebagai "deteksi kloning semantik."

Dave Clarke juga memberikan jawaban yang bagus untuk pertanyaan ini di CS StackExchange: /cs/2059/how-do-you-check-if-two-algorithms-return-the-same-result -untuk-input apa saja

Ini semua berada di bawah payung metode formal dan bahasa pemrograman . Semantik denotasional adalah satu kelas teknik untuk pemodelan semantik, tetapi mereka tidak disukai karena sulit digunakan dibandingkan dengan semantik operasional.

James Koppel
sumber
Terima kasih atas jawabannya! Ini persis apa yang saya cari.
Matthijs Steen
4
Saya sangat tidak setuju dengan pernyataan bahwa semantik denotasional telah "tidak disukai". Itu sangat tergantung pada siapa Anda bertanya.
Andrej Bauer
5

Kesetaraan ekstensional dalam bahasa pemrograman lengkap Turing tidak dapat diputuskan secara umum, tetapi itu tidak akan menghentikan Anda untuk dapat memverifikasi atau memalsukan bahwa dua fungsi spesifik mana pun secara ekstensi sama.

f=g⇔∀xα.f(x)=g(x)fgα→β

Martin Berger
sumber
Terima kasih atas jawabannya. Saya akan melihat ke logika Hoare. Apakah semantik denotasional sulit untuk didefinisikan dibandingkan dengan logika Hoare, atau hanya kurang cocok untuk sebagian besar bahasa? Apakah kesetaraan ekstensional tidak dapat diputuskan secara umum karena Masalah yang Terputus? Lalu jika fungsi selalu berhenti, seperti dalam bahasa fungsional total, bukankah itu akan dianggap umum? Atau adakah alasan lain untuk tidak dapat diputuskan secara umum?
Matthijs Steen
P0
... memiliki kesetaraan kontekstual yang dapat ditentukan. Tetapi perhatikan bahwa R. Loader menunjukkan bahwa PCF finansial sekalipun memiliki kesetaraan kontekstual yang tidak dapat ditentukan.
Martin Berger
-2

Sebuah jawaban cepat (saya akui saya tidak menghabiskan banyak waktu ...) Teorema Rice mengatakan bahwa untuk pertanyaan yang tidak sepele, tidak dapat dipungkiri untuk mengatakan apakah fungsi yang dihitung oleh suatu program akan memiliki properti atau tidak. Karena itu pertanyaan di sini tidak dapat dipastikan

pria biasa
sumber
1
Apakah itu tidak menyatakan bahwa "... untuk properti non-sepele dari fungsi parsial ...", jadi apakah itu tidak dapat dianggap sebagai decidable untuk fungsi total?
Matthijs Steen