Bisakah Anda menjelaskan intuisi di balik Ruang Koheren?

Linear Logic diinterpretasikan menggunakan spasi yang koheren , dan fitur-fitur tersebut menonjol dalam makalah Girard. Saya tahu semua tiga cara utama untuk mendefinisikan mereka secara formal, dan mereka tidak benar-benar menimbulkan masalah untuk digunakan dan membuktikan hal-hal tentang, tetapi saya tidak bisa mengerti apa artinya .

Rasanya benar-benar ada semacam cara untuk memahaminya . Pertama-tama, ada beberapa contoh tentang mereka yang menggunakan fungsi pada boolean (seperti di wiki di suatu tempat ). Dan itu mengisyaratkan sesuatu yang menarik dan bermakna di balik definisi formal. Namun, booladalah ruang koheren yang sangat sederhana, tanpa klik ukuran > 1. Bisakah seseorang menjelaskan?

Hal lain yang Girard katakan di suatu tempat bahwa setiap titik ruang yang koheren mewakili "urutan pertanyaan / jawaban" yang spesifik, dengan dua poin menjadi koheren jika mereka "membagi dua secara negatif (yaitu, pada pertanyaan yang berbeda)", dan tidak koheren jika mereka membagi dua jawaban yang berbeda [1]. Sepertinya ide yang mudah dipahami tetapi saya tidak bisa menciptakan contoh sehingga itu berarti saya tidak benar-benar mengerti ...

Bisakah seseorang tolong saya dengan itu?

[1] JY Girard, Hantu transparansi . URL: http://iml.univ-mrs.fr/~girard/longo1.pdf

Intuisi di balik ruang koherensi adalah bahwa elemen ruang koherensi mewakili pengamatan beberapa data yang mendasarinya, dan relasi koherensi memberi tahu Anda apakah dua pengamatan bisa berasal dari bagian data yang sama.

Konkretnya, misalkan kita memiliki seperangkat hewan

Animals = {cat, duck, fish}

Sekarang, kita dapat memiliki satu set pengamatan:

Observations = {warm-blooded, swims, water-breathing, furry}

Mari kita katakan bahwa dua pengamatan cocok jika keduanya bisa dibuat dari hewan yang sama. Setiap pengamatan kompatibel dengan dirinya sendiri, dan sebagai tambahan:

• $\stackrel{{\large\frown}}{{\small\smile}}$
• berdarah panas$\stackrel{{\large\frown}}{{\small\smile}}$
• $\stackrel{{\large\frown}}{{\small\smile}}$
• $\stackrel{{\large\frown}}{{\small\smile}}$

Kita tahu bahwa berdarah panas cocok dengan berenang, karena bebek sama-sama berdarah panas dan berenang. Tetapi berdarah panas dan bernafas air tidak cocok, karena kita tidak memiliki hewan yang berdarah panas dan bernafas air.

Observations$\stackrel{{\large\frown}}{{\small\smile}}$Observations$\stackrel{{\large\frown}}{{\small\smile}}$

Saya selalu kesulitan membentuk intuisi untuk ruang koherensi, sampai saya menjadi lebih akrab dengan teori domain dan membaca "Sistem F dari tipe variabel, lima belas tahun kemudian" dari Girard. Ruang koherensi hanyalah jenis domain khusus, dan saya merasa jauh lebih mudah untuk memahami apa arti koherensi dimulai dari sana. Saya akan mencoba memberikan penjelasan yang lebih masuk akal bagi saya.

Bayangkan Anda ingin mempelajari program-program yang mengambil input integer ke output integer. Secara umum, program-program ini dapat diulang selamanya, jadi masuk akal untuk memodelkannya secara matematis sebagai fungsi parsial dari bilangan bulat ke bilangan bulat: jika program tersebut berulang, fungsi parsial yang terkait tidak ditentukan pada input tersebut. Kita dapat melihat fungsi parsial fseperti itu sebagai grafik : satu set pasangan bilangan bulat (n, m)sehingga fdidefinisikan ndan sama dengan m. Ini memungkinkan kami untuk mewakili fungsi-fungsi ini sebagai ruang koherensi:

• Web ruang koherensi adalah himpunan pasangan bilangan bulat (n, m).
• Dua pasangan (n, m)dan (n', m')koheren jika dan hanya jika ndan n'berbeda, atau mdan m'sama.

Dengan membongkar definisi, kita melihat bahwa setiap klik dari ruang koherensi ini adalah grafik dari fungsi parsial, dan sebaliknya. Kita dapat menafsirkan hubungan koherensi dengan mengatakan bahwa, satu fungsi parsial didefinisikan pada input, hanya menghasilkan satu hasil untuk input itu. Jika Anda terbiasa dengan semantik teori-domain lainnya, dimasukkannya klik-klik sesuai dengan urutan Scott pada fungsi parsial pada bilangan bulat.