Une question de vie ou de mort

13»

Réponses

  • christophe c
    christophe c
    Oui je pense que tu as compris le principe, on prend une preuve et on se demande "ce qu'elle fait en tant que programme".

    Il est rare qu'on prenne un programme P et qu'on se demande quelle preuve D serait telle qu'elle donnerait P une fois les coms effacés

    Par exemple quel théorème de maths est prouvé par une preuve qui donne les programmes de Bu ou Zephir ?

    Ce sont des questions passionnantes, par exemple, les axiomes sont à peu près compris, mais il reste les théorèmes. J'ai déjà fait des fils ici où j'explique par exemple ce que fait le raisonnement par l'absurde (c'est l'astuce qui consiste à bluffer en faisant un chèque d'un montant "infini" de banque à un gangster pour l'attraper quand il viendra l'encaisser (c'est un "wanted" de western).

    JLKrivine a découvert que certaines formes affaiblies de l'axiome du choix utilisent une instruction qui correspond à "l'horloge" du PC par exemple

    Je me demande par exemple ce que peuvent bien faire les preuves du th de Tychonoff par exemple.

    Sinon, il y a une sorte de réciproque (peu à la mode) qui dit que si un programme ne boucle pas, il existe une preuve qui lui est attaché (c'est expliqué dans le livre "lambda calcul typé" de JLKrivine si tu veux.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • zephir
    zephir
    @cc : y-a-t-il lieu de distinguer entre algorithme et programme? Un algorithme, ça se démontre, non?
  • christophe c
    christophe c
    oui, pour moi c'est la même chose programme ou algorithme (enfin dans ce genre de discussion). Donc ce que je dis à propos de programmes peut se dire à propos d'algorithme
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    A noter (mais je ne veux pas trop digresser) que la crrespondance de Curry Howard ( même si ce n'est pas signalé par la communauté mathématique, souvent trop pudique) établit une sorte de morphisme entre pas seulement les preuves et les algorithmes, mais entre les preuves et les plans d'action dans la vie comme je l'ai déjà décrit dans un autre fil: je rappelle succintement comment:

    [size=x-small](priorité à gauche pour les parenthèses)
    1) L'axiome A=>(B=>C) =>(B=>(A=>C)) correspond à changer l'ordre dans lequel on présente des garanties
    2) L'axiome A=>B=>( (B=>X)=>(A=>X) ) correspond à la possibilité d'enchainer des actions
    3) L'axiome A=>(A=>X) =>(A=>X) correspond à la possibilité de photocopier des garanties (à noter que dans la vraie vie, certaines garanties ne sont pas "photocopiables" légalement, les chèques par exemple
    4) L'axiome A=>tout=>tout =>A correspond à une action plus compliquée qui est celle de mentir institutionnellement pour la bonne cause (c'est le wanted des western)
    5) L'axiome A=>(X=>A) correspond à la possibilité (ou la peu chère) action de ne pas utiliser une garantie qu'on possède, ie de jeter des choses à la poubelle (idem dans la vraie vie, l'environnement en prend un coup dans la casserole)

    Ces 5 axiomes sont exhaustifs en maths, ie à eux seuls ils suffisent à obtenir le théorème de complétude. En informatique, tout programme peut s'écrire à l'aide des 5 instructions qui correspondent comme suit:
    1) G a b c := b a c (on échange a et b)
    2) D a b c := b (a c) (on compose les effets de a et b)
    3) W a b := a b b (on duplique b avant de lancer a)
    4) CC x gestion des exceptions (voir ci-dessous ***)
    5) K a b :=a (on "jette" b)

    Tout programme peut s'écrire uniquement en implémentant G,D,W,K + gestion des exceptions

    *** CC x donne un cheque sans provision $\alpha$ à x, ie lance x $\alpha$, mais reprend la main si le processus lancé aboutit à un moment donné à vouloir exécuter une action de la forme "$\alpha$ t" (alpha est une "fausse" garantie et le processus ne le sait pas, donc quand il veut se servir de alpha en lui donnat l'argument t, il se retrouverait trahi. En reprenant la main, on récupère t (en fait "t" était le "bandit" que l'institution (processus appelant de départ) désirait tant, elle a donc publié un "wanted", et le fait de simuler un alpha qui n'est qu'un leurre a permis de "faire venir t" au guichet de la banque pour le capturer.[/size]
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • samok
    samok
    [size=x-small](ce qui me perfore c'est que la correspondance de Curry-Howard, de ce que j'en ai humblement capté grâce à JL.Krvine, c'est que cela pourrait s'appliquer à notre petite tête, genre le "connais-toi toi même")
    (à suivre aux alentours de 2017 ...)[/size]

    S
  • christophe c
    christophe c
    samok, pour ne pas polluer ce fil, je transfers la réponse ici: http://www.les-mathematiques.net/phorum/read.php?16,358198,661874#msg-661874
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • zephir
    zephir
    @Bu : On peut encore gagner du temps (1/3 environ) en remplaçant dans la boucle intérieure de Jafar(n) le "if e>=0 then" par "if e<0 then break else".
    Un dernier raffinement : MatrixIneq étant appelé une seule fois, on peut mettre le code en ligne dans la procédure Testcas qui l'appelle. (gain # 12\%).

    Reste la question posée par Christophe. Que fait le nombre de stratégie gagnante lorsque n tend vers l'infini ? peut-on l'estimer ?

    Amicalement,
    zephir.

    edit : j'ai parlé trop vite. Il faut inverser la dernière boucle ainsi:
    for d from min(a,k-c,l-b) to 0 by -1 do
    le gain est moins sensible (10\% environ)
  • zephir
    zephir
    @cc (et ceux que cela intéresse) : voici la liste du nombre de stratégies gagnantes en fonction du nombre de pièces entre 5 et 40. Le graphique est plus parlant, mais je ne sais pas comment le recopier ici. Il est facile de récupérer cette liste et d'en faire un plot.

    [5, 11], [6, 6], [7, 21], [8, 0], [9, 36], [10, 6], [11, 55], [12, 1], [13, 83], [14, 7], [15, 114], [16, 3], [17, 157], [18, 9], [19, 204], [20, 5], [21, 265], [22, 12], [23, 330], [24, 8], [25, 413], [26, 15], [27, 499], [28, 12], [29, 606], [30, 19], [31, 717], [32, 16], [33, 851], [34, 24], [35, 989], [36, 21], [37, 1154], [38, 29], [39, 1322], [40, 27]
  • christophe c
    christophe c
    Pour 12, il n'y a qu'une stratégie!!! Bravo à celui qui l'a trouvé avant dans le fil du coup :D
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Connectez-vous ou Inscrivez-vous pour répondre.

Bonjour!

Pour participer au forum, cliquer sur l'un des boutons :

Connexion S'inscrire

Catégories

In this Discussion

Qui est en ligne 33

BibixCidrolinMatricule_63Médiat_SuprèmePaul Broussousbiguine_equationbisami.zitoussimanupldx1raoul.Szeste +21 Invités