Publicité
+ Répondre à la discussion
Page 7 sur 9 PremièrePremière ... 3456789 DernièreDernière
Affichage des résultats 121 à 140 sur 165
  1. #121
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 63

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 339
    Points
    339

    Par défaut

    Citation Envoyé par Steki-kun Voir le message
    Oui c'est exactement ça :-)
    Très bien. Dans ce cas, je ne vais pas attendre plus longtemps pour donner la réponse à la question 24, qui est de toute façon une question un peu particulière. Je signale tout de suite que dans le point de vue que je développe ici je suis arrivé aux même conclusions que celles qui ont été exposées par Steki-kun concernant Coq. Pour cela j'ai deux arguments, et je vais exposer le premier plus loin.

    La réponse est donc ``non'' pour la question 24, c'est à dire ``non en général'', mais pas forcément non dans tous les cas. En effet si a est tout simplement identique à b (disons alpha-equivalent), il est bien clair que W(E[ a/x ]) et W(E[ b/x ]) sont le même type et donc que c est bien un terme de type W(E[ b/x ]). Mais en général la réponse est ``non'', tout simplement parce que les règles de ce système ne donnent aucun moyen d'identifier les deux types. Si on parcourt le fil, on verra que le seul endroit où on énonce une égalité entre types est la règle dite ``Sémantique de Heyting'' qui identifie W(?x:T E) avec (x:T) -> W(E). C'est clairement insuffisant pour pouvoir répondre ``oui'' à la question 24.

    Voyons maintenant les deux arguments évoqués plus haut. Le premier est très simple. Si E=F entrainait W(E) = W(F) alors pour tout énoncé E, démontrable (donc égal à vrai par un axiome d'extentionalité que je n'ai pas encore évoqué; I'm sorry !), toute preuve de vrai serait aussi une preuve de E. Comme il existe une preuve triviale de vrai (on l'a vue plus haut), cette preuve triviale serait une preuve de tout énoncé démontrable. En soi, ce n'est sans doute pas contradictoire, mais on voit bien que vérifier que notre preuve triviale de vrai est une preuve de E revient à rechercher une preuve de E, et donc qu'un compilateur devient incapable de vérifier les preuves.

    Par ailleurs, le fait d'identifier W(E[ a/x ]) et W(E[ b/x ]) quand a et b ont la même forme normale rend un appréciable service. Cela nous évite d'avoir à écrire des preuves pour le cas où a=b résulte d'un simple calcul. Enorme simplification pour l'utilisation du système. En fait, si on procédait pas ainsi, chaque règle de calcul devrait faire l'objet d'un axiome. En d'autres termes, il faudrait ``Hilbertiser'' le système, ce qui le rendrait beaucoup moins maniable. L'écriture des preuves serait un vrai cauchemar.

    L'autre argument vient de la Théorie des Topos. L'exposer requiert pas mal de préliminaires. Il n'est pas exclu que je le fasse, mais sans doute pas dans un post, plutôt dans un document séparé.

  2. #122
    Membre du Club
    Inscrit en
    janvier 2007
    Messages
    64
    Détails du profil
    Informations personnelles :
    Âge : 35

    Informations forums :
    Inscription : janvier 2007
    Messages : 64
    Points : 40
    Points
    40

    Par défaut

    Citation Envoyé par DrTopos Voir le message


    Question 24. Question 25. Construire un terme f de type Boole -> O tel que f(Bfaux) = faux et f(Bvrai) = vrai.
    Je regarde cette question. J'avoue que je n'ai pas très bien compris ce qu'est la somme de types. Pour le produit cartésien, je vois, cela correspond grosso modo à une structure.
    Mais une somme? c'est juste une juxtaposition des éléments?
    Et pourquoi, pour le type booléen, ne pas prendre un type à deux éléments?

    Bfaux = *+One et Bvrai = One+*
    Bvrai et Bfaux sont donc des termes (d'après le résumé)?
    Si je comprend bien, Bfaux correspond à l'élément du premier One, plus n'importe lequel du second One (donc soit aucun, soit le seul élément de ce One)?

    Il faudrait trouver un truc tel que:
    f(Bfaux) => ?q:O q
    f(Bvrai) => ?q:O ?x:W(q) q


    Mais euh...

  3. #123
    Membre confirmé Avatar de Steki-kun
    Profil pro
    Inscrit en
    janvier 2005
    Messages
    222
    Détails du profil
    Informations personnelles :
    Âge : 31
    Localisation : France, Paris (Île de France)

    Informations forums :
    Inscription : janvier 2005
    Messages : 222
    Points : 273
    Points
    273

    Par défaut

    Salut ta confusion vient du fait que tu n'as pas compris ce qu'est un type somme en maths. Tu connais le produit cartésien de deux ensembles A et B, qui consiste à prendre l'ensemble des couplets (a,b)a est dans A, et b est dans B : il correspond qque part à la conjonction de A et B.
    Et de même que la conjonction a un opérateur logique dual, la disjonction, eh bien le produit cartésien a comme opérateur dual la somme d'ensembles, que l'on peut définir comme suit :
    A + B = {(a,1) | a dans A} U {(b,2) | b dans B}
    Autrement dit, c'est l'ensemble qui comprend d'un côté les éléments de A, et de l'autre les éléments de B. Je dis bien "d'un côté .... et de l'autre", car cette opération est différente de l'union traditionnelle ! Dans le cas d'une union, les éléments qui sont à la fois dans A et dans B seraient "fusionnés" dans A U B. Ici, on tagge les valeurs qui viennent de A avec un 1, et celles qui viennent de B avec un 2, comme ça même si A et B ont des éléments en commun, la somme A + B réalise bien une union disjointe des deux ensembles A et B.

    Maintenant, quand tu fais la somme A+B, tu disposes des "injections canoniques" inj1 et inj2 qui sont des fonctions respectivement de A -> A+B et de B -> A+B telles que : pour tout a dans A, inj1(a) = (a,1) ; pour tout b dans B, inj2(b) = (b,2).
    Note que dans ma définition et dans mes injections, j'ai mis 1 et 2 pour tagger les éléments qui proviennent du premier opérande et ceux qui proviennent du second, mais j'aurais pu mettre n'importe quoi, et en particulier l'autre ensemble. C'est ce que fait le docteur Topos en écrivant :
    • x + B la première injection canonique inj1(x)
    • A + x la seconde inj2(x)

    Donc, le type booléen tel que le DrTopos l'a défini a bien exactment deux éléments : un * de gauche, et un * de droite, ou pour les appeler par leurs noms : Bfaux et Bvrai.

    Edit : si tu vois le produit comme une structure C, alors tu peux voir la somme comme une union C
    I'm the kind of guy that until it happens, I won't worry about it. - R.H. RoY05, MVP06

  4. #124
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 63

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 339
    Points
    339

    Par défaut

    Citation Envoyé par kaukau Voir le message
    Je regarde cette question. J'avoue que je n'ai pas très bien compris ce qu'est la somme de types. Pour le produit cartésien, je vois, cela correspond grosso modo à une structure.
    Mais une somme? c'est juste une juxtaposition des éléments?
    Et pourquoi, pour le type booléen, ne pas prendre un type à deux éléments?
    Ensemblistement, la somme est l'union disjointe. Dans le cas de Boole c'est l'union disjointe de deux exemplaires de One. Comme One a un seul élément qui est *, ça lui fait deux éléments, un dans le premier exemplaire et un dans l'autre. Ce sont ces deux éléments qui sont notés *+One et One+*. Boole est bien un type à deux éléments.

    Citation Envoyé par kaukau Voir le message
    Bfaux = *+One et Bvrai = One+*
    Bvrai et Bfaux sont donc des termes (d'après le résumé)?
    Si je comprend bien, Bfaux correspond à l'élément du premier One, plus n'importe lequel du second One (donc soit aucun, soit le seul élément de ce One)?
    Bfaux est seulement le * du premier exemplaire de One. C'est tout. La notation *+One (apparemment somme d'un terme et d'un type) est juste une astuce pour que * comme premier élément de One+One ne soit pas confondu avec * élément de One, et pour que son type soit facilement déterminé d'après sa notation. Boole contient bien deux éléments et deux seulement qui sont *+One et One+*.

    Citation Envoyé par kaukau Voir le message
    Il faudrait trouver un truc tel que:
    f(Bfaux) => ?q:O q
    f(Bvrai) => ?q:O ?x:W(q) q
    Oui, c'est exactement ce qu'il faut faire, et bien sûr l'écrire sous forme d'un terme bien typé.

  5. #125
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 63

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 339
    Points
    339

    Par défaut

    Bon on a encore posté presque en même temps. Si j'avais lu ton post, je n'aurai sans doute pas écrit le mien de cette façon. Ce n'est pas grave bien sûr.

    Citation Envoyé par Steki-kun Voir le message
    Edit : si tu vois le produit comme une structure C, alors tu peux voir la somme comme une union C
    Là je ne suis pas d'accord. La structure du C est bien un produit, mais l'union du C est très loin d'être une somme. Comme il se fait tard et qu'il me reste moins de 6 heures pour dormir, je développerai cette question dans la semaine. Bonne nuit à tous.

  6. #126
    Membre confirmé Avatar de Steki-kun
    Profil pro
    Inscrit en
    janvier 2005
    Messages
    222
    Détails du profil
    Informations personnelles :
    Âge : 31
    Localisation : France, Paris (Île de France)

    Informations forums :
    Inscription : janvier 2005
    Messages : 222
    Points : 273
    Points
    273

    Par défaut

    Citation Envoyé par DrTopos Voir le message
    Bon on a encore posté presque en même temps. Si j'avais lu ton post, je n'aurai sans doute pas écrit le mien de cette façon. Ce n'est pas grave bien sûr.
    Désolé Je trouve qu'ils se complètent bien en tout cas.

    Citation Envoyé par DrTopos Voir le message
    Là je ne suis pas d'accord. La structure du C est bien un produit, mais l'union du C est très loin d'être une somme. Comme il se fait tard et qu'il me reste moins de 6 heures pour dormir, je développerai cette question dans la semaine. Bonne nuit à tous.
    Je vous le concède mais vous pinaillez un peu Le but était de donner une intuition à kaukau plus qu'autre chose. Pour être exact, je dirai donc "un type somme OCaml" au lieu de "une union C". Bonne nuit !
    I'm the kind of guy that until it happens, I won't worry about it. - R.H. RoY05, MVP06

  7. #127
    Membre du Club
    Inscrit en
    janvier 2007
    Messages
    64
    Détails du profil
    Informations personnelles :
    Âge : 35

    Informations forums :
    Inscription : janvier 2007
    Messages : 64
    Points : 40
    Points
    40

    Par défaut

    Citation:
    Envoyé par kaukau
    Il faudrait trouver un truc tel que:
    f(Bfaux) => ?q:O q
    f(Bvrai) => ?q:O ?x:W(q) q

    Oui, c'est exactement ce qu'il faut faire, et bien sûr l'écrire sous forme d'un terme bien typé.
    Je développe juste un cran de plus:
    Bfaux:Boole |-> q:O |-> q
    et
    Bvrai:Boole |-> q:O |-> x:W(q) |-> q

    Pour aller plus loin, il faudrait utiliser un genre de projection (p1 et p2)?

  8. #128
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 63

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 339
    Points
    339

    Par défaut

    Citation Envoyé par kaukau Voir le message
    Je développe juste un cran de plus:
    Bfaux:Boole |-> q:O |-> q
    et
    Bvrai:Boole |-> q:O |-> x:W(q) |-> q

    Pour aller plus loin, il faudrait utiliser un genre de projection (p1 et p2)?
    Si tu utilises Bfaux comme variable locale, il n'a plus rien à voir avec le Bfaux défini dans le post #117. Indication: il faut utiliser la règle D2 du résumé (et non pas des projections).

  9. #129
    Membre du Club
    Inscrit en
    janvier 2007
    Messages
    64
    Détails du profil
    Informations personnelles :
    Âge : 35

    Informations forums :
    Inscription : janvier 2007
    Messages : 64
    Points : 40
    Points
    40

    Par défaut

    La règle D2! Justement celle que j'ai le moins compris
    (Règle D2 ) Si a est un terme de type T+U dans le contexte Γ,
    si V est un type dans le contexte Γ,
    et si E et F sont des termes de type V respectivement dans le contexte Γ(x:T) et dans le contexte Γ(y:U),
    alors [x > E, y > F](a) est un terme de type V dans le contexte Γ.
    Je n'ai pas très bien compris ce qu'est un contexte. C'est juste un ensemble de types?
    Γ(x:T) C'est un contexte augmenté d'un élément?
    Effectivement dans la définition T+U fait partie de Γ, mais T n'en fait pas nécessairement partie.
    Ou alors c'est un ensemble de types dans lequel on s'autorise une variable dépendants de type T...

    Que signifie la règle D2? Elle permet de sélectionner E ou F (ou un peu des deux) selon le "a" qu'on met?
    Dans notre cas, ça donnerais:
    si on pose T=U=One et V=O (pourquoi pas!):

    [*+One > q:O, One+*> p:O] (a:Boole)
    avec q=?r:O r et p=?r:O ?x:W(r) r

    Pour se rapprocher du résulat...

  10. #130
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 63

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 339
    Points
    339

    Par défaut

    Citation Envoyé par kaukau Voir le message
    La règle D2! Justement celle que j'ai le moins compris
    Je vais revenir sur la question des sommes dans un prochain post. Je donnerai des explications détaillées.

    Citation Envoyé par kaukau Voir le message
    Je n'ai pas très bien compris ce qu'est un contexte.
    C'est une succession de déclarations. Les contextes sont construits récursivements par les règles Γ1 et Γ2. Ils permettent d'utiliser les symboles qui y sont déclarés. Cette utilisation est régie par les règles S1 et S2.

    Citation Envoyé par kaukau Voir le message

    [*+One > q:O, One+*> p:O] (a:Boole)
    Syntax error: dans une expression de la forme [x > E, y > F](a), x et y doivent être des symboles.

    Petite indication: comme indiqué dans le résumé, le terme [x > E, y > F](a) est une conditionnelle. Ce terme se lit comme suit: ``si a provient d'un x de T, alors E, et s'il provient d'un y de U, alors F''. Bien entendu, E peut faire usage de x, puisqu'il a un sens dans le contexte Γ(x:T). De même, F peut faire usage de y.

    Ces notions relatives au contextes sont très habituelles et existent (nécessairement) dans tous les langages qui font usage de variables. Ce qui est dit ici sur les contextes n'a rien d'original.

  11. #131
    Membre du Club
    Inscrit en
    janvier 2007
    Messages
    64
    Détails du profil
    Informations personnelles :
    Âge : 35

    Informations forums :
    Inscription : janvier 2007
    Messages : 64
    Points : 40
    Points
    40

    Par défaut

    Je comprend mieux ce qu'est un contexte. J'aurais du percuter plus tôt, c'est comme un contexte en C par exemple (avec les notions de porté et de visibilité)... Je vais vraiment chercher 12h à 14h...

    Sinon est-ce que je suis parti dans la bonne direction avec mon p, q:O et mon a:Boole?

  12. #132
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 63

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 339
    Points
    339

    Par défaut

    Citation Envoyé par kaukau Voir le message
    Sinon est-ce que je suis parti dans la bonne direction avec mon p, q:O et mon a:Boole?
    A part l'erreur de syntaxe déjà signalée, c'est presque bon, en ce sens que le terme que tu proposes sera de type O et non pas de type Boole -> O. Il suffit de rajouter une flèche |-> pour arranger cela. En définitive, on a le terme suivant:

    (a:Boole) |-> [x > faux, y > vrai](a)

    qui est bien de type Boole -> O, et où faux et vrai sont bien sûr respectivement ?q:O q et ?q:O ?x:W(q) q. Je te laisses nous faire le type-checking de ce terme (qui consiste tout simplement à bien comprendre comment on applique la règle D2).

    Remarque: On peut se demander pourquoi j'ai adopté la notation tordue [x > E, y > F](a) pour les conditionnelles, qui auraient peut-être été mieux représentées par:

    if a is x+One then E, One+y then F

    c'est à dire en y mettant le sucre syntaxique usuel.

    La raison est que la notation [x > E, y > F](a) est celle que m'inspire la théorie des catégories. J'expliquerai cela plus loin dans le post que je consacrerai aux somme. Cette notation permet (via quelque chose qui ressemble à une eta-réduction) de considérer [x > E, y > F] comme une fonction de T+U vers le type commun à E et F. Ceci fait que le terme qui est la solution de la question 25 pourrait aussi s'écrire plus simplement:

    [x > faux, y > vrai]

    C'est sous cette forme que les conditionnelles apparaîssent en théorie des catégories (dans le problème universel qui définit les sommes), et non pas sous une forme comprenant aussi l'argument a.

  13. #133
    Membre du Club
    Inscrit en
    janvier 2007
    Messages
    64
    Détails du profil
    Informations personnelles :
    Âge : 35

    Informations forums :
    Inscription : janvier 2007
    Messages : 64
    Points : 40
    Points
    40

    Par défaut

    C'est vrai que la notation [x > E, y > F](a) m'a beaucoup perturbé, surtout parceque on dirait qu'on compare 2 choses de types différents avec le symbole ">".
    Ce qui m'embète encore c'est qu'on utilise des variables x et y sans les déclarer...
    Il est implicite que x est du premier type de la somme et y du second?
    Dans notre cas, E n'utilise pas d'occurence de x et de même pour F, rassure moi?

    Merci pour ta patience en tout cas

  14. #134
    Membre du Club
    Inscrit en
    janvier 2007
    Messages
    64
    Détails du profil
    Informations personnelles :
    Âge : 35

    Informations forums :
    Inscription : janvier 2007
    Messages : 64
    Points : 40
    Points
    40

    Par défaut

    Je regarde la
    Question 26. En utilisant le tiers exclu, construire la fonction réciproque de f construite dans la question 25.
    Par réciproque on entend ~f ?
    Si c'est le cas je dirais intuitivement
    (a:Boole) |-> [x > vrai, y > faux](a)
    En inversant vrai et faux.
    On voit bien qu'on aura toujours f|~f pour toute valeur booléene.

    Si c'est f-1, elle est du type O -> Boole.
    J'imagine qu'il faut utiliser les "inclusions canoniques” (Règle C2).

    Je reposte le lien du résumé:
    résumé

  15. #135
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 63

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 339
    Points
    339

    Par défaut

    Citation Envoyé par kaukau Voir le message
    C'est vrai que la notation [x > E, y > F](a) m'a beaucoup perturbé, surtout parceque on dirait qu'on compare 2 choses de types différents avec le symbole ">".
    Le symbole ``>'' veut dire ``then'' (c'est à dire ``alors'') dans ce contexte.

    Citation Envoyé par kaukau Voir le message
    Ce qui m'embète encore c'est qu'on utilise des variables x et y sans les déclarer...
    Il est implicite que x est du premier type de la somme et y du second?
    C'est cela. Le type est implicite, encore que ce n'est plus le cas si on enlève (a).


    Citation Envoyé par kaukau Voir le message
    Dans notre cas, E n'utilise pas d'occurence de x et de même pour F, rassure moi?
    C'est exact, et c'est surtout dû au fait que One n'ayant qu'un seul élément, ce dernier ne peut pas contenir une information utile. Dans le cas de la question 22, les occurrences seront nécessaires.

    Citation Envoyé par kaukau Voir le message
    Si c'est f-1, elle est du type O -> Boole.
    C'est bien de cela qu'il s'agit.

  16. #136
    Membre du Club
    Inscrit en
    janvier 2007
    Messages
    64
    Détails du profil
    Informations personnelles :
    Âge : 35

    Informations forums :
    Inscription : janvier 2007
    Messages : 64
    Points : 40
    Points
    40

    Par défaut

    Pour le question 26 il faut utiliser une conditionnelle aussi?
    On pourrait construire le type somme des propositions vrai et des propositions fausses.
    A cause du tiers exclus, ce type somme = O.
    On peut donc écrire une conditionnelle
    [x > *+One, y > One+*]...

  17. #137
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 63

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 339
    Points
    339

    Par défaut

    Citation Envoyé par kaukau Voir le message
    On peut donc écrire une conditionnelle
    [x > *+One, y > One+*]...
    Non, on ne peut pas écrire ceci, car O n'est pas une somme.

  18. #138
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 63

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 339
    Points
    339

    Par défaut

    Je viens de m'apercevoir que la question 26 était prématurée. J'aurais dû vérifier la solution avant de poser la question. Mea culpa ! On a besoin (autant que je sache) de l'opérateur de description pour résoudre cette question. Je vais donc expliquer de quoi il sagit.

    On commence par définir !1x:T E (lire: ``il existe un unique x dans T tel que E'') comme une abbréviation pour:

    !x:T (E & ?y:T E[ y/x ] => x = y)

    (où y est une variable fraîche c'est à dire distincte de x et non utilisée dans T ni dans E). Cet énoncé parle de lui-même: il affirme l'existence d'un x de T ayant la propriété E et ajoute que si un autre élément y de T a aussi la propriété E, alors il est égal à x. Autrement-dit il affirme l'existence et l'unicité d'un x de T ayant la propriété E.

    L'opérateur de description sera noté #. C'est une fonction de type (pour tout type T et tout énoncé E pouvant dépendre d'un x de type T):

    W(!1x:T E) -> T

    L'idée est que si p est une preuve de !1x:T E, alors #(p) représente l'unique élément dont l'existence est prouvée par p. Aussi étonnant que cela puisse paraître, cet opérateur est constructif. L'opérateur de description est le destructeur que j'avais anoncé pour les types de témoins depuis le début de ce fil (post #16). Ce destructeur a un compagnon qu'on va noter ## qui est de type:

    W(!1x:T E) -> W(E[ #(p)/x ])

    Autrement-dit, ##(p) prouve que #(p) a la propriété E. Note: # et ## sont les deux projections pour les paires de Heyting qui correspondent à un cas où il y a unicité.

    J'en profite pour poser une question à propos de cet opérateur.

    Question 28. Soit T un type, et E un énoncé pouvant dépendre de x de type T. Trouver un terme de type:

    W(?p:W(!1x:T E) ?y:T E[ y/x ] => y = #(p))

  19. #139
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 63

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 339
    Points
    339

    Par défaut

    Bonjour à tous.

    Voici les explications promises sur les sommes de types (et sur les produits de types par la même occasion).

    Commençons par une notion qui doit être familière aux informaticiens, celle de graphe. Un graphe (orienté) est composé de deux sortes de choses:
    • un ensemble de sommets (encore appelés objets),
    • un ensemble d'arêtes (encore appelées flèches).

    Imaginons les sommets comme des points, et les arêtes comme des chemins (ou des flèches) allant d'un sommet à un autre. Formellement, ceci signifie qu'à chaque arête sont associés deux sommets qu'on appelle la source (ou l'origine) et le but (ou l'extrémité ou la cible) de cette arête. On peut faire un dessin comme celui-ci:
    qui représente un graphe avec seulement deux sommets A et B et une seule arête a, dont la source est A et dont le but est B.

    Une catégorie n'est rien d'autre qu'un graphe ayant des propriétés particulières. Ces propriétés sont les suivantes:
    • Pour tout objet A, on a une flèche notée 1 dont la source et le but sont A. Cette flèche est appelée l'identité de l'objet A (A --- 1 ---> A).
    • Chaque fois qu'on a trois objets A, B et C et deux flèches f et g comme ceci: A ---- f ----> B ---- g ----> C, on a une flèche A ---- g o f ----> C appelée la composition de f et g.
    • La composition est associative: si on a A --- f ---> B --- g ---> C --- h ---> D alors (h o g) o f = h o (g o f).
    • Les flèches identité son neutres pour la composition: si on a A --- 1 ---> A --- f ---> B --- 1 ---> B, alors f o 1 = f et 1 o f = f.


    L'exemple le plus classique de catégorie est celle des ensembles. Les objets sont tous les ensembles et les flèches sont toutes les applications entre ensembles. Celle qui nous intéresse plus précisément ici est la catégorie des types et des programmes. Les objets sont les types et les flèches du type T vers le type U sont les progammes (disons les fonctions) prenant un argument de type T et renvoyant une donnée de type U. Il est clair qu'il s'agit d'une catégorie. Une autre catégorie intéressante est celle des énoncés et des démonstrations (le tout dans un contexte donné). Ici on ne considère que les démonstrations ayant une seule hypothèse (la source de la flèche) et une seule conclusion (le but de la flèche). On considérera deux démonstrations de même source et même but comme égales (proof-irrelevance).

    Un objet final dans une catégorie est un objet F qui a la propriété suivante:
    • Pour tout objet X de la catégorie, il y a une et une seule flèche de X vers F.


    Je vous laisse vous assurer vous-même que tout singleton est un objet final dans la catégorie des ensembles, que le type One est un objet final dans la catégorie des types et que l'énoncé vrai est un objet final dans celle des énoncés.

    Un objet initial dans une catégorie est un objet I tel que:
    • Pour tout objet X de la catégorie, il y a une et une seule flèche de I vers X.


    Je vous laisse vous assurer que l'ensemble vide est initial dans la catégorie des ensembles, que le type Empty (voir le résumé) est initial dans la catégorie des types, et que l'énoncé faux est initial dans celle des énoncés.

    On aura remarqué la symétrie entre les notions d'objet final et d'objet initial, symétrie qui consiste tout simplmeent à renverser le sens des flèches. C'est ce qu'on appelle la dualité catégorique.

    Un isomorphisme dans une catégorie est une flèche A --- f ---> B telle qu'il existe une flèche B --- g ---> A (appelée l'inverse de f) telle que f o g = 1 et g o f = 1.

    Exercice: Montrer que si F1 et F2 sont tous les deux finals dans une catégorie, alors il existe un unique isomorphisme entre eux. Même chose pour deux objets initiaux.

    Il résulte de l'exercice ci-dessus que le fait de déclarer qu'un objet est final dans une catégorie, même si cela n'implique par l'existence de cet objet, le définit néanmoins parfaitement à isomorphisme unique près. Par exemple, le fait d'être final dans la catégorie des ensembles caractérise les singletons, qui sont tous isomorphes d'une unique façon.

    La caractérisation comme objet final ou initial dans une catégorie appropriée est donc une méthode pour définir des concepts. Ceci n'a l'air de rien, mais ça a révolutionné les mathématiques, et les informaticiens théoriciens en font aussi grand usage. Il faut remarquer plusieurs choses très importantes:
    • Cette façon de définir un concept ne construit rien, en particulier elle n'implique pas qu'il existe un objet satisfaisant la définition (il y a des catégories sans objet final ou sans objet initial).
    • Dans le cas où l'objet défini existe, il peut en exister plusieurs, mais ils sont canoniquement isomorphes, c'est à dire jouent le même rôle en pratique. Les informaticiens diraient que cette définition est indépendante des détails d'implémentation. Si l'objet existe, il peut y avoir plusieurs façons de le réaliser, mais peu importe puisqu'il y a une unique traduction (réversible) entre les diverses constructions possibles (l'isomorphisme canonique).


    Cette philosophie de la définition peut être qualifiée de behavioriste (en Français: comportementaliste) puisqu'elle définit les objets non pas en les construisant, mais en disant comment ils se comportent par rapport à tous les autres objets de même nature.

    Suite dans un prochain post.

    Help ! J'aimerais include des diagrammes dans mes posts pour illustrer ces explications. Je sais faire de très jolis PDF avec des diagrammes en utilisant LaTeX+xypic+dvipdfm, mais j'ai du mal à les convertir en images (par exemple PNG). J'ai essayé avec Gimp, mais le résultat est pratiquement illisible (je n'arrive pas à trouver des réglages corrects). Quelqu'un connaîtrait-il un outil pratique et facile d'emploi. Je suis sous Linux Ubuntu.

  20. #140
    Rédacteur
    Avatar de SpiceGuid
    Homme Profil pro Damien Guichard
    Inscrit en
    juin 2007
    Messages
    1 569
    Détails du profil
    Informations personnelles :
    Nom : Homme Damien Guichard
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 569
    Points : 2 571
    Points
    2 571

    Par défaut

    En même temps pourquoi refaire ce que vous avez déjà fait ?
    Les diagrammes correspondants (et plus encore) sont disponibles par le lien Ma page maths de votre signature, et si ma mémoire est bonne votre Leçon 2: Catégories bicartésiennes traite justement de ce sujet, de façon au moins aussi claire, avec les diagrammes et les égalités appropriées.

    Le diagramme ci-dessous représente la catégorie:
    • dont les objets sont des parties de l'ensemble E = {a,b,c}
    • dont les flèches A -> B signifient B inclut A



    c'est une simple copie d'écran

    Avec F = {a,b,c,d} on aurait sans doute un joli hyper-cube.
    Du même auteur: le cours OCaml, le dernier article publié, le projet, le blog dvp et le jeu vidéo.
    Avant de poser une question je lis les règles du forum.

Liens sociaux

Règles de messages

  • Vous ne pouvez pas créer de nouvelles discussions
  • Vous ne pouvez pas envoyer des réponses
  • Vous ne pouvez pas envoyer des pièces jointes
  • Vous ne pouvez pas modifier vos messages
  •