Quelle est exactement la différence sémantique entre set et type?

33

EDIT: J'ai maintenant posé une question similaire sur la différence entre les catégories et les ensembles.

Chaque fois que je lis sur la théorie du type (qui est certes plutôt informelle), je ne peux pas vraiment comprendre comment elle diffère de la théorie des ensembles, concrètement .

Je comprends qu’il existe une différence conceptuelle entre dire "x appartient à un ensemble X" et "x est de type X", car intuitivement, un ensemble est simplement une collection d’objets, alors qu’un type a certaines "propriétés". Néanmoins, les ensembles sont souvent définis en fonction des propriétés également, et s'ils le sont, j'ai du mal à comprendre en quoi cette distinction est importante.

Ainsi , dans le plus concret façon possible, qu'est-ce exactement cela implique au sujet de x à dire qu'il est de type , par rapport à dire qu'il est un élément dans l'ensemble ?TS

(Vous pouvez choisir n’importe quel type et jeu qui rend la comparaison plus précise).

utilisateur56834
la source
Quel est le contexte dans lequel vous utilisez / entendez le mot "type"? Est-ce, comme votre nom l'indique, des langages de programmation? Parce que je pense que les réponses ci-dessous supposent le contraire.
einpoklum - réintègre Monica le
@einpoklum, je ne suis pas sûr à 100% de savoir comment décrire le "contexte", mais quelque chose du genre: J'essaie de comprendre le rôle des types en mathématiques. Les ensembles (à mon avis) ont essentiellement deux contextes: d’abord, ils servent de collections d’objets utilisés pour les mathématiques quotidiennes. parler des mathématiques dans la logique du premier ordre, en laissant les ensembles correspondre à des fonctions et à des nombres, etc. Je m'intéresse principalement à la relation entre "set" dans le premier sens et "type".
user56834
Le rôle de quels types? Les types que vous voyez dans les papiers de mathématiques / manuels, ou les types de variables dans les programmes informatiques?
einpoklum - réintègre Monica le
1
@einpoklum, cette question concerne les articles de mathématiques. (Bien qu'il m'intéresse aussi de connaître la différence fondamentale entre les types en mathématiques et les types dans les langages de programmation, s'il en existe. Mais ce n'était pas le propos de cette question).
user56834

Réponses:

29

Pour comprendre la différence entre les séries et les types, les doit revenir à pré idées -mathematical de « collection » et « construction », et voir comment les ensembles et les types mathématiser ceux - ci.

Il existe un large éventail de possibilités sur le sujet des mathématiques. Deux d'entre eux sont:

  1. Nous pensons que les mathématiques sont une activité dans laquelle les objets mathématiques sont construits selon certaines règles (pensez à la géométrie en tant qu'activité de construction de points, de lignes et de cercles avec une règle et une boussole). Ainsi, les objets mathématiques sont organisés en fonction de la manière dont ils sont construits et il existe différents types de construction. Un objet mathématique est toujours construit dans une façon unique, qui détermine son type unique.

  2. Nous pensons aux mathématiques comme à un vaste univers rempli d'objets mathématiques préexistants (pensez au plan géométrique comme étant donné). Nous découvrons, analysons et pensons à propos de ces objets (nous observons qu'il y a des points, des lignes et des cercles dans le plan). Nous les recueillons en set . Habituellement, nous collectons des éléments qui ont quelque chose en commun (par exemple, toutes les lignes passant par un point donné), mais en principe, un ensemble peut contenir une sélection arbitraire d'objets. Un ensemble est spécifié par ses éléments et uniquement par ses éléments. Un objet mathématique peut appartenir à plusieurs ensembles.

Nous ne disons pas que les possibilités ci-dessus sont les deux seules, ni que l’un d’entre elles décrit complètement ce que sont les mathématiques. Néanmoins, chaque vue peut servir de point de départ utile à une théorie mathématique générale décrivant utilement un large éventail d'activités mathématiques.

Il est naturel de prendre un type et imaginez la collecte de toutes les choses que nous pouvons construire en utilisant les règles de T . C'est l' extension de T , et ce n'est pas T lui-même. Par exemple, voici deux types qui ont des règles de construction différentes, mais qui ont la même extension:TTT T

  1. Le type de paires n est construit sous forme de nombre naturel et p est construit sous forme de preuve démontrant que n est un nombre premier pair supérieur à 3 .(n,p)npn3

  2. Le type de paires m est construit sous la forme d'un nombre naturel et q est construit comme une preuve démontrant que m est un nombre impair inférieur à 2 .(m,q)mqm2

Oui, ce sont des exemples triviaux et ridicules, mais le problème est clair: les deux types n’ont rien dans leur extension, mais ils ont des règles de construction différentes. En revanche, les ensembles et { m N | m  est un nombre impair premier inférieur à  2 } sont égaux parce qu'ils ont les mêmes éléments.

{nN|n est un nombre premier plus grand que 3}
{mN|m est un nombre impair plus petit que 2}

Notez que la théorie des types ne concerne pas la syntaxe. C'est une théorie mathématique des constructions, tout comme la théorie des ensembles est une théorie mathématique des collections. Il se trouve que les présentations habituelles de la théorie des types mettent l’accent sur la syntaxe et, par conséquent, les gens finissent par penser que la théorie des types est la syntaxe. Ce n'est pas le cas. Confondre un objet mathématique (construction) avec une expression syntaxique qui le représente (un terme ancien) est une erreur de catégorie de base qui a longtemps laissé perplexe les logiciens, mais plus maintenant.

Andrej Bauer
la source
1
Magnifique merci! Pourriez-vous clarifier un détail? quand vous listez les deux types dont les extensions sont toutes deux vides, vous dites que "le type dont les éléments sont ...". Purement pour ma clarté, est-ce une manière 100% correcte de le dire? Vous avez dit dans la phrase précédente qu'un type n'est pas une collection, il semble donc qu'il ne puisse pas avoir d '"éléments" (que j'associe à des ensembles). En gros, comme vous l'avez écrit maintenant, c'est comme si vous définissiez le Type en fonction de l'ensemble qui en est l'extension. Si vous ne le vouliez pas, pourriez-vous les reformuler plus précisément pour capturer leur idée en tant que types?
user56834
L' extension d'un type est un concept très utile, et puisqu'il s'agit d'une sorte de collection, on peut dire "élément de l'extension d'un type". C'est fastidieux et souvent abrégé en "élément de type". J'ai supprimé le libellé pour réduire les risques de confusion, mais attention, c'est une terminologie courante.
Andrej Bauer
Merci, cela clarifie. Donc, pour faire un suivi, est-il correct de dire ce qui suit? Dire qu'un objet est "de type T" signifie la même chose que, que l'objet est "un élément de l'extension de T", de sorte qu'il existe une surjection naturelle des types aux ensembles. Mais l'inverse ne tient pas, car n'importe quel jeu peut être construit de plusieurs manières. Essentiellement, la différence entre jeu et le type n'est pas important dans la perspective d'un objet particulier , dans le sens où x : T et x X T (où X T est l'extension de T ) nous donne les mêmes informations exactes sur x . Cependant,XX:TXXTXTTX
utilisateur56834
La différence est pertinente lorsque nous voulons parler de types et de jeux, ainsi que de leurs propriétés et relations. En d'autres termes, les informations que nous perdons lorsque nous disons plutôt que x : T ne nous disent rien de pertinent sur x , mais la même chose peut ne pas être vraie si nous voulons par exemple parler de super ensemble-type ou de type- relations de sous-type? Est-ce exact? XXTX:TX
user56834
4
Oui, on se demande où sont ces livres. Quelqu'un devrait les écrire.
Andrej Bauer
11

Pour commencer, les ensembles et les types ne sont même pas dans la même arène. Les ensembles sont les objets d’une théorie du premier ordre, telle que la théorie des ensembles ZFC. Alors que les types sont comme des sortes envahies. Pour mettre une autre manière, une théorie des ensembles est une théorie du premier ordre au sein de la logique du premier ordre. Une théorie des types est une extension de la logique elle-même. La théorie de type de Martin-Löf, par exemple, n'est pas présentée comme une théorie du premier ordre dans la logique du premier ordre. Il n'est pas courant de parler d'ensembles et de types en même temps.

En tant qu'états discrets de lézards, les types (et les tris) remplissent une fonction syntaxique. Une sorte / type se comporte comme une catégorie syntaxique . Cela nous permet de savoir quelles expressions sont bien formées. Pour un exemple simple utilisant des tris, supposons que nous avons décrit la théorie des espaces vectoriels sur un champ arbitraire comme une théorie à 2 triés. Nous avons une sorte de scalaires, , et une sorte de vecteurs, V . Parmi beaucoup d' autres choses, nous aurions une opération de mise à l' échelle: s c a l e : S × VV . Cela nous permet de savoir que l c un l e ( s c a l eSVscale:S×VV n’est tout simplement pas un terme bien formé. Dans un contextetype théorique, une expression comme f ( x ) exige f avoir un type X Y pour certains types X et Y . Si f n'a pas le type d'une fonction, alors f ( x ) n'est tout simplement pas une expression bien formée. Qu'une expression soit ou non d'un type est une déclaration méta-logique. Cela n'a aucun sens d'écrire quelque chose comme: ( x : X )scale(scale(s,v),v)f(x)fXYXYff(x) . Premièrement, x : X n’est tout simplement pas une formule, et deuxièmement, cela n’a même aucun sens conceptuel puisque ce sont les types / types qui nous permettent de savoir quelles formules sont bien formées. Nous ne tenons compte que de la valeur de vérité des formules bien formées. Par conséquent, si nous déterminons si une formule est valable, nous ferions mieux de savoir déjà qu’elle est bien formée!(x:X)y=3x:X

En théorie des ensembles, et en particulier ZFC, le seul symbole non-logique du tout est le symbole de la relation d'adhésion ensemble, . Donc, x y est une formule bien formée avec une valeur de vérité. Il n'y a pas d'autres termes que variables. Toute la notation habituelle de la théorie des ensembles en est une extension définitionnelle. Par exemple, une formule comme f ( x ) = y est souvent considéré comme un raccourci pour ( x , y ) F qui lui - même peut être considéré comme un raccourci pour p . p f p = ( xxyf(x)=y(x,y)f qui estraccourci pourp . p f ( z . z pp.pfp=(x,y) En tout cas,tout ensemble peut prendre la place de f et tout est ensemble! Comme je l'ai soulignérécemmentdansune question différente, π ( 7 ) = 3 π

p.pf(z.zp[z=x(w.wzw=y)])
fπ(7)=3πest le nombre réel est une expression théorique d'ensemble parfaitement légitime et significative (et potentiellement même vraie). Fondamentalement, tout ce que vous écrivez qui analyse en théorie des ensembles peut avoir une signification. C'est peut-être une signification complètement fausse, mais elle en a une. Les ensembles sont également des objets "de première classe" dans la théorie des ensembles. (Il faut qu'ils soient tels qu'ils sont seulement des objets en général.) Une fonction similaire
f(x)={N,if x=17,if x=QxRR,if x=(Z,N)
est une fonction complètement légitime dans la théorie des ensembles. Il n’ya rien, même de loin, analogue à cela dans la théorie des types. Le plus proche serait d'utiliser des codes pour un univers tarskien. Les ensembles sont les objets de la théorie des ensembles; les types ne sont pas l'objet de la théorie des types.

Un type n'est pas une collection de choses (ni un ensemble, d'ailleurs ...), et il n'est pas défini par une propriété. Un type est une catégorie syntaxique qui vous permet de savoir quelles opérations sont applicables aux termes de ce type et quelles expressions sont bien formées. Dans la perspective propositions-as-types, quels types classent sont les preuves valides de la proposition à laquelle correspond le type. C'est-à-dire que les termes bien formés (c'est-à-dire bien typés) d'un type donné correspondent aux preuves valides (qui sont aussi des objets syntaxiques) de la proposition correspondante. Rien de tel ne se passe dans la théorie des ensembles.

La théorie des ensembles et la théorie des types ne ressemblent vraiment pas.

Derek Elkins
la source
1
Il est faux que les types ne soient que des entités syntaxiques.
Andrej Bauer
1
C'est très utile, mais un élément principal de votre réponse me dérange. Il me semble que c'est une erreur (que beaucoup de gens commettent, ou bien ce n'est pas une erreur et je me trompe), de dire qu'un ensemble n'est pas une collection de choses. Je dirais qu'un ensemble est une collection de choses. C'est la propriété essentielle la plus fondamentale d'un ensemble. En fait, comment pourrions-nous savoir, par exemple, que les ZFC sont les bons axiomes à choisir (plutôt que des formules complètement arbitraires), sans pouvoir dire qu'ils sont vrais, étant donné que les ensembles sont des collections d'objets? Bien sûr, je comprends que ...
user56834
Théorie des ensembles axiomatique traite des ensembles comme des objets, et comme un simple symbole, parce que la théorie des ensembles axiomatique n'est pas une structure mathématique dans le sens de la logique mathématique.
user56834
1
@ Programmer2134 Pour répondre à cette question, il nous faudrait entrer dans le sens sémantique du mot "collection". Nous ne pouvons pas être sûrs qu'ils ont "raison" à moins que vous preniez le temps de définir précisément ce que "droit" signifie. Cependant, ce que nous pouvons dire, c’est que "set" est le résultat de plus de cent ans de mathématiciens qui ont défié le concept de collection, cherchant un système cohérent qui correspond au concept intuitif d’une collection. Pour atteindre cette cohérence, ils devaient prendre des décisions. Par exemple, les ensembles ne sont pas la seule collection en mathématiques. Une "classe" décrit également une collection.
Cort Ammon - Rétablir Monica le
1
@AndrejBauer Je prends une position (principalement) non philosophique et n'essaie pas d'expliquer ce que sont vraiment les types, mais comment ils sont utilisés. (Je dis "sert comme" et "se comporte comme" au début mais je me suis glissé dans un "est" à la fin.) Il y a un risque de penser qu'une variable étant de type T signifie que les seules "valeurs" que x peut « prendre » sont les termes (probablement fermés) de type T . Ce n'est pas vrai et n'est impliqué dans rien de ce que je dis ci-dessus. Je conviens que vous pouvez voir les types comme étant plus que des entités syntaxiques, mais je pense que les différents types de rôles syntaxiques jouent contrastent nettement avec les ensembles. XTXT
Derek Elkins
9

En pratique, l'affirmation que est de type T est généralement utilisée pour décrire la syntaxe , alors que l'affirmation que x est dans l'ensemble S est généralement utilisée pour indiquer une propriété sémantique . Je vais donner quelques exemples pour clarifier cette différence d’ utilisation des types et des ensembles. Pour la différence de quels types et ensembles en fait sont , je me réfère à la réponse de Andrej Bauer .XT XS

Un exemple

Pour clarifier cette distinction, je vais utiliser l'exemple donné dans les notes de cours d'Herman Geuvers . Tout d’abord, examinons un exemple d’habitation d’un type:

3+(7*8)5:Nunet,
3{nN|X,y,zN+(Xn+ynzn)}

La principale différence ici est que pour vérifier si la première expression est un nombre naturel, nous n’avons pas à calculer de signification sémantique, nous devons simplement "lire" le fait que tous les littéraux sont de type Nat et que tous les opérateurs sont fermé sur le type Nat.

33

Algorithmes vs preuves

Pour résumer, les types sont souvent utilisés pour des revendications «simples» sur la syntaxe d'une expression, telle que l'appartenance à un type puisse être vérifiée par un algorithme , alors que pour tester l'appartenance à un ensemble, nous aurions généralement besoin d'une preuve .

Pour voir pourquoi cette distinction est utile, considérons un compilateur d’un langage de programmation typé. Si ce compilateur doit créer une preuve formelle pour «vérifier les types», il lui est demandé de faire une tâche presque impossible (la démonstration automatique d'un théorème est généralement difficile). Si par contre le compilateur peut simplement exécuter un algorithme (efficace) pour vérifier les types, il peut alors effectuer la tâche de manière réaliste.

Une motivation pour une interprétation stricte

Il existe plusieurs interprétations de la signification sémantique des ensembles et des types. Bien que, selon la distinction faite ici, les types d'extension et les types avec vérification de type indécidable (tels que ceux utilisés dans NuPRL, comme indiqué dans les commentaires) ne soient pas des "types", d'autres sont bien entendu libres de les appeler en tant que tels (tout aussi comme ils sont appelés à les appeler autre chose, tant que leurs définitions correspondent).

Cependant, nous (Herman Geuvers et moi), préférons ne pas jeter cette interprétation par la fenêtre, pour laquelle moi (pas Herman, même s'il pourrait être d'accord) avons la motivation suivante:

Tout d’abord, l’intention de cette interprétation n’est pas si éloignée de celle d’Andrej Bauer. L'intention d'une syntaxe est généralement de décrire comment construire quelque chose et qu'il est généralement utile de disposer d'un algorithme pour le construire. De plus, les fonctionnalités d'un ensemble ne sont généralement nécessaires que lorsque nous voulons une description sémantique, pour laquelle l'indécidabilité est autorisée.

L’avantage de notre description plus stricte est donc de garder la séparation plus simple , d’obtenir une distinction plus directement liée à l’utilisation pratique courante. Cela fonctionne bien tant que vous n'avez pas besoin ou ne voulez pas assouplir votre utilisation, comme vous le feriez pour, par exemple, NuPRL.

Lézard discret
la source
3
La vérification de type n'a pas besoin d'être décisive (même si c'est certainement souhaitable). NuPRL, par exemple, oblige l'utilisateur à fournir la preuve qu'un terme habite un type.
Derek Elkins
3
3...
1
@DerekElkins Je ne connais pas NuPRL, mais par exemple, l'assistant aux preuves, Coq, vérifie certainement le dactylographie en lui-même (c'est-à-dire qu'il s'agit du terme fourni par le «type de mon théorème»). Comment NuPRL vérifie-t-il la preuve si l'utilisateur doit "prouver" le fait qu'un terme d'un certain type? (en d'autres termes, cela semble indiquer que NuPRL n'utilise pas la correspondance Curry-Howard, alors à quoi sert-il?)
Lézard discret
1
@ Discretelizard Je ne dis pas que NuPRL est typique. C'est certainement le cas habituel pour que la vérification de type soit décidable. Je vous recommande fortement de vous familiariser avec cette technique simplement parce que le chemin emprunté est assez différent. NuPRL est un calcul de style Curry plutôt que de style église, ce qui en fait un système de raffinement de type. Quoi qu’il en soit, au lieu d’écrire simplement des termes (ou des tactiques produisant des termes), vous disposez essentiellement d’un système de preuves de type LCF pour taper les dérivés eux-mêmes. On peut soutenir que ce sont les dérivations qui importent, et c’est un peu un "coup de chance" que nous pouvons les déduire à partir de termes.
Derek Elkins
3
4

Je crois que l'une des différences les plus concrètes concernant les ensembles et les types est la différence dans la manière dont les "choses" de votre esprit sont codées dans le langage formel.

Les ensembles et les types vous permettent de parler de choses et de collections de choses. La principale différence est qu'avec les sets, vous pouvez poser toutes les questions que vous voulez et ce sera peut-être vrai, peut-être pas; tandis qu'avec les caractères, vous devez d'abord prouver que la question a un sens.

B={vrai,faux}N={0,1,}vrai=1

0[0]={}n+1[n+1]={[n]}[n]vraifauxvrai=1vrai1

une=bunebvrai=1SBNιB:BSιN:NS, vous pourriez demander si ιB(vrai)=ιN(1) mais le fait que cette question dépende des encodages (et du choix des encodages) est maintenant explicite.

Notez que dans ces cas, il était facile de voir si la question avait du sens, mais elle pourrait être beaucoup plus difficile, comme dans, par exemple, (sivery_hard_questionpuis1autrevrai)=1.

En résumé, les ensembles vous permettent de poser toutes les questions de votre choix, mais les types vous obligent à rendre explicites les encodages lorsque la réponse peut en dépendre.

xavierm02
la source
You are probably thinking of one specific kind of set theory (something along a single-sorted theory a la ZFC). However, there are other kinds of set theory which require lots of checking that it makes sense. And the way set theory is used in practice is much closer to these other set theories. Do you think a student could ask "Is R an element of sin(2)?" without being scolded? The distinction between type theory and set theory is not in the formalism, it's in the meaning.
Andrej Bauer
@AndrejBauer Right. Would you agree that this answer gives a differences between single-sorted theories (including most set theories, or at least the most common ones), and multi-sorted theories (including all (?) type theories)?
xavierm02
Même dans une théorie simple triée, vous devez distinguer les termes des formules ...
Andrej Bauer
@AndrejBauer Je ne comprends pas votre deuxième commentaire.
xavierm02
A single-sorted first-order theory has two syntactic categories: logical formulas and terms. One has to make sure they're not mixed up, or else you could end up writing "(xX.ϕ(x))N".
Andrej Bauer