[Quizz] Fonctions et démonstrations.

[Steki-kun]

Envoyé par DrTopos

Question 14. Soient T et U deux types ne dépendant pas des variables x et y, et E un énoncé pouvant dépendre de x et y. Le terme suivant est-il bien typé, et quel est son type ?

(p:W(!x:T ?y:U E)) |-> (y:U) |-> p(!x:T E)((x:T) |-> (r: (y:U) -> W(E)) |-> <x,r(y)>)

Bon, alors, je suis de retour sur developpez.net après de longs mois d'absence et je vois qu'il s'y passe des trucs très intéressants Malheureusement, j'ai pas eu le temps de lire les 6 pages de posts, je me suis contenté de la syntaxe donnée dans le post #2, donc j'espère que vous ne m'en voudrez pas si je suis à côté de la plaque.

Alors, la réponse courte : ce terme est bien typé et c'est une preuve de !x:T.?y:U.E => ?y:U.!x:T.E, en d'autres termes la permutation des deux quantificateurs.

La réponse longue : on suppose une preuve p du fait qu'il existe un x de type T tel que pour tout y de type U, E(implictement de x,y) est vrai. On suppose également un élément y de type U. Avec tout ça, on sent bien qu'on va montrer qu'il existe un x tel que E est vrai (avec le y supposé, qui n'est plus libre, donc je devrais écrire E[y/y] en toute rigueur, mais bon...). En d'autre termes, on va construire une preuve de !x:T.E.

Alors en maths, c'est facile, on dirait

D'après p, il existe x tel que pour tout y, E est vrai. En appliquant à notre y à nous, on a bien trouvé un x tel que E est vrai.

. Ici on est en codage du second ordre, donc pour détruire un quantificateur existentiel !x:T.Q, on l'applique simplement à la propriété P que l'on veut établir, puis à une preuve de ?x:T.Q=>P. Autrement dit, on montre que n'importe quel x de type T vérifiant Q fait l'affaire pour montrer P.

Ca se traduit bien par le fait que le terme de la question commence précisément par p(!x:T.E), donc par l'utilisation de l'hypothèse existentiellement quantifiée p pour établir !x:T.E. Là, pas besoin de comprendre le reste, on sait déjà que si le terme est bien typé il aura ce type là (ou tout du moins un suffixe commun, si jamais le machiavélique DrT. l'appliquait à son tour à une nouvelle proposition q, etc etc).

Mais vérifions quand même la suite On veut donc appliquer p(!x:T.E) à une preuve du fait que "pour tout x, si ce x est tel que E pour tout y, alors !x:T.E". Donc on prend un x:T, une preuve r du fait que ?y:U.E :

p(!x:T E)((x:T) |-> (r: (y:U) -> W(E)) |-> ...)

on note au passage qu'on utilise l'isomorphisme W(?y:U.E) ~~ (y:U) -> W(E). Il nous reste, armés de toutes ces hypothèses, à retourner une preuve du fait qu'il existe bien un x tel que E est vrai. Or, r(y) est une preuve de E, donc la paire de heyting <x,r(y)> relie précisément un élément x de type T et un "témoin" du fait que E(x) est vrai, et a en particulier le type voulu !x:T.E.

Voilà j'ai essayé d'être didactique comme ça si je me suis trompé on m'en voudra moins et merci à ceux qui auront lu jusqu'en bas

[DrTopos]

Bonjour à tous.

Pour une raison que j'ignore, je ne reçois plus les mails automatiques concernant cette discussion à laquelle je suis pourtant abonné. Je viens donc tout juste de découvrir les 3 derniers messages (grâce à un mail envoyé par l'un des participants).

Je me réjouis évidemment du rédémarrage de ce fil. J'ai cru qu'il était devenu trop abstrait, mais je vois qu'il n'en est rien.

Envoyé par Steki-kun

Alors, la réponse courte : ce terme est bien typé et c'est une preuve de !x:T.?y:U.E => ?y:U.!x:T.E, en d'autres termes la permutation des deux quantificateurs.

C'est exact.

Envoyé par Steki-kun

La réponse longue : on suppose une preuve p du fait qu'il existe un x de type T tel que pour tout y de type U, E(implictement de x,y) est vrai. On suppose également un élément y de type U. Avec tout ça, on sent bien qu'on va montrer qu'il existe un x tel que E est vrai (avec le y supposé, qui n'est plus libre, donc je devrais écrire E[y/y] en toute rigueur, mais bon...).

Ici, il y a effectivement un petit problème rigueur. La question pragmatique étant à mon avis de s'assurer qu'un compilateur peut vérifier le typage de ce terme sans risque de se tromper (et sans risque d'annoncer qu'il est bien typé si par hasard il ne l'était pas). Pour répondre à cette question, voici ce que donnerait l'énoncé de ce théorème sous forme de paragraphe Anubis 2 (je rappelle que $T et $U sont des paramètres de type):

Code :

1
2
3
4
5
for E[x:$T,y:$U]:O,
   define commutation_of_quantifiers:W((!x:$T ?y:$U E) => ?y:$U !x:$T E) 
       =
    ...

où les points de suspension seraient une formulation syntaxiquement très ``sucrée'' du terme de la question 14. On remarquera le prémbule for E[x:$T,y:$U]:O qui prévient le compilateur que le méta-symbole E représente un terme de type O n'ayant de sens que dans un contexte où x est déclaré de type $T et y déclaré de type $U. C'est d'ailleurs parce que j'avais cela en tête au moment où j'ai posé la question 14, que l'énoncé précise bien que E peut dépendre de x et y. A l'aide de ces indications le compilateur rejeterait un énoncé comme par exemple !x:$T ?z:$U E (en précisant que y est inconnu dans E). En fait, la complication ici vient du fait qu'on travaille à un niveau méta-mathématique, avec des méta-variables comme E, et que le statut de x et y qui sont des ``méta-variables de variables'' n'est pas clair. Une façon de rendre tout cela clair est de remplacer x et y par des profondeurs de de Bruijn. On n'a plus de cette façon qu'un seul niveau de variable (les méta-variables) et tout devient très clair.

Envoyé par Steki-kun

En d'autre termes, on va construire une preuve de !x:T.E.

Alors en maths, c'est facile, on dirait . Ici on est en codage du second ordre, donc pour détruire un quantificateur existentiel !x:T.Q, on l'applique simplement à la propriété P que l'on veut établir, puis à une preuve de ?x:T.Q=>P. Autrement dit, on montre que n'importe quel x de type T vérifiant Q fait l'affaire pour montrer P.

Ca se traduit bien par le fait que le terme de la question commence précisément par p(!x:T.E), donc par l'utilisation de l'hypothèse existentiellement quantifiée p pour établir !x:T.E.

En effet. De tout façon, arrivé à ce stade, on n'a pas beaucoup de choix. En fait, un programme même assez rudimentaire de recherche de preuve n'a pas besoin de chercher très longtemps pour voir que la seule conclusion de clause de Horn dans les hypothèses disponibles qui puisse s'unifier avec le résultat à démontrer est le symbole q dans l'hypothèse p qui n'est autre que ?q:O ((?x:T ((?y:U E) => q))) => q. Cela conduit immédiatement au terme p(!x:T E). (Remarque: à cause du fait que tout s'exprime avec le seul quantificateur universel, il n'y a que des clauses de Horn dans le système ce qui fait que l'algorithme de résolution de Robinson s'applique directement)

Envoyé par Steki-kun

Là, pas besoin de comprendre le reste, on sait déjà que si le terme est bien typé il aura ce type là (ou tout du moins un suffixe commun, si jamais le machiavélique DrT. l'appliquait à son tour à une nouvelle proposition q, etc etc).

Mais vérifions quand même la suite On veut donc appliquer p(!x:T.E) à une preuve du fait que "pour tout x, si ce x est tel que E pour tout y, alors !x:T.E". Donc on prend un x:T, une preuve r du fait que ?y:U.E :

En effet, puisqu'après remplacement de q par !x:T E, l'hypothèse dont p est une preuve devient ((?x:T ((?y:U E) => !x:T E))) => !x:T E.

Envoyé par Steki-kun

on note au passage qu'on utilise l'isomorphisme W(?y:U.E) ~~ (y:U) -> W(E). Il nous reste, armés de toutes ces hypothèses, à retourner une preuve du fait qu'il existe bien un x tel que E est vrai. Or, r(y) est une preuve de E, donc la paire de heyting <x,r(y)> relie précisément un élément x de type T et un "témoin" du fait que E(x) est vrai, et a en particulier le type voulu !x:T.E.

C'est tout à fait cela. Remarque: c'est mieux qu'un isomorphisme. Il s'agit bien du fait que W(?y:U E) et (y:U) -> W(E) sont le même type.

Envoyé par Steki-kun

Voilà j'ai essayé d'être didactique comme ça si je me suis trompé on m'en voudra moins et merci à ceux qui auront lu jusqu'en bas

Tu as été parfait.

La raison pour laquelle j'ai posé la question 14 est que la solution qui avait été donnée pour la question 12 ne faisait pas usage des paires de Heyting. Le terme de la question 14 est une solution de la question 12 en faisant usage.

Je vais bien sûr poser de nouvelles questions sous peu.

[kaukau]

Salut à tous,
Je me passionne pour ce fils.
Mais j'avoue que depuis la page 3-4, j'ai décroché et je n'arrive plus à raccrocher )

Je n'ai plus trop l'habitude des maths, donc il m'a fallut relire relire plusieurs fois les 4 premières pages, pour tout assimiler
Je suis aussi novice en langages fonctionnels, ce qui n'arrange sans doutes pas les choses.

La preuve de programmes, je trouve ça passionnant, et ce fils m'a aidé à y toucher un peu du doigt (ainsi qu'un autre fils ouvert par DrTopos, [Fondements] Preuve de programme: utopie ou réalité ?)

Mais pour l'instant, je manque encore d'exemples concrets:
Par exemple comment prouver dans mon programme qu'une division par zero n'arrivera pas?
Ou est écrit la preuve? juste après la division? Dans une zone réservés aux preuves? Que fait la preuve? Elle référence les identifiants de la "partie programme" pour prouver des propriétés de ceux-ci?
Pourrait-on avoir un exemple simple en psoeudo-langage?

Ce fils va vite (pour moi) et est devenu assez abstrait.. Ce qui serait sympa, ce serait d'avoir plus d'exemples dans la vie courante, comme dans ton post #67 DrTopos.
Je vote aussi pour un petit récapitulatif pour brosser une image complète à ce stade
En plus du lexique donné au post #2.
Par exemple, j'ai zappé ce qu'était les paires de Heyting.

Voila, j'espère que toutes ces demandes ne vous paraîtrons pas abusives.
Et encore bravo pour ce fils didactique et instructif.

[DrTopos]

Envoyé par kaukau

Salut à tous,
Je me passionne pour ce fils.
Mais j'avoue que depuis la page 3-4, j'ai décroché et je n'arrive plus à raccrocher )

Bienvenue sur ce fil et bravo d'avoir fait l'effort de le comprendre, même partiellement.

Envoyé par kaukau

Par exemple comment prouver dans mon programme qu'une division par zero n'arrivera pas?
Ou est écrit la preuve? juste après la division? Dans une zone réservés aux preuves? Que fait la preuve? Elle référence les identifiants de la "partie programme" pour prouver des propriétés de ceux-ci?
Pourrait-on avoir un exemple simple en psoeudo-langage?

J'ai déjà discuté de cela dans le fil [Fondements] Preuve de programme: utopie ou réalité ?. Je donnerai plus loin d'autres explications plus précises et même tout à fait détaillées sur ce problème, mais pour cela j'ai besoin de notions non encore introduites (ensembles (ce ne sont pas des types), opérateur de description, fonctions entre ensembles). Elle seront introduites sous peu.

Envoyé par kaukau

Ce fils va vite (pour moi) et est devenu assez abstrait.. Ce qui serait sympa, ce serait d'avoir plus d'exemples dans la vie courante, comme dans ton post #67 DrTopos.
Je vote aussi pour un petit récapitulatif pour brosser une image complète à ce stade
En plus du lexique donné au post #2.

Les exemples relevant de la langue naturelle ne sont pas ma spécialité. La théorie qui a inspiré ce fil (la theorie des Topos), est appliquée par les linguistes, mais j'avoue ne pas avoir eu le temps de me pencher sérieusement sur cet aspect des choses.

Par contre, l'idée du récapitulatif est excellente. Il facilitera sans aucun doute la prise du train en marche, et devrait permettre à certains de participer alors qu'ils ont probablement renoncé à décrypter toutes les interventions. Je vais m'y coller sous quelques jours.

Envoyé par kaukau

Et encore bravo pour ce fils didactique et instructif.

Merci bien.

[kaukau]

Envoyé par DrTopos

J'ai déjà discuté de cela dans le fil [Fondements] Preuve de programme: utopie ou réalité ?. Je donnerai plus loin d'autres explications plus précises et même tout à fait détaillées sur ce problème, mais pour cela j'ai besoin de notions non encore introduites (ensembles (ce ne sont pas des types), opérateur de description, fonctions entre ensembles). Elle seront introduites sous peu.

OK, patience, patience...
Une question ma turlupine quand même. Je la pose ici, mais si tu le préfère je la déplace dans l'autre fils, les 2 sujets sont proches:
Si je comprend bien, un programme est un énoncé. Dans la cadre d'un refactoring, on obtient un autre programme qui doit être sémantiquement équivalent. La preuve de programme peut-elle nous servir à prouver que les deux programmes sont "égaux"? Ce serait super!
Cette preuve peut-elle être automatique?

[DrTopos]

Envoyé par kaukau

Si je comprend bien, un programme est un énoncé.

Justement non. Ce sont plutôt les preuves qui sont des programmes. Les énoncés s'apparentent à des types. En effet, la donnée de l'énoncé E est équivalente à celle du type W(E). Par contre, les preuves de E (c'est à dire les termes de type W(E)) sont bien des programmes en général, puisque ce sont la plupart du temps des fonctions via la sémantique de Heyting.

D'ailleurs, comme je l'ai dit dans l'un des messages, les données de type O (les énoncés) s'implémentent sur zéro bits, bien que le type O soit loin d'être vide, puisqu'il y a plein d'énoncé. C'est dû à l'absence de destructeur pour le type O. Du fait qu'il n'y a pas de destructeur, un énoncé est inutilisable comme donnée. mais il est utilisable comme type via le W.

Envoyé par kaukau

Dans la cadre d'un refactoring, on obtient un autre programme qui doit être sémantiquement équivalent.

Je suppose que tu parles de refactoring automatique (techniques d'optimisation). Si ces techniques sont correctes, les anciennes preuves correctes se factorisent également pour donner forcément de nouvelles preuves correctes. Dans ce cas il n'y a donc rien à prouver.

Envoyé par kaukau

La preuve de programme peut-elle nous servir à prouver que les deux programmes sont "égaux"? Ce serait super!

Si le refactoring est automatique comme décrit ci-dessus, c'est inutile à condition qu'on ait prouvé une fois pour toutes que les techniques utilisées sont correctes.

Maintenant, évidemment, s'il s'agit non pas de refactoring automatique mais d'évolution, on peut avoir à modifier des preuves qui ne seraient plus correctes, et bien sûr des algorithmes de recherche automatique peuvent être utiles. Mais il ne faut pas en attendre de miracle (encore qu'ils nous étonnent parfois).

[kaukau]

Je pensais plutôt à un refactoring manuel.
Dans mon métier d'informaticien, on est souvent amené à faire des refactoring, comme par exemple de déplacer des traitements d'un package à l'autre.
Les réticences sont grandes, car ça n'apporte pas de nouvelles fonctionnalités, mais il faut quand même tout retester.
Si un processus automatique pouvait prendre les 2 programmes et dire "OK, ils sont équivalents", ce serait énorme.

Dans le cadre d'un programme où on n'a pas écrit de preuves, c'est possible?

Dans le cas où des preuves sont écritent pour le programme, effectivement il doit suffir de porter les preuves pour la nouvelle architecture pour valider à nouveau le programme.

[DrTopos]

Envoyé par kaukau

Si un processus automatique pouvait prendre les 2 programmes et dire "OK, ils sont équivalents", ce serait énorme.

Dans le cadre d'un programme où on n'a pas écrit de preuves, c'est possible?

Un tel procédé serait peut-être envisageable sous l'hypothèse que les transformations opérées lors du refactoring appartiennent à des types connus et facilement identifiables.

Toutefois, faire un tel logiciel sera de toute façon plus difficile que de faire un programme de refactoring automatique. Je pense donc qu'il vaut mieux abandonner cette idée et se concentrer sur les outils de refactoring automatique (avec éventuellement une part d'interactivité, par exemple pour choisir les noms des symboles).

[kaukau]

Effectivement,
un refactoring peut être vu comme une suite d'opérations élémentaires appliquées à un programme.
Si ces opérations sont certifiées "invariants sémantiques", elles peuvent être appliquées au programme sans craintes.

se concentrer sur les outils de refactoring automatique (avec éventuellement une part d'interactivité, par exemple pour choisir les noms des symboles).

Effectivement, je crois qu'il faudrait une bonne part d'interactivité, un refactoring étant essentiellement guidé par des considérations métier à mon avis (changement du niveau de modélisation, ajout de nouvelle fonctionnalité qui requiert un préalable etc.).

[DrTopos]

Voici quelques nouvelles questions. Ce ne sont que des classiques du genre, mais utiles pour la suite. La difficulté est variable.

Question 15. Trouver un terme de type W(?q:O (q => ~~q)).

Question 16. Trouver un terme de type W(?q:O (~~~q => ~q)).

Question 17. Montrer que si on a un terme de type W(?q:O (~~q => q)), alors on peut construire un terme de type W(?q:O (~q | q)), et réciproquement.

Question 18. Trouver un terme de type W(?p:O ? q:O ~(p | q) => (~p & ~q)).

Question 19. Trouver un terme de type W(?q:O ~~(q | ~q)).

[kaukau]

Je tente la question 15. Mes maths sont bien rouillés, mais le ridicule ne tue pas En m'inspirant du post #17 :

le type W(?q:O (q => ~~q)) est équivalent à
(q:O) -> W( q => ~~q).
qui est équivalent à
(q:O) -> W( ?x:W(q) ~~q)
car q => ~~q peut aussi s'écrire ?x:W(q) ~~q

Donc le terme recherché est de type:
(q:O) -> ((x:W(q)) -> W(~~q))

Heu comment conclure?
Je pourrais dire
~~q équivalent à
((q => Faux) => Faux) soit q
Mais je pense qu'il y a un hic.

[Steki-kun]

Question 15. Trouver un terme de type W(?q:O (q=>~~q)).

(q:O) |-> ((urd : W(q)) -> (abs : W(~q)) -> (p: O) -> (abs urd) p).

Avec le terme Coq correspondant :

Code :

1
2
3
4
Theorem Q15 : forall Q : Prop, Q -> ~~Q.
Proof.
 exact (fun Q urd abs => abs urd).
Defined.

Question 16. Trouver un terme de type W(?q:O (~~~q => ~q)).

(q:O) |-> (abs : W(~~~q)) |-> (urd : W(q)) |-> (p : 0) -> abs (Q15 q urd) p.

où Q15 correspond au terme de la question précédente. Avec le code Coq correspondant :

Code :

1
2
3
4
5
Theorem Q16 : forall Q : Prop, ~~~Q -> ~Q.
Proof.
  exact (fun Q abs urd => abs (Q15 Q urd)).
Defined.

Certains remarqueront que par rapport aux termes que je donne, mes termes Coq sont êta-réduits, mais je préfère tout détailler dans les réponses.

Question 17. Montrer que si on a un terme de type >(?q:O (~~q => q)), alors on peut construire un terme de type W(?q:O (~q | q)), et réciproquement.

Gauche vers droite :
(EM : W(?q:O.~~q => q)) |-> (q : O) -> (p : O) ->
(Hq : W(q => p)) |-> (Hnq : W(~q => p)) |->
EM p ((nP : W(~p)) |-> (r : O) |->
(aux ~q p Hnq nP (aux q p Hq nP) r)).

où aux est un terme qui prouve en gros (A -> B) -> ~B -> ~A, soit la seule partie de la contraposition qui est vraie en logique intuitionniste :

(a: O) |-> (b : O) |-> (H : W(a => b)) |-> (H' : W(~b)) |-> (abs : W(a)) |-> (r: O) |-> H' (H abs) r).

De la droite vers la gauche, c'est plus simple :
(EM : W(?q:O.(q | ~q))) |-> (q: O) |-> (nnq : W(~~q)) |->
EM q ((p : W(q)) |-> p) ((np : W(~q)) |-> nnq np q).

Code :

1
2
3
4
5
6
7
8
9
10
11
12
Theorem Q17 : (forall Q : Prop, ~~Q -> Q) <-> 
 (forall Q P : Prop, (Q -> P) -> (~Q -> P) -> P).
Proof.
  split.

  pose (aux := 
    fun (A B : Prop) (H : A -> B) (H' : ~B) (abs :A) => H' (H abs)).
  exact (fun EM Q P Hq Hnq =>
    EM P (fun nP => (aux (~Q) P Hnq nP (aux Q P Hq nP)))).

  exact (fun EM Q nnQ => EM Q _ (fun q => q) (fun nq => False_ind Q (nnQ nq))).
Defined.

Question 18. Trouver un terme de type W(?p:O ? q:O ~(p | q) => (~p & ~q)).

(p : O) |-> (q : O) |-> (H : W(~(p|q))) |->
(r : O) |-> (Hpqr : W(~P => ~Q => R)) |->
Hpqr
((tp : W(p)) |-> H ((s : 0) |-> (Hp : W(p=>s)) |-> (_ : W(q=>s)) |-> Hp tp))
((tq : W(q)) |-> H ((s : 0) |-> (_ : W(p=>s)) |-> (Hq : W(q=>s)) |-> Hq tq))

Avec encore une fois le code Coq correspondant :

Code :

1
2
3
4
5
6
7
8
9
10
11
Theorem Q18 : forall P Q : Prop, 
  ~(forall R : Prop, (P -> R) -> (Q -> R) -> R) ->
  (forall R : Prop, (~P -> ~Q -> R) -> R).
Proof.
  exact (fun P Q H R Hpqr =>
    (Hpqr 
      (fun np => (H (fun R Hp _ => Hp np))) 
      (fun nq => (H (fun R _ Hq => Hq nq)))
    )).
Defined.

Question 19. Trouver un terme de type W(?q:O. ~~(q | ~q)).

(q: O) |-> (H : W(~(q|~q))) |-> (r : O) |->
Q18 r q (~q) H ((urd : W(~q)) |-> (abs : W(~~q)) |-> abs urd r).

où Q18 est le terme de la question précédente.

Code :

1
2
3
4
5
6
7
Theorem Q19 : forall Q : Prop, 
  ~~(forall R : Prop, (Q -> R) -> (~Q -> R) -> R).
Proof.
  exact (fun Q H => 
    Q18 Q (~ Q) H False (fun (urd : ~ Q) (abs : ~ ~ Q) => abs urd)).
Defined.

Voilou :-) Si je me sens le courage de détailler la construction de ces termes dans la soirée, j'éditerai mon post en conséquence.

[kaukau]

Steki-kun pourrait-tu m'expliquer:

Question 15. Trouver un terme de type W(?q:O (q=>~~q)).

(q:O) |-> ((urd : W(q)) -> (abs : W(~q)) -> (p: O) -> (abs urd) p).

Ton terme est une fonction qui prend un énoncé q, une preuve de q et de non q, ce qui effectivement est absurde...
Mais ensuite comment combine tu deux preuves: (abs urd)
et comment ça s'applique à une nouvelle énoncé p??
(Et dailleurs les -> ne devrait-il pas être des |->?)

Question subsidiaire: Un énoncé peut-il être vu comme une proposition du style "le chat est gris"? Je n'ai pas très bien compris la différence entre signifiant et signifié évoqué plus tôt...

KauKau, qui tente desepérément de nager vers la surface...

[Steki-kun]

Pour prouver ~~q, il faut prouver que ~q est absurde, ou encore que ~q => Faux.
Or, dans le formalisme du DrTopos (et pas seulement), Faux est en fait défini comme "pour tout P, P". Autrement dit, montrer que qque chose est absurde, ou encore "prouver Faux", revient à prendre n'importe quelle proposition et à la prouver.

Donc pour prouver q => ~~q, je suppose q, ~q, et je m'attaque à une preuve de Faux : je prends une proposition quelconque p et je la montre.
Pour la montrer, j'applique ma preuve de ~q (ie. q => Faux) à q lui même, ce qui me donne une preuve de Faux, et je l'applique ensuite à p, ce qui me donne une preuve de p. C'est la signification de ce (abs urd) p.

J'aurais pu ne pas introduire p et montrer directement Faux en appliquant ~q à q, c'est ce que j'ai fait dans mon script Coq si tu regardes bien. De manière générale, remplacer un terme (x:T) |-> P x par P lorsque x n'apparait pas dans P s'appelle faire une êta-réduction, et tu comprends bien que deux tels termes sont équivalents.

Ah oui, pour les flèches, j'ai pas fait gaffe (trop l'habitude de Coq) donc -> ou |->, mais ne te laisse pas décontenancer par ça

[DrTopos]

Envoyé par kaukau

Question subsidiaire: Un énoncé peut-il être vu comme une proposition du style "le chat est gris"?

Bien entendu, puisque cette phrase est susceptible de valoir 'vrai' ou 'faux' (ou 'je ne sais pas' si la logique n'est pas binaire, etc...), c'est à dire une valeur de vérité. C'est d'ailleurs le cas de toutes les phrases qui sont construites autour d'un verbe, pourvu qu'elles ne soient pas impératives (si je dis: ``Toto, manges ta soupe !'', c'est de l'impératif, et cela ne représente pas 'vrai' ou 'faux'). Quant-aux phrases interrogatives comme ``le chat est-il gris ?'', je ne sais pas bien quel est leur statut. J'aurai tendance à penser que ma phrase impérative est un 'output' ('write', puisque j'attends un effet) et que ma phrase interrogative est un 'input' ('read', puisque j'attends une réponse). Autrement-dit, tout cela est de l'IO, c'est à dire autre chose que de la logique.

Envoyé par kaukau

Je n'ai pas très bien compris la différence entre signifiant et signifié évoqué plus tôt...

Un signifiant est de nature syntaxique. C'est une expression dans un langage. Le signifié correspondant est la chose qui est représentée par ce signifiant, autrement-dit son 'sens' ou sa 'signification' ou sa 'sémantique'. Par exemple, un énoncé est un signifiant, puisque c'est une expression du langage (un terme), alors qu'une valeur de vérité est un signifié, puisque c'est ce que représente un énoncé. De même, une preuve est un signifiant (terme de type W(...) par exemple dans ce système), alors qu'un témoin est un signifié puisque c'est ce que la preuve représente.

Puisque Steki-kun se mets aussi à mettre du Coq à droite à gauche, pourrait-on avoir une idée de la puissance de la théorie présentée par rapport au calcul inductif des constructions ?

(Je rappelle au passage que dans celui là, le "pour tout" est un produit dépendant et que "faux" est un type sans constructeur, ce qui pour l'instant me semble globalement être les deux différence notable. J'attends de voir l'arithmétique et ce genre de chose)

[Steki-kun]

Ben en ce qui concerne le Faux, les deux présentations sont strictement équivalentes : en fait forall P.P correspond exactement au schéma d'induction associé à un inductif sans constructeur. Autrement dit comme le type est vide, on montre n'importe quoi dès qu'on a un objet de type False sur lequel raisonner par induction.

Ex:

Code :

1
2
3
4
5
6
7
8
Theorem false_false :
 (forall P : Prop, P) <-> False.
Proof.
 split.
 exact (fun H => H False).
 intro H; induction H.
Qed.

Simplement, comme le CIC a les inductifs, ça parait plus naturel de définir False par

Code :

Inductive False := .

que par

Code :

1
2
Definition False := forall P : Prop, P.

Pour le quantificateur universel, il me semble tout aussi dépendant dans un cas que dans l'autre : quand on écrit ?q:O.?p:W(q).q, le produit est bien dépendant puisque le type de p dépend de la proposition q introduite.

Pour ma part, si je me souviens bien ce que j'ai vu en Master, on est pour l'instant dans un codage du 2nd ordre de la logique intuitionniste du premier ordre : on garde que la construction "quantification existentielle" et on se permet de quantifier sur les Propositions en plus des termes, ce qui permet de redéfinir les autres opérateurs logiques. Au passage, la sorte O est imprédicative puisqu'elle permet d'exprimer des choses sur elle-même.

NB : je suis intarissable sur les vertus de Coq donc je me laisse facilement aller mais je veux pas troller le quizz très intéressant du DrTopos donc si tu veux approfondir n'hésite pas à me MP.

[DrTopos]

Envoyé par alex_pi

Puisque Steki-kun se mets aussi à mettre du Coq à droite à gauche, pourrait-on avoir une idée de la puissance de la théorie présentée par rapport au calcul inductif des constructions ?

C'est bien d'avoir des utilisateurs de Coq qui vont pouvoir nous aider à mieux comprendre ce système, que pour ma part, je ne maîtrise pas du tout. La seule chose que je connaisse assez bien en matière de théorie de types est le système de Martin-Löf dont Coq est, me semble-t-il, issu, via le calcul des constructions inductives. Mais bien sûr , depuis sa conception il y a maintenant plus de 20 ans, ce système a beaucoup évolué. Il s'est donc sans doute éloigné de ce modèle d'origine. Qu'en pensent ceux d'entre vous qui le connaîssent bien ?

En particulier, il y a une question à laquelle je ne parvient pas à répondre clairement concernant Coq. Quand on parcourt la bibliothèque standard, on trouve des théorème démontrant le principe de proof-irrelevance à partir de divers autres principes. Par ailleurs, j'ai vu dans le tutoriel de la version la plus récente que le principe de proof-irrelevance faisait partie des propriétés du système. Donc il y a quelque chose que je ne comprends pas: proof-irrelevance est-il obligatoire ou non en Coq ? C'est probablement une option, un paramétrage du système, autrement-dit il n'y a sans doute pas un système Coq, mais plusieurs. J'aimerais que les spécialistes nous renseignent sur ce point.

Envoyé par alex_pi

(Je rappelle au passage que dans celui là, le "pour tout" est un produit dépendant et que "faux" est un type sans constructeur, ce qui pour l'instant me semble globalement être les deux différence notable. J'attends de voir l'arithmétique et ce genre de chose)

Il semble que Coq soit, du moins à l'origine, fortement influencé par l'isomorphisme de Curry-Howard. C'est sans doute la raison pour laquelle les énoncés sont des types, alors qu'ils sont des termes (avec un type associé toutefois bien sûr) dans le système présenté dans ce quizz. En conséquence, le quantificateur universel est un ``produit indexé'' (analogue au produit d'une famille d'ensembles), c'est à dire non pas un produit dépendant comme tu le dis, mais un ``type fonctionnel dépendant''. Dans le formalisme du quizz par exemple, l'énoncé ?x:TE correspond au type (x:T) -> E (type fonctionnel dépendant) et non pas au type (x:T)*E (produit dépendant). par ailleurs le produit dépendant est une ``somme indexée'' (analogue à l'union disjointe d'une famille d'ensembles).

Dans un système comme Martin-Löf, le quantificateur existentiel est la somme indéxée, alias produit dépendant. Le résultat de cette définition, et des autres axiomes du système est que deux preuves de l'énoncé !x:T E réalisées par deux paires de Heyting <a,p> et <b,q> pour lesquelles a est différent de b sont elles-mêmes différentes. C'est rendu obligatoire par le fait que la première projection pour les paires de Heyting est une opération légale qui de plus respecte l'égalité. Ainsi donc ces deux preuves sont différentes, ce qui fait que le système de Martin-Löf est incompatible avec proof-irrelevance.

D'après ce que j'ai lu dans le tutoriel Coq, l'obligation de proof-irrelevance est assortie d'une interdiction d'utiliser la première projection pour les paires de Heyting (qui portent un autre nom en Coq, je ne me souviens plus lequel). C'est évidemment indispensable pour conserver la cohérence logique.

Donc, mon opinion (à ce jour du moins) est que c'est le fait qu'on puisse ou non travailler sous le régime de proof-irrelevance qui fait la différence (au moins sur le plan de la logique, voir plus loin) entre Coq et le système que j'ai en tête, dans lequel proof-irrelevance sera de toute façon obligatoire. En effet, j'ai expliqué dans mon exposé de Luminy pourquoi ce principe est patent en mathématiques aussi bien classiques qu'intuitionnistes, et pourquoi le fait d'avoir un système qui ne le satisfait pas conduit à des mathématiques exotiques. Je précise que je n'ai rien contre ces mathématiques, mais mon but est de formaliser les mathématiques traditionnelles, pas des mathématiques nouvelles qui ne seraient certainement pas acceptées par les mathématiciens (du fait en particulier que certaines inclusions de sous ensembles dans des ensembles ne sont pas prouvablement injectives). En fait, la grande question à mon avis à propos de tous ces systèmes, sur laquelle tout le monde a travaillé depuis 20 ans, est de trouver un système dans lequel les notions de sous-ensemble et d'ensemble quotient se comportent comme on a l'habitude de les voir se comporter en mathématiques traditionnelles. Ma conclusion est que sans proof-irrelevance, ce n'est pas possible.

En conséquence, je comprends que les versions récentes de Coq imposent proof-irrelevance, du moins c'est ce qui apparaît dans le tutoriel. Malgré cela, Coq semble autoriser de très nombreuses variantes de systèmes d'axiomes (si j'en juge par le contenu de la bibliothèque) et reste donc un système très ouvert sur le plan de la logique et donc plutôt difficile à utiliser.

Mon but est de faire un système simple, non exotique au sens décrit plus haut (donc satisfaisant obligatoirement proof-irrelevance), et dans lequel l'écriture des preuves ressemble de très près aux textes mathématiques usuels. Sur ce dernier point au moins, on est obligé de reconnaître que l'écriture des preuves en Coq ne ressemble pas du tout à un texte mathématique usuel. J'ai essayé de lire la section consacrée à l'intégrale de Riemann dans la bibilothèque Coq. C'est un véritable supplice, même pour quelqu'un qui connait bien le sujet. Coq est totalement ésotérique, au moins en ce qui concerne l'écriture des preuves, quelques soient ses qualités par ailleurs. Pour cette raison, la plupart des mathématiciens ne voudront jamais l'utiliser. En particulier, il est clairement inutilisable en tant qu'outil pédagogique pour l'enseignement des maths. Il y a donc de la place pour un autre système, et c'est pour cela que je n'ai aucun complexe à essayer d'inventer autre chose.

Donc, autant que je puisse en juger, il y a deux différences essentielles: (1) obligation/non obligation de proof-irrelevance, (2) aspect des preuves. Bien entendu, en ce qui concerne (2), le quizz ne permet pas de juger de ce que j'ai en projet, puisque je n'ai pas parlé des preuves ``informelles'' mais seulement des preuves formelles. Les jolies formules, qui comme tu le dis deviennent difficiles à manier, seront générées par le compilateur à partir des preuves informelles. J'aurai sans doute l'occasion de donner quelques éclaircissements sur cette question dans le quizz.

Se souvenir aussi qu'à ce point du quizz, je n'ai pas encore donné tous les axiomes du système. Il reste à parler des types récursifs, de l'égalité, des axiomes d'extentionalité (dont proof-irrelevance), du principe de description et de l'axiome du choix (au minimum), si on veut avoir une vision complète du système.

[gorgonite]

Envoyé par DrTopos

C'est bien d'avoir des utilisateurs de Coq qui vont pouvoir nous aider à mieux comprendre ce système, que pour ma part, je ne maîtrise pas du tout. La seule chose que je connaisse assez bien en matière de théorie de types est le système de Martin-Löf dont Coq est, me semble-t-il, issu, via le calcul des constructions inductives. Mais bien sûr , depuis sa conception il y a maintenant plus de 20 ans, ce système a beaucoup évolué. Il s'est donc sans doute éloigné de ce modèle d'origine. Qu'en pensent ceux d'entre vous qui le connaîssent bien ?

perso, lorsqu'on a voulu me présenter la théorie soujacente de Coq, on m'a parlé de logique intuitionniste, calcul des séquents, et seulement ensuite de systèmes de type (système T, Martin-Löf, système F)



le poly en question...
http://www.lix.polytechnique.fr/~dow...es_types.ps.gz

[Steki-kun]

Pour répondre à certaines de vos interrogations Dr T., l'axiome de Proof-irrelevance, ainsi que beaucoup d'autres qui sont parfois plus forts (ie qui l'impliquent) comme l'extensionnalité et le tiers exclu, ne font pas partie de la logique de Coq de base. Cependant, ils ne rendent pas le système inconsistent pour autant et on peut les ajouter sans risque : c'est au choix, et ils se marient assez bien avec la sorte Prop, qui correspond à votre sorte O. Tout ceci est expliqué en détail dans la FAQ Coq sur le site de Coq.

Aussi je ne comprends pas trop la distinction que vous opérez : on peut tout à fait travailler sous le régime de la proof irrelevance dans Coq. J'irais même plus loin, puisque vous voulez faire de 'vraies' maths, alors la logique classique ne serait-elle pas plus naturelle que la logique intuitionniste ? Et avec le tiers-exclu, on peut prouver la proof-irrelevance des propositions dans Prop. Il y a ici une distinction importante dans le système Coq qui est peut être à la source de la confusion : celle entre la sorte Prop et la sorte Set. On peut avoir la proof-irrelevance sur des propositions de Prop c'est à dire :

Code :

Pour toute proposition P, toutes preuves p et p' de P, p = p'.

mais la proof-irrelevance des élements de Set est bien sûr inconsistante puisqu'il y a des ensembles à au moins deux éléments (autrement dit, si b et b' sont des booléens, il n'y a aucune raison que b et b' soient le même booléen). Cela explique qu'on ne puisse faire l'injection sur les premiers éléments d'une paire de Heyting par exemple.

Enfin, les scripts Coq sont peu lisibles c'est vrai mais là c'est un autre problème. On ne parle pas à une machine comme on parle à un humain, et c'est un problème des programmes informatiques en général, ils sont toujours moins faciles à comprendre que ce qu'ils font en réalité. Et puis, puisqu'on parle de proof irrelevance, lire un script Coq n'a d'intérêt que pour celui qui a changé son système et doit reprendre la preuve (de la "maintenance de preuve" si l'on veut...), la nature des théorèmes devrait suffire à comprendre de quoi ils parlent, et surtout le bon Coq-eur met les arguments de haut niveau dans des commentaires dans la preuve

Maintenant, c'est sûr que je rêve d'un système qui me permettrait de faire des maths comme je fais des maths sur papier, et qui me permettrait aussi de créer des fonctions 'computables' et d'en extraire un programme, mais pour l'instant il n'y a bien que Coq qui réponde à mes besoins.