+ Répondre à la discussion
Page 2 sur 9 PremièrePremière 123456 ... DernièreDernière
Affichage des résultats 21 à 40 sur 165
  1. #21
    Rédacteur
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    juin 2007
    Messages
    1 578
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 578
    Points : 2 712
    Points
    2 712

    Par défaut

    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

  2. #22
    alex_pi
    Invité(e)

    Par défaut

    Citation Envoyé par DrTopos Voir le message
    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) ff = ?q:O q, mais par commutativité non prouvé des quantificateurs universels, c'est la même :-))

    Citation Envoyé par DrTopos Voir le message
    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".

  3. #23
    Rédacteur
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    juin 2007
    Messages
    1 578
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 578
    Points : 2 712
    Points
    2 712

    Par défaut

    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

  4. #24
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 360
    Points
    360

    Par défaut

    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.

  5. #25
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 360
    Points
    360

    Par défaut

    Citation Envoyé par SpiceGuid Voir le message
    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]

  6. #26
    alex_pi
    Invité(e)

    Par défaut

    Citation Envoyé par DrTopos Voir le message
    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

    Citation Envoyé par DrTopos Voir le message
    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.

  7. #27
    alex_pi
    Invité(e)

    Par défaut

    Citation Envoyé par alex_pi Voir le message
    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.

  8. #28
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 360
    Points
    360

    Par défaut

    Citation Envoyé par alex_pi Voir le message
    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.

  9. #29
    Rédacteur
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    juin 2007
    Messages
    1 578
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 578
    Points : 2 712
    Points
    2 712

    Par défaut

    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.

  10. #30
    alex_pi
    Invité(e)

    Par défaut

    Citation Envoyé par DrTopos Voir le message
    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]

  11. #31
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 360
    Points
    360

    Par défaut

    Citation Envoyé par SpiceGuid Voir le message
    ?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 ?

  12. #32
    Rédacteur
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    juin 2007
    Messages
    1 578
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 578
    Points : 2 712
    Points
    2 712

    Par défaut

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

  13. #33
    Rédacteur
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    juin 2007
    Messages
    1 578
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 578
    Points : 2 712
    Points
    2 712

    Par défaut

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

  14. #34
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 360
    Points
    360

    Par défaut

    Citation Envoyé par SpiceGuid Voir le message
    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.

  15. #35
    Membre Expert
    Inscrit en
    avril 2007
    Messages
    831
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 831
    Points : 1 130
    Points
    1 130

    Par défaut

    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 ?

  16. #36
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 360
    Points
    360

    Par défaut

    Citation Envoyé par bluestorm Voir le message
    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.

  17. #37
    Membre Expert
    Inscrit en
    avril 2007
    Messages
    831
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 831
    Points : 1 130
    Points
    1 130

    Par défaut

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

  18. #38
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 360
    Points
    360

    Par défaut

    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.

  19. #39
    Rédacteur
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    juin 2007
    Messages
    1 578
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 578
    Points : 2 712
    Points
    2 712

    Par défaut

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

  20. #40
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 360
    Points
    360

    Par défaut

    Quelques remarques à propos de certaines réponses.

    Citation Envoyé par SpiceGuid Voir le message
    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.

    Citation Envoyé par bluestorm Voir le message
    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.

    Citation Envoyé par SpiceGuid Voir le message
    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.

Liens sociaux

Règles de messages

  • Vous ne pouvez pas créer de nouvelles discussions
  • Vous ne pouvez pas envoyer des réponses
  • Vous ne pouvez pas envoyer des pièces jointes
  • Vous ne pouvez pas modifier vos messages
  •