• [^] # Re: prouveur automatique/assistant de preuve

    Posté par (Mastodon) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.

    Cela fait qu'en gros, moyennant une machine suffisament puissante, on peut émuler un cerveau humain

    Ce qui a plein d'implications philosophiques rigolotes. Par exemple on peut facilement écrire un programme qui exécute tous les programmes possibles. Et donc, si on le laisse tourner suffisamment longtemps et avec suffisamment de mémoire, ce programme simulera toutes les consciences imaginables, y compris la mienne pendant que j'écris ça, mais aussi une version de moi où je n'écris pas ça.

    On pourrait pousser encore plus loin et d'autres l'ont fait, voir entre autres les travaux de Bruno Marchal, ou bien le roman de Greg Egan, "permutation city".

    Ca ne garantie pas qu'à données d'entrées égales, la sortie soit égale.

    Si, parce qu'une machine de Turing est déterministe.

    Nous connaissons des sortes de macro-lois, donc nous perdons de la précision, d'oû le non déterminisme.

    Ça c'est la version du monde datant d'avant la découverte de la mécanique quantique: si on savait simuler avec assez de précision, alors le monde serait déterministe. La mécanique quantique affirme que le monde que nous observons est par nature non déterministe, et qu'il ne s'agit pas d'un problème de précision.

    Ce qui ne veut pas dire que notre conscience est soumise à ça, car la mécanique quantique ne s'applique pas à notre niveau. Les histoires de Roger Penrose me semblent être une tentative de "sauver" le libre arbitre en ajoutant de l'aléa en ajoutant des "phénomènes quantiques" agissant sur nous. Ça me parait violer le principe d'Okham, mais pourquoi pas. Et Penrose est quelqu'un de fort respectable par ailleurs, donc ça mérite d'être considéré au moins un instant.