Publicité
+ Répondre à la discussion
Page 8 sur 9 PremièrePremière ... 456789 DernièreDernière
Affichage des résultats 141 à 160 sur 165
  1. #141
    Membre éclairé

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

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

    Par défaut

    Citation Envoyé par SpiceGuid Voir le message
    En même temps pourquoi refaire ce que vous avez déjà fait ?
    Mon idée est de faire dans ce fil un résumé très court sur ces questions. Il est vrai que j'ai écrit cela avec des détails dans ma Leçon 2: Catégories bicartésiennes, que je recommande donc pour ceux qui veulent en savoir plus. Malgré cela je vais terminer mes explications courtes dans ce fil.

    Citation Envoyé par SpiceGuid Voir le message
    c'est une simple copie d'écran
    C'était cela la bonne idée à laquelle je n'avais pas pensé. Merci SpiceGuid.

  2. #142
    Membre éclairé

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

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

    Par défaut

    Voyons maintenant la question des sommes et des produits.

    Prenons une catégorie C. Un cône dans la catégorie C est un couple de flèches de même source:



    L'objet S s'appelle le sommet du cône. Le couple d'objets (A,B) s'appelle la base du cône.

    Considérons maintenant deux cônes de même base (A,B) et de sommets respectifs S1 et S2:



    Un morphisme du premier cône vers le deuxième est une flèche S1 --- f ---> S2 entre leurs sommets, qui est compatibles avec les cotés des cônes, c'est à dire telle que:
    • a2 o f = a1
    • b2 o f = b1




    Il est facile de vérifier qu'on a maintenant une catégorie dont les objets sont tous les cônes de base (A,B) et dont les flèches sont tous les morphismes entre ces cônes.

    Définition: Un produit des objets A et B est un objet final dans la catégorie des cônes de base (A,B).

    Le sommet de ce cône final sera noté A*B, ses deux cotés seront notés p1 et p2 et appelés ``projections canoniques''. L'unique morphisme d'un cône de cotés a et b vers ce cône final sera noté <a,b>:



    On remarquera que cette définition définit à la fois le produit des objets A et B en tant qu'objet (l'objet A*B) mais définit en même temps les outils qui vont avec, à savoir les deux projections (destructeurs) et le mécanisme qui construit la flèche <a,b> à partir des flèches a et b (constructeur). Plus encore, la définition contient les équations p1 o <a,b> = a et p2 o <a,b> = b (beta-conversion), et la propriété d'unicité entraine que <p1,p2> = 1 (eta-conversion). N'est-ce pas absolument merveilleux ?

    Qui plus est, on est sûr d'avoir tous les outils qu'il faut et juste ce qu'il faut, puisque qu'une telle définition caractérise le produit à équivalence (isomorphisme) canonique près. je crois qu'on peut rendre hommage au génie de Saunders McLane et Samuel Eilenberg pour cette remarquable invention qu'est la notion de ``problème universel'' (qui peut être vu comme le fait d'être initial ou final dans une catégorie).

    Exercice: Identifier un produit de deux objets quelconques dans la catégorie des ensembles, dans celle des types et dans celle des énoncés.

    Une fois qu'on a compris le produit, il est très facile de comprendre la somme, car c'est exactement la même chose avec toutes les flèches en sens inverse. Aussi on introduit la notion de ``cocône'':



    etc ... (je ne recommence pas tout) ... et on définit enfin la somme des objets A et B comme un objet initial dans la catégorie des cocônes de base (A,B).



    Ceci définit donc à la fois la somme des deux objets A et B en tant qu'objet (l'objet A+B), et les outils qui vont avec, à savoir les ``injections canoniques'' i1 et i2 (qui sont ici les constructeurs) et le mécanisme qui donne la flèche [a,b] à partir des flèches a et b. La flèche [a,b] joue ici le rôle de destructeur et s'appelle une conditionnelle (nous y voila). Bien entendu, la définition donne aussi [a,b] o i1 = a et [a,b] o i2 = b (beta-conversion) et la propriété d'unicité donne [i1,i2] = 1 (eta-convesion).

    Exercice: Identifier une somme de deux objets quelconques dans la catégorie des ensembles, dans celle des types et dans celle des énoncés.

    La même méthode (celle des problèmes universels) s'applique pour définir les types fonctionnels, les types récursifs et corésursifs (cf. Coq). Par contre, il faut un autre outil du même genre (la notion de ``classifiant'') pour modéliser ce qui dans ce fil correspond aux types O et W(...).

    Dans un prochain post, on va comparer cette ``théorie'' à ce qu'on trouve en pratique dans les langages de progammation.

  3. #143
    Membre du Club
    Inscrit en
    janvier 2007
    Messages
    65
    Détails du profil
    Informations personnelles :
    Âge : 35

    Informations forums :
    Inscription : janvier 2007
    Messages : 65
    Points : 43
    Points
    43

    Par défaut

    Exercice: Identifier un produit de deux objets quelconques dans la catégorie des ensembles, dans celle des types et dans celle des énoncés.
    Dans les ensembles: le produit cartésien
    Dans les types: l'aggrégation, la structure
    Dans les énoncés: le "et" ?

  4. #144
    Membre éclairé

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

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

    Par défaut

    Citation Envoyé par kaukau Voir le message
    Dans les ensembles: le produit cartésien
    Dans les types: l'aggrégation, la structure
    Dans les énoncés: le "et" ?
    Bien sûr, alors pendant qu'on y est qu'en est-il dans la catégorie dont les objets sont les entiers naturels strictement positifs et dont les flèches de source n et de but m sont les couples (n,m) tels que n divise m ?

  5. #145
    Membre du Club
    Inscrit en
    janvier 2007
    Messages
    65
    Détails du profil
    Informations personnelles :
    Âge : 35

    Informations forums :
    Inscription : janvier 2007
    Messages : 65
    Points : 43
    Points
    43

    Par défaut

    Si je reprend les définitions:

    Un produit des objets A et B est un objet final dans la catégorie des cônes de base (A,B).

    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.
    Il me semble que les seuls objets qui n'ont qu'une seule flèche qui pointe vers eux sont les nombres premiers.

    les n = tous les entiers naturels strictement positifs
    les m = tous les multiples de n (donc pas les nombres premiers)

    Le produit dans cet ensemble serait donc la décomposition en produit de nombres premiers?
    Edit: ou le PGCD, je suis pas convaincu

  6. #146
    Membre éclairé

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

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

    Par défaut

    Citation Envoyé par kaukau Voir le message
    Il me semble que les seuls objets qui n'ont qu'une seule flèche qui pointe vers eux sont les nombres premiers.
    Hum... Il y a deux flèches de cible 3, qui sont (1,3) et (3,3).

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

    Informations forums :
    Inscription : janvier 2007
    Messages : 65
    Points : 43
    Points
    43

    Par défaut

    Bon, il reste (1,1).
    Il y a un seul objet final dans la catégorie, ce qui n'est pas très utile.
    Il n'y a donc pas de produit?

  8. #148
    Membre éclairé

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

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

    Par défaut

    Citation Envoyé par kaukau Voir le message
    Bon, il reste (1,1).
    Il y a un seul objet final dans la catégorie, ce qui n'est pas très utile.
    Il n'y a donc pas de produit?
    Si, il y en a, mais il ne faut pas se tromper de catégorie. Un produit dans la catégorie C est un objet final dans une autre catégorie que C.

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

    Informations forums :
    Inscription : janvier 2007
    Messages : 65
    Points : 43
    Points
    43

    Par défaut

    Daccord, il faut un
    objet final dans la catégorie des cônes de base (A,B).
    et
    les flèches sont tous les morphismes entre ces cônes.
    A et B étant les buts m tel que n divise m, n, m appartiennent à N+.

    Mais je n'ai pas très bien compris comment on trouve un objet final:
    Je vous laisse vous assurer vous-même que tout singleton est un objet final dans la catégorie des ensembles
    Comment on montre ça?
    La seule différence entre un singleton et un autre ensemble est que son cardinal=1. Je ne trouve rien dans les définitions données qui fasse intervenir les éléments de l'ensemble, alors comment faire?
    Il se peut que je n'ai pas très bien compris ce qu'est une application entre ensembles.

    Faut-il le démontrer par l'absurde: "Je suppose 2 applications ayant pour but un singleton et je montre qu'elles sont égales"?

    Edit: Le PGCD étant unique entre 2 nombres m et m', est-ce que cela suffit pour en faire un produit?

  10. #150
    Membre éclairé

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

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

    Par défaut

    Citation Envoyé par kaukau Voir le message
    La seule différence entre un singleton et un autre ensemble est que son cardinal=1. Je ne trouve rien dans les définitions données qui fasse intervenir les éléments de l'ensemble, alors comment faire?
    Justement, l'esprit de ces définitions catégoriques est que les objets (ensembles dans ce cas) peuvent être caractérisés sans qu'on ait besoin de faire mention de leurs élements. C'est le cas pour les singletons. Si je prends un ensemble X quelconque et un singleton S, combien y a-t-il d'applications (fonctions partout définies) de X vers S ?

    Pour le PGCD, ton intuition est bonne, c'est bien la solution. Si tu tiens compte des définitions en étant parfaitement précis, ça va sortir tout seul.

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

    Informations forums :
    Inscription : janvier 2007
    Messages : 65
    Points : 43
    Points
    43

    Par défaut

    OK, je croyais qu'une application transformait un ensemble en un autre.
    Elle transforme plutôt un élément de l'ensemble de départ en un élément de l'ensemble d'arrivée.

    Dans le cas du singleton, la seule fonction partout définie est celle qui transforme n'importe quel élément de l'ensemble de départ en l'élément du singleton.

  12. #152
    Membre éclairé

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

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

    Par défaut

    Citation Envoyé par kaukau Voir le message
    Dans le cas du singleton, la seule fonction partout définie est celle qui transforme n'importe quel élément de l'ensemble de départ en l'élément du singleton.
    Exact. Il y en a donc toujours une et une seule quel que soit l'ensemble X, ce qui veut exactement dire qu'être un ensemble singleton est la même chose qu'être un objet final dans la catégorie des ensembles.

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

    Informations forums :
    Inscription : janvier 2007
    Messages : 65
    Points : 43
    Points
    43

    Par défaut

    Exercice: Identifier une somme de deux objets quelconques dans la catégorie des ensembles, dans celle des types et dans celle des énoncés.
    Dans les ensembles: l'union disjointe
    Dans les types: la somme "à la CAML"
    Dans les énoncés: le "ou"

    Voila. Pour le PGCD, je crois que je suis bien incapable de le démontrer...

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

    Informations forums :
    Inscription : janvier 2007
    Messages : 65
    Points : 43
    Points
    43

    Par défaut

    Comment utilise t'on l'opérateur de description? Que décrit-il?
    Si j'ai bien compris, il donne la valeur de x fesant que E est vrai:
    x=#(p) avec p = W(!1x:T E)

    Comment l'utilise t-on dans la question 26?

    Question 25. Construire un terme f de type Boole -> O tel que f(Bfaux) = faux et f(Bvrai) = vrai. *résolue*

    Question 26. En utilisant le tiers exclu, construire la fonction réciproque de f construite dans la question 25.

    Question 27. Que pensez-vous d'une fonction constructive (donc construite en particulier sans utilisation du tiers exclu) de type O -> Boole ?

  15. #155
    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 : 277
    Points
    277

    Par défaut

    Citation Envoyé par kaukau Voir le message
    Comment utilise t'on l'opérateur de description? Que décrit-il?
    Si j'ai bien compris, il donne la valeur de x fesant que E est vrai:
    x=#(p) avec p = W(!1x:T E)

    Comment l'utilise t-on dans la question 26?
    Je peux difficilement te dire comment l'utiliser dans la question 26 sans te donner la réponse à la question 26. Cependant, je peux répondre à tes premières questions ce qui te donne comment on l'utilise (ou plutôt, à quelle fin on l'utilise) en général, et en particulier dans la question 26.

    Comme tu l'écris, l'opérateur de description te permet de récupérer la valeur x pour laquelle une proposition E (de x) est vraie, lorsque celle-ci est bien vraie pour un seul et unique x évidemment. C'est pourquoi il prend en argument une preuve de !1x:T.E et te renvoit un terme de type T.

    Ca peut n'avoir l'air de rien comme ça (après tout, quoi de plus naturel, quand on a prouvé l'existence et l'unicité d'un élément vérifiant une propriété, de prendre cet élément, lui donner un nom et l'utiliser par la suite ?) mais tout l'intérêt de cet opérateur, ainsi que le rapport étroit qu'il entretient avec la question 26, c'est qu'il te permet de passer du domaine des preuves de proposition logique (les W(q) pour un q : O) à celui du type T
    sur lequel tu es en train de prouver une propriété, et ce quelle que soit la nature de ton type T ! En d'autres termes, il fait en quelque sorte office de "destructeur" du domaine propositionnel : sans lui, la seule chose que tu pourrais établir à partir de formules serait... d'autres formules ! Avec lui, tu peux (sous la condition contraignante que ta formule soit une preuve d'existence et d'unicité) récupérer un témoin à partir d'une preuve d'une formule.

    Maintenant, la fonction que tu dois construire dans la question 26 à le type O -> Boole, ie qu'elle doit prendre une proposition logique et renvoyer un booléen (qui sont un type d'objets que l'on a arbitrairement défini et qui n'a rien à voir avec les formules). Je pense que tu peux maintenant mieux cerner le rapport avec le rôle de l'opérateur de description
    I'm the kind of guy that until it happens, I won't worry about it. - R.H. RoY05, MVP06

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

    Informations forums :
    Inscription : janvier 2007
    Messages : 65
    Points : 43
    Points
    43

    Par défaut

    Bon, je tente:
    q:O |-> p:W(!1x:Boole q) |-> #(p)
    Mais c'est juste pour dire une connerie

  17. #157
    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 : 277
    Points
    277

    Par défaut

    Ben ce terme est de type ?q:O. (!1x:Boole.q) => Boole ce qui correspond pas vraiment à la question posée Ici tu te donnes une preuve de !1x:Boole.q pour pouvoir appliquer l'opérateur de description.. mais tu n'y couperas pas, pour répondre à la question, il faut que tu prouves toi-même un truc du type !1x:Boole.r pour un r bien choisi, sur lequel tu pourras ensuite appliquer #. C'est là que le tiers-exclu entre en jeu !
    I'm the kind of guy that until it happens, I won't worry about it. - R.H. RoY05, MVP06

  18. #158
    Membre du Club
    Inscrit en
    janvier 2007
    Messages
    65
    Détails du profil
    Informations personnelles :
    Âge : 35

    Informations forums :
    Inscription : janvier 2007
    Messages : 65
    Points : 43
    Points
    43

    Par défaut

    pff je nage.
    Comment construire un r alors qu'on a pas d'opérateur de construction pour les types O?
    C'est encore un peu flou pour moi ce qu'est une proposition.
    Est-ce que x=Bvrai est une proposition?

  19. #159
    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 : 277
    Points
    277

    Par défaut

    on en a bien un (et un seul) c'est le quantificateur existentiel. Rappelle toi qu'on a défini tous les autres opérateurs, (et le = aussi, ce qui répond à ta question) en termes du quantificateur existentiel.

    Pour te mettre sur la voie, que dire d'un booléen b tel que [x > Vrai, y > Faux]b ?
    I'm the kind of guy that until it happens, I won't worry about it. - R.H. RoY05, MVP06

  20. #160
    Membre du Club
    Inscrit en
    janvier 2007
    Messages
    65
    Détails du profil
    Informations personnelles :
    Âge : 35

    Informations forums :
    Inscription : janvier 2007
    Messages : 65
    Points : 43
    Points
    43

    Par défaut

    On peut dire qu'il existe un unique booléen b tel que [x > Vrai, y > Faux]b=Vrai?
    On peut donc utiliser l'opérateur de description?

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
  •