Ketik sistem berdasarkan teori himpunan naif

Seperti yang saya mengerti, dalam ilmu komputer tipe data tidak didasarkan pada teori himpunan karena hal-hal seperti paradoks Russell, tetapi seperti dalam bahasa pemrograman dunia nyata kita tidak dapat mengekspresikan tipe data yang kompleks seperti "set yang tidak mengandung dirinya sendiri", dapatkah kita katakanlah bahwa dalam tipe praktik adalah himpunan tak terbatas dari anggotanya di mana keanggotaan instan ditentukan oleh sejumlah fitur yang intrinsik dengan tipe / himpunan ini (keberadaan properti, metode)? Jika tidak, apa yang akan menjadi contoh tandingan?

type-theory set-theory type-systems Nutel
sumber

Paradoks Russell tidak ada hubungannya dengan hal itu secara langsung.

Andrej Bauer

Jawaban:

Alasan utama untuk menghindari set dalam semantik jenis adalah bahwa bahasa pemrograman yang khas memungkinkan kita untuk mendefinisikan fungsi rekursif sewenang-wenang. Oleh karena itu, apa pun arti suatu tipe, ia harus memiliki properti titik tetap. Satu-satunya set dengan properti seperti itu adalah set singleton.

Untuk lebih tepatnya, nilai yang didefinisikan secara rekursif dari tipe (di mana biasanya adalah tipe fungsi) didefinisikan oleh persamaan titik tetap mana dapat menjadi program apa pun. Jika diartikan sebagai himpunan maka kita akan mengharapkan setiap memiliki titik tetap. Tetapi satu-satunya set dengan properti ini adalah singleton. $v$ $\tau$ $\tau$ $v = \Phi(v)$ $\Phi : \tau \to \tau$ $\tau$ $T$ $f : T \to T$ $T$

Tentu saja, Anda juga bisa menyadari bahwa pelakunya adalah logika klasik. Jika Anda bekerja dengan teori himpunan intuitionistic, maka konsisten untuk mengasumsikan bahwa ada banyak set dengan properti titik tetap. Bahkan, ini telah digunakan untuk memberikan semantik bahasa pemrograman, lihat misalnya

Alex Simpson, Kecukupan Komputasi untuk Jenis Rekursif dalam Model Teori Set Intuitionistic , Dalam Sejarah Logika Murni dan Terapan, 130: 207-275, 2004.

Andrej Bauer
sumber

Subtipe semantik didasarkan pada interpretasi teoretis set yang mendasari jenis, di mana subtipe adalah subset. Asli pekerjaan , saya percaya, adalah dengan Castagna dalam konteks bahasa pengolahan XML CDuce. Jenis sesuai dengan set dokumen XML. Ide-ide tersebut telah diterapkan kembali ke -kalkulus dan ke objek dan kelas kalkulus . $\pi$

Dave Clarke
sumber

Ada prekursor untuk Castagna. Dahulu orang sudah menggunakan relasi subset untuk pemodelan subtipe dalam model PER. Ada jenis yang sesuai dengan hubungan parsial kesetaraan (PER) dan subtyping hanyalah penyertaan dari hubungan tersebut.

Andrej Bauer

Dengan beberapa pengecualian (salah satu yang Dave Clarke kutip), semantik set-theoretik tipe sulit untuk digunakan. Alasannya adalah bahwa abstraksi data tidak bermain dengan sangat baik dengan semantik teori-set.

$\forall \alpha.\; \alpha \to \alpha$ $U$

[[\forall α . α \to α]] = Π X \in U . X \to X

$[\![\forall \alpha.\; \alpha \to \alpha]\!] = \Pi X \in \mathrm{U}.\;X \to X$

$U$ $U$ $X \to X$ $X \in U$ $\alpha$

$\forall \alpha.\; \alpha \to \alpha$

Neel Krishnaswami
sumber

Neel, kurasa jawaban ini tidak masuk akal. Jika semantik bahasa adalah semantik gaya-F standar, maka kompiler dapat melakukan optimasi dengan baik, berdasarkan pada sistem tipe. Jika semantik adalah semantik teori-set, maka optimasi akan menjadi tidak sehat. Model apa yang Anda gunakan untuk tipe tidak masuk ke dalamnya.

Sam Tobin-Hochstadt

Sam, saya tidak mengerti maksud Anda: sepertinya Anda setuju sepenuhnya dengan saya! Semantik teori set standar tidak dapat membuktikan bahwa satu-satunya penghuni jenis itu adalah identitas, jadi Anda memerlukan semantik yang berbeda.

Neel Krishnaswami

@Neel: masalah yang Anda gambarkan tetap ada bahkan ketika kita menjauh dari set. Solusinya bukan mengubah kategori set dengan sesuatu yang lain, tetapi untuk memodelkan parametrik secara berbeda. Yaitu, kita harus menggunakan parametrikitas relasional , karena saya yakin Anda tahu. Tetapi kemudian hal-hal bekerja dengan baik, jika saya tidak salah. Masalah "hanya" dengan set adalah kurangnya titik tetap (baik pada tingkat nilai rekursif dan jenis rekursif).

Andrej Bauer

Ah, kurasa aku mengerti mengapa aku membingungkanmu dan Sam! Saya tentu tidak bermaksud mengatakan bahwa tidak sehat untuk menggunakan model set-theory yang naif, hanya saja model ini sering memberikan jawaban yang tidak membantu - itu sebabnya saya mengatakan "sulit digunakan", dan bukan "salah". Anda tentu saja dapat menggunakan set untuk membangun model yang berguna (yaitu, secara relasional), tetapi kemudian kita tidak lagi mengintepretasikan tipe-sebagai-set dengan cara yang disarankan dalam pertanyaan. (Juga, seperti yang Anda tahu, dengan polimorfisme impredikatif tidak ada model yang naif, tetapi parametrisitas masih bermakna secara predikatif.)

Neel Krishnaswami

Saya pikir poin Anda adalah tentang korespondensi antara semantik - semantik teori set tidak cocok untuk polimorfisme Sistem F-style, karena memiliki penghuni yang tidak dapat diekspresikan. Tapi itu bukan poin terhadap semantik set-theoretik, hanya pernyataan bahwa semantik kita harus setuju. Jika bahasa kami memungkinkan kami mengekspresikan fungsi yang sedang Anda bicarakan (seperti yang dilakukan Typed Racket, misalnya), maka kami mungkin menginginkan semantik set-theoretik.

Sam Tobin-Hochstadt