Dans la première partie de l'article sur le langage Arend, nous avons examiné les types inductifs les plus simples, les fonctions récursives, les classes et les ensembles.
2. Listes de tri à Arend
2.1 Listes ordonnées à Arend
Nous définissons le type de listes ordonnées comme une paire composée d'une liste et d'une preuve de son ordre. Comme nous l'avons déjà dit, dans Arend, les paires dépendantes sont définies à l'aide du mot clé
\Sigma . Nous donnons la définition du type
Sorted par comparaison avec l'échantillon, inspiré de la définition de l'
article déjà mentionné
sur les listes ordonnées. \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))
Remarque: Arend a pu déduire automatiquement que le type
Sorted est contenu dans l'univers
\Prop . Cela s'est produit parce que les trois modèles de la définition
consSorted s'excluent mutuellement et que le constructeur
consSorted a deux paramètres, qui appartiennent tous deux à
\Prop .
Prouvons une propriété évidente du prédicat
Sorted , disons que la queue d'une liste ordonnée est elle-même une liste ordonnée (cette propriété nous sera utile à l'avenir).
\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
Dans l'
tail-sorted la
tail-sorted nous avons utilisé la correspondance de modèles sur la liste
xs et le prédicat
tail-sorted même temps, en outre, nous avons utilisé le
caractère de saut «_», qui peut être substitué aux variables inutilisées.
On peut se demander s'il est possible à Arend de prouver la propriété des listes ordonnées, mentionnées dans la section 1.3 comme exemple d'un fait qui ne peut être prouvé dans Agda sans annotations d'immatérialité. Rappelons que cette propriété prétend que pour prouver l'égalité des listes ordonnées définies par des paires dépendantes, il suffit de vérifier l'égalité des premiers composants des paires.
On fait valoir que dans Arend cette propriété est facilement obtenue en conséquence de la construction
inProp mentionnée ci-dessus et de la propriété d'extensionnalité pour les paires
SigmaExt dépendantes.
\func sorted-equality {A : LinearOrder.Dec} (l1 l2 : SortedList A) (P : l1.1 = l2.1) : l1 = l2 => SigmaPropExt Sorted l1 l2 P
La propriété
SigmaPropExt prouvée dans le module
Paths de la bibliothèque standard, et de nombreux autres faits du deuxième chapitre
du livre HoTT , y compris la
propriété de l'extensionnalité fonctionnelle , y sont également prouvés.
L'opérateur
.n utilisé dans Arend pour accéder au projecteur de type sigma avec le numéro n (dans notre cas, le type sigma est
SortedList A , et l'expression
l1.1 signifie que le premier composant de ce type est une expression de type
List A ).
2.2 Implémentation de la propriété «be permutation»
Essayons maintenant d'implémenter la fonction de tri de liste sur Arend. Naturellement, nous voulons avoir non pas une simple implémentation de l'algorithme de tri, mais une implémentation avec une preuve de certaines propriétés.
En clair, cet algorithme doit avoir au moins 2 propriétés:
1. Le résultat de l'algorithme doit être une liste ordonnée.
2. La liste résultante doit être une permutation de la liste d'origine.
Tout d'abord, essayons d'implémenter la propriété "be permutation" des listes sur Arend. Pour ce faire, nous adaptons la définition prise
ici pour 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)
Le prédicat
InsertSpec introduit par nous a la signification intuitive suivante:
InsertSpec xs a ys signifie exactement que la liste
ys est le résultat de l'insertion de l'élément a à l'intérieur de la liste
xs (à n'importe quelle position). Ainsi,
InsertSpec peut être considéré comme une spécification de la fonction d'insertion.
De toute évidence, le type de données
Perm définit vraiment la relation «be permutation»: le constructeur
permInsert exactement que
xs et
ys sont mutuellement permutables si
xs et
ys sont obtenus en insérant le même élément a dans certaines listes
xs' et
ys' des longueurs plus courtes, qui sont déjà permutations les unes des autres.
Pour notre définition de la propriété «be permutation», il est facile de vérifier la propriété de symétrie.
\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
La propriété de transitivité est également satisfaite pour
Perm , mais sa vérification est beaucoup plus compliquée. Cette propriété ne jouant aucun rôle dans l'implémentation de notre algorithme de tri, nous laissons le lecteur s'exercer.
\func Perm-transitive {A : \Set} (xs ys zs : List A) (P1 : Perm xs ys) (P2 : Perm ys zs) : Perm xs zs => {?}
2.3 Changement des niveaux d'homotopie par rapport à l'échantillon
Essayons maintenant d'implémenter une fonction qui insère un élément dans une liste ordonnée afin que la liste résultante reste ordonnée. Commençons par l'implémentation naïve suivante.
\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' }
La construction
\case permet la correspondance avec un échantillon d'une expression arbitraire (
\elim ne peut être utilisé qu'au plus haut niveau d'une définition de fonction et uniquement pour ses paramètres). Si vous demandez à Arend de vérifier le type d'
insert , le message d'erreur suivant s'affiche.
[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
Le problème est que dans la classe
LinearOrder.Dec définition de la
trichotomy donnée en utilisant l'opérateur
|| , qui, à son tour, est déterminée à l'aide de la troncature propositionnelle. Comme déjà mentionné, pour les types appartenant à l'univers
\Prop , la correspondance avec un modèle dans Arend n'est autorisée que si le type de l'expression résultante est lui-même une assertion (pour la fonction ci-dessus, le résultat est de type
List OE et ce type est un ensemble).
Existe-t-il un moyen de contourner ce problème? La manière la plus simple de résoudre ce problème consiste à modifier la définition de la propriété de la trichotomie. Considérez la définition suivante de la trichotomie, en utilisant le type non tronqué
Or au lieu du tronqué
|| :
\func set-trichotomy {A : StrictPoset} (xy : A) => ((x = y) `Or` (x < y)) `Or` (y < x)
Cette définition
trichotomy t-elle en quoi que ce soit de la définition originale de
trichotomy par
|| ? Pourquoi avons-nous même utilisé un type propositionnellement tronqué si cela ne fait que compliquer notre vie et nous empêche d'utiliser la correspondance de modèles?
Essayons de répondre à la première question pour commencer: pour les ordres
StrictPoset stricts
StrictPoset différence entre
trichotomy et
set-trichotomy n'est en fait pas du tout. Notez que le type
set-trichotomy est une déclaration. Ce fait découle du fait que les trois alternatives dans la définition de la trichotomie s'excluent mutuellement en raison des axiomes d'ordre, et chacun des trois types
x = y, x < y, y < x est lui-même une déclaration (
x = y est une déclaration, donc comme dans la définition de la classe
BaseSet nous avons exigé que le média
E un ensemble!).
\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) }
Dans la liste ci-dessus,
absurd est la désignation du principe ex falso quodlibet, qui est défini dans le module
Logic . Le type
Empty n'ayant pas de constructeur dans la définition (voir section 1.2), il n'est pas nécessaire de passer par des cas dans la définition d'
absurd :
\func absurd {A : \Type} (x : Empty) : A
Puisque nous savons maintenant que
set-trichotomy est une déclaration, nous pouvons dériver la propriété
set-trichotomy propriété de
trichotomy habituelle des ordres décidables. Pour ce faire, nous pouvons utiliser la construction
\return \level , qui indique au temporisateur Arend qu'à ce stade, la correspondance avec le modèle est une opération autorisée (dans ce cas, nous devons montrer la preuve que le résultat de la fonction
set-trichotomy-property est une instruction).
\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) }
Essayons maintenant de répondre à la deuxième question, à savoir pourquoi il est préférable d'utiliser des constructions non ordinaires, mais propositionnellement tronquées lors de la formulation des propriétés des objets mathématiques. Considérez pour cela un fragment de la définition des ordres linéaires non linéaires (les définitions complètes de
Lattice et
TotalOrder peuvent être trouvées dans le module
LinearOrder ):
\class TotalOrder \extends Lattice { | totality (xy : E) : x <= y || y <= x }
Essayons maintenant d’imaginer comment la signification de la classe
TotalOrder changerait si nous écrivions la définition du champ de totalité par la construction
Or non tronquée.
\class BadTotalOrder \extends Lattice { | badTotality (xy : E) : (x <= y) `Or` (y <= x) }
Dans ce cas, le type
(x <= y) `Or` (y <= x) n'est plus une instruction, car en cas de valeurs égales de
x et
y deux alternatives dans la définition de
badTotality peuvent être mises en œuvre, et le choix de la branche gauche ou droite dans la preuve de
badTotality absolument arbitraire et reste à la discrétion de l'utilisateur - il n'y a aucune raison de préférer un constructeur
Or à un autre.
Maintenant, il est clair quelle est la différence entre
TotalOrder et
BadTotalOrder . Deux ensembles ordonnés
O1 O2 :
TotalOrder sont toujours égaux lorsqu'il est possible de prouver l'égalité des ensembles
O1.E, O2.E et des ordres
O1.<, O2.< Étant donné sur eux (c'est la propriété souhaitée). En revanche, pour
O1 O2 :
BadTotalOrder il est
BadTotalOrder de prouver l'égalité de
O1 et
O2 uniquement lorsque, en plus de tous les éléments
x de
E égalité
O1.badTotality xx et
O2.badTotality xx .
Ainsi, il s'avère que la classe
BadTotalOrder doit intuitivement être considérée non pas comme un "ensemble ordonné linéairement", mais comme un "ensemble ordonné linéairement avec le choix pour chaque élément
x champ
E branche gauche ou droite
Or dans l'implémentation de
badTotality xx ".
2.4 Algorithme de tri
Nous allons maintenant mettre en œuvre l'algorithme de tri. Essayons de corriger l'implémentation naïve de la fonction d'
insert de la section précédente en utilisant la
set-trichotomy-property éprouvée (dans ce cas, en raison de la disposition plus réussie des crochets dans la définition de la
set-trichotomy , nous avons réduit le nombre de cas considérés).
\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 }
Essayons maintenant d'implémenter un analogue de cette définition pour les listes ordonnées. Nous utiliserons la construction spéciale
\let … \in , qui nous permet d'ajouter de nouvelles variables locales au contexte.
\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, {?})
Nous avons laissé dans la preuve un fragment incomplet (indiqué par l'expression
{?} ) À l'endroit où vous souhaitez montrer que la liste
x :-: result ordonnée. Bien qu'il existe des preuves dans le contexte de l'ordre de la liste de
result , il reste à vérifier que
x ne dépasse pas la valeur du premier élément de la liste de
result , ce qui n'est pas si facile à suivre depuis les locaux dans le contexte (pour voir tous les locaux dans la cible actuelle - c'est ce que nous appelons branche actuelle des calculs - vous devez demander une vérification de type à la fonction d'
insert ).
Il s'avère que l'
insert beaucoup plus facile à implémenter si nous prouvons l'ordre de la liste résultante en parallèle avec la preuve de la spécification de l'
insert . Modifiez la signature de l'
insert et écrivez la preuve de cette spécification dans les cas les plus simples:
\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)
Pour un seul fragment laissé sans preuve, Arend affichera la valeur de contexte suivante:
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
Pour compléter la preuve, nous devrons utiliser
toute la puissance de l'opérateur
\case : nous utiliserons la correspondance de modèles avec 5 variables différentes, et puisque les types de certaines variables peuvent dépendre des valeurs d'autres variables, nous utiliserons la correspondance de modèles dépendants.
La construction des deux points indique explicitement comment le type de certaines variables à comparer dépend de la valeur des autres variables (ainsi, dans le type de variables
xs-sorted, result-spec result-sorted par
result-sorted dans chacun des
\case au lieu de
xs' et
result correspondra aux échantillons correspondants).
La construction
\return associe les variables utilisées pour faire correspondre le modèle avec le type de résultat attendu. En d'autres termes, dans la cible actuelle, dans chacune des clauses
\case , l'échantillon correspondant sera substitué à la variable de
result . Sans cette construction, un tel remplacement ne serait pas effectué et l'objectif de toutes les clauses
\case coïnciderait avec la cible à la place de l'expression
\case elle-même.
\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)
Dans le bloc de code ci-dessus, les premiers arguments complexes du constructeur
consSorted dans les deux derniers paragraphes de la comparaison de modèles méritent des commentaires supplémentaires. Pour comprendre ce que ces deux expressions signifient, nous les remplaçons par l'expression
{?} Et demandons au temporisateur Arend de déterminer les cibles aux deux positions.
Vous pouvez voir que là et là la cible actuelle est le type
(x = r) || O.< xr (x = r) || O.< xr . De plus, dans le cadre du premier objectif, il existe des prémisses
x<=y : Or (x = y) (O.< xy) y=r : y = r
et dans le cadre du second - locaux
x<=x' : (x = x') || O.< xx' x2=r : x' = r.
Intuitivement clair: pour prouver le premier objectif, il suffit de substituer la variable
r dans la déclaration correcte
Or (x = y) (O.< xy) , puis de passer au type propositionnellement tronqué
|| en utilisant la fonction
Or-to-|| définie dans la section 1.3 . Pour prouver le deuxième objectif, il suffit de remplacer par
(x = x') || O.< x x' (x = x') || O.< x x' au lieu de la variable
x' variable
r .
Pour formaliser l'opération de substitution d'expression décrite, une fonction de
transport spéciale existe dans la bibliothèque Arend standard. Considérez sa signature:
\func transport {A : \Type} (B : A -> \Type) {aa' : A} (p : a = a') (b : B a) : B a'
Dans notre cas, au lieu de la variable
A nous devons remplacer le type
OE (il peut être omis explicitement si les autres arguments de
transport sont spécifiés), et au lieu de
B , l'expression
\lam (z : O) => (x = z) || (x < z) \lam (z : O) => (x = z) || (x < z) .
La mise en œuvre de l'algorithme de tri par insertion avec la spécification ne pose plus de difficultés particulières: pour trier la liste
x :-: xs' , nous trions d'abord la queue de la liste
xs' aide d'un appel récursif à
insertSort , puis insérons l'élément
x dans cette liste tout en préservant l'ordre lorsque aider à accéder à la fonction d'
insert déjà implémentée.
\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)
Nous avons atteint l'objectif initial et mis en œuvre le tri des listes sur Arend. Le code Arend complet donné dans ce paragraphe peut être téléchargé dans un fichier à
partir d'ici .
On pourrait se demander comment il faudrait changer l'implémentation de la fonction d'
insert si au lieu des ordres
LinearOrder.Dec stricts, nous
LinearOrder.Dec ordres
LinearOrder.Dec non stricts? Comme nous le rappelons, dans la définition de la fonction de totalité, l'utilisation de l'opération tronquée
|| était assez significatif, c'est-à-dire que cette définition n'est pas équivalente à une définition dans laquelle au lieu de
|| utilisé par
Or .
La réponse à cette question est la suivante: il est toujours possible de construire un analogue d'
insert pour
TotalOrder , cependant, pour cela, nous devons prouver que le type de la fonction d'
insert est une instruction (cela nous permettrait dans la définition d'
insert de faire une comparaison avec l'échantillon en fonction de la déclaration de
totality xy ).
Autrement dit, il faudrait prouver qu'il n'y a qu'une seule liste ordonnée jusqu'à égalité, ce qui résulte de l'insertion de l'élément
y dans la liste ordonnée
xs . Il est facile de voir que c'est un fait réel, mais sa preuve formelle n'est plus si triviale. Nous laissons la vérification de ce fait comme exercice au lecteur intéressé.
3. Observations finales
Dans cette introduction, nous nous sommes familiarisés avec les principales constructions du langage Arend et avons également appris à utiliser le mécanisme de classe. Nous avons réussi à implémenter l'algorithme le plus simple avec la preuve de sa spécification. Ainsi, nous avons montré qu'Arend est tout à fait adapté à la résolution de problèmes "quotidiens", comme par exemple la vérification de programme.
Nous avons mentionné loin de toutes les fonctionnalités et fonctionnalités d'Arend. Par exemple, nous n'avons presque rien dit sur les
types avec des conditions qui vous permettent de «coller» divers constructeurs de types avec des valeurs de paramètre spéciales pour ces constructeurs. Par exemple, une implémentation du type entier dans Arend est donnée en utilisant des types avec des conditions comme suit:
\data Int | pos Nat | neg Nat \with { zero => pos zero }
Cette définition dit que les entiers sont constitués de deux copies du type de nombres naturels, dans lesquels des zéros "positifs" et "négatifs" sont identifiés. Une telle définition est beaucoup plus pratique que la définition de la bibliothèque Coq standard, où la «copie négative» des nombres naturels doit être «décalée d'une» afin que ces copies ne se recoupent pas (c'est beaucoup plus pratique lorsque la notation
neg 1 signifie le nombre -1, pas -2) .
Nous n'avons rien dit sur l'algorithme de dérivation des niveaux de prédiction et d'homotopie dans les classes et leurs instances. Nous avons également à peine mentionné le type d'intervalle
I , bien qu'il joue un rôle clé dans la théorie des types avec intervalles, qui sont la base logique d'Arend. Pour comprendre l'importance de ce type, il suffit de mentionner que dans le type Arend, l'égalité est définie par le concept d'un intervalle. , , , (.. ).
:
,
HoTT JetBrains Research.