Discussion :

[DrTopos]

Bonjour à tous.

Je vous propose un quizz portant sur les rapports entre fonctions et démonstrations. Il a été décidé de ne pas inclure ce quizz dans la série des défis fonctionnels à cause de son caractères plus théorique, et de ses objectifs assez différents.

Je tiens aussi à préciser que ce qui va être décrit ici n'est pas Anubis 2. Il y a bien sûr de nombreux points communs, mais ces concepts seront présentés dans Anubis 2 d'une manière beaucoup plus pratique pour l'utilisateur (avec pas mal de sucre syntaxique). Autrement-dit, vous devez considérer ce fil comme un jeu, et j'espère que vous vous amuserez bien. Les questions seront très progressives, et tout le monde peut essayer sans complexe.

Je remercie les modérateurs, et en particulier millie, pour le soutien qu'ils ont apporté à ce projet.

Aux nouvaux arrivants: Un résumé qui vous évitera de lire tout le fil se trouve ici. Par ailleurs, le deuxième post (ci-dessous) contient un glossaire des principales notions.

Je vais donc commencer par planter le décor. Nous sommes dans un langage fonctionnel 'imaginaire'. Dans ce langage, nous avons d'abord les types d'usage, c'est à dire les sommes, les produits et les types fonctionnels, ces types pouvant aussi être récursifs (avec certaines restrictions). Mais bien sûr, il y a d'autres types qui ne sont pas habituels dans un tel langage. Le premier d'entre eux est un type que je noterai O. Ce type a un seul constructeur, qui est défini par la règle suivante:

Si T est un type, si x est une variable de type T, et si E est un terme de type O, pouvant contenir des occurrences libres de x, alors:

?x:T E

est un terme de type O. Dans ce terme, la variable x est liée.

Je rappelle que le mot ``terme'' signifie tout simplement ``expression représentant une donnée''. C'est une construction du langage lui-même. C'est la dénomination usuelle en lambda-calcul. Une lambda-expression est un lambda-terme. Par contre, une expression représentant un type n'est pas un terme (du moins dans le langage qui nous occupe ici).

Dans un langage typé, chaque terme a un type bien défini, qui est également le type de la donnée représentée par ce terme. Toutefois, il arrive qu'on emploie un autre vocabulaire que ``terme'' pour les termes de certains types. Ce sera le cas pour le type O, mais nous y reviendrons.

Pour ceux qui auraient un doute sur le sens de l'expression ``Dans ce terme, la variable x est liée.'', je précise qu'il s'agit du même concept que pour un lambda-terme. Dans le lambda-terme \x:T E, qu'on peut aussi écrire (x:T) |-> E, la variable x est liée. Voici donc la première question.


Question 1. Vous avez remarqué sans doute que pour construire un terme de type O, il nous faut un terme de type O. Dans ces conditions, on peut se demander s'il existe ne serait-ce qu'un seul terme de type O. La réponse est oui, et la question est d'en trouver un (et même plusieurs).

[DrTopos]

Je maintiens dans ce post une liste de liens sur divers explications données dans ce fil. C'est une sorte de glossaire, ou d'index, qui devrait vous aider à retouver le sens d'un mot ou la définition d'un concept. Certains de ces liens pointent sur ce glossaire lui-même. C'est le cas quand les seules explications disponibles sont celles du glossaire.

Voir également le résumé.

• Boole Types des Booléens, défini comme la somme One+One.
  
• conjonction L'énoncé E & F est une abbréviation pour !x:W(E) F.
  
• constructeur Un constructeur pour un type T est un procédé pour construire des données de type T. Pour les types fonctionnels, le constructeur est la flèche: |->.
  
• constructivisme
  
• dépendance (dans la langue naturelle et en mathématiques)
  
• description (opérateur de _) une fonction de W(!1x:T E) vers T.
  
• destructeur Un destructeur pour un type T est un procédé permettant de détruire (utiliser) les données de type T. Pour les types fonctionnels le destructeur est l'applicateur (qui permet d'appliquer une fonction à un argument).
  
• disjonction notée E | F, où E et F sont deux énoncés. Abbréviation pour ?q:O (E => q) => ((F => q) => q).
  
• énoncé Un énoncé est un terme de type O.
  
• faux (énoncé) abbréviation pour ?q:O q
  
• Heyting (Sémantique de) Identification de W(?x:T E) avec (x:T) -> W(E).
  
• hypothèse Faire l'hypothèse E (où E est un énoncé) consiste à déclarer un témoin de E, comme dans l'expression (t:W(E)) |-> ...
  
• implication notée: E => F, où E et F sont deux énoncés. Abbréviation pour ?p:W(E) F.
  
• négation notée: ~E, où E est un énoncé. Abbréviation pour E => faux.
  
• O Le type des ``valeurs de vérité''.
  
• O Règles d'usage du type O.
  
• paire de Heyting notée <a,t>. Abbréviation pour (q:0) |-> (p:W(?x:T (E => q)) |-> p(a)(t), où a est de type T, et t de type W(E[ a/x ]).
  
• preuve Une preuve de l'énoncé E est un terme de type W(E).
  
• quantificateur existentiel noté: ! L'énoncé !x:T E est une abbréviation pour ?q:O ((?x:T (E => q)) => q).
  
• quantificateur universel noté: ? Unique constructeur du type O. Le type O n'a pas de destructeur.
  
• remplacement noté: E[ a/x ], où E et a sont des expressions, et x un symbole. Se lit: ``E dans lequel a remplace x''.
  
• témoin Un témoin de l'énoncé E est une donnée de type W(E).
  
• tiers exclu noté EM. C'est une preuve de ?q:O (q | ~q) (non constructif).
  
• unicité L'énoncé !1x:T E est une abbréviation pour !x:T (E & ?y:T E[ y/x ] => x = y) (``il existe un unique x de T tel que E'')
  
• variable (variable pouvant en cacher une autre)
  
• vrai (énoncé) abbréviation pour ?q:O ?p:W(q) q
  
• W(E) Type des témoins de E.
  

[gasche]

Mon essai de réponse :

?x:O x

(on peut alors construire d'autres valeurs, comme ?y:T ?x:O x, si T est un type existant)

[DrTopos]

bluestorm a raison. On est en effet obligé de déclarer une variable de type O dans la construction même d'un premier terme de type O. Il n'y a pas moyen de faire autrement. Ensuite évidemment, on peut compliquer le terme en utilisant éventuellement d'autres types, puisqu'on en a sous la main. Je signale que la première réponse m'a été envoyée par mp par SpiceGuid. Elle est similaire à celle de bluestorm, sauf qu'il donne un deuxième exemple n'utilisant pas de type autre que O:

?f:O -> O ?x:O f(x)


Voici maintenant la suite de notre feuilleton. D'abord, quelques explications sur les intentions qui sont cachées derrière le type O et les termes de ce type. L'expression:


?x:T E


s'écrirait en mathématiques de la façon suivante:



et se lirait: ``quelque soit x dans T, E''. Il s'agit de ce qu'on appelle habituellement un ``énoncé''. Bien sûr, c'est un énoncé particulier, car c'est un énoncé ``universellement quantifié'', c'est à dire commençant par le signe qu'on appelle ``quantificateur universel'', et qui est ici noté: ? . On verra toutefois qu'il n'est pas si particulier que cela, car le type O ne recevra aucun autre constructeur.

Le sens intuitif de l'énoncé ?x:T E est celui de la phrase ci-dessus, à savoir que l'énoncé E (qui dépend de x) est vrai pour toute valeur de x de type T. Ceci bien sûr n'est pas une définition précise du quantificateur universel. Son sens formel apparaîtra plus tard, car il est conséquence de ce qui va suivre.

Les termes de type O seront donc désormais appelés des ``énoncés''. Comme tous les termes, ils représentent quelque chose. Il est traditionnel d'appeler ``valeur de vérité'' ce qui est représenté par un énoncé. Le type O est donc le ``type des valeurs de vérité''. N'allez pas croire pour autant qu'il s'agit du type des booléens. C'est un type différent, mais qui a des liens avec le type des booléens comme on le verra plus tard. Pourquoi l'ai-je appelé O ? C'est parce que O est la première lettre du mot Omega, et que la lettre grecque ``grand Omega'' est le symbole traditionnellement utilisé en Théorie des Topos pour représenter ce type. Par ailleurs, de même qu'on a l'habitude d'utiliser la lettre n ou m pour représenter un nombre entier, ou la lettre z pour représenter un nombre complexe, l'habitude est d'utiliser la lettre q pour une variable de type O. Mais évidemment, ce n'est pas obligatoire.


Voici maintenant la question. Ce n'est pas une question très formelle, car elle est destinée à raccrocher les concepts définis ici à une notion familière dont je n'ai pas donné de définition précise. Mais comme elle est familière, chacun doit avoir son idée. Bien sûr il faut tenir compte de l'interprétation donnée plus haut de ?, à savoir que c'est le quantificateur universel. Ce qui va être intéressant est de voir comment chacun pense cette notion familière.

Question 2. Quel sens attribuez-vous à l'énoncé ?q:O q ?

[gasche]

On peut sans doute le lire comme la tautologie logique "q implique q" ?


edit :
la transposition littérale de l'interprétation proposée est "l'énoncé $q$ est vrai pour tout énoncé $q$".
Si l'on considère une énoncé comme une valeur logique, ça me semble bien ressembler à du "q implique q".
Si on voit l'énoncé comme une valeur, ça ressemble à la fonction identité (sur O), et on peut sans doute voir ça aussi comme une règle de construction de preuve "si on a q, on peut en déduire q", mais j'ai l'impression que ce ne sont que des variations de la première idée, où l'on change le sens (informel de toute façon) du mot "implique".

J'attend avec impatience que quelqu'un ait une autre idée, je me sens "inhibé" sur le coup ^^

[DrTopos]

On peut sans doute le lire comme la tautologie logique "q implique q" ?

Ce n'est pas cela. J'invite tous les participants à ne pas se laisser inhiber par cette première réponse et à donner leur avis.

[alex_pi]

Question 2. Quel sens attribuez-vous à l'énoncé ?q:O q ?

Je lis ça "pour toute proposition A, A", mais je ne suis pas sûr que ça réponde à la question (même si ça me parle) :-)

[DrTopos]

la transposition littérale de l'interprétation proposée est "l'énoncé $q$ est vrai pour tout énoncé $q$"

C'est juste.

Si l'on considère une énoncé comme une valeur logique, ça me semble bien ressembler à du "q implique q"

Mais là tu fais erreur.

Je lis ça "pour toute proposition A, A"

C'est encore juste, et c'est d'ailleurs la même interprétation que celle de bluestorm.

Toutefois, ceci ne répond que partiellement à la question. Je donne une indication: la réponse tient en un seul mot. Mais quand vous l'aurez trouvée, il faudra encore l'expliquer, c'est à dire la justifier.