Aluminium95 a écrit 223 commentaires

Je vois pas comment c'est possible :

Voici une explication possible.
Petit résumé rapide, un graphe c'est soit :

• Un graphe vide
• Un nœud v et les arêtes de v vers un graphe

Cette définition est bien inductive et représentable avec des types récursifs. Elle possède certains avantages : on peut faire des inductions structurelles dessus. Par exemple, faire un parcours en largeur/profondeur ne nécessite plus de marquer des nœuds. Extraire des sous-graphes est naturel, on peut insérer des nœuds en O(1). Après, il est vrai que le parcours sans destruction est assez peu efficace … Avec un peu d'effort on peut la rendre moins inefficace qu'elle n'en a l'air.

En fait, il y a deux choses à distinguer

1. Le fait de construire une structure intermédiaire (qui serait sinon implicite dans le code)
2. Le fait de construire/détruire cette structure « à la même vitesse » (ce qui n'est possible que dans certains cas) et qui permet de ne jamais à avoir l’intégralité de la structure en mémoire

Ce qui est illustré avec cat est le deuxième point (selon moi).

Le map va charger en mémoire tes données puis les rendre accessible à la réduction

C'est bien la différence : ce qui est illustré est le fait de construire une donnée qui n'était pas explicitement construite avant. Dans les premiers exemples du journal, cela consiste simplement à construire l'arbre d'appel réellement, puis de le parcourir, le dernier consiste à construire l'arbre de décisions que l'algorithme allait parcourir de manière physique, plutôt que de continuer à raisonner sur des décisions locales.

De plus, dans ta définition, le map est « inutile » : on peut quasi-systématiquement écrire map en fonction de reduce

map (f,coll) = reduce (lambda x,y: insertColl(x,f(y)), emptyColl, coll)

Mieux encore, en utilisant quelques équations algébriques sur les compositions de reduce, le map-reduce peut se ré-écrire sans map :

reduce (action, init, map (fonction, collection)) = reduce (lambda x,y: action (x, fonction(y)), init, collection)

à une chose sur la quelle on peut itérer

C'est déjà assez puissant : une grande partie des données sont définies de manière inductive dans les langages fonctionnels, et donc un reduce vient automatiquement. Par exemple, il existe une manière de représenter les graphes de manière inductive (ce qui vient avec un certain cout toutefois).

Dans un langage qui t'impose l'usage de classes

Donc du coup il y a bien une hiérarchie :

1. Les différents concepts qui sont accessibles facilement dans le langage
2. Les différents patterns qui sont associés

De plus, pour moi un design pattern c'est un choix qui est en un sens arbitraire, parce que sinon, ce n'est pas un design pattern, c'est simplement une technique nécessaire. Or, quand on fait un choix de type « monade / objet / groupe / interface / protocole » on considère une représentation, ensuite dans un design pattern, on sélectionne un choix d'implémentation dans le cadre que l'on a fixé.

Je vois un peu mieux ta conception, mais pour être sûr : faire des objets, c'est un design pattern ? Dans ma perception (peut-être erronée), j'aurais dit que un objet c'est un concept « méta », à partir duquel on peut construire un design pattern particulier, quand on regarde sur wikipédia on trouve par exemple :

• Abstract factory : Provide an interface for creating families of related or dependent objects without specifying their concrete classes.
• Builder : Separate the construction of a complex object from its representation, allowing the same construction process to create various representations.
• Publish/subscribe : Define a one-to-many dependency between objects where a state change in one object results in all its dependents being notified and updated automatically.

Ce qui me semble vraiment différent de la définition même d'un objet, qui est un concept régi par des lois (même si c'est moins fort que pour une monade). Si on voulait ajouter « monadic code » dans la liste la seule définition que je vois est une tautologie :

• Monadic code : see if the code can be represented with a monad, and if so, do it.

Les monades sont juste un design pattern

Je pense que c'est un peu plus que cela, c'est un « design pattern » au même titre que des objets dans un langage à objets. Mieux, c'est autant un design pattern qu'un groupe commutatif (int), qu'un monoïde libre sur un type (listes) : c'est une représentation mathématique formelle qui se trouve être implémentable et calculable dans une certaine mesure. Je ne sais pas si se rendre compte qu'un objet formel (int/liste) est un modèle d'une certaine théorie (groupe/monoïde) est considéré comme un pattern.

D'un autre côté je ne connais pas beaucoup les « design pattern », donc je dis peut-être des absurdités et c'est une propriété commune aux différents patterns.

regex (le mot pour ne pas le terme expression rationnelles beaucou trop limitatif)

Je suis curieux, quelle différence fais-tu entre « regular expression (regex) » et « expression rationnelle » ? En effet il y a une équivalence entre langage rationnel et régulier. Donc c'est peut-être que « regex » fait implicitement référence à des expression étendues ?

Les systèmes dit d'expressions régulières ne sont pas modulaires et donc ne peuvent pas traiter les cas complexes.
Perl 6 utilise un système de grammaires

Il faut quand même faire attention, parce qu'une grammaire n'est pas une expression régulière. Le pouvoir expressif d'une expression rationnelle est plus faible, mais en contre partie tout est plus facile : stabilité des langages par intersection, union, complémentaire, morphismes, algorithmes (très) efficaces pour les traiter etc… Donc quand une expression suffit, il ne sert à rien d'aller chercher une grammaire.

Bon, je crois qu'au final on s'est à peu près compris − même si, ayant lu la même définition que toi sur Wikipedia je n'y comprends pas la même chose.

J'avais cru comprendre que tu avais « accepté » que sa définition pouvait être admise. De là, je n'avais pas compris ton contre exemple qui revenait exactement sur ce même point.

on n'est pas plus royaliste en étant sujet d'un royaume qu'on n'est républicain en étant citoyen d'une république.

D'un autre côté, être citoyen n'est pas seulement un titre et un droit de vote : l'état s'engage à garantir des droits (sécurité sociale, chômage, gestion administrative des infrastructures etc.), en échange, tu participes (plus ou moins activement) à la société ainsi administrée (par exemple via des cotisations).

Ce qui est amusant c'est que pour faire ton contre-exemple, tu sélectionnes spécifiquement un terme qui a aussi une connotation politique (au sens d'une orientation politique personnelle).

En effet, le travail demandé est plutôt trivial (conversion d'un ast déjà généré en code machine valide) : Le journal n'était pas pour demander de l'aide (ça serait plutôt dans un forum que je demanderais ce genre de choses) mais pour dire que mon code caml était plutôt répétitif (chaque appel de fonction demande un contexte, qui change parfois, mais peu souvent) et que la méthode pour « cacher » cet argument, qui marcherait bien en haskell, était bien trop pénible à mettre en place en caml par rapport aux gains (retirer un argument des fonctions).

Bien sûr, si on propose une solution élégante, je suis preneur (même si j'ai déjà rendu le projet, ça peut toujours servir !).

PS: Un camarade a trouvé une solution plutôt élégante, en remarquant que la création d'un nouveau contexte ne se fait que quand on déclare des variables locales à un bloc, et que donc on peut utiliser une variable globale, qui est modifiée quand on entre dans ce bloc, fait un appel récursif pour les différents calculs d'expression (qui utiliseront la variable globale, donc le nouveau contexte), puis la remet « comme avant » à la fin de la compilation du bloc. C'est doublement élégant parce que cela utilise moins de mémoire (enfin, j'en ai l'impression) en plus de virer les contextes dans les appels de fonctions.

Bien sûr, si on propose une solution élégante, je suis preneur (même si j'ai déjà rendu le projet, ça peut toujours servir !).

PS: Un camarade a trouvé une solution plutôt élégante, en remarquant que la création d'un nouveau contexte ne se fait que quand on déclare des variables locales à un bloc, et que donc on peut utiliser une variable globale, qui est modifiée quand on entre dans ce bloc, fait un appel récursif pour les différents calculs d'expression (qui utiliseront la variable globale, donc le nouveau contexte), puis la remet « comme avant » à la fin de la compilation du bloc. C'est doublement élégant parce que cela utilise moins de mémoire (enfin, j'en ai l'impression) en plus de virer les contextes dans les appels de fonctions.

La monade reader est un artifice Haskellien pour palier aux restrictions sur les effets de bords. Elle ne sert rigoureusement a rien en caml.

D'accord, encore un problème de communication de ma part ! Je ne veux pas forcer l'utilisation de cette méthode en OCaml. Voilà ce qui se passe :

1. J'ai un problème avec un contexte
2. Pour simplifier la lecture, l'écriture, la maintenance de mon code je le passe en argument des fonctions (même si elles ne demandent qu'un sous-ensemble des informations du contexte)
3. Je constate que toutes les fonctions ou presque sont donc de la forme f ctx ... =
4. Je remarque qu'en haskell ce paradigme aurait permis d'éviter de passer explicitement le contexte
5. J'essaye de l'appliquer pour constater que c'est vraiment lourd (même si je n'y ai pas mis toute ma volonté, en utilisant des bibliothèques et extensions de syntaxes pour palier à ce problème)

Juste pour préciser, mon contexte est clairement modifiable (compteur de variables sur la pile par exemple) et que mes fonctions sont tout sauf pures (printf). Donc je ne vois pas en quoi l'impératif a un rapport avec ça : au contraire, en haskell, il faut utiliser ReaderT ctx IO pour pouvoir faire ce que je veux (ce qui devient déjà plus lourd).

Donc une fois de plus, hors sujet.

Je vais passer pour un inculte, mais que fait >|= exactement ? Et cela veut dire que quand on écrit >> en caml c'est équivalent à >|= ignore >>= en haskell, ou bien c'est l'inverse ?

En effet, c'est assez joli, mais quand tu fais bind tu dois préciser depuis quel module visiblement (j'ai parcouru très rapidement la doc) ? Si on utilise une unique monade (comme dans mon cas) un open ou un renommage peut faire l'affaire, mais sinon, ne trouves-tu pas ça un peu lourd ?

Il pourrait aussi trouver les lens intéressantes

Pour le coup je ne comprend pas à quoi les lens peuvent servir. Je n'ai jamais vraiment touché aux lens, mais ce n'est pas plus dans l'idée de modifier une structure compliquée en appliquant des modificateurs/lecteurs aux différentes parties ? Si tu pouvais éclaircir ce point j'en serais ravi.

Je pense que le moinssage vient du fait que la notation infixe ne change pas « le problème » que j'ai soulevé (enfin, c'est un problème pour moi), qui est ici le fait de devoir construire des « lambda » à chaque appel de bind (ou >>=).

D'ailleurs, même en haskell, pour une longue composition de fonctions, où tous les résultats intermédiaires sont utilisés dans le dernier bloc, c'est vraiment plus pratique d'avoir une syntaxe plus « impérative », plutôt que a >>= (\x -> b >>= (\y -> c >>= (\z -> ...))). Enfin, c'est une question de goûts, mais la notation infixe n'est pas une réponse à ce problème.

Après, oui (comme je l'ai déjà dit dans un autre commentaire), si on fait des fonctions séparées, bien compartimentées, on a pas besoin de créer des lambdas (en fait, ce sont des fonctions normales), et c'est ce que tu proposes : « Autant dire : je compose les opérateurs ». Sauf que parfois, on construit beaucoup d'opérateurs différents … et c'est là que la notation est pratique.

Enfin, dernier argument pour dire que « la notation infixe ne change pas ce problème » (je note quand même que j'ai précisé dans le journal que, comme toujours, j'ai pris pour seul exemple un qui pouvait se simplifier de manière triviale, et pourtant c'est 2ème commentaire à le reprendre et le simplifier …) :

let ( >>= ) = bind;;

let push_var_on_stack s = get_var_addr s >>= pushq;;

(* 
 * sans la notation infixe on perd ~ 4 caractères à la louche,
 * quelle victoire !
 *)
let push_var_on_stack s = bind (get_var_addr s) pushq;;

Une petite remarque, comme dans 99% du temps, les fonctions retournaient un unit (et écrivaient dans la sortie le code correspondant), on peut avoir une syntaxe dans le genre : List.fold (>>) (return ()) [ a ; b ; c ; d ; e ; f], qui peut se transformer en un opérateur asm_code_block [ a ; b ; c ; d ... ], qui avec une bonne indentation permet de retrouver la « forme » du code assembleur (et une notation pseudo impérative de caml) et qui est « facilement compréhensible¹ » :

asm_code_block [
    popq "%rdi";
    movq "$1" "%rsi";
    call  "printf";
    ...
] ctx

Donc le problème n'est pas « je ne sais pas définir un opérateur infixe en OCaml ».

PS: un autre problème est que l'évaluation n'est pas paresseuse, et donc il faudrait utiliser le module Lazy, en ajoutant une syntaxe encore plus lourde^2, parce que return (Printf.fprintf out "coucou") est différent de (fun _ -> Printf.fprintf out "coucou"), l'un écrit « coucou » à la construction, l'autre à l'exécution du « reader ».

@kantien : pourquoi pas, je ne suis jamais allé dans un meetup jusqu'à présent.

---

[1] : parce que cela « ressemble » à une sémantique dénotationnelle, du type [code]{contexte} = valeur,nouveau contexte
[2] : ou en utilisant des extensions de syntaxe pour que return x === return' (lazy x). Mais je viens de voir qu'un commentaire de Michaël en parlait, du coup je ne suis pas catégorique sur ce point.

Je me suis peut-être mal fait comprendre … Mais j'ai bien précisé que vu que le code était moche, j'avais abandonné l'idée, et je passe le contexte en argument des fonctions de manière explicite, ce qui n'est pas ce qui est fait dans le journal (cf: commentaire auquel tu réponds).

J'en suis arrivé exactement à la même conclusion que toi : sans syntaxe adaptée, c'est plus lourd qu'autre chose, et donc je ne l'ai pas utilisé.

Sinon, « peut être, juste peut être » est un peu condescendant je trouve, même si le problème de communication vient probablement de moi.

Il est tellement moche que je n'oserais pas mettre un lien ;-).

En plus, comme je n'ai pas utilisé des extensions caml, les opérations monadiques sont moches, donc, finalement, je me trimballe le contexte (du coup il n'a pas vraiment de rapport avec ce qui est fait dans le journal).

En revanche, pour ce qui est la sémantique du sous-ensemble, des références x86_64, et les contraintes du projet en général, voilà le lien qui va bien.

Pour finir, je n'ai eu à écrire que la partie « compilation » (donc pas de parsing), et sans aucune obligation de produire du code assembleur « optimisé » à partir de l'AST : en gros c'est plus ou moins traduire de manière naïve chaque construction C en assembleur, et faire le code Caml qui s'en charge. Donc je doute fortement que lire le code serve à quelque chose : une explication écrite de « comment traduire naïvement telle construction » serait bien plus compréhensible (et apporterait autant).

Je n'ai été jamais complètement convaincu par la notation do comparé à utiliser directement >>= et >>.

Cela dépend vraiment des utilisations, mais dans le cas où on fait énormément de calculs séquentiels, c'est vraiment plus clair. Par exemple, on peut imaginer (encore dans le cadre d'un compilo) écrire le code suivant

compileExpr (Bin o a b) = compileExpr a >> compileExpr b >> popq "%rax" >> popq "%rdx" >> asmBinop o "%rdx" "%rax" >> pushq "%rax"

-- Or, c'est pénible à lire, pénible à modifier facilement (couper/coller des lignes, sélectionner des parties du code)
-- donc on finit par écrire comme ça pour que cela soit plus pratique : 

compileExpr (Bin o a b) = compileExpr a >> 
                          compileExpr b >> 
                          popq "%rax" >>
                          popq "%rdx" >>
                          asmBinop o "%rdx" "%rax" >>
                          pushq "%rax"

-- Et on a ré-inventé la notation do en moins bien

La vraie question, c'est si on retire la notation do, pourquoi ne pas retirer les list comprehension ? Parce que c'est exactement la même chose : [ x + y | x <- [1..], y <- maListe ] est parfaitement équivalent à [1..] >>= (\x -> maListe >>= (\y -> return (x + y))) … Je suis presque sûr que la première est bien plus claire, et bien plus utilisée, en fait, elle est même ajoutée dans des langages comme Python (qui n'a pas de monade liste explicite).

nombreuses extensions de syntaxe qui permettent d'utiliser la notation do en OCaml; j'en compte au moins 4 disponibles directement avec opam.

En effet, mais ce n'est pas intégré au langage, il faut gérer cette dépendance si on l'utilise dans un projet, et il faut sélectionner un des 4, qui sont certainement légèrement différents, ce qui demande un travail supplémentaire (et je suis flemmard).

quand on peut faire cela :

main = do
    getLine >>=
    putStrLn

Le do ne sert à rien ici par contre, autant écrire main = getLine >>= putStrLn directement ;-).

Mmh, oui. C'est une question pertinente, sauf que si la syntaxe existe, c'est parce qu'elle permet de simplifier de manière élégante les multiples binds imbriqués.

faire_un_calcul_complexe x = do 
                             a <- premiere_etape 
                             deuxieme_etape
                             c <- troisieme_etape a
                             return (a,c)

Qui est quand même bien plus simple que la même chose avec des binds (lisibilité, et le code facilement modifiable) :

faire_un_calcul_complexe x =  
                             premiere_etape >>= (\a -> 
                             deuxieme_etape >> 
                             troisieme_etape a >>= (\ b -> 
                             return (a,c)))

La solution, c'est de faire des fonctions très simples, pour que ce soit toujours raisonnable, sauf que dans le cadre d'un compilateur, quand tu veux traduire une opération, la manière naturelle de décrire un while va être triviale avec la notation do (alors que sans, on va utiliser pleins de >> qui ne feront que « décorer » le code de manière inutile) :

compile (While e c) = do
                         cond <- makeLabel "COND"
                         body <- makeLabel "BODY"
                         jump cond
                         printLabel body
                         compile c
                         printLabel cond
                         compileExpr e
                         jumpIfNonZero body

Qui se comprend en regardant la « traduction assembleur »

[While e do c]
    jmp .COND
.BODY
    [c]
.COND
    [e]
    popq %rax
    cmpq $0, %rax
    jne .BODY

La notation do permet de conserver la même « forme » de traduction, ce qui est pratique à la fois pour la lecture (compréhension) et la modification (on peut facilement permuter deux lignes si on a loupé un truc).

reviens toujours à la surjectivité

La surjectivité humaine, c'est un concept à creuser ;-).

Plus sérieusement, quand tu dis que le consensus (puisqu'on peut appliquer ton raisonnement à autre chose que « l'intrinsèquement mauvais » sans qu'il change sensiblement) est « la base de la manipulation », c'est vrai, mais ce même consensus est à la base de la civilisation/société. Par exemple, on parle de tabou de l'inceste qui serait plus ou moins universel à travers les sociétés humaines, même si certains individus le pratiquent, cela est considéré comme « mal », ou au moins « bizarre ». Cela permet d'avoir une base plus ou moins commune de références et de valeurs pour communiquer plus facilement au sein d'une société.

Bien entendu, la diversité des opinions est nécessaires, et il faut penser par soi même, mais refuser toute notion de bien et de mal limite les discussions à des échanges de faits objectifs qui n'apportent à la discussion qu'une très faible valeur humaine. Dans un cadre scientifique, c'est très bien (c'est même souhaitable), mais dès qu'on parle de problèmes de société, on ne peut pas renier cette dimension du problème.

En effet, en prenant un avis objectif sur la situation, on arrive bientôt à déresponsabiliser les individus : si le mal n'existe pas, que chaque action est simplement menée pour répondre de manière optimale aux besoins de la personne, alors le massacre d'enfants est une conséquence logique de la configuration actuelle du monde, et ce n'est ni bien, ni mal.

D'ailleurs, une preuve que la notion de « bien » et de « mal » est présente dans tes commentaires : « oui, c'est horrible ». Ce jugement de valeur non-objectif mérite une sanction immédiate de ta part, puisque tu parlais plus tôt d'auto-flagellation …

Ça s'appelle la réfutabilité des théories scientifiques

Oui, j'en ai bien conscience, seulement je répondais au fait que la religion (chrétienne) était critiquée parce qu'elle changeait son interprétation de la bible / du monde en fonction des évolutions des mentalités et des expériences. C'est justement un signe de progrès : le contraire serait tout simplement pire !

Ensuite, comparer la religion chrétienne à des gens qui font « bouillir leur mélange de plante » je trouve ça un peu marrant : c'est quand même une institution qui a mis en place un système de taxe hors norme, mené des guerres relativement importantes, institutionnalisé le rapport à Dieu sur un territoire assez vaste, mené l'inquisition, et servait en partie à l'érudition des élites. En plus, je pense que le prêtre ne se mouillerait pas à proposer un mélange de plantes, la foi en Dieu est le meilleur remède¹ (et en plus c'est pas de sa faute si cela ne marche pas).

¹ Mine de rien, ça peut avoir un effet placebo non négligeable !

A noter que la définition change avec les avancées technologiques : en effet, Dieu était avant "en haut", on est allé voir "en haut" et personne, du coup les religieux ont bidouillé "nan, mais en haut en fait c'est pas au dessus des nuages, même si on a représenté ça partout comme ça".

Mmmh, comme la science : on fait évoluer le modèle avec les découvertes/expériences. Pendant longtemps on a pensé que la loi de composition des vitesses était « vraie ». Seulement, on a vu que cela ne fonctionnait pas vraiment pour la lumière : qu'à cela ne tienne, on a plus qu'à fixer la vitesse de la lumière dans un référentiel ! Une ou deux formules qui changent, qui ont le bon goût d'être très proche quand on est à des faibles vitesses et c'est reparti les amis !

Je ne crois pas en Dieu, mais c'est tout simplement parce que croire en Dieu n'a jamais réellement apporté une prédiction fiable. La science permet à partir du modèle établi de prédire de nouveaux résultats, et de se rendre compte de la validité de la théorie (capacité de prédiction). Avec Dieu, on « subit » les nouveaux résultats, et on en vient à simplement changer sa définition pour suivre l'expérience.

En général on cherche à prouver l'existence de quelque chose. Parce que le chemin inverse est autrement plus dur.
Tu t'arrêtes où pour prouver la non-existence de la licorne rose invisible ?

Prouves-moi que la gravité existe, si prouver que quelque chose existe est bien plus facile ;-). J'attends une preuve hein, pas un « oh mais on a fait N expériences qui le confirment approximativement avec erreurs de mesure » (même si N est très grand).

Finalement, prouver l'inexistence de Dieu est soit inintéressant, soit impossible, soit inutile, en fonction du type de Dieu considéré.

Je suis parfaitement d'accord avec ça, seulement quand on me répond qu'il est impossible de prouver que quelque chose n'existe pas, bah j'ai un peu de mal à ne pas réagir ;-).

En plus, comme tu l'as si bien dit, il n'y a pas de définition précise, donc aucune preuve ne serait recevable … Mieux, si on considère que la définition peut varier (et donc la réponse peut varier) alors le coup de l'athéiste qui ne croit en aucun Dieu est une position beaucoup plus dure (il a un quantificateur universel de plus dans sa phrase) que celui qui croit en un Dieu (avec une définition fixée).

la structure réelle

J'aimerais revenir sur ce point, parce que « prouver par la structure réelle », ça veut dire quoi ?
Si je prend une formule qui coïncide presque parfaitement avec celle pour la force gravitationnelle en ajoutant un terme qui est négligeable. Alors l'expérience réelle prouve (à erreur de mesure près) que ma formule fonctionne, mais c'est une preuve « à la physicienne ». Certes c'est mieux que rien du tout, mais c'est une science par définition expérimentale, qui cherche à faire coïncider un modèle avec la réalité en se confrontant à l'expérience : par construction elle sera toujours plus ou moins « fausse » (approximation du réel).

Par contre la recherche exhaustive sur un univers fini, je suis d'accord.

botte secrète imparable consistant à dire que Dieu ne se manifeste pas dans le plan physique.

Ça c'est changer de définition en cours de preuve, d'où la nécessité d'en avoir une au départ, qui permet de conclure assez vite que tout débat est inutile ;-).

"Une charge en comptabilité crée une diminution du résultat de l'entreprise (et donc un appauvrissement de son patrimoine)."

Oui, je suis parfaitement d'accord avec toi sur ce point. Seulement, les « cotisations » sont plus qu'un appauvrissement du patrimoine de l'entreprise : cet argent est plus un « investissement ».

Par exemple, si tu (ou une entreprise) places ton argent en bourse, tu vas dire que c'est une charge ? Je sais bien que la comparaison n'est pas tout à fait réaliste, parce que tu n'es pas obligé de le faire. Mais si tu le fais, c'est un investissement (et ensuite, il est bon ou mauvais, ça c'est autre chose).

L'analogie n'est pas exacte, mais on peut comprendre que (par exemple) la délocalisation revient en réalité à faire « d'autres placements » : des investissements qui sont (supposés) plus rentables.

Du coup, parler de « charge » je trouve que c'est un peu « exagéré », bien que ce soit du jargon comptable usuel (point sur lequel je suis parfaitement en accord).

Ce qui est impossible.

Dans le cas général ou pour ce problème précis ? Parce que sinon c'est assez nul comme réponse hein.

On peut montrer qu'il n'existe pas de morphisme du groupe des permutations d'un ensemble à N éléments dans (C*,×) différent de l'identité et de la signature … C'est une preuve, elle marche, ça montre que quelque chose n'existe pas : où est donc le problème ?

Pour prendre un exemple plus « informatique », prenons la calculabilité. Typiquement : existe-t-il une machine de Turing qui prend en argument le code d'une machine de Turing, et une entrée, et détermine si le calcul de la machine sur l'entrée termine ? Et bien on peut prouver que non.

On arrive donc à la conclusion que ton affirmation était nécessairement à comprendre dans le sens « prouver que Dieu n'existe pas est impossible ». Ce qui montre déjà qu'il y a eu un quiproquo parce que j'avais compris que l'on parlait de démarche générale, mais continuons tout de même.

Je ne vois pas en quoi il est formellement impossible de prouver l'existence de Dieu, tout comme prouver sa non existence … Pour le coup, tu affirmes qu'il n'existe pas de preuve (dans un sens comme dans l'autre), et j'aimerais alors une démonstration de ce théorème ;-).