Bukti penggunaan asisten dalam penelitian teori kompleksitas?

14

Mempertimbangkan topik yang dibahas dalam konferensi seperti STOC, apakah ada algoritma atau kompleksitas peneliti aktif menggunakan COQ atau Isabelle? Jika demikian, bagaimana mereka menggunakannya dalam penelitian mereka? Saya berasumsi kebanyakan orang tidak akan menggunakan alat seperti itu karena buktinya terlalu rendah. Adakah yang menggunakan asisten bukti ini dengan cara yang sangat penting untuk penelitian mereka, sebagai lawan suplemen yang bagus?

Saya tertarik karena saya mungkin mulai mempelajari salah satu alat itu dan akan menyenangkan untuk belajar tentang mereka dalam konteks bukti pengurangan, kebenaran, atau waktu berjalan.

cc.complexity-theory approximation-algorithms soft-question proof-assistants nish2575
sumber
1
Apakah Anda ingin mengecualikan "Teori B" dan khususnya teori bahasa pemrograman? Pemahaman saya adalah bahwa asisten bukti lebih sering digunakan di PL ...
Joshua Grochow
1
Saya mencari istilah itu, saya kira saya fokus pada aplikasi dalam "Theory A"
nish2575
1
Sejauh yang saya ketahui, sebagian besar Teori A berada dalam kategori yang sama dengan sebagian besar matematika lainnya: beberapa fondasi telah ditambahkan sejauh ini ke sistem ini, sehingga teorema yang paling menarik akan mengambil upaya signifikan untuk pertama mengembangkan infrastruktur untuk mengimplementasikan definisi yang diperlukan. Ada beberapa bagian menarik dari teori automata yang telah diformalkan, sehingga dapat menjadi tempat untuk mencari.
András Salamon
1
Hasil dalam teori kompleksitas cenderung terbukti dalam sistem yang jauh lebih lemah, Anda biasanya bahkan tidak memerlukan PA. Coq dan Isabeller tidak terlalu cocok untuk teori kompleksitas yang akan saya katakan. Ada sketsa bukti yang hampir formal seperti yang ada di buku Cook dan Nguyen tetapi minat utama adalah membuktikannya dalam sistem bukti yang berkaitan dengan kelas kompleksitas. Mengapa seseorang ingin membuktikannya dengan mengatakan Switching Lemma dalam Coq ketika itu dapat dibuktikan dalam sistem yang jauh lebih lemah?
Kaveh
2
@Kaveh Kelemahan / kekuatan dari berbagai sistem bukti bukanlah masalah di sana: kami ingin secara resmi memverifikasi bukti dalam teori kompleksitas untuk alasan yang sama kami ingin memverifikasi program: memiliki tingkat keandalan yang lebih tinggi. Selain itu, ini juga merupakan tantangan yang menarik untuk memperluas teori yang tepat sehingga mereka dapat menangani bukti teori kompleksitas dengan lebih mudah.
Martin Berger

Jawaban:

15

Aturan umum adalah bahwa semakin abstrak / eksotis matematika yang ingin Anda mekanisasi, semakin mudah didapat. Sebaliknya, semakin konkret / familiar matematika, semakin sulit. Jadi (misalnya) hewan langka seperti topologi titik bebas predikatif jauh lebih mudah untuk dimekanisasi daripada topologi metrik biasa.

Ini mungkin awalnya tampak sedikit mengejutkan, tetapi ini pada dasarnya karena benda konkret seperti bilangan real berpartisipasi dalam berbagai macam struktur aljabar, dan bukti yang melibatkannya dapat memanfaatkan properti apa pun dari sudut pandang mana pun. Jadi untuk dapat menggunakan alasan biasa yang biasa digunakan oleh ahli matematika, Anda harus memekanisasi semua hal ini. Sebaliknya, konstruksi yang sangat abstrak memiliki properti yang kecil dan terbatas (sengaja), jadi Anda harus lebih sedikit mekanisasinya sebelum Anda bisa mendapatkan bagian yang baik.

Bukti dalam kompleksitas-teori dan algoritma / struktur data cenderung (sebagai aturan) menggunakan properti canggih dari gadget sederhana seperti angka, pohon, atau daftar. Misalnya, argumen kombinatorial, probabilistik, dan bilangan teoretis secara rutin muncul pada saat bersamaan di dalam teorema dalam teori kompleksitas. Mendapatkan dukungan perpustakaan asisten bukti ke titik di mana hal ini baik dilakukan cukup banyak pekerjaan!

Satu konteks di mana orang bersedia untuk dimasukkan ke dalam pekerjaan adalah dalam algoritma kriptografi. Ada kendala algoritmik yang sangat halus di tempat untuk alasan matematika yang kompleks, dan karena kode crypto berjalan dalam lingkungan permusuhan, bahkan kesalahan sekecil apa pun dapat menjadi bencana. Jadi misalnya, proyek Certicrypt telah membangun banyak infrastruktur verifikasi untuk tujuan membangun bukti yang diperiksa mesin dari kebenaran algoritma kriptografi.

Neel Krishnaswami
sumber
6

Salah satu contoh yang sangat menonjol tentu saja formalisasi Gonthiers Coq dari teorema 4 warna dalam Coq yang menggunakan banyak kombinatorik.

Rekan saya Uli Schöpp menggunakan perpustakaan ssreflect yang dikembangkan oleh Gonthier untuk tujuan ini untuk memverifikasi (dan sedikit memperluas) juga dalam Coq hasil oleh Cook dan Rackoff pada grafik automata. https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de (Schöpp, U. (2008). Batas bawah yang diformalkan pada tingkat keterjangkauan yang tidak terarah. Dalam Logika untuk Pemrograman, Kecerdasan Buatan, dan Penalaran ( hlm. 621-635). Springer Berlin / Heidelberg.)

Martin Hofmann
sumber