Im ersten Teil des Artikels über die Arend-Sprache haben wir die einfachsten induktiven Typen, rekursiven Funktionen, Klassen und Mengen untersucht.
2. Sortieren von Listen in Arend
2.1 Bestellte Listen in Arend
Wir definieren den Typ der geordneten Listen als ein Paar, das aus einer Liste und einem Nachweis ihrer Reihenfolge besteht. Wie bereits erwähnt, werden in Arend abhängige Paare mit dem Schlüsselwort
\Sigma definiert. Wir geben die Definition des
Sorted Typs durch Vergleich mit der Stichprobe an, inspiriert von der Definition aus dem bereits erwähnten
Artikel über geordnete Listen. \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))
Hinweis: Arend konnte automatisch schließen, dass der
Sorted Typ im
\Prop Universum enthalten ist. Dies geschah, weil sich alle drei Muster in der
Sorted Definition gegenseitig ausschließen und der
consSorted Konstruktor zwei Parameter hat, die beide zu
\Prop .
Lassen Sie uns eine offensichtliche Eigenschaft des
Sorted Prädikats beweisen, sagen wir, dass das Ende einer geordneten Liste selbst eine geordnete Liste ist (diese Eigenschaft wird uns in Zukunft nützlich sein).
\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
In der nach
tail-sorted wir gleichzeitig den Mustervergleich für die
xs Liste und das
Sorted Prädikat verwendet. Außerdem haben wir das
Überspringzeichen "_"
verwendet , das nicht verwendete Variablen ersetzen kann.
Man kann sich fragen, ob es in Arend möglich ist, die Eigenschaft geordneter Listen zu beweisen, die in Abschnitt 1.3 als Beispiel für eine Tatsache erwähnt werden, die in Agda ohne Anmerkungen zur Immaterialität nicht bewiesen werden kann. Denken Sie daran, dass diese Eigenschaft behauptet, dass es ausreicht, die Gleichheit der ersten Komponenten der Paare zu überprüfen, um die Gleichheit der durch abhängige Paare definierten geordneten Listen zu beweisen.
Es wird argumentiert, dass in Arend diese Eigenschaft als Folge der
inProp erwähnten
inProp Konstruktion und der Extensionalitätseigenschaft für abhängige
SigmaExt Paare leicht erhalten werden kann.
\func sorted-equality {A : LinearOrder.Dec} (l1 l2 : SortedList A) (P : l1.1 = l2.1) : l1 = l2 => SigmaPropExt Sorted l1 l2 P
Die
SigmaPropExt Eigenschaft
SigmaPropExt im
Paths- Modul der Standardbibliothek bewiesen. Dort werden auch viele andere Fakten aus dem zweiten Kapitel
des HoTT-Buches , einschließlich der
Eigenschaft der funktionalen Erweiterbarkeit , bewiesen.
Der Operator
.n in Arend verwendet, um auf den Sigma-Projektor mit der Nummer n zuzugreifen (in unserem Fall ist der Sigma-Typ
SortedList A , und der Ausdruck
l1.1 bedeutet, dass die erste Komponente dieses Typs ein Ausdruck vom Typ
List A ).
2.2 Implementierung der Eigenschaft "be permutation"
Versuchen wir nun, die Listensortierfunktion in Arend zu implementieren. Natürlich wollen wir keine einfache Implementierung des Sortieralgorithmus, sondern eine Implementierung zusammen mit einem Nachweis einiger Eigenschaften.
Dieser Algorithmus muss mindestens zwei Eigenschaften haben:
1. Das Ergebnis des Algorithmus sollte eine geordnete Liste sein.
2. Die resultierende Liste sollte eine Permutation der ursprünglichen Liste sein.
Versuchen wir zunächst, die Eigenschaft "be permutation" von Listen in Arend zu implementieren. Dazu passen wir die Definition
von hier für Arend an.
\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)
Das von uns eingeführte
InsertSpec Prädikat hat die folgende intuitive Bedeutung:
InsertSpec xs a ys bedeutet genau, dass die Liste
ys das Ergebnis des Einfügens des Elements a in die Liste
xs (an einer beliebigen Position) ist. Somit kann
InsertSpec als Spezifikation der
InsertSpec verwendet werden.
Es ist klar, dass der Datentyp
Perm tatsächlich die Beziehung "be permutation" definiert: Der Konstruktor
permInsert genau an, dass
xs und
ys für beide Seiten durchlässig sind, wenn
xs und
ys erhalten werden, indem dasselbe Element a in einige Listen
xs' und
ys' kürzere Längen, die bereits Permutationen voneinander sind.
Für unsere Definition der Eigenschaft "be permutation" ist es einfach, die Symmetrieeigenschaft zu überprüfen.
\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
Die Transitivitätseigenschaft ist auch für
Perm erfüllt, aber ihre Überprüfung ist viel komplizierter. Da diese Eigenschaft bei der Implementierung unseres Sortieralgorithmus keine Rolle spielt, überlassen wir sie dem Leser als Übung.
\func Perm-transitive {A : \Set} (xs ys zs : List A) (P1 : Perm xs ys) (P2 : Perm ys zs) : Perm xs zs => {?}
2.3 Änderung der Homotopie im Vergleich zur Probe
Versuchen wir nun, eine Funktion zu implementieren, die ein Element in eine geordnete Liste einfügt, damit die resultierende Liste geordnet bleibt. Beginnen wir mit der folgenden naiven Implementierung.
\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' }
Das
\case Konstrukt ermöglicht den Abgleich mit einer Stichprobe eines beliebigen Ausdrucks (
\elim kann nur auf der höchsten Ebene einer Funktionsdefinition und nur für deren Parameter verwendet werden). Wenn Sie Arend bitten, den Einfügetyp zu überprüfen, wird die folgende Fehlermeldung angezeigt.
[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
Das Problem ist, dass in der
LinearOrder.Dec Klasse
LinearOrder.Dec Definition der
trichotomy mit dem Operator
|| wird , die wiederum unter Verwendung von Satzkürzungen bestimmt wird. Wie bereits erwähnt, ist für Typen, die zum
\Prop Universum gehören, die Übereinstimmung mit einem Muster in Arend nur zulässig, wenn der Typ des resultierenden Ausdrucks selbst eine Behauptung ist (für die obige Funktion ist das Ergebnis vom Typ
List OE , und dieser Typ ist eine Menge).
Gibt es einen Weg um dieses Problem herum? Der einfachste Weg, dies zu lösen, besteht darin, die Definition der Eigenschaft der Trichotomie zu ändern. Betrachten Sie die folgende Definition der Trichotomie unter Verwendung des nicht abgeschnittenen Typs
Or anstelle des abgeschnittenen
|| ::
\func set-trichotomy {A : StrictPoset} (xy : A) => ((x = y) `Or` (x < y)) `Or` (y < x)
trichotomy diese Definition in irgendetwas von der ursprünglichen
trichotomy Definition durch
|| ? Warum haben wir überhaupt einen propositionell abgeschnittenen Typ verwendet, wenn dies unser Leben nur kompliziert und uns daran hindert, Mustervergleiche zu verwenden?
Versuchen wir zunächst, die erste Frage zu beantworten: Bei strengen
StrictPoset Ordnungen
StrictPoset Unterschied zwischen
trichotomy und
set-trichotomy eigentlich gar nicht. Beachten Sie, dass der
set-trichotomy Typ eine Aussage ist. Diese Tatsache folgt aus der Tatsache, dass sich alle drei Alternativen in der Definition der Trichotomie aufgrund von Ordnungsaxiomen gegenseitig ausschließen und jeder der drei Typen
x = y, x < y, y < x selbst eine Aussage ist (
x = y ist also eine Aussage Wie in der Definition der
BaseSet Klasse
BaseSet wir gefordert, dass das Medium
E eine Menge ist!).
\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) }
absurd ist in der obigen Auflistung die Bezeichnung für das Ex-Falso-Quodlibet-Prinzip, das im Logikmodul definiert ist. Da der
Empty Typ keine Konstruktoren in der Definition enthält (siehe Abschnitt 1.2), ist es nicht erforderlich, Fälle in der Definition von
absurd :
\func absurd {A : \Type} (x : Empty) : A
Da wir jetzt wissen, dass die
set-trichotomy eine Aussage ist, können wir die
set-trichotomy Eigenschaft aus der üblichen
trichotomy Eigenschaft entscheidbarer Ordnungen ableiten. Dazu können wir die Konstruktion
\return \level verwenden, die dem Arend-Timer mitteilt, dass zu diesem Zeitpunkt der Mustervergleich eine zulässige Operation ist (in diesem Fall müssen wir beweisen, dass das Ergebnis der Funktion
set-trichotomy-property eine Anweisung ist).
\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) }
Versuchen wir nun, die zweite Frage zu beantworten, nämlich warum es bei der Formulierung der Eigenschaften mathematischer Objekte vorzuziehen ist, nicht gewöhnliche, sondern propositionell verkürzte Konstruktionen zu verwenden. Betrachten Sie dazu ein Fragment der Definition nichtlinearer linearer Ordnungen (vollständige Definitionen von
Lattice und
TotalOrder finden Sie im
LinearOrder- Modul):
\class TotalOrder \extends Lattice { | totality (xy : E) : x <= y || y <= x }
Versuchen wir uns jetzt vorzustellen, wie sich die Bedeutung der
TotalOrder Klasse ändern würde, wenn wir die Definition des Totalitätsfelds durch die nicht abgeschnittene
Or Konstruktion
TotalOrder würden.
\class BadTotalOrder \extends Lattice { | badTotality (xy : E) : (x <= y) `Or` (y <= x) }
In diesem Fall ist der Typ
(x <= y) `Or` (y <= x) keine Aussage mehr, weil Bei gleichen Werten von
x und
y beide Alternativen bei der Definition von
badTotality implementiert werden, und die Wahl des linken oder rechten Zweigs beim Nachweis von
badTotality absolut willkürlich und liegt im Ermessen des Benutzers - es gibt keinen Grund, einen
Or Konstruktor einem anderen vorzuziehen.
Jetzt ist klar, was der Unterschied zwischen
TotalOrder und
BadTotalOrder . Zwei geordnete Mengen
O1 O2 :
TotalOrder sind immer gleich, wenn es möglich ist, die Gleichheit der Mengen
O1.E, O2.E und der Ordnungen
O1.<, O2.< Zu beweisen (dies ist die gewünschte Eigenschaft). Andererseits ist es für
O1 O2 :
BadTotalOrder nur
BadTotalOrder , die Gleichheit von
O1 und
O2 zu beweisen, wenn zusätzlich zu allen Elementen
x aus
E Gleichheit
O1.badTotality xx und
O2.badTotality xx .
Es stellt sich also heraus, dass die Klasse
BadTotalOrder intuitiv nicht als "linear geordnete Menge" betrachtet werden muss, sondern als "linear geordnete Menge zusammen mit der Auswahl für jedes Element
x Feldes
E linken oder rechten Zweigs
Or bei der Implementierung von
badTotality xx ".
2.4 Sortieralgorithmus
Wir fahren nun mit der Implementierung des Sortieralgorithmus fort. Versuchen wir, die naive Implementierung der
insert Funktion aus dem vorherigen Abschnitt mithilfe der bewährten
set-trichotomy-property (in diesem Fall haben wir aufgrund der erfolgreicheren Anordnung von Klammern bei der Definition der
set-trichotomy die Anzahl der berücksichtigten Fälle reduziert).
\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 }
Versuchen wir nun, ein Analogon dieser Definition für geordnete Listen zu implementieren. Wir werden das spezielle Konstrukt
\let … \in verwenden, mit dem wir dem Kontext neue lokale Variablen hinzufügen können.
\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, {?})
Wir haben im Beweis ein unvollständiges Fragment hinterlassen (angezeigt durch den Ausdruck
{?} ). An der Stelle, an der Sie zeigen möchten, dass das
x :-: result der Liste
x :-: result geordnet ist. Obwohl es im Kontext Hinweise auf die Reihenfolge der
result , müssen wir überprüfen, ob
x den Wert des ersten Elements der
result nicht überschreitet, was von den Prämissen im Kontext nicht so einfach zu verfolgen ist (um alle Prämissen im aktuellen Ziel zu sehen - das nennen wir Derzeitiger Berechnungszweig - Sie müssen die Typprüfung bei der
insert anfordern.
Es stellt sich heraus, dass das
insert viel einfacher zu implementieren ist, wenn wir die Reihenfolge der resultierenden Liste parallel zum Nachweis der
insert . Ändern Sie die Unterschrift der
insert und schreiben Sie in den einfachsten Fällen den Nachweis dieser Spezifikation:
\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)
Für ein einzelnes Fragment ohne Beweis gibt Arend den folgenden Kontextwert aus:
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
Um den Beweis zu vervollständigen, müssen wir
die volle Leistung des Operators
\case : Wir werden den Mustervergleich mit 5 verschiedenen Variablen verwenden, und da die Typen einiger Variablen von den Werten anderer Variablen abhängen können, werden wir den abhängigen Mustervergleich verwenden.
Die Doppelpunktkonstruktion gibt explizit an, wie der Typ einiger verglichener Variablen von den Werten anderer Variablen abhängt (also in der Art der Variablen
xs-sorted, result-spec und
result-sorted in jedem von
\case anstelle von
xs' und
result stimmt mit den entsprechenden Stichproben überein).
Das Konstrukt
\return ordnet die Variablen, die zum Abgleichen des Musters verwendet werden, dem Typ des erwarteten Ergebnisses zu. Mit anderen Worten, im aktuellen Ziel wird in jeder der
\case Klauseln die entsprechende Stichprobe durch die entsprechende Stichprobe ersetzt. Ohne diese Konstruktion würde eine solche Ersetzung nicht durchgeführt, und das Ziel aller
\case Klauseln würde mit dem Ziel anstelle des
\case Ausdrucks selbst übereinstimmen.
\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)
Im obigen Codeblock verdienen die komplexen ersten Argumente des
consSorted Konstruktors in den letzten beiden Absätzen des Mustervergleichs einen zusätzlichen Kommentar. Um zu verstehen, was diese beiden Ausdrücke bedeuten, ersetzen wir sie durch den Ausdruck
{?} Und bitten den Arend-Timer, Ziele an beiden Positionen zu bestimmen.
Sie können sehen, dass sowohl dort als auch dort das aktuelle Ziel der Typ
(x = r) || O.< xr (x = r) || O.< xr . Darüber hinaus gibt es im Rahmen des ersten Ziels Prämissen
x<=y : Or (x = y) (O.< xy) y=r : y = r
und im Kontext der zweiten Prämisse
x<=x' : (x = x') || O.< xx' x2=r : x' = r.
Intuitiv klar: Um das erste Ziel zu beweisen, reicht es aus, die Variable
r durch die richtige Aussage
Or (x = y) (O.< xy) zu ersetzen und dann zum propositionell abgeschnittenen Typ
|| wechseln Verwenden der in Abschnitt 1.3 definierten
Or-to-|| -Funktion . Um das zweite Ziel zu beweisen, setzen Sie einfach
(x = x') || O.< x x' (x = x') || O.< x x' anstelle der Variablen
x' Variable
r .
Zur Formalisierung der beschriebenen Ausdruckssubstitutionsoperation existiert in der Standard-Arend-Bibliothek eine spezielle
transport . Betrachten Sie ihre Unterschrift:
\func transport {A : \Type} (B : A -> \Type) {aa' : A} (p : a = a') (b : B a) : B a'
In unserem Fall müssen wir anstelle der Variablen
A den Typ
OE ersetzen (er kann explizit weggelassen werden, wenn die anderen
transport angegeben werden) und anstelle von
B den Ausdruck
\lam (z : O) => (x = z) || (x < z) \lam (z : O) => (x = z) || (x < z) .
Die Implementierung des Einfügungssortierungsalgorithmus zusammen mit der Spezifikation verursacht keine besonderen Schwierigkeiten mehr: Um die Liste
x :-: xs' zu sortieren, sortieren wir zuerst den Schwanz der Liste
xs' mit einem rekursiven Aufruf von
insertSort und fügen dann das Element
x in diese Liste ein, wobei die Reihenfolge für
insertSort wird Hilfe beim Zugriff auf die bereits implementierte
insert .
\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)
Wir haben das ursprüngliche Ziel erreicht und die Sortierung der Listen auf Arend implementiert. Der gesamte in diesem Absatz angegebene Arend-Code kann
von hier aus in einer Datei heruntergeladen
werden .
Man könnte sich fragen, wie man die Implementierung der
LinearOrder.Dec ändern müsste, wenn wir anstelle der strengen
LinearOrder.Dec Befehle die nicht strengen
TotalOrder Befehle verwenden würden. Wie wir uns erinnern, wird bei der Definition der Totalitätsfunktion die Verwendung der abgeschnittenen Operation
|| war ziemlich bedeutsam, das heißt, diese Definition entspricht nicht einer Definition, in der anstelle von
|| verwendet von
Or .
Die Antwort auf diese Frage lautet wie folgt: Es ist immer noch möglich, ein
insert Analogon für
TotalOrder zu
TotalOrder . Dazu müssten wir jedoch beweisen, dass der Typ der
insert Funktion eine Anweisung ist (dies würde es uns bei der Definition von
insert , mit der Stichprobe gemäß der
totality xy Anweisung
totality xy ).
Mit anderen Worten, wir müssten beweisen, dass es nur eine geordnete Liste bis zur Gleichheit gibt, was das Ergebnis des Einfügens des Elements
y in die geordnete Liste
xs . Es ist leicht zu erkennen, dass dies eine wahre Tatsache ist, aber der formale Beweis ist nicht mehr so trivial. Wir überlassen die Überprüfung dieser Tatsache dem interessierten Leser als Übung.
3. Schlussbemerkungen
In dieser Einführung haben wir die Hauptkonstrukte der Arend-Sprache kennengelernt und auch gelernt, wie man den Klassenmechanismus verwendet. Es ist uns gelungen, den einfachsten Algorithmus zusammen mit dem Nachweis seiner Spezifikation zu implementieren. So haben wir gezeigt, dass Arend gut zur Lösung "alltäglicher" Probleme geeignet ist, wie zum Beispiel zur Programmüberprüfung.
Wir haben weit entfernt von allen Funktionen und Merkmalen von Arend erwähnt. Zum Beispiel haben wir fast nichts über
Typen mit Bedingungen gesagt, die es Ihnen ermöglichen, verschiedene Typkonstruktoren mit einigen speziellen Parameterwerten für diese Konstruktoren zu „kleben“. Beispielsweise wird eine Implementierung des Integer-Typs in Arend unter Verwendung von Typen mit folgenden Bedingungen angegeben:
\data Int | pos Nat | neg Nat \with { zero => pos zero }
Diese Definition besagt, dass ganze Zahlen aus zwei Kopien des Typs natürlicher Zahlen bestehen, in denen "positive" und "negative" Nullen identifiziert werden. Eine solche Definition ist viel praktischer als die Definition aus der Standard-Coq-Bibliothek, bei der die „negative Kopie“ natürlicher Zahlen „um eins verschoben“ werden muss, damit sich diese Kopien nicht überschneiden (es ist viel bequemer, wenn die Notation
neg 1 die Zahl -1, nicht -2 bedeutet). .
Wir haben nichts über den Algorithmus zum Ableiten von Prädikativ- und Homotopieebenen in Klassen und deren Instanzen gesagt. Wir haben auch die Art des Intervalls
I kaum erwähnt, obwohl es eine Schlüsselrolle in der Theorie der Typen mit Intervallen spielt, die die logische Grundlage von Arend sind. Um zu verstehen, wie wichtig dieser Typ ist, muss erwähnt werden, dass in Arend die Typgleichheit durch das Konzept eines Intervalls definiert wird. , , , (.. ).
:
,
HoTT JetBrains Research.