🔚 ❄️ 👧🏿 Arend - bahasa tipe dependen berbasis HoTT (bagian 1) 🎒 🐧 😎

Dalam posting ini, kita akan berbicara tentang bahasa JetBrains yang baru dirilis dengan tipe dependen Arend (bahasa ini dinamai Gating Rent ). Bahasa ini telah dikembangkan oleh JetBrains Research selama beberapa tahun terakhir. Dan meskipun repositori setahun yang lalu diposting secara publik di github.com/JetBrains , rilis penuh Arend hanya terjadi pada bulan Juli tahun ini.

Kami akan mencoba memberi tahu bagaimana Arend berbeda dari sistem matematika formal yang ada berdasarkan tipe dependen, dan fungsi apa yang sekarang tersedia untuk penggunanya. Kami berasumsi bahwa pembaca artikel ini umumnya akrab dengan tipe dependen dan telah mendengar setidaknya satu bahasa berdasarkan tipe dependen: Agda, Idris, Coq, atau Lean. Namun, kami tidak berharap pembaca memiliki tipe dependen pada level lanjutan.

Untuk kesederhanaan dan konkret, cerita kami tentang tipe Arend dan homotopy akan disertai dengan implementasi pada Arend dari algoritma pengurutan daftar paling sederhana - bahkan dengan contoh ini Anda dapat merasakan perbedaan antara Arend dan Agda dan Coq. Sudah ada sejumlah artikel tentang Habré yang ditujukan untuk tipe-tipe dependen. Katakanlah tentang implementasi daftar penyortiran menggunakan metode QuickSort di Agda ada artikel seperti itu . Kami akan menerapkan algoritma yang lebih sederhana untuk menyortir sisipan. Dalam hal ini, kami akan fokus pada konstruksi bahasa Arend, dan bukan pada algoritma penyortiran itu sendiri.

Jadi, perbedaan utama antara Arend dan bahasa lain dengan tipe dependen adalah teori logis yang menjadi dasarnya. Arend menggunakan teori jenis homotopy V. Voevodsky yang baru-baru ini ditemukan ( HoTT ). Lebih khusus lagi, Arend didasarkan pada variasi HoTT yang disebut "teori tipe dengan spasi." Ingat bahwa Coq didasarkan pada apa yang disebut kalkulus konstruksi induktif (Kalkulus Konstruksi Induktif), sedangkan Agda dan Idris didasarkan pada teori tipe intensifikasi Martin-Löf . Fakta bahwa Arend didasarkan pada HoTT secara signifikan memengaruhi konstruksi sintaksisnya dan pengoperasian algoritma pengecekan tipe (typcheker). Kami akan membahas fitur-fitur ini dalam artikel ini.

Mari kita coba menggambarkan secara singkat keadaan infrastruktur bahasa. Untuk Arend ada plugin untuk IntelliJ IDEA, yang dapat diinstal langsung dari repositori plugin IDEA. Pada prinsipnya, menginstal plugin cukup untuk sepenuhnya berfungsi dengan Arend, Anda masih tidak perlu mengunduh dan menginstal apa pun. Selain memeriksa jenis, plugin Arend menyediakan fungsionalitas yang akrab bagi pengguna IDEA: ada penyorotan dan penyelarasan kode, berbagai refactor dan tips. Ada juga opsi untuk menggunakan versi konsol Arend. Penjelasan lebih rinci tentang proses instalasi dapat ditemukan di sini .

Contoh kode dalam artikel ini didasarkan pada pustaka standar Arend, jadi kami sarankan mengunduh kode sumbernya dari repositori . Setelah mengunduh, direktori sumber harus diimpor sebagai proyek IDEA menggunakan perintah Impor Proyek. Di Arend, beberapa bagian dari teori tipe homotopy dan teori cincin telah diformalkan. Sebagai contoh, di perpustakaan standar ada implementasi dari cincin bilangan rasional Q bersama dengan bukti dari semua sifat teori-cincin yang diperlukan.

Dokumentasi bahasa terperinci, di mana banyak poin yang dibahas dalam artikel ini dijelaskan lebih terinci, juga ada dalam domain publik. Anda dapat langsung mengajukan pertanyaan kepada Arend pengembang di saluran telegram .

1. Ikhtisar HoTT / Arend

Teori tipe homotopy (atau, singkatnya, HoTT) adalah jenis teori tipe intensional yang berbeda dari teori tipe Martin-Lof klasik (MLTT, yang menjadi dasar Agda) dan kalkulus konstruksi induktif (CIC, yang menjadi dasar Coq), dalam hal itu, bersama dengan pernyataan dan set berisi apa yang disebut jenis tingkat homotopy yang lebih tinggi.

Dalam artikel ini, kami tidak menetapkan tujuan untuk menjelaskan dasar-dasar HoTT secara detail - untuk penjelasan terperinci tentang teori ini, perlu untuk menceritakan kembali seluruh buku (lihat posting ini ). Kami hanya mencatat bahwa teori yang didasarkan pada aksioma HoTT, dalam arti tertentu, jauh lebih elegan dan menarik daripada teori tipe klasik Martin-Löf. Dengan demikian, sejumlah aksioma yang sebelumnya harus dipostulatkan tambahan (misalnya, ekstensionalitas fungsional) dibuktikan dalam HoTT sebagai teorema. Selain itu, di HoTT, seseorang dapat secara internal mendefinisikan bola homotopy multidimensi dan bahkan menghitung beberapa kelompok homotopy mereka.

Namun, aspek-aspek HoTT ini terutama menarik bagi matematikawan, dan tujuan dari artikel ini adalah untuk menjelaskan bagaimana Arend berbasis HoTT dibandingkan dengan Agda / MLTT dan Coq / CIC dengan contoh mewakili yang sederhana dan akrab bagi entitas pemrogram seperti daftar pesanan. Saat membaca artikel ini, cukup untuk memperlakukan HoTT sebagai semacam teori tipe intensional dengan aksioma yang lebih maju, yang memberikan kenyamanan ketika bekerja dengan alam semesta dan persamaan.

1.1 Jenis ketergantungan, korespondensi Curry - Howard, semesta

Ingatlah bahwa bahasa dengan tipe dependen berbeda dari bahasa pemrograman fungsional biasa selain tipe data biasa, seperti daftar atau angka alami, ada beberapa tipe yang bergantung pada nilai parameter. Contoh paling sederhana dari jenis tersebut adalah vektor dengan panjang tertentu n atau pohon seimbang dengan kedalaman tertentu d. Beberapa contoh lebih lanjut dari jenis-jenis tersebut disebutkan di sini.

Ingat bahwa korespondensi Curry - Howard memungkinkan seseorang untuk menafsirkan pernyataan logika sebagai tipe dependen. Gagasan utama dari korespondensi ini adalah bahwa tipe kosong sesuai dengan pernyataan salah, dan tipe populasi sesuai dengan pernyataan yang benar. Jenis elemen dapat dianggap sebagai bukti dari pernyataan logis yang sesuai. Sebagai contoh, setiap elemen seperti bilangan bulat dapat dianggap sebagai bukti dari fakta bahwa bilangan bulat ada (yaitu, jenis bilangan bulat diisi).

Konstruksi alami yang berbeda untuk tipe sesuai dengan koneksi logis yang berbeda:

Produk tipe A × B kadang-kadang disebut tipe pasangan Pair A B. Karena tipe ini terisi jika dan hanya jika kedua tipe A dan B terisi, konstruksi ini sesuai dengan "dan" logis.
Jumlah tipe A + B. Dalam Haskell, tipe ini disebut E A. Karena tipe ini terisi jika dan hanya jika salah satu tipe A atau B terisi, konstruksi ini sesuai dengan "atau" yang logis.
Tipe fungsional A → B. Setiap fungsi dari tipe ini mengubah elemen A ke elemen B. Dengan demikian, fungsi seperti itu ada tepat ketika keberadaan elemen tipe A menyiratkan keberadaan elemen tipe B. Oleh karena itu, konstruksi ini sesuai dengan implikasi.

Misalkan sekarang kita diberi tipe A tertentu dan keluarga tipe B yang diparameterisasi oleh elemen a dari tipe A. Mari kita berikan contoh konstruksi yang lebih kompleks daripada tipe dependen.

Jenis fungsi dependen Π (a: A) (B a). Tipe ini bertepatan dengan tipe fungsional A → B yang biasa jika B tidak bergantung pada A. Fungsi tipe Π (a: A) (B a) mengubah elemen apa pun dari tipe A menjadi elemen tipe B a. Jadi, fungsi semacam itu ada jika dan hanya jika, untuk a : A, ada elemen B a. Oleh karena itu, konstruksi ini sesuai dengan kuantifier universal ∀. Untuk tipe fungsional dependen, Arend menggunakan sintaks \Pi (x : A) -> B a , dan istilah yang mendiami tipe ini dapat dikonstruksikan menggunakan ekspresi lambda \lam (a : A) => f a.
Jenis pasangan tergantung adalah Σ (a: A) (B a). Tipe ini bertepatan dengan tipe pasangan A × B yang biasa jika B tidak bergantung pada A. Tipe Σ (a: A) (B a) terisi persis ketika ada elemen a: A dan elemen tipe B a. Jadi, tipe ini sesuai dengan quantifier keberadaan ∃ . Jenis pasangan dependen dalam Arend dilambangkan dengan \Sigma (a : A) (B a) , dan istilah yang mendiami itu dibangun menggunakan konstruktor dari pasangan (tergantung) (a, b) .
Jenis kesetaraan adalah a = a ', di mana a dan' adalah dua elemen dari beberapa jenis A. Jenis tersebut dihuni jika a dan a 'sama, dan kosong sebaliknya. Jelas, tipe ini adalah analog dari predikat kesetaraan dalam logika.

Pada titik ini, kami merujuk pembaca ke sumber di mana korespondensi Curry - Howard dibahas secara lebih rinci (lihat, misalnya, kursus kuliah atau artikel di sini atau di sini ).

Semua ekspresi yang dipertimbangkan dalam teori tipe harus memiliki beberapa tipe. Karena ekspresi yang menunjukkan tipe juga dipertimbangkan dalam kerangka teori ini, mereka juga perlu diberi tipe tertentu. Pertanyaannya adalah, seperti apa jenisnya?

Keputusan naif pertama yang muncul di pikiran adalah untuk menetapkan semua tipe tipe formal \Type , yang disebut alam semesta (disebut demikian karena berisi semua tipe pada umumnya). Jika kita menggunakan alam semesta ini, jumlah konstruksi dan jenis produk yang disebutkan di atas akan menerima tanda tangan \Type → \Type → \Type , dan konstruksi yang lebih kompleks dari produk tergantung dan jumlah bergantung akan menerima tanda tangan Π (A : \Type) → ((A → \Type) → \Type) .

Pada titik ini, muncul pertanyaan, tipe apa yang seharusnya dimiliki oleh \Type semesta itu sendiri? Upaya naif untuk mengatakan bahwa jenis alam semesta \Type , menurut definisi, adalah \Type itu sendiri mengarah ke paradoks Girard , jadi alih-alih sebuah alam semesta tunggal \Type mempertimbangkan hierarki alam semesta yang tak terbatas, mis. rantai bersarang alam semesta \Type 1 < \Type 2 < … , yang levelnya diberi nomor oleh bilangan alami, dan tipe alam semesta \Type i , menurut definisi, adalah alam semesta \Type (i+1) . Untuk jenis konstruksi yang disebutkan di atas, tanda tangan yang lebih kompleks juga harus diperkenalkan.

Dengan demikian, alam semesta dalam teori tipe diperlukan sehingga setiap ekspresi memiliki tipe tertentu. Dalam beberapa varietas teori tipe, alam semesta digunakan untuk tujuan lain: untuk membedakan antara varietas jenis. Kita telah melihat bahwa set dan pernyataan adalah tipe kasus khusus. Ini menunjukkan bahwa masuk akal untuk memperkenalkan ke dalam teori Prop universe yang terpisah untuk pernyataan dan hierarki yang terpisah dari alam semesta Set _i . Ini persis pendekatan yang digunakan dalam Kalkulus Konstruksi Induktif, teori di mana sistem Coq didasarkan.

1.2 Contoh tipe induktif paling sederhana dan fungsi rekursif

Pertimbangkan definisi Arend dari tipe data induktif yang paling sederhana: tipe Boolean, tipe angka alami, dan daftar polimorfik. Arend menggunakan \data kata kunci untuk memperkenalkan tipe induktif baru.

\data Empty -- ,

\data Bool
| true
| false

\data Nat
| zero
| suc Nat

\data List (A : \Set)
| nil
| \infixr 5 :-: A (List A)

Seperti yang Anda lihat dari contoh di atas, setelah \data kata kunci, Anda perlu menentukan nama tipe induktif dan daftar konstruktornya. Pada saat yang sama, tipe data dan konstruktor mungkin memiliki beberapa parameter. Katakanlah dalam contoh di atas tipe List memiliki satu parameter A Konstruktor daftar nil tidak memiliki parameter, dan konstruktor: -: memiliki dua parameter (salah satunya adalah tipe A , dan yang lainnya adalah tipe List A ). The Univers \Set terdiri dari tipe-tipe yang merupakan set (definisi dari set akan diberikan pada bagian selanjutnya). \infixr memungkinkan Anda untuk menggunakan notasi infiks untuk konstruktor: -: dan, selain itu, memberi tahu parser Arend bahwa operator: -: adalah operasi asosiatif-kanan dengan prioritas 5.

Di Arend, semua kata kunci dimulai dengan karakter garis miring terbalik (“\”), sebuah implementasi yang terinspirasi oleh LaTeX. Perhatikan bahwa aturan leksikal di Arend sangat liberal: Circle_HSpace, contrFibers=>Equiv, suc/=0, zro_*-left dan bahkan n:Nat - semua literal ini adalah contoh pengidentifikasi yang valid di Arend. Contoh terakhir menunjukkan betapa pentingnya bagi pengguna Arend untuk mengingat untuk menempatkan spasi antara pengidentifikasi dan karakter titik dua . Perhatikan bahwa dalam pengidentifikasi Arend tidak diperbolehkan untuk menggunakan karakter Unicode (khususnya, Anda tidak dapat menggunakan Cyrillic).

Arend menggunakan kata kunci \func untuk mendefinisikan fungsi. Sintaks dari konstruksi ini adalah sebagai berikut: setelah kata kunci \func , Anda perlu menentukan nama fungsi, parameternya dan jenis nilai kembali. Elemen terakhir dalam mendefinisikan suatu fungsi adalah tubuhnya.

Jika dimungkinkan untuk secara eksplisit menentukan ekspresi di mana fungsi yang diberikan dihitung, maka untuk menunjukkan tubuh fungsi, token => digunakan. Pertimbangkan, misalnya, definisi fungsi negasi jenis.

 \func Not (A : \Type) : \Type => A -> Empty

Tipe kembalinya suatu fungsi tidak selalu harus ditentukan secara eksplisit. Pada contoh di atas, Arend akan dapat secara independen menyimpulkan tipe Not , dan kita dapat menghilangkan ungkapan ": \Type " setelah tanda kurung.

Seperti dalam kebanyakan sistem matematika yang diformalkan, pengguna tidak harus menentukan tingkat prediktif eksplisit untuk \Type semesta, dan definisi di mana alam semesta digunakan tanpa secara eksplisit menentukan tingkat prediksi dianggap polimorfik .

Sekarang mari kita coba mendefinisikan fungsi yang menghitung panjang daftar. Fungsi seperti itu mudah diidentifikasi melalui pencocokan pola. Arend menggunakan \elim kata kunci untuk ini. Setelah itu, Anda harus menentukan variabel tempat perbandingan dilakukan (jika ada lebih dari satu variabel seperti itu, maka mereka harus ditulis dengan koma). Jika perbandingan dilakukan untuk semua parameter eksplisit, maka \elim beserta variabel dapat dihilangkan. Ini diikuti oleh blok titik perbandingan, dipisahkan satu sama lain oleh bilah vertikal "|". Setiap item dalam blok ini adalah ekspresi dari bentuk «, » => «» .

 \func length {A : \Set} (l : List A) : Nat | nil => 0 | :-: x xs => suc (length xs)

Pada contoh di atas, parameter A dari fungsi length dikelilingi oleh kurung kurawal. Tanda kurung di Arend ini digunakan untuk menunjukkan argumen implisit, mis. argumen yang dapat dihilangkan pengguna saat memanggil suatu fungsi atau menggunakan tipe. Perhatikan bahwa di Arend Anda tidak dapat menggunakan notasi infiks untuk menunjuk konstruktor saat mencocokkan dengan pola, sehingga notasi awalan digunakan dalam contoh sampel.

Seperti dalam Coq / Agda, dalam Arend semua fungsi harus dijamin akan selesai (mis., Pemeriksaan penghentian hadir di Arend). Dalam definisi fungsi panjang, pemeriksaan ini berhasil, karena panggilan rekursif secara ketat mengurangi argumen eksplisit pertama. Jika pengurangan seperti itu tidak terjadi, Arend akan memberikan pesan kesalahan.

 \func bad : Nat => bad [ERROR] Termination check failed for function 'bad' In: bad

Arend memungkinkan dependensi melingkar dan fungsi saling rekursif yang pemeriksaan kelengkapannya juga dilakukan. Algoritma pemeriksaan ini dilaksanakan berdasarkan artikel oleh A. Abel. Di dalamnya Anda akan menemukan deskripsi yang lebih rinci tentang kondisi yang harus dipenuhi fungsi rekursif bersama.

1.3 Apa perbedaan set dari pernyataan?

Kami sebelumnya menulis bahwa contoh tipe adalah himpunan dan pernyataan. Selain itu, kami menggunakan kata kunci \Type dan \Set untuk menunjukkan semesta di Arend. Pada bagian ini, kami akan mencoba menjelaskan secara lebih rinci bagaimana pernyataan berbeda dari set dalam hal varietas dari teori tipe intensional (MLTT, CIC, HoTT), dan pada saat yang sama menjelaskan apa arti dari kata kunci \Prop , \Set dan \Type dalam Arend terdiri.

Ingatlah bahwa dalam teori klasik Martin-Lof tidak ada pemisahan tipe menjadi himpunan dan pernyataan. Secara khusus, dalam teori hanya ada satu kumulatif alam semesta (yang dilambangkan dengan Set in Agda, atau Type in Idris, atau Sort in Lean). Pendekatan ini adalah yang paling sederhana, tetapi ada situasi di mana kekurangannya terwujud. Misalkan kita sedang berusaha mengimplementasikan tipe "daftar pesanan" sebagai pasangan tidak tetap yang terdiri dari daftar dan bukti pemesanannya. Ternyata kemudian, dalam kerangka MLTT "murni", tidak akan mungkin untuk membuktikan kesetaraan daftar terurut yang terdiri dari elemen identik, yang pada saat bersamaan berbeda dalam hal bukti pemesanan. Untuk memiliki kesetaraan seperti itu akan sangat alami dan diinginkan, sehingga ketidakmungkinan untuk membuktikannya dapat dianggap sebagai cacat teoritis dalam MLTT.

Di Agda, masalah ini sebagian diselesaikan dengan bantuan yang disebut annotations of immateriality (lihat sumbernya , di mana contoh daftar dibahas lebih rinci). Anotasi ini, bagaimanapun, bukan merupakan konstruk dari teori MLTT, juga bukan merupakan konstruk penuh pada tipe (tidak mungkin untuk menandai dengan anotasi tipe yang tidak digunakan dalam argumen fungsi).

Dalam CIC, berdasarkan CIC, ada dua alam semesta berbeda yang saling bersarang: Prop (alam semesta pernyataan) dan Set (alam semesta himpunan), yang dicelupkan ke dalam hierarki komprehensif semesta Type . Perbedaan utama antara Prop dan Set adalah bahwa ada sejumlah batasan pada variabel yang jenisnya termasuk Prop dalam Coq. Sebagai contoh, mereka tidak dapat digunakan dalam perhitungan, dan perbandingan dengan sampel untuk mereka hanya mungkin dilakukan di dalam bukti pernyataan lain. Di sisi lain, semua elemen dari jenis milik Prop semesta adalah sama dalam aksioma bukti tidak penting, lihat pernyataan di Coq.Logic.ProofIrrelevance . Dengan menggunakan aksioma ini, kita dapat dengan mudah membuktikan kesetaraan dari daftar pesanan yang disebutkan di atas.

Akhirnya, pertimbangkan pendekatan Arend / HoTT untuk pernyataan dan alam semesta. Perbedaan utama adalah bahwa HoTT membuang dengan aksioma bukti tidak penting. Artinya, tidak ada aksioma khusus dalam HoTT yang mendalilkan bahwa semua elemen pernyataan adalah sama. Tetapi dalam HoTT, tipe, menurut definisi , adalah pernyataan jika dapat dibuktikan bahwa semua elemennya sama satu sama lain. Kita dapat mendefinisikan predikat pada tipe yang benar jika tipenya adalah pernyataan:

 \func isProp (A : \Type) => \Pi (aa' : A) -> a = a'

Muncul pertanyaan: apa jenis yang memenuhi predikat ini, yaitu, pernyataan? Sangat mudah untuk memverifikasi bahwa ini berlaku untuk jenis kosong dan tunggal. Untuk tipe yang paling tidak memiliki dua elemen berbeda, ini tidak lagi benar.

Tentu saja, kami ingin semua penghubung logis yang perlu ditentukan berdasarkan pernyataan. Dalam Bagian 1.1, kita sudah membahas bagaimana mereka dapat ditentukan menggunakan konstruksi tipe-teori. Namun, ada masalah berikut: tidak semua operasi yang kami masukkan mempertahankan properti isProp . Konstruksi produk tipe dan tipe fungsional (tergantung) mempertahankan properti ini, sedangkan konstruksi jumlah tipe dan pasangan dependen tidak. Jadi, kita tidak bisa menggunakan disjungsi dan kuantifikasi keberadaan.

Masalah ini dapat diselesaikan dengan bantuan konstruksi baru, yang ditambahkan ke HoTT, yang disebut pemotongan proposisional . Desain ini memungkinkan Anda untuk mengubah tipe apa pun menjadi pernyataan. Ini dapat dianggap sebagai operasi formal, menyamakan semua istilah yang mendiami tipe ini. Operasi ini agak mirip dengan penjelasan immaterialitas dari Agda, namun, tidak seperti mereka, ini adalah operasi penuh pada jenis dengan tanda tangan \Type -> \Prop .

Contoh pernyataan penting terakhir adalah kesetaraan dua elemen dari beberapa tipe. Ternyata dalam kasus umum jenis kesetaraan a = a' tidak harus berupa pernyataan. Jenis yang disebut satu set:

 \func isSet (A : \Type) => \Pi (aa' : A) -> isProp (a = a')

Semua jenis yang ditemukan dalam bahasa pemrograman biasa memenuhi predikat ini, yaitu, kesetaraan pada mereka adalah pernyataan. Sebagai contoh, ini berlaku untuk bilangan asli, bilangan bulat, produk set, jumlah set, fungsi lebih dari set, daftar set, dan tipe data induktif lainnya yang dibangun dari set. Ini berarti bahwa jika kita hanya tertarik pada konstruksi yang sudah dikenal seperti itu, maka kita tidak dapat berpikir tentang tipe arbitrer yang tidak memenuhi predikat ini. Semua tipe yang ditemukan dalam Coq adalah set .

Tipe yang tidak disetel menjadi berguna jika Anda ingin berurusan dengan teori tipe homotopy. Untuk saat ini, kami cukup merujuk pembaca ke modul perpustakaan standar yang berisi definisi bola n-dimensi , contoh dari jenis yang bukan kumpulan.

Arend memiliki alam semesta khusus \Prop dan \Set , yang masing-masing terdiri dari pernyataan dan set. Jika kita sudah tahu bahwa tipe A terkandung dalam alam semesta \Prop (atau \Set ), maka bukti properti isProp (atau isSet ) yang sesuai di Arend dapat diperoleh dengan menggunakan aksioma Path.inProp dibangun di awal (kami memberikan contoh menggunakan aksioma ini dalam bagian 2.3).

 \func inProp {A : \Prop} : \Pi (aa' : A) -> a = a'

Kami telah mencatat bahwa tidak semua konstruksi alami pada tipe mempertahankan properti isProp . Misalnya, tipe data induktif dengan dua atau lebih konstruktor tidak pernah memuaskannya. Seperti disebutkan di atas, kita dapat menggunakan konstruksi pemotongan proposisional yang mengubah tipe apa pun menjadi pernyataan.
Di perpustakaan Arend, implementasi standar pemotongan proposisional disebut Logic.TruncP . Kita bisa mendefinisikan tipe logis "atau" di Arend sebagai memotong jumlah jenis:

 \data \fixr 2 Or (AB : \Type) -- Sum of types; analogue of Coq's type "sum" | inl A | inr B \func \infixr 2 || (AB : \Type) => TruncP (sum AB) -- Logical “or”, analogue of Coq's type "\/"

Di Arend, ada cara lain, lebih sederhana dan lebih nyaman untuk mendefinisikan tipe induktif yang terpotong proposisi. Untuk melakukan ini, tambahkan saja kata kunci \truncated sebelum mendefinisikan tipe data. Sebagai contoh, definisi logis “atau” di pustaka standar Arend diberikan sebagai berikut.

 \truncated \data \infixr 2 || (AB : \Type) : \Prop -- Logical “or”, analogue of Coq's type "\/" | byLeft A | byRight B

Pekerjaan lebih lanjut dengan jenis terpotong proposisional menyerupai jenis yang ditugaskan ke alam semesta Prop di Coq. Misalnya, pencocokan pola variabel yang jenisnya adalah pernyataan hanya diizinkan dalam situasi di mana jenis ekspresi itu sendiri merupakan pernyataan. Dengan demikian, selalu mudah untuk mendefinisikan fungsi Or-to-|| melalui perbandingan dengan sampel, tetapi fungsi terbalik untuk itu, hanya jika tipe A `Or` B adalah pernyataan (yang cukup langka, misalnya, ketika tipe A dan B keduanya pernyataan dan saling terpisah satu sama lain).

 \func Or-to-|| {AB : \Prop} (a-or-b : A `Or` B) : A || B | inl a => byLeft a | inr b => byRight

Ingat juga bahwa kekhasan mekanisme alam semesta dalam Coq adalah bahwa jika beberapa definisi diberikan ke alam semesta Prop , maka sama sekali tidak mungkin untuk menggunakannya dalam perhitungan. Untuk alasan ini, pengembang Coq sendiri tidak merekomendasikan penggunaan konstruksi proposisional, tetapi menyarankan untuk menggantinya dengan analog dari set semesta, jika memungkinkan. Mekanisme alam semesta Arend tidak memiliki kelemahan ini, yaitu, dalam situasi tertentu dimungkinkan untuk menggunakan pernyataan dalam perhitungan. Kami akan memberikan contoh situasi seperti itu ketika kami membahas implementasi algoritma pengurutan daftar.

1.4 Kelas di Arend

Karena tujuan kami adalah menerapkan algoritma penyortiran yang paling sederhana, tampaknya berguna untuk membiasakan diri Anda dengan penerapan set yang dipesan yang tersedia di pustaka standar Arend.

Di Arend, kelas digunakan untuk merangkum operasi dan aksioma yang mendefinisikan struktur matematika, dan juga untuk menyoroti hubungan antara struktur ini menggunakan pewarisan. Kelas juga ruang nama, yang di dalamnya nyaman untuk menempatkan konstruksi dan teori yang sesuai dengan makna.

Kelas dasar dari mana semua kelas pesanan di Arend diwarisi adalah kelas BaseSet , yang tidak mengandung anggota apa pun selain penunjukan E untuk set host (mis., Set di mana BaseSet turunan BaseSet sudah memperkenalkan berbagai operasi). Pertimbangkan definisi kelas ini dari pustaka Arend standar.

 \class BaseSet (E : \Set) -- ,

Dalam definisi di atas, operator E dinyatakan sebagai parameter kelas. Orang mungkin bertanya, apakah ada perbedaan dalam definisi BaseSet dari definisi berikut, di mana carrier E didefinisikan sebagai bidang kelas?

 \class BaseSet' --      | E : \Set

Jawaban yang sedikit tidak terduga adalah bahwa dalam Arend tidak ada perbedaan antara dua definisi dalam arti bahwa setiap parameter kelas (bahkan implisit) dalam Arend, pada kenyataannya, adalah bidangnya. Dengan demikian, untuk kedua implementasi BaseSet , orang dapat menggunakan ekspresi xE untuk mengakses bidang E. BaseSet perbedaan antara varian di atas dari definisi BaseSet , tetapi lebih halus, kita akan memeriksanya lebih detail di bagian selanjutnya ketika kita membahas contoh kelas ( instance kelas).

Operasi pengurutan daftar masuk akal hanya jika urutan linier ditentukan pada jenis objek dalam daftar, jadi kami pertama-tama mempertimbangkan definisi dari himpunan sebagian yang dipesan secara ketat dan rangkaian yang dipesan secara linear.

 \class StrictPoset \extends BaseSet { | \infix 4 < : E -> E -> \Prop | <-irreflexive (x : E) : Not (x < x) | <-transitive (xyz : E) : x < y -> y < z -> x < z } \class LinearOrder \extends StrictPoset { | <-comparison (xyz : E) : x < z -> x < y || y < z | <-connectedness (xy : E) : Not (x < y) -> Not (y < x) -> x = y }

Dari sudut pandang teori tipe, kelas-kelas di Arend dapat dianggap sebagai analog dari tipe sigma dengan sintaksis yang lebih nyaman untuk proyeksi dan konstruktor. , Arend- -, .

, . , . , StrictPoset <-irreflexive <-transitive , E < — . , (, , ) , .

, , . , Arend , , . , . , , , , . :

 \class DecSet \extends BaseSet | decideEq (xy : E) : Dec (x = y)

Dec , Dec E , E , E , E .

 \data Dec (E : \Prop) | yes E | no (Not E)

, , Dec ( decidable) Order.LinearOrder . Dec , , , trichotomy , , E , <. , Dec Comparable Java.

 \class Dec \extends LinearOrder, DecSet { | trichotomy (xy : E) : (x = y) || (x < y) || (y < x) | <-comparison xyz x<z => {?} --   | <-connectedness xyx/<yy/<x => {?} | decideEq xy => {?} }

Dec Dec , , , , . Dec , .

, Dec ( ). Dec , Arend ( Dec LinearOrder, DecSet ), , (diamond inheritance).

: , ( , ).

Dec Order.LinearOrder IDEA ( [Ctrl]+[H]), , .

Arend ( IDEA BaseSet ). , .

1.5 , , .

StrictPoset Nat. Arend , . -, , , - ( ), .

: . .

 data \infix 4 < (ab : Nat) \with | zero, suc _ => zero<suc_ | suc a, suc b => suc<suc (a < b) \lemma irreflexivity (x : Nat) (p : x < x) : Empty | suc a, suc<suc a<a => irreflexivity a a<a \lemma transitivity (xyz : Nat) (p : x < y) (q : y < z) : x < z | zero, suc y', suc z', zero<suc_, suc<suc y'<z' => zero<suc_ | suc x', suc y', suc z', suc<suc x'<y', suc<suc y'<z' => suc<suc (transitivity x' y' z' x'<y' y'<z')

\func \lemma . , , , . , \lemma , \Prop .

x'<y' — -, x' < y' . - (.. , , ).

(instance) StrictPoset . Arend . \new . « ».

 \func NatOrder => \new StrictPoset { | E => Nat | < => < | <-irreflexive => irreflexivity | <-transitive => transitivity }

StrictPoset { … } \new : - StrictPoset . - , , , \new . \new C { … } C { … } . C, C. , , NatOrder StrictPoset .

, . , StrictPoset Nat StrictPoset { | E => Nat } . , NatOrder StrictPoset , ( ).

NatOrder \cowith ( - ).

 \func NatOrder : StrictPoset \cowith { | E => Nat | < => < | <-irreflexive => irreflexivity | <-transitive => transitivity }

, , \instance.

 \instance NatOrder : StrictPoset { | E => Nat | < => < | <-irreflexive => irreflexivity | <-transitive => transitivity }

Arend , Haskell. NatOrder \instance \cowith , StrictPoset ( ).

, BaseSet - E ( ), , E . .

, Arend . Arend , , ( , « » \classifying \field , Arend ). :

Arend . , X StrictPoset , List X List XE .
Arend .

, . , \instance StrictPoset , Nat Int ( NatOrder IntOrder ).

, x < y , x, y , , x, y . Arend , NatOrder.< , — IntOrder.< .

, . Arend , < StrictPoset , E. , Arend x<y StrictPoset ( ), E . , < .

, Arend. , \use \coerce . Arend — , , . - , \where .

. fromNat .

 \data Int | pos Nat | neg Nat \with { zero => pos zero } \where { \use \coerce fromNat (n : Nat) => pos n }

\use \coerce \func , . , , (, , ).

: HoTT JetBrains Research.