Pada bagian pertama artikel tentang bahasa Arend, kami memeriksa jenis induktif yang paling sederhana, fungsi rekursif, kelas dan set.
2. Menyortir Daftar di Arend
2.1 Daftar Pesanan di Arend
Kami mendefinisikan jenis daftar yang dipesan sebagai pasangan yang terdiri dari daftar dan bukti pemesanannya. Seperti yang telah kami katakan, dalam Arend, pasangan tergantung didefinisikan menggunakan kata kunci
\Sigma . Kami memberikan definisi dari jenis yang
Sorted melalui perbandingan dengan sampel, terinspirasi oleh definisi dari artikel yang telah disebutkan
tentang daftar dipesan. \func SortedList (O : LinearOrder.Dec) => \Sigma (l : List O) (Sorted l) \data Sorted {A : LinearOrder.Dec} (xs : List A) \elim xs | nil => nilSorted | :-: x nil => singletonSorted | :-: x1 (:-: x2 xs) => consSorted ((x1 = x2) || (x1 < x2)) (Sorted (x2 :-: xs))
Catatan: Arend dapat secara otomatis menyimpulkan bahwa tipe
Sorted terkandung dalam
\Prop universe. Ini terjadi karena ketiga pola dalam definisi
Sorted adalah saling eksklusif, dan konstruktor yang
consSorted memiliki dua parameter, yang keduanya milik
\Prop .
Mari kita buktikan beberapa properti yang jelas dari predikat
Sorted , katakan bahwa ekor dari daftar yang diurutkan itu sendiri adalah daftar yang dipesan (properti ini akan berguna bagi kita di masa depan).
\func tail-sorted {O : LinearOrder.Dec} (x : O) (xs : List O) (A : Sorted (x :-: xs)) : Sorted xs \elim xs, A | nil, _ => nilSorted | :-: _ _, consSorted _ xs-sorted => xs-sorted
Dalam
tail-sorted kami menggunakan pencocokan pola pada daftar
xs dan predikat
Sorted pada saat yang sama, di samping itu, kami menggunakan
karakter lewati “_”, yang dapat diganti dengan variabel yang tidak digunakan.
Orang mungkin bertanya apakah mungkin dalam Arend untuk membuktikan properti dari daftar yang dipesan, yang disebutkan dalam bagian 1.3 sebagai contoh dari fakta yang tidak dapat dibuktikan di Agda tanpa anotasi immaterialitas. Ingatlah bahwa properti ini mengklaim bahwa untuk membuktikan kesetaraan dari daftar yang dipesan yang ditentukan melalui pasangan terikat, cukup untuk memeriksa kesetaraan komponen pertama dari pasangan tersebut.
Dikatakan bahwa dalam Arend properti ini mudah diperoleh sebagai konsekuensi dari konstruksi
inProp disebutkan di atas dan properti ekstensionalitas untuk pasangan
SigmaExt bergantung.
\func sorted-equality {A : LinearOrder.Dec} (l1 l2 : SortedList A) (P : l1.1 = l2.1) : l1 = l2 => SigmaPropExt Sorted l1 l2 P
Properti
SigmaPropExt terbukti dalam modul
Paths dari perpustakaan standar, dan banyak fakta lain dari bab kedua
buku HoTT , termasuk
properti ekstensionalitas fungsional , juga terbukti di sana.
Operator
.n digunakan di Arend untuk mengakses proyektor tipe sigma dengan angka n (dalam kasus kami, tipe sigma adalah
SortedList A , dan ekspresi
l1.1 berarti komponen pertama dari tipe ini adalah ekspresi dari tipe
List A ).
2.2 Implementasi properti "menjadi permutasi"
Sekarang mari kita coba menerapkan fungsi pengurutan daftar di Arend. Secara alami, kami ingin memiliki bukan implementasi sederhana dari algoritma pengurutan, tetapi implementasi bersama dengan bukti dari beberapa properti.
Jelas, algoritma ini harus memiliki setidaknya 2 properti:
1. Hasil algoritma harus berupa daftar yang diurutkan.
2. Daftar yang dihasilkan harus permutasi dari daftar asli.
Pertama, mari kita coba menerapkan properti "menjadi permutasi" dari daftar di Arend. Untuk melakukan ini, kami menyesuaikan definisi yang diambil
dari sini untuk Arend.
\truncated \data InsertSpec {A : \Set} (xs : List A) (a : A) (ys : List A) : \Prop \elim xs, ys | xs, :-: y ys => insertedHere (a = y) (xs = ys) | :-: x xs, :-: y ys => insertedThere (x = y) (InsertSpec xs a ys) \truncated \data Perm {A : \Set} (xs ys : List A) : \Prop | permInsert (xs' ys' : List A) (a : A) (Perm xs' ys') (InsertSpec xs' a xs) (InsertSpec ys' a ys) | permTrivial (xs = ys)
Predikat
InsertSpec diperkenalkan oleh kami memiliki arti intuisi berikut:
InsertSpec xs a ys persis berarti bahwa daftar
ys adalah hasil dari memasukkan elemen a di dalam daftar
xs (di posisi mana pun). Dengan demikian,
InsertSpec dapat diambil sebagai spesifikasi dari fungsi insert.
Jelas bahwa tipe data
Perm benar-benar mendefinisikan hubungan "menjadi permutasi": konstruktor
permInsert tepat bahwa
xs dan
ys dapat diijinkan bersama jika
xs dan
ys diperoleh dengan memasukkan elemen yang sama ke dalam beberapa daftar
xs' dan
ys' Panjang lebih pendek, yang sudah permutasi satu sama lain.
Untuk definisi kami tentang properti "menjadi permutasi", mudah untuk memverifikasi properti simetri.
\func Perm-symmetric {A : \Set} {xs ys : List A} (P : Perm xs ys) : Perm ys xs \elim P | permTrivial xs=ys => permTrivial (inv xs=ys) | permInsert perm-xs'-ys' xs-spec ys-spec => permInsert (Perm-symmetric perm-xs'-ys') ys-spec xs-spec
Properti transitivitas juga puas untuk
Perm , tetapi verifikasi jauh lebih rumit. Karena properti ini tidak memainkan peran apa pun dalam penerapan algoritme penyortiran kami, kami serahkan pada pembaca sebagai latihan.
\func Perm-transitive {A : \Set} (xs ys zs : List A) (P1 : Perm xs ys) (P2 : Perm ys zs) : Perm xs zs => {?}
2.3 Perubahan tingkat homotopy jika dibandingkan dengan sampel
Sekarang mari kita coba mengimplementasikan fungsi yang memasukkan elemen ke dalam daftar yang diurutkan sehingga daftar yang dihasilkan tetap terurut. Mari kita mulai dengan implementasi naif berikut.
\func insert {O : LinearOrder.Dec} (xs : List O) (y : O) : List O \elim xs | nil => y :-: nil | :-: x xs' => \case LinearOrder.trichotomy xy \with { | byLeft x=y => x :-: insert xs' y | byRight (byLeft x<y) => x :-: insert xs' y | byRight (byRight y<x) => y :-: x :-: xs' }
Konstruk
\case memungkinkan pencocokan dengan sampel ekspresi arbitrer (
\elim dapat hanya digunakan pada level tertinggi dari definisi fungsi dan hanya untuk parameternya). Jika Anda meminta Arend untuk memeriksa jenis
insert , pesan kesalahan berikut akan ditampilkan.
[ERROR] Data type '||' is truncated to the universe \Prop which does not fit in the universe of the eliminator type: List OE In: | byLeft x-leq-y => x :-: insert xs' y While processing: insert
Masalahnya adalah bahwa di kelas
LinearOrder.Dec definisi
trichotomy diberikan menggunakan operator
|| , yang, pada gilirannya, ditentukan menggunakan pemotongan proposisional. Seperti yang telah disebutkan, untuk tipe yang dimiliki alam semesta
\Prop , pencocokan dengan pola di Arend hanya diperbolehkan jika tipe ekspresi yang dihasilkan itu sendiri merupakan pernyataan (untuk fungsi di atas, hasilnya adalah tipe
List OE , dan tipe ini adalah himpunan).
Apakah ada cara untuk mengatasi masalah ini? Cara termudah untuk menyelesaikan ini adalah mengubah definisi properti trikotomi. Pertimbangkan definisi trikotomi berikut, dengan menggunakan tipe yang tidak terpotong
Or alih-alih
|| terpotong :
\func set-trichotomy {A : StrictPoset} (xy : A) => ((x = y) `Or` (x < y)) `Or` (y < x)
Apakah definisi ini
trichotomy dalam hal apa pun dari definisi
trichotomy asli melalui
|| ? Mengapa kita bahkan menggunakan tipe terpotong proposisi jika hanya mempersulit hidup kita dan mencegah kita menggunakan pencocokan pola?
Mari kita coba menjawab pertanyaan pertama sebagai permulaan: untuk pesanan
StrictPoset ketat
StrictPoset perbedaan antara
trichotomy dan
set-trichotomy sebenarnya tidak sama sekali. Perhatikan bahwa jenis
set-trichotomy adalah pernyataan. Fakta ini mengikuti dari fakta bahwa ketiga alternatif dalam definisi trikotomi adalah saling eksklusif karena aksioma keteraturan, dan masing-masing dari ketiga jenis
x = y, x < y, y < x sendiri merupakan pernyataan (
x = y adalah pernyataan, jadi seperti dalam definisi kelas
BaseSet kami menuntut agar media
E ditetapkan!).
\func set-trichotomy-isProp {A : StrictPoset} (xy : A) (l1 l2 : set-trichotomy xy): l1 = l2 \elim l1, l2 | inl (inl l1), inl (inl l2) => pmap (\lam z => inl (inl z)) (Path.inProp l1 l2) | inl (inr l1), inl (inr l2) => pmap (\lam z => inl (inr z)) (Path.inProp l1 l2) | inr l1, inr l2 => pmap inr (Path.inProp l1 l2) | inl (inl l1), inl (inr l2) => absurd (lt-eq-false l1 l2) | inl (inr l1), inl (inl l2) => absurd (lt-eq-false l2 l1) | inl (inl l1), inr l2 => absurd (lt-eq-false (inv l1) l2) | inr l1, inl (inl l2) => absurd (lt-eq-false (inv l2) l1) | inl (inr l1), inr l2 => absurd (lt-lt-false l1 l2) | inr l1, inl (inr l2) => absurd (lt-lt-false l2 l1) \where { \func lt-eq-false {A : StrictPoset} {xy : A} (l1 : x = y) (l2 : x < y) : Empty => A.<-irreflexive x (transport (x <) (inv l1) l2) \func lt-lt-false {A : StrictPoset} {xy : A} (l1 : x < y) (l2 : y < x) : Empty => A.<-irreflexive x (A.<-transitive _ _ _ l1 l2) }
Dalam daftar di atas,
absurd adalah sebutan untuk prinsip ex falso quodlibet, yang didefinisikan dalam modul
Logic . Karena tipe
Empty tidak memiliki konstruktor dalam definisi (lihat bagian 1.2), tidak perlu melalui kasus dalam definisi
absurd :
\func absurd {A : \Type} (x : Empty) : A
Karena kita sekarang tahu bahwa
set-trichotomy adalah sebuah pernyataan, kita dapat memperoleh properti
set-trichotomy dari properti
trichotomy biasa dari pesanan yang dapat ditentukan. Untuk melakukan ini, kita dapat menggunakan konstruksi
\return \level , yang memberitahu timer Arend bahwa pada titik ini, pencocokan dengan pola adalah operasi yang diizinkan (dalam hal ini, kita harus menunjukkan bukti bahwa hasil dari fungsi
set-trichotomy-property adalah pernyataan).
\func set-trichotomy-property {A : LinearOrder.Dec} (xy : A) : set-trichotomy xy => \case A.trichotomy xy \return \level (set-trichotomy xy) (set-trichotomy-isProp xy) \with { | byLeft x=y => inl (inl x=y) | byRight (byLeft x<y) => inl (inr x<y) | byRight (byRight y<x) => inr (y<x) }
Mari kita coba menjawab pertanyaan kedua, yaitu, mengapa, ketika merumuskan sifat-sifat objek matematika, lebih disukai menggunakan konstruksi yang tidak biasa, tetapi secara proposisi terpotong. Pertimbangkan untuk ini sebuah fragmen dari definisi perintah linear non-linear (definisi lengkap
Lattice dan
TotalOrder dapat ditemukan dalam modul
LinearOrder ):
\class TotalOrder \extends Lattice { | totality (xy : E) : x <= y || y <= x }
Mari kita coba bayangkan sekarang bagaimana arti dari kelas
TotalOrder akan berubah jika kita menulis definisi bidang totalitas melalui konstruksi yang tidak terpotong
Or konstruksi.
\class BadTotalOrder \extends Lattice { | badTotality (xy : E) : (x <= y) `Or` (y <= x) }
Dalam hal ini, tipe
(x <= y) `Or` (y <= x) tidak lagi merupakan pernyataan, karena dalam hal nilai
x dan
y sama
y kedua alternatif dalam definisi
badTotality dapat diimplementasikan, dan pilihan cabang kiri atau kanan dalam bukti
badTotality benar-benar sewenang-wenang dan tetap pada kebijaksanaan pengguna - tidak ada alasan untuk memilih satu
Or konstruktor ke yang lain.
Sekarang sudah jelas apa perbedaan antara
TotalOrder dan
BadTotalOrder . Dua set yang dipesan
O1 O2 :
TotalOrder selalu sama ketika dimungkinkan untuk membuktikan kesetaraan set
O1.E, O2.E dan perintah
O1.<, O2.< Diberikan pada mereka (ini adalah properti yang diinginkan). Di sisi lain, untuk
O1 O2 :
BadTotalOrder untuk membuktikan kesetaraan
O1 dan
O2 hanya ketika, selain semua elemen
x dari
E persamaan
O1.badTotality xx dan
O2.badTotality xx .
Dengan demikian, ternyata kelas
BadTotalOrder secara intuitif perlu dipertimbangkan bukan sebagai "himpunan
BadTotalOrder linear", tetapi sebagai "himpunan
BadTotalOrder linier bersama dengan pilihan untuk setiap elemen
x bidang
E cabang
E cabang kiri atau kanan
Or dalam implementasi
badTotality xx ".
2.4 Sortir Algoritma
Kami sekarang melanjutkan untuk menerapkan algoritma pengurutan. Mari kita coba untuk memperbaiki implementasi naif dari fungsi
insert dari bagian sebelumnya menggunakan properti
set-trichotomy-property terbukti (dalam hal ini, karena pengaturan kurung yang lebih sukses dalam definisi
set-trichotomy , kami telah mengurangi jumlah kasus yang dipertimbangkan).
\func insert {O : LinearOrder.Dec} (xs : List O) (y : O) : List O \elim xs | nil => y :-: nil | :-: x xs' => \case set-trichotomy-property xy \with { | inr y<x => y :-: x :-: xs' | inl x<=y => x :-: insert xs' y }
Sekarang mari kita coba mengimplementasikan analog dari definisi ini untuk daftar yang diurutkan. Kami akan menggunakan konstruksi khusus
\let … \in , yang memungkinkan kami untuk menambahkan variabel lokal baru ke konteksnya.
\func insert {O : LinearOrder.Dec} (xs : SortedList O) (y : O) : SortedList O \elim xs | (nil, _) => (y :-: nil, singletonSorted) | (:-: x xs', xs-sorted) => \case set-trichotomy-property xy \with { | inr y<x => (y :-: x :-: xs', consSorted (byRight y<x) xs-sorted) | inl x<=y => \let (result, result-sorted) => insert (xs', tail-sorted x xs' xs-sorted) y \in (x :-: result, {?})
Kami meninggalkan di bukti fragmen tidak lengkap (ditunjukkan oleh ekspresi
{?} ) Di tempat Anda ingin menunjukkan bahwa daftar
x :-: result dipesan. Meskipun dalam konteks terdapat bukti urutan daftar
result , tetap bagi kami untuk memverifikasi bahwa
x tidak melebihi nilai elemen pertama dari daftar
result , yang tidak begitu mudah untuk diikuti dari tempat dalam konteks (untuk melihat semua tempat dalam target saat ini - inilah yang kami sebut cabang perhitungan sekarang - Anda perlu meminta pemeriksaan jenis dari fungsi
insert ).
Ternyata
insert jauh lebih mudah diimplementasikan jika kita membuktikan urutan daftar yang dihasilkan secara paralel dengan bukti spesifikasi
insert . Ubah tanda tangan
insert dan tulis bukti spesifikasi ini dalam kasus paling sederhana:
\func insert {O : LinearOrder.Dec} (xs : SortedList O) (y : O) : \Sigma (ys : SortedList O) (InsertSpec xs.1 y ys.1) \elim xs | (nil, _) => ((y :-: nil, singletonSorted), insertedHere idp idp) | (:-: x xs', xs-sorted) => \case set-trichotomy-property xy \with { | inr y<x => ((y :-: x :-: xs', consSorted (byRight y<x) xs-sorted), insertedHere idp idp) | inl x<=y => \let ((result, result-sorted), result-spec) => insert (xs', tail-sorted x xs' xs-sorted) y \in ((x :-: result, {?}), insertedThere idp result-spec)
Untuk satu fragmen yang dibiarkan tanpa bukti, Arend akan menampilkan nilai konteks berikut:
Expected type: Sorted (x :-: (insert (\this, tail-sorted x \this \this) \this).1.1) Context: result-sorted : Sorted (insert (\this, tail-sorted \this \this \this) \this).1.1 xs-sorted : Sorted (x :-: xs') x : O x<=y : Or (x = y) (O.< xy) O : Dec result : List O y : O xs' : List O result-spec : InsertSpec xs' y (insert (xs', tail-sorted \this xs' \this) y).1.1
Untuk melengkapi buktinya, kita harus menggunakan
kekuatan penuh dari operator
\case : kita akan menggunakan pencocokan pola dengan 5 variabel berbeda, dan karena tipe-tipe dari beberapa variabel mungkin bergantung pada nilai-nilai variabel lain, kita akan menggunakan pencocokan pola dependen.
Konstruksi usus besar secara eksplisit menunjukkan bagaimana jenis beberapa variabel yang dibandingkan tergantung pada nilai-nilai variabel lain (dengan demikian, dalam jenis variabel
xs-sorted, result-spec dan
result-sorted dalam setiap
\case bukan
xs' dan
result akan cocok dengan sampel yang sesuai).
Konstruk
\return mengaitkan variabel yang digunakan untuk mencocokkan pola dengan jenis hasil yang diharapkan. Dengan kata lain, dalam target saat ini, dalam setiap
\case klausa, sampel yang sesuai akan diganti untuk variabel
result . Tanpa konstruksi ini, penggantian seperti itu tidak akan dilakukan, dan tujuan dari semua klausa
\case akan bertepatan dengan target menggantikan ekspresi
\case itu sendiri.
\func insert {O : LinearOrder.Dec} (xs : SortedList O) (y : O) : \Sigma (ys : SortedList O) (InsertSpec xs.1 y ys.1) \elim xs | (nil, _) => ((y :-: nil, singletonSorted), insertedHere idp idp) | (:-: x xs', xs-sorted) => \case set-trichotomy-property xy \with { | inr y<x => ((y :-: x :-: xs', consSorted (byRight y<x) xs-sorted), insertedHere idp idp) | inl x<=y => \let ((result, result-sorted), result-spec) => insert (xs', tail-sorted x xs' xs-sorted) y \in ((x :-: result, \case result \as result, xs' \as xs', xs-sorted : Sorted (x :-: xs'), result-spec : InsertSpec xs' y result, result-sorted : Sorted result \return Sorted (x :-: result) \with { | nil, _, _, _, _ => singletonSorted | :-: r rs, _, _, insertedHere y=r _, result-sorted => consSorted (transport (\lam z => (x = z) || (x < z)) y=r (Or-to-|| x<=y)) result-sorted | :-: r rs, :-: x' _, consSorted x<=x' _, insertedThere x2=r _, result-sorted => consSorted (transport (\lam z => (x = z) || (x < z)) x2=r x<=x') result-sorted }), insertedThere idp result-spec)
Dalam blok kode di atas, argumen kompleks pertama dari konstruktor yang
consSorted dalam dua paragraf terakhir dari perbandingan pola layak mendapatkan komentar tambahan. Untuk memahami apa arti kedua ekspresi ini, kami menggantinya dengan ekspresi
{?} Dan meminta timer Arend untuk menentukan target di kedua posisi.
Anda dapat melihat bahwa di sana dan di sana target saat ini adalah tipe
(x = r) || O.< xr (x = r) || O.< xr . Selain itu, dalam konteks tujuan pertama, ada premis
x<=y : Or (x = y) (O.< xy) y=r : y = r
dan dalam konteks premis kedua
x<=x' : (x = x') || O.< xx' x2=r : x' = r.
Secara intuitif jelas: untuk membuktikan tujuan pertama, cukup untuk mengganti variabel
r ke dalam pernyataan yang benar
Or (x = y) (O.< xy) , dan kemudian beralih ke tipe terpotong proposisi
|| menggunakan fungsi
Or-to-|| didefinisikan dalam Bagian 1.3 . Untuk membuktikan tujuan kedua, cukup gantikan
(x = x') || O.< x x' (x = x') || O.< x x' bukan variabel
x' variabel
r .
Untuk memformalkan operasi substitusi ekspresi yang dijelaskan, fungsi
transport khusus ada di perpustakaan Arend standar. Pertimbangkan tanda tangannya:
\func transport {A : \Type} (B : A -> \Type) {aa' : A} (p : a = a') (b : B a) : B a'
Dalam kasus kami, alih-alih variabel
A kita perlu mengganti tipe
OE (dapat dihilangkan secara eksplisit jika argumen
transport lainnya ditentukan), dan alih-alih
B ekspresi
\lam (z : O) => (x = z) || (x < z) \lam (z : O) => (x = z) || (x < z) .
Implementasi algoritma penyisipan penyisipan bersama dengan spesifikasi tidak lagi menyebabkan kesulitan khusus: untuk menyortir daftar
x :-: xs' , pertama-tama kita menyortir ujung daftar
xs' menggunakan panggilan rekursif untuk
insertSort , dan kemudian memasukkan elemen
x di dalam daftar ini sambil menjaga pesanan untuk membantu akses ke fungsi
insert sudah diterapkan.
\func insertSort {O : LinearOrder.Dec} (xs : List O) : \Sigma (result : SortedList O) (Perm xs result.1) \elim xs | nil => ((nil, nilSorted), permTrivial idp) | :-: x xs' => \let | (ys, perm-xs'-ys) => insertSort xs' | (zs, zs-spec) => insert ys x \in (zs, permInsert perm-xs'-ys (insertedHere idp idp) zs-spec)
Kami memenuhi tujuan awal dan menerapkan pengurutan daftar di Arend. Seluruh kode Arend yang diberikan dalam paragraf ini dapat diunduh dalam satu file
dari sini .
Orang mungkin bertanya bagaimana kita harus mengubah implementasi dari fungsi
insert jika alih-
LinearOrder.Dec perintah
LinearOrder.Dec ketat kita menggunakan perintah
LinearOrder.Dec yang tidak ketat? Seperti yang kita ingat, dalam definisi fungsi totalitas, penggunaan operasi terpotong
|| cukup signifikan, yaitu definisi ini tidak setara dengan definisi di mana alih-alih
|| digunakan oleh
Or .
Jawaban untuk pertanyaan ini adalah sebagai berikut: masih dimungkinkan untuk membuat analog
insert untuk
TotalOrder , namun, untuk ini kita harus membuktikan bahwa jenis fungsi
insert adalah pernyataan (ini akan memungkinkan kita dalam definisi
insert untuk membuat perbandingan dengan sampel sesuai dengan
totality xy pernyataan).
Dengan kata lain, kita harus membuktikan bahwa hanya ada satu daftar terurut hingga kesetaraan, yang merupakan hasil dari memasukkan elemen
y ke dalam daftar berurutan
xs . Sangat mudah untuk melihat bahwa ini adalah fakta yang benar, tetapi bukti formalnya tidak lagi sepele. Kami meninggalkan verifikasi fakta ini sebagai latihan untuk pembaca yang tertarik.
3. Pengamatan penutup
Dalam pengantar ini, kami berkenalan dengan konstruksi utama bahasa Arend, dan juga belajar bagaimana menggunakan mekanisme kelas. Kami berhasil menerapkan algoritma paling sederhana beserta bukti spesifikasinya. Jadi, kami telah menunjukkan bahwa Arend cukup cocok untuk menyelesaikan masalah "sehari-hari", seperti, misalnya, verifikasi program.
Kami telah menyebutkan jauh dari semua fitur dan fitur Arend. Sebagai contoh, kami hampir tidak mengatakan apa pun tentang
tipe dengan kondisi yang memungkinkan Anda untuk "merekatkan" berbagai konstruktor tipe dengan beberapa nilai parameter khusus untuk konstruktor ini. Misalnya, implementasi tipe integer di Arend diberikan menggunakan tipe dengan ketentuan sebagai berikut:
\data Int | pos Nat | neg Nat \with { zero => pos zero }
Definisi ini mengatakan bahwa bilangan bulat terdiri dari dua salinan dari tipe bilangan alami, di mana nol "positif" dan "negatif" diidentifikasi. Definisi seperti itu jauh lebih nyaman daripada definisi dari perpustakaan Coq standar, di mana "salinan negatif" dari bilangan asli harus "digeser oleh satu" sehingga salinan ini tidak berpotongan (itu jauh lebih nyaman ketika
neg 1 notasi berarti angka -1, tidak -2) .
Kami tidak mengatakan apa-apa tentang algoritma untuk memperoleh tingkat predikatif dan homotopi di kelas dan instance mereka. Kami juga hampir tidak menyebutkan jenis interval
I , meskipun memainkan peran kunci dalam teori jenis dengan interval, yang merupakan dasar logis dari Arend. Untuk memahami betapa pentingnya jenis ini, cukup untuk menyebutkan bahwa dalam jenis Arend, kesetaraan didefinisikan melalui konsep interval. , , , (.. ).
:
,
HoTT JetBrains Research.