[Quizz] Fonctions et démonstrations. - Page 8

DrTopos · 06/12/2007, 07h54

Citation:

Envoyé par SpiceGuid

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

c'est une simple copie d'écran

C'était cela la bonne idée à laquelle je n'avais pas pensé. Merci SpiceGuid.

DrTopos · 06/12/2007, 09h19

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.

kaukau · 06/12/2007, 14h37

Citation:

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" ?

DrTopos · 06/12/2007, 15h20

Citation:

Envoyé par kaukau

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 ?

kaukau · 06/12/2007, 16h00

Si je reprend les définitions:

Citation:

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

DrTopos · 06/12/2007, 16h31

Citation:

Envoyé par kaukau

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).

kaukau · 06/12/2007, 17h20

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?

DrTopos · 06/12/2007, 17h27

Citation:

Envoyé par kaukau

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.

kaukau · 09/12/2007, 15h56

Daccord, il faut un

Citation:

objet final dans la catégorie des cônes de base (A,B).

et

Citation:

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:

Citation:

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?

DrTopos · 09/12/2007, 17h33

Citation:

Envoyé par kaukau

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.

kaukau · 09/12/2007, 17h56

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.

DrTopos · 09/12/2007, 18h38

Citation:

Envoyé par kaukau

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.

kaukau · 11/12/2007, 10h29

Citation:

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...

kaukau · 11/12/2007, 10h39

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?

Citation:

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 ?

Steki-kun · 12/12/2007, 00h48

Citation:

Envoyé par kaukau

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

kaukau · 12/12/2007, 11h16

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

Steki-kun · 12/12/2007, 13h03

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 !

kaukau · 16/12/2007, 00h46

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?

Steki-kun · 16/12/2007, 01h22

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 ?

kaukau · 16/12/2007, 14h51

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?

06/12/2007, 09h19	#142
DrTopos Membre éclairé Inscription : 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	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é *AB, 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 AB) 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. __________________ Ma page maths.
	00

12/12/2007, 13h03	#157
Steki-kun Membre confirmé Inscription : janvier 2005 Messages : 222 Détails du profil Informations personnelles : Âge : 30 Localisation : France, Paris (Île de France) Informations forums : Inscription : janvier 2005 Messages : 222 Points : 273 Points : 273	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
	00

16/12/2007, 01h22	#159
Steki-kun Membre confirmé Inscription : janvier 2005 Messages : 222 Détails du profil Informations personnelles : Âge : 30 Localisation : France, Paris (Île de France) Informations forums : Inscription : janvier 2005 Messages : 222 Points : 273 Points : 273	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
	00

06/12/2007, 17h20	#147
kaukau Membre du Club Inscription : janvier 2007 Messages : 64 Détails du profil Informations personnelles : Âge : 34 Informations forums : Inscription : janvier 2007 Messages : 64 Points : 40 Points : 40	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?
	00

09/12/2007, 17h56	#151
kaukau Membre du Club Inscription : janvier 2007 Messages : 64 Détails du profil Informations personnelles : Âge : 34 Informations forums : Inscription : janvier 2007 Messages : 64 Points : 40 Points : 40	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.
	00

12/12/2007, 11h16	#156
kaukau Membre du Club Inscription : janvier 2007 Messages : 64 Détails du profil Informations personnelles : Âge : 34 Informations forums : Inscription : janvier 2007 Messages : 64 Points : 40 Points : 40	Bon, je tente: q:O \|-> p:W(!1x:Boole q) \|-> #(p) Mais c'est juste pour dire une connerie
	00

16/12/2007, 00h46	#158
kaukau Membre du Club Inscription : janvier 2007 Messages : 64 Détails du profil Informations personnelles : Âge : 34 Informations forums : Inscription : janvier 2007 Messages : 64 Points : 40 Points : 40	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?
	00

16/12/2007, 14h51	#160
kaukau Membre du Club Inscription : janvier 2007 Messages : 64 Détails du profil Informations personnelles : Âge : 34 Informations forums : Inscription : janvier 2007 Messages : 64 Points : 40 Points : 40	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?
	00

Outils de la discussion
Afficher une version imprimable Envoyer un lien vers cette page par email