[Quizz] Fonctions et démonstrations.

[DrTopos]

Envoyé par Steki-kun

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

[kaukau]

Envoyé par DrTopos

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

[Steki-kun]

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) où 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

[DrTopos]

Envoyé par kaukau

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.

Envoyé par kaukau

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

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

[DrTopos]

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.

Envoyé par Steki-kun

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.

[Steki-kun]

Envoyé par DrTopos

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.

Envoyé par DrTopos

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 !

[kaukau]

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

[DrTopos]

Envoyé par kaukau

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

[kaukau]

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

[DrTopos]

Envoyé par kaukau

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.

Envoyé par kaukau

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.

Envoyé par kaukau

[*+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.

[kaukau]

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?

[DrTopos]

Envoyé par kaukau

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.

[kaukau]

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

[kaukau]

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é

[DrTopos]

Envoyé par kaukau

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.

Envoyé par kaukau

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

Envoyé par kaukau

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.

Envoyé par kaukau

Si c'est f-1, elle est du type O -> Boole.

C'est bien de cela qu'il s'agit.

[kaukau]

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+*]...

[DrTopos]

Envoyé par kaukau

On peut donc écrire une conditionnelle
[x > *+One, y > One+*]...

Non, on ne peut pas écrire ceci, car O n'est pas une somme.

[DrTopos]

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

[DrTopos]

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:

Code :

1
2
     
A --- a ---> B

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.

[SpiceGuid]

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.