Discussion :

[SpiceGuid]

On pourrait peut-être commencer par donner un type, je propose:

Question 4: O->O

Question 5: (E:O) -> (F:O) -> W(E) -> W(F)


EDIT:

Après énoncé des réponses je développe le commentaire de DrTopos.

alex_pi a trouvé grâce à une approche sémantique, voici quelle était d'après moi la solution purement syntaxique.
Les deux énoncés recherchés étaient de type O, la bonne approche était de typer un témoin des énoncés recherchés:

Question 4: (x:W(E)) -> W(faux)

Question 5: (x:W(E)) -> W(F)

La sémantique de Heyting donnait alors un type plus direct du témoin:

Question 4: W(?x:W(E) faux)

Question 5: W(?x:W(E) F)

Connaissant le type du témoin on connaît l'énoncé que le témoin prouve, la réponse était donc:

Question 4: ?x:W(E) faux

Question 5: ?x:W(E) F

[alex_pi]

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

J'écrirai ça ?q:O ?x:W(E) q qui dit "pour tout énoncé q, une preuve de E donne une preuve de q" (en gros, "le faux implique n'importe quoi". D'ailleurs, si les questions avaient été dans l'autre sens, j'aurais écris ça ?x:W(E) f où f = ?q:O q, mais par commutativité non prouvé des quantificateurs universels, c'est la même :-))

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

J'écrirai ça ?x:W(E) F, ce qui se lit "une preuve de E prouve F".

[SpiceGuid]

D'accord avec alex_pi pour la question 5, la fonction => est:
(E:O) |-> (F:O) |-> ?p:W(E) F qui est de type O->O->O

[DrTopos]

Excellente réponse d'alex_pi.

?q:O ?x:W(E) q est en effet une façon d'exprimer ~E. Car en fait, quelle est la définition de la négation de E ? Cela doit être un énoncé qui nous dit que E est faux. Pour cela il suffit qu'il dise que E entraine faux (car comme faux entraine tout énoncé, l'autre sens est acquis d'avance). Donc, il suffit qu'il dise que si jamais E était vrai, alors faux le serait aussi. Cette dernière phrase peut s'écrire:

?x:W(E) faux

c'est à dire ?x:W(E) ?q:O q.

Maintenant, les quantificateurs universels peuvent s'intervertir dans ce terme, mais ce n'est pas le cas pour tous les termes, ce qui me fournit l'occasion de poser deux nouvelles question (ci-dessous).

De même, le terme ?x:W(E) F est une bonne définition de E => F, puisque qu'un témoin de cet énoncé est une fonction de W(E) vers W(F), donc un outil qui fabrique un témoin de F pour tout témoin de E. Ici encore cette interprétation pourrait s'appeler ``sémantique de Heyting''. En effet, Heyting à énoncé une règle pour chaque connecteur logique. Dans ce système, on n'a besoin que d'une seule règle puisqu'on fait la logique avec un seul connecteur logique: le quantificateur universel.

Question 6. Soit E un énoncé. Programmez une fonction de W(?x:W(E) ?q:O q) vers W(?q:O ?x:W(E) q) et une autre en sens inverse.

Question 7. Donnez un exemple d'un énoncé correct qui devient incorrect (c'est à dire mal formé) quand on y intervertit deux quantificateurs universels.

[DrTopos]

D'accord avec alex_pi pour la question 5, la fonction => est:
(E:O) |-> (F:O) |-> ?p:W(E) F qui est de type O->O->O

Ceci est effectivement bien typé, mais la question était de définir E => F, sachant que E et F sont déjà donnés, et non pas de définir la fonction qui envoie deux énoncés sur leur implication. Aussi la bonne réponse est ?p:W(E) F, qui est de type O bien sûr, sans les deux premières déclarations.

[edit]
En relisant, je m'aperçois que j'ai été un peu injuste avec SpiceGuid. Il a dit ``la fonction => ...''. C'est donc une très bonne réponse. J'avais cru qu'il avait confondu une definition de E => F avec une définition de =>, ce qui n'est pas le cas. Mille excuses.
[/edit]

[alex_pi]

Question 6. Soit E un énoncé. Programmez une fonction de W(?x:W(E) ?q:O q) vers W(?q:O ?x:W(E) q) et une autre en sens inverse.

Rappelons que W(?x:W(E) ?q:O q), c'est (x:W(E)) -> (q:O) -> W(q) et que W(?q:O ?x:W(E) q) est (q:O) -> (x:W(E)) -> W(q). Il suffit donc d'écrire une fonction inversant l'ordre des arguments, soit :
f:W(?x:W(E) ?q:O q) |-> (q:O) |-> (x:W(E)) |-> f x q (avec curryfication et parenthesage à droite)
Et dans l'autre sens :
g:W(?q:O ?x:W(E) q) |-> (x:W(E)) |-> (q:O) |-> g q x

Question 7. Donnez un exemple d'un énoncé correct qui devient incorrect (c'est à dire mal formé) quand on y intervertit deux quantificateurs universels.

Là par contre, je coince un peu. On a un type avec un seul constructeur, donc tous les "pour tout" sont en début d'énoncé, et par permuations successives, on peut tous les permuter. J'ai du louper un truc.

[alex_pi]

Là par contre, je coince un peu.

Maintenant que j'y pense, vous suggérez peut être quelque chose comme
?E:O ?x:W(?q:O q) E
Où l'inversion de ?q et ?x n'aurait aucun sens.

[DrTopos]

Maintenant que j'y pense, vous suggérez peut être quelque chose comme
?E:O ?x:W(?q:O q) E
Où l'inversion de ?q et ?x n'aurait aucun sens.

Non, je voulais parler de deux quantificateurs qui se suivent, autrement-dit d'un énoncé bien formé de la forme ?x:T ?y:U E, qui devient mal formé quand on l'écrit ?y:U ?x:T E.

[SpiceGuid]

C'est du aux types dépendants.

?q:O ?x:W(q) q

On échange les deux quantificateurs:

?x:W(q) ?q:O q

Ce terme n'est plus correct car W(q) n'est pas dans la portée de la définition de q.

[alex_pi]

Non, je voulais parler de deux quantificateurs qui se suivent, autrement-dit d'un énoncé bien formé de la forme ?x:T ?y:U E, qui devient mal formé quand on l'écrit ?y:U ?x:T E.

Lorsque le sage montre la lune, le fou regarde le doigt...


?q:O ?x:W(q) q



[EDIT]Je me suis fait doubler :-( [/EDIT]

[DrTopos]

?q:O ?x:W(q) q

On échange les quantificateurs:

?x:W(q) ?q:O q

Ce terme n'est plus correct car q n'est pas dans la portée de W(q).

Exactement. C'est un effet des types dépendants.

Par ailleurs, la réponse d'alex_pi à la question 6 est tout à fait bonne.

Question 8. Un énoncé de la forme E => F, qui n'est donc qu'une abbréviation pour ?x:W(E) F, est bien formé même si F a des occurrences libres de x. Autrement-dit, l'implication peut être dépendante. Pouvez-vous donner un exemple réaliste (c'est à dire non tiré par les cheveux) d'une telle dépendance dans la langue naturelle et dans les mathématiques élémentaires ?

[SpiceGuid]

Dans les mathématiques pour prouver P(n) pour tout n positif on doit notamment prouver l'implication P(n)=>P(n+1).

[SpiceGuid]

Ok, c'est bidon parce que, si j'ai bien compris, x n'est pas défini dans E.

[DrTopos]

Ok, c'est bidon parce que, si j'ai bien compris, x n'est pas défini dans E.

Cette remarque m'incite à donner une précision.

Si on a un lambda-terme de la form (x:T) |-> E, ou un énoncé de la forme ?x:T E, avec des occurrences libres de x dans T, alors la déclaration x:T cache une précédente déclaration de x, car il est entendu (ou sous-entendu, mais ça va mieux en le disant) que la partie type d'une déclaration ne peut pas dépendre de la variable déclarée dans la même déclaration.

Notre système marche en préemption, c'est à dire que toute nouvelle déclaration d'une variable cache les précédentes déclarations de la même variable.

Toutefois, pour que tout soit plus clair et plus facile, on adoptera la règle qu'une variable n'a pas le droit d'en cacher une autre. Autrement, dit, dans une même expression, les variables de toutes les déclarations doivent avoir des noms distincts.

[gasche]

J'essaie de bien comprendre la question (le concept de "dépendance" n'est pas encore complètement clair pour moi).

Voici mon interprétation (est-elle correcte ?) : On travaille sur des termes de la forme ?x:W(E) F, que l'on peut interpréter "si x est une preuve de E, alors F". En général, F ne dépend pas de x, parce que quand on dit "E implique F", on ne s'occupe pas de la manière dont on a prouvé E (le x), mais seulement du fait qu'on a une preuve, et on considère toutes les preuves comme équivalentes. Ce que demande la question, c'est un cas où F dépend de x, c'est à dire où la conclusion prend en compte la manière dont ont été prouvées les prémisses. C'est bien ça ?

[DrTopos]

J'essaie de bien comprendre la question (le concept de "dépendance" n'est pas encore complètement clair pour moi).

Voici mon interprétation (est-elle correcte ?) : On travaille sur des termes de la forme ?x:W(E) F, que l'on peut interpréter "si x est une preuve de E, alors F". En général, F ne dépend pas de x, parce que quand on dit "E implique F", on ne s'occupe pas de la manière dont on a prouvé E (le x), mais seulement du fait qu'on a une preuve, et on considère toutes les preuves comme équivalentes. Ce que demande la question, c'est un cas où F dépend de x, c'est à dire où la conclusion prend en compte la manière dont ont été prouvées les prémisses. C'est bien ça ?

Ton raisonnement est bien mené, sauf quand tu dis: c'est à dire où la conclusion prend en compte la manière dont ont été prouvées les prémisses.

[gasche]

Hum, on dirait que je me suis (encore une fois) laissé aller à une interprétation excessive. La conclusion utilise x, qui représente la preuve de E, mais ça ne veut pas forcément dire qu'on exploite une particularité de x par rapport aux autres preuves de E (je dirais que ça ressemble au polymorphisme paramétrique, mais je préfère rester prudent maintenant ).

[DrTopos]

On m'a signalé par mp que certaines personnes, qui aimeraient sans doute participer, avait parfois du mal à suivre ce fil, pour la raison que j'ai supposé certains concepts acquis, alors que cela peut ne pas être le cas. Il se peut aussi que le vocabulaire que j'emploie ne fasse pas partie de vos standards selon votre parcours.

Il vaut sans doute mieux que je ne donne pas d'explication non sollicitée, car je risque de noyer le poisson. J'essaye de maintenir mes explications dans des limites de volume raisonables.

Toutefois, si certaines choses vous paraîssent obscures, n'hésitez pas à poster une demande d'explication. Je donnerai les explications dans un post, et je maintiens dans le deuxième post de ce fil une liste de liens sur ces explications, pour qu'on puisse les retrouver facilement.

[SpiceGuid]

Oui, ce qui est demandé ce sont des exemples pour lesquels la conclusion contient une occurence du témoin du prémisse.

[DrTopos]

Quelques remarques à propos de certaines réponses.

Dans les mathématiques pour prouver P(n) pour tout n positif on doit notamment prouver l'implication P(n)=>P(n+1).

Oui, mais cette implication n'est pas dépendante.

Hum, on dirait que je me suis (encore une fois) laissé aller à une interprétation excessive. La conclusion utilise x, qui représente la preuve de E, mais ça ne veut pas forcément dire qu'on exploite une particularité de x par rapport aux autres preuves de E (je dirais que ça ressemble au polymorphisme paramétrique, mais je préfère rester prudent maintenant ).

L'un des axiomes (dont je n'ai pas encore parlé) de ce système dit qu'un type de la forme W(E) ne peut pas contenir plus d'une seule donnée. La manière dont on démontre n'intervient donc pas (du moins au niveau de la logique, par contre au niveau des performances à l'exécution, elle intervient). Par ailleurs, je ne vois pas le rapport avec le polymorphisme paramétrique, puisqu'il n'a pas été question de variable de type (variable représentant un type quelconque) jusqu'ici.

Oui, ce qui est demandé ce sont des exemples pour lesquels la conclusion contient une occurence du témoin du prémisse.

Oui, ou pour être plus précis: une occurrence de la variable qui représente le témoin déclaré. Toutefois, je précise (et c'est une conséquence de l'axiome cité ci-dessus) que cette occurrence peut être implicite, c'est à dire invisible dans l'écriture de l'expression.