Inscrivez-vous gratuitement
pour pouvoir participer, suivre les réponses en temps réel, voter pour les messages, poser vos propres questions et recevoir la newsletter
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.Envoyé par SpiceGuid
C'était cela la bonne idée à laquelle je n'avais pas pensé. Merci SpiceGuid.
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.
Dans les ensembles: le produit cartésienExercice: 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 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 ?
Si je reprend les définitions:
Il me semble que les seuls objets qui n'ont qu'une seule flèche qui pointe vers eux sont les nombres premiers.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.
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
Hum... Il y a deux flèches de cible 3, qui sont (1,3) et (3,3).
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.
Daccord, il faut un
etobjet final dans la catégorie des cônes de base (A,B).A et B étant les buts m tel que n divise m, n, m appartiennent à N+.les flèches sont tous les morphismes entre ces cônes.
Mais je n'ai pas très bien compris comment on trouve un objet final:
Comment on montre ça?Je vous laisse vous assurer vous-même que tout singleton est un objet final dans la catégorie des ensembles
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?
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.
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.
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.
Dans les ensembles: l'union disjointeExercice: 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 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...
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 ?
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
Bon, je tente:
q:O |-> p:W(!1x:Boole q) |-> #(p)
Mais c'est juste pour dire une connerie
Ben ce terme est de type ?q:O. (!1x:Boole.q) => Boole ce qui correspond pas vraiment à la question poséeIci 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
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?
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
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?
Vous avez un bloqueur de publicités installé.
Le Club Developpez.com n'affiche que des publicités IT, discrètes et non intrusives.
Afin que nous puissions continuer à vous fournir gratuitement du contenu de qualité, merci de nous soutenir en désactivant votre bloqueur de publicités sur Developpez.com.
Répondre avec citation
Partager