Jenis universal dan eksistensial

Saya mencoba menyelubungi konsep-konsep tipe universal dan eksistensial tetapi di mana pun saya melihat, saya melihat intuisi logis atau operasional (atau implementasi) (misalnya buku TAPL oleh B. Pierce), yang, yah ... bagus , tapi saya ingin melihat definisi (di mana kita melihatnya sebagai set) - dan dari mereka, turunan dari beberapa undang-undang, serta pembenaran untuk intuisi kita.

Jadi, karena saya tidak dapat menemukan definisi tersebut, saya memutuskan untuk melakukannya sendiri dan saya pikir ini masuk akal:

∃ x . T d e f : = ⋃ S - t y p e T [ x : = S

$$\forall x.T \overset{def}{:=} \bigcap_{S - type} T[x := S]$$ $$\exists x.T \overset{def}{:=} \bigcup_{S - type} T[x := S]$$

Tetapi, dalam buku TAPL tersebut di atas, kita diberikan definisi ini (meskipun saya akan menyebutnya identitas)

$$\exists x.T \overset{def}{:=} \forall y. (\forall x. T \rightarrow y) \rightarrow y \quad (*)$$

Saya memiliki dua masalah dengan ini:

1. Pada LHS dari saya akan berharap bahwa x adalah satu-satunya variabel bebas dari T (karena bagaimana cara melihat tipe "belum-dibangun" dengan beberapa variabel bebas yang menggantung di dalamnya?), Tetapi pada RHS sepertinya y mungkin memiliki beberapa dampak pada T , sehingga lebih baik menjadi variabel bebas dalam T . Maka LHS tidak bisa sama dengan RHS karena set variabel bebas T berbeda di kedua sisi, kan?$(*)$$x$$T$$y$$T$$T$$T$
2. Bahkan mengabaikan masalah pada poin 1. - Saya mencoba menulis ulang RHS menggunakan definisi saya dan melihat apakah saya bisa mendapatkan definisi saya tentang tipe eksistensial tetapi saya terjebak: $$RHS = \bigcap_{S} (\forall x.T \rightarrow y)[y := S] \rightarrow S = \bigcap_{S} \left(\bigcap_{R} T[x := R, y := S] \rightarrow S\right) \rightarrow S$$

Bahkan tidak mirip dengan definisi saya. Apakah mungkin untuk menyederhanakan formula tempat saya tiba? Secara intuitif, karena ada tipe fungsi, mungkin tidak akan pernah sama dengan definisi saya. Tetapi jika mereka tidak setara - apakah mereka setidaknya 'isomorfis' dalam arti tertentu? Jika tidak - apa yang "salah"?

Teori himpunan membuat Anda sedikit terluka di sini dan semakin cepat Anda membebaskan diri darinya, semakin baik pemahaman Anda tentang ilmu komputer.

Lupakan persimpangan dan serikat pekerja. Orang-orang mendapatkan ide bahwa dan ∃ seperti ⋂ dan ⋃ , yang merupakan hal yang dilakukan sekolah Polandia sejak lama dengan aljabar Boolean, tetapi itu benar-benar bukan cara untuk pergi (pasti bukan dalam ilmu komputer).$\forall$$\exists$$\bigcap$$\bigcup$

Anda ingin melihatnya sebagai set. Ok, tapi kemudian kita harus mengabaikan masalah ukuran dan berpura-pura bahwa ada satu set semua set. (Dimungkinkan untuk memperbaiki masalah ukuran dengan meneruskan ke kategori yang berbeda.) Jenis adalah benar-benar seperti Cartesian produk ∀ X . T : = ∏ S : S e t T [ X ↦ S ] . Artinya, unsur ∀ X . T adalah fungsi f dari set ke set: untuk setiap set S memberikan elemen$\forall x . T$

$$\forall X . T \mathrel{{:}{=}} \prod_{S : \mathsf{Set}} T[X \mapsto S].$$ $\forall X . T$ $f$$S$ dari tipe T [ x ↦ S ] . Misalnya, unsur ∀ X . ( X → X ) → ( X → X ) adalah fungsi f yang mengambil set S dan memberikan fungsi tipe ( S → S ) → ( S → S ) . Berikut beberapa fungsi tersebut: f 0 ( S ) ( g ) $f(S)$$T[x \mapsto S]$$\forall X. (X \to X) \to (X \to X)$$f$$S$$(S \to S) \to (S \to S)$ Jadi kita mendapatkan satu untuk setiap bilangan alami, dan agak sulit untuk memikirkan contoh lainnya. (Latihan: google "Pengkodean angka alamiah Gereja".) $$\begin{align*} f_0(S)(g)(x) &\mathrel{{:}{=}} x \\ f_1(S)(g)(x) &\mathrel{{:}{=}} g(x) \\ f_2(S)(g)(x) &\mathrel{{:}{=}} g(g(x)) \\ f_3(S)(g)(x) &\mathrel{{:}{=}} g(g(g(x))) \end{align*}$$

$\exists$$\forall$

$$\exists X . T \mathrel{{:}{=}} \forall Y . (\forall X . (T \to Y)) \to Y$$ $Y$$T$$\exists X . T$ $$\exists X . T \mathrel{{:}{=}} \coprod_{S : \mathsf{Set}} T[X \mapsto S].$$ $\exists X . T$ $(S, a)$$S$$a$$T[X \mapsto S]$$\exists X . (X \times X \to X)$$(S, m)$$S$$m : S \times S \to S$

$\exists$$\forall$$\exists X. T$$\forall Y . (\forall X . (T \to Y)) \to Y$$Y$

$$A \mathrel{{:}{=}} \coprod_{S : \mathsf{Set}} T[X \mapsto S]$$ $$B \mathrel{{:}{=}} \prod_{R : \mathsf{Set}} \left(\prod_{S : \mathsf{Set}} (T[X \mapsto S] \to R) \right) \to R.$$ $\lambda$$f : A \to B$ $$f(S,a)(R)(h) \mathrel{{:}{=}} h(S)(a)$$ $g : B \to A$ $$g(\phi) \mathrel{{:}{=}} \phi(A)(\lambda S . \lambda a . (S, a)).$$ $\lambda S . \lambda a . (S, a)$$S \mapsto a \mapsto (S, a)$$f$$g$ $$g(f(S,a)) = f(S,a)(A)(\lambda S' . \lambda a' . (S', a')) = (\lambda S' . \lambda a' . (S', a')(S)(a) = (S, a).$$ $$f(g(\phi))(R)(h) = h(\pi_1(g(\phi))(\pi_2(g(\phi))).$$ $g(\phi)$$\phi(A)(\lambda S . \lambda a . (S, a))$

$\exists$$\forall$

$$\exists x . \phi(x)$$ $$\forall{P : \mathsf{Prop}} . (\forall x . (\phi(x) \Rightarrow P)) \Rightarrow P,$$ $P$$P$$\phi$

$Y$ $Y$$Y$$T$$\exists T$

$$((\forall x. T\rightarrow U_0)\rightarrow U_0)\wedge((\forall x. T\rightarrow U_1)\rightarrow U_1)\wedge\ldots$$ $U_i$$U$ $$\exists x.T \rightarrow ((\forall x. T\rightarrow U)\rightarrow U)$$

Dalam kata kata:

$x$$T(x)$$U$ $x$$T(x)$$U$

$U$$x$

$U$

$\bigcap_S A(S)$$A(\varnothing)$

$$\left(\bigcap_R \left(T[x:=R]\rightarrow \varnothing\right)\right)\rightarrow\varnothing$$

$R$$T[x:=R]\rightarrow \varnothing$$T[x:=R]$

Saya menyarankan untuk tidak menyerah pada intuisi operasional. Operasional adalah yang utama, semua semantik diturunkan, dan hanyalah teknik bukti untuk semantik operasional. Gagasan utama adalah sebagai berikut.

$P$$x$ $P$$x$$x$$\lambda$

• $\lambda x.x.$
• $\lambda (x,y,z). (z,x, y)$
• $\lambda x.(x,x)$
• $\lambda x.7$

$P$$x$ $P$$x$$x$$P$$x$$x$

$\lambda$