Formaliser la théorie des ensembles finis en théorie des types

10

La plupart des assistants de preuve ont formalisé le concept de "jeu fini". Ces formalisations diffèrent cependant énormément (même si l'on espère qu'elles sont toutes essentiellement équivalentes!). Ce que je ne comprends pas à ce stade, c'est l'espace de conception impliqué et quels sont les avantages et les inconvénients de chaque formalisation.

En particulier, je voudrais comprendre ce qui suit:

  • Puis-je axiomatiser des ensembles finis (c'est-à-dire des types habités par un nombre fini d'habitants) dans la théorie des types simples? Système F? Quels sont les inconvénients de procéder de cette façon?
  • Je sais que cela peut être fait «avec élégance» dans un système typé de manière dépendante. Mais, d'un point de vue classique, les définitions qui en résultent semblent extrêmement étrangères. [Je ne dis pas qu'ils ont tort, loin de là!]. Mais je ne comprends pas non plus pourquoi ils ont «raison». Je comprends qu'ils choisissent le bon concept, mais la raison profonde pour «le dire ainsi» est ce que je ne saisis pas complètement.

Fondamentalement, je voudrais une introduction raisonnée à l'espace de conception des formalisations du concept d '«ensemble fini» dans la théorie des types.

Jacques Carette
la source

Réponses:

8

Je sais que cela peut être fait «avec élégance» dans un système typé de manière dépendante. Mais, d'un point de vue classique, les définitions qui en résultent semblent extrêmement étrangères.

Pouvez-vous expliquer ce que vous entendez par «étranger»? Il me semble que vous formalisez le concept d'ensemble fini exactement de la même manière en théorie des types et en théorie des ensembles.

Fin(n)

Fin(n){kN|k<n}
Finite(X)nN.XFin(n)
AB

En théorie des types, vous pouvez faire exactement la même chose! Notez que est un type avec éléments (puisque le deuxième composant de la paire n'est pas pertinent pour la preuve). Ensuite, vous pouvez définir le constructeur du type de finitude comme: Où signifie l'isomorphisme des types.

Fin(n)Σk:N.ifk<nthenUnitelseVoid
Fin(n)n
Finite(X)Σn:N.XFin(n)
AB
Neel Krishnaswami
la source
Extraterrestre parce que je n'ai vu que les définitions brutes sans test d'accompagnement qui explique comment lire ces définitions. De plus, le fait que la définition habituelle de Fin, effectuée par induction, obscurcit davantage les choses. Votre courte explication est ce dont j'avais besoin pour le faire cliquer.
Jacques Carette
5

Voyons si je peux ajouter quelque chose d'utile à la réponse de Neel. L '"espace de conception" pour les ensembles finis est beaucoup plus vaste de manière constructive qu'il ne l'est classiquement parce que diverses définitions de "fini" n'ont pas besoin de s'accorder de manière constructive. Diverses définitions de la théorie des types donnent des concepts légèrement différents. Voici quelques possibilités.

Les ensembles finis de Kuratowski ( -finite) peuvent être caractérisés comme des -semilattices libres: étant donné un ensemble, un type ou un objet , les éléments du libre -semilattice peuvent être des sous-ensembles finis de . En effet, chacun de ces éléments est généré par:KXK(X)X

  • l'élément neutre , qui correspond à l'ensemble vide, ou0
  • un générateur , qui correspond au singleton , ouxX{x}
  • une jointure de deux éléments, ce qui correspond à une union.ST

Une formulation équivalente de est: est -fini si, et seulement si, il existe et une surjection .K(X)SXKnN e:{1,,n}S

Si l' on compare cela avec la définition de Neel on voit qu'il a besoin d' un bijection . Cela revient à prendre les -sous-ensembles finis qui ont une égalité décidable: . Utilisons pour la collecte des décidable sous - ensembles -finite de .e:{1,,n}SKSXx,yS.x=yxyD(X)KX

Évidemment, est fermé sous des unions finies, mais il n'a pas besoin d'être fermé sous des intersections finies. Et n'est fermé sous aucune opération. Étant donné que les gens s'attendent à ce que les ensembles finis se comportent un peu comme une "aglèbre booléenne sans sommet", on pourrait également essayer de les définir comme l'algèbre booléenne généralisée libre ( , , et compléments relatifs ), mais en fait je n'ai jamais entendu parler d'un tel effort.K(X)D(X)0

Pour décider de la définition «correcte», vous devez faire attention à ce que vous voulez faire avec les ensembles finis. Et il n'y a pas de définition correcte unique. Par exemple, dans quel sens de «fini» est l'ensemble des racines complexes d'un polynôme fini ?

Voir Constructivement fini? par Thierry Coquand et Arnaud Spiwack pour une discussion détaillée de la finitude. La leçon est que la finitude est loin d'être évidente de manière constructive.

Andrej Bauer
la source
Bon, j'en savais juste assez pour savoir que ma question n'était pas banale. Maintenant, je peux aller relire les parties des bibliothèques Coq, Isabelle et Agda qui traitent des ensembles finis et espérer comprendre quels choix (jeu de mots voulu) ils ont faits.
Jacques Carette
Je me demande dans quelle mesure les auteurs des bibliothèques étaient conscients des choix. Ils sont probablement entrés dans l'une des définitions. Une chose naturelle à faire est de supposer que a une égalité décidable car alors coïncide avec et tout se passe bien et un peu comme dans le cas classique. Le problème commence une fois que n'a pas d'égalité décidable. AK(A)D(A)A
Andrej Bauer
Pour être juste, on utilise souvent des ensembles finis pour formaliser les aspects de la vérification du programme, et dans ce cas, vous pouvez généralement supposer que l'égalité décidable est valable.
cody