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.

[SpiceGuid]

C'est l'axiome de l'identité (du calcul des séquents).
Pour toute hypothèse q on peut démontrer q.

EDIT:

Flûte bluestorm l'avait déjà dit et ce n'est pas la réponse attendue.

J'ai une autre idée: cela signifie que q ne dépend d'aucun autre type que O donc q est polymorphe.

[DrTopos]

c'est l'axiome du calcul des séquents.
pour toute hypothèse q on peut démontrer q.

Non, ce n'est pas cela. Tu fais la même erreur que bluestorm. J'expliquerai un peu plus tard en quoi consiste cette erreur exactement (quand on aura les moyens de l'expliquer).

J'ai une autre idée: cela signifie que q ne dépend d'aucun autre type que O donc q est polymorphe.

C'est beaucoup plus simple, et surtout plus familier que cela.

[SpiceGuid]

Cet enoncé dit que la valeur de vérité de tous les énoncés est vrai, intuitivement la valeur de vérité de cet énoncé est faux, donc cet énoncé se contredit, sa valeur est absurde.

[monstre]

Cet enoncé dit que la valeur de vérité de tous les énoncés est vrai, intuitivement la valeur de vérité de cet énoncé est faux

Jusque là, je suis d'accord.

donc cet énoncé se contredit, sa valeur est absurde.

Là, je ne suis plus. Pourquoi dis-tu qu'il est absurde et non simplement faux? Parce qu'il affirme sa propre vérité?

[SpiceGuid]

Remarque:
On admet l'existence d'une primitive ~ de type O->O qui renvoie la négation d'un énoncé.

Démonstration par l'absurde:
?q:O q implique ~ ?q:O q
Conclusion: le sens de ?q:O q est faux.

[alex_pi]

Démonstration par l'absurde:

Manque de bol, les démonstrations par l'absurde, ni même par contraposition, ne sont admise en logique constructiviste où on ne dispose pas du tiers exclus

De plus, la négation d'un énoncé "pour tout blahblah" commence par "il existe blihblih", donc n'est pas dans O dans lequel on ne dispose que de "pour tout". Donc ça ne colle pas

En revanche, je ne nie pas forcément la conclusion :-)

[alex_pi]

Donc tu n'admet pas l'existence d'une fonction de négation de type O->O.

Voilà.

Bon, sinon, je pense effectivement que tu as raison sur le fait que ça représente le faux. Ma façon de le voir :

\forall b, (\forall a, a) -> b (se démontre en instanciant a à b)

or seul "faux" vérifie cette propriété. Malheureusement, on n'a pas encore l'implication, donc je ne suis pas sûr que la justification soit valide, mais je ne vois pas comment faire autrement. J'y réfléchirai en dormant

[DrTopos]

Manque de bol, les démonstrations par l'absurde, ni même par contraposition, ne sont admise en logique constructiviste où on ne dispose pas du tiers exclus

exact (sauf que pour la contraposition il y a une petite ambiguïté)

De plus, la négation d'un énoncé "pour tout blahblah" commence par "il existe blihblih", donc n'est pas dans O dans lequel on ne dispose que de "pour tout". Donc ça ne colle pas

On définira la négation sans 'il existe', et on construira 'il existe' quand même.

En revanche, je ne nie pas forcément la conclusion :-)

et tu as raison, car la collaboration entre SpiceGuid et monstre a produit la bonne solution:

La réponse à la question 2 est: faux.

Les explications sont difficiles à donner si on n'a pas de définition de faux. mais si on en a une ça va mieux.

Comme vous avez été plusieurs à le remarquer, l'énoncé ?q:O q se lit: ``l'énoncé q est vrai pour tout énoncé q'' ou encore ``pour toute proposition A, A'', ce qui revient au même, le mot ``proposition'' étant synonyme d'énoncé. Autrement-dit, ce que dit cet énoncé est ``tous les énoncés sont vrais''. Eh bien, c'est faux ! Du moins on l'espère car sinon on est mal du point de vue de la logique. En tout cas, le fait d'entrainer tous les autres énoncés est la définition habituelle de faux. C'est comme cela qu'on utilise faux dans les démonstrations. Dès qu'il est démontré, tout le reste suit automatiquement.

Un système logique est un système dans lequel on a des énoncés et des preuves. La raison d'être des preuves est de permettre de s'assurer qu'un énoncé est vrai, le principe étant que tout énoncé qui a été démontré est vrai (je n'ai pas dit: ``et réciproquement'' bien sûr). Si pour une raison quelconque, tous les énoncés peuvent être démontrés, ils sont tous vrais, et le fait de prouver perd tout son intérêt. S'ils sont tous vrais, plus n'est besoin de se casser la tête à chercher des démonstrations. Dans ce cas, on dit que le système logique est ``contradictoire'' ou ``incohérent'' ou ``inconsistant'' ou ``effondré''.

Ce qui est certain en tous cas, est que quelque soit la façon (raisonable quand même) dont on définira les preuves par la suite, l'énoncé ?q:O q doit entrainer tous les autres, puisqu'il dit qu'ils sont tous vrais. Si jamais on a le malheur de démontrer cet énoncé, on aura démontré tous les énoncés, et notre système logique sera effondré. On souhaite donc que cet énoncé soit un énoncé indémontrable.

Démontrer qu'il est effectivement indémontrable est une tâche difficile, car cela entraine que le système tout entier est cohérent. On sait depuis les travaux de Kürt Gödel, qu'une telle démonstration ne peut pas se faire dans le système lui-même s'il est cohérent. Autrement-dit, un système capable de prouver sa propre cohérence a en fait prouvé qu'il est incohérent.

Toutefois, si on simplifie un peu notre système en renonçant aux types récursifs, on peut assez facilement en démontrer la cohérence en en exhibant un modèle. Je vous proposerai de le faire un peu plus tard sous forme d'une série de questions (on peut le faire aussi avec les types récursifs, mais c'est nettement plus difficile). Pour prouver que le système (y compris avec des types récursifs) est non contradictoire, et sans en passer par des modèles ensemblistes, il faut utiliser les méthodes de la théorie de la démonstration (Tait-Girard). Je ne sais pas si nous irons jusque là.

Dans l'immédiat, vous allez donc admettre (ou tout au moins espérer) que l'énoncé ?q:O q n'est pas démontrable.




Vous êtes tous des habitués des langages fonctionnels, et donc vous connaissez les types fonctionnels. Si T et U sont des types, T -> U est un type (qu'on appelle ``type des fonctions de T vers U''). Vous savez aussi que ce type fonctionnel a un unique constructeur, qui est défini par la règle suivante:

Si T et U sont deux types, si x est une variable de type T, et si E est un terme de type U pouvant contenir des occurrences libres de x, alors

(x:T) |-> E

est un terme de type T -> U.

J'adopte la notation ci-dessus parce que c'est celle qui ressemble le plus à la notation mathématique usuelle (une flèche avec une barre verticale à l'origine). Mais bien entendu, j'aurais pu choisir une notation imitant celle du lambda-calcul: \x:T E. Faites comme bon vous semblera.

Les types fonctionnels ont aussi un destructeur qui s'appelle ``applicateur'', et qui permet l'application d'une fonction à un argument. La règle est la suivante:

Si f est un terme de type T -> U, et si a est un terme de type T, alors f(a) est un terme de type U.

Pour caractériser complètement notre type fonctionnel, ce n'est pas encore assez. On a besoin de dire que la construction et la destruction sont deux opérations réciproques l'une de l'autre. Ceci s'exprime de la façon suivante, ou E est un terme pouvant avoir des occurrences libres de x, et f un terme ne pouvant pas en avoir:

(1) ((x:T) |-> E)(x) est égal à E

(2) (x:T) |-> f(x) est égal à f

Les deux règles ci--dessus s'appellent respectivement ``beta-équivalence'' et ``eta-équivalence'' (je ne dis pas ``réduction'', car telles qu'elles sont formulées ici, ce ne sont pas des règles de calcul, mais des règles d'égalité).

Je suppose que tout le monde sait ce que veut dire ``substituer l'expression a à la variable x dans l'expression E''. Le résultat de cette substitution sera noté E[ a/x ], qui se lit ``E dans lequel a remplace x''. On remarquera que:

(((x:T) |-> E)(x))[ a/x ] n'est autre que ((x:T) |-> E)(a)

ce qui fait que la règle (1) ci-dessus donne l'égalité entre ((x:T) |-> E)(a) et E[ a/x ], ce qui est une façon plus habituelle de présenter la beta-équivalence.

Il y a divers arguments pour expliquer le fait que ce qui précède caractérise bien le type T -> U. On aura sans doute l'occasion d'en reparler.

Pour les besoins de ce qui va suivre, il est nécessaire de généraliser un peu cette notion de type fonctionnel. Imaginez que vous avez une variable x de type T, et un type U, qui dépend de x, c'est à dire que l'expression qui décrit le type U contient des occurences libres de la variable x. On n'a pas ce genre de chose (qu'on appelle ``type dépendant'') dans la plupart des langages fonctionnels. C'est par contre courant dans les systèmes de preuves (par exemple COQ).

Voici donc cette généralisation de la notion de type fonctionnel:

Si T est un type, x une variable de type T et U un type pouvant dépendre de x, l'expression (x:T) -> U est un ``type fonctionnel dépendant''.

Si E est un terme de type U (U peut dépendre de x), pouvant contenir des occurrences libres de x, (x:T) |-> E est un terme de type (x:T) -> U (``fonction dépendante'').

Si f est un terme de type (x:T) -> U, et a un terme de type T, le terme f(a) est de type U[ a/x ].

((x:T) |-> E)(a) est égal à E[ a/x ] (lequel est donc de type U[ a/x ])

(x:T) |-> f(x) est égal à f (pourvu que f n'ait pas d'occurence libre de x)

Voyons maintenant une nouvelle construction de types (la dernière en fait):

(1) Pour chaque terme E de type O, on a un type noté W(E).

(2) Le type W(?x:T E) est identique au type (x:T) -> W(E).

``Identique'' implique en particulier que tout terme de type W(?x:T E) est aussi un terme de type (x:T) -> W(E) et réciproquement.

Une donnée de type W(E) est appelée un ``témoin'' de E (en anglais, ``témoin'' se dit ``witness'', d'où le W). Un témoin de E est une donnée qui ``témoigne'' de la vérité de E. Si E a un témoin, il est vrai. Un terme de type W(E) est évidemment appelé une ``preuve'' de E.

Vous remarquerez l'extrême simplicité de cette définition de la notion de preuve (elle n'est pas tout à fait complète, car certains types de témoin ont un destructeur dont on parlera plus tard).


Une dernière remarque avant la question. La règle (2) ci-dessus dit qu'un témoin de ?x:T E est une fonction qui associe à tout x de T un témoin de E. C'est, exprimée d'une façon légèrement différente, une idée qui a été soutenue dès 1930 par le logicien Arend Heyting, l'un des pères de la logique constructive. Aussi, appellerons nous cette règle la ``sémantique de Heyting''.



Question 3. Ecrivez un terme de type W(?q:O ?x:W(q) q), et donnez la signification de l'énoncé ?q:O ?x:W(q) q.

[alex_pi]

Question 3. Ecrivez un terme de type W(?q:O ?x:W(q) q)

Allez hop, je m'y colle.

Bon, je ne suis pas sûr d'avoir exactement compris tout ce qui figure au dessus (il est tôt quand même :-)), mais tentons le coup :

le type W(?q:O ?x:W(q) q) est identique au type (q:O) -> W(?x:W(q) q). Or le type W(?x:W(q) q) est identique au type (x:W(q)) -> W(q)

On cherche donc un terme de type (q:O) -> ((x:W(q)) -> W(q))

Il me semble qu'un bon client est q |-> (x |->x) avec le typage qui va bien.

et donnez la signification de l'énoncé ?q:O ?x:W(q) q.

Pour tout énoncé q, la donné d'un témoin de q prouve q.

[DrTopos]

Il me semble qu'un bon client est q |-> (x |->x) avec le typage qui va bien.

Exact. Personellement, je préfère l'écrire avec les déclarations complètes:

(q:O) |-> (x:W(q)) |-> x

Pour tout énoncé q, la donné d'un témoin de q prouve q.

Exact, mais cela ne répond pas encore complètement à la question, dont la réponse, comme pour la précédente, tient en un seul mot.

[SpiceGuid]

alex_pi a exhibé un terme de type W(?q:O ?x:W(q) q) c'est-à-dire un témoin de l'énoncé ?q:O ?x:W(q) q, donc l'énoncé ?q:O ?x:W(q) q est vrai.

EDIT: j'ai utilisé la propriété à démontrer donc ça n'est pas vraiment une démonstration.

[DrTopos]

alex_pi a exhibé un terme de type W(?q:O ?x:W(q) q) c'est-à-dire un témoin de l'énoncé ?q:O ?x:W(q) q, donc l'énoncé ?q:O ?x:W(q) q est vrai.

Exact. la réponse est donc: vrai.

En fait, l'énoncé ?q:O ?x:W(q) q se lit ``tout énoncé qui a un témoin est vrai'', ou encore ``tout énoncé qu'on peut prouver est vrai''. Cette affirmation a des chances d'être vraie. De fait, on peut la prouver, comme l'a fait alex_pi. En conclusion, un énoncé qu'on peut prouver sans avoir besoin d'aucune hypothèse mérite de s'appeler ``vrai''.

Le terme (q:O) |-> (x:W(q)) |-> x est donc une preuve de vrai.

Toutefois, il y a d'autres façons (une infinité bien sûr) de définir vrai. La seule chose qui compte est d'avoir un énoncé fermé (sans variable libre), qu'on puisse démontrer sans hypothèse. Celui que j'ai proposé est seulement le plus simple que je connaisse.

Dans les deux questions précédentes, je vous ai demandé d'interpréter des énoncés. On va maintenant faire le contraire. Je vais vous demander de donner des définitions, dans le système construit ici, de concepts familiers. Bien sûr, il faut justifier vos propositions.

Question 4. Soit E un énoncé. Donnez une définition de la négation de E (qu'on notera ~E).

Question 5. Soient E et F des énoncés. Donnez une définition de l'implication de F par E (qu'on notera E => F).