Version imprimable
Bonjour à tous.
Vous qui fréquentez ce forum sur les maths, serez sans doute intéressés par un fil traitant des rapports entre démonstrations mathématiques et programmation fonctionnelle. Vous y trouverez une présentation des mathématiques constructives sous forme de concepts de programmation dans un système de types approprié.
Ce fil est sous forme de quizz et votre participation sera appréciée.
Cordialement.
De la pub? :mouarf:
Non, juste une info, justifiée par le fait que ce quizz qui se trouve dans le forum langages fonctionnels aurait tout aussi bien trouvé sa place ici.Citation:
Envoyé par Nemerle
Pas tout à fait d'accord... c'est un quizz plus fonctionnel (d'ailleurs!), qui se rapproche plus de la réécriture que des mathématiques "standards". Mais d'accord, tout ça fait se fait aussi en UFR de math...
en tous cas, pour moi, désolé DrTopos, mais c'est un langage d'initié...
Les notations me semblent obscures et incompréhensibles, et si c'est bien ce genre de choses dont vous vous servez pour la preuve de programme et du langage "fonctionnel", ça ne me semble guère fonctionnel...
Je "skipperais" donc le quizz...
C'est parce que ce n'est que le début. Quand on aura l'axiome du choix et qu'on aura introduit quelques abbréviations et quelques locutions, tu verras que cela ressemble tout à fait aux mathématiques standard (y compris classiques). En particulier, on verra que toutes ces flèches |-> et tous ces termes applicatifs peuvent se traduire en phrases de la langue naturelle, qui donneront des démonstrations d'un aspect tout à fait ordinaire.Citation:
Envoyé par Nemerle
Les notations sont juste une imitation des notations mathématiques standard en ``ASCII art'' si on peut dire.Citation:
Envoyé par souviron34
Il faut dans l'immédiat le prendre pour ce qu'il est, c'est à dire comme je l'ai indiqué dans le premier post pour un jeu. Pour être amusant, un jeu doit être original et un peu déroutant. C'est aussi la raison pour laquelle il n'est pas réaliste comme langage de programmation tel qu'il est présenté. Par contre, ces principes deviennent tout à fait réalistes avec une bonne surcouche de sucre syntaxique.
Ce n'est un langage d'initié à mon avis que pour ceux qui n'ont jamais fait de programmation fonctionnelle, et pour ceux-là, ça peut aussi être une initiation (un peu spéciale il est vrai) à la programmation fonctionnelle. Il résulte de cette présentation que les preuves mathématiques ne sont que des imbrications de fonctions et de termes applicatifs. C'est une façon de faire remarquer aux programmeurs auxquels les maths font un peu peur (il y en a) que les mathématiques ne sont pas aussi difficiles qu'ils peuvent le croire, du moins dans les principes, puisque ce n'est que de la programmation.
Si j'ai créé ce fil pointant sur le quizz, c'est parce qu'il est notoire qu'on peut naviguer longtemps sur DVP sans avoir idée de ce qu'il se passe sur les fils des autres forums. Je pense que ce quizz, qui n'est jamais rien d'autre qu'un tutoriel interactif, peut intéresser des gens qui font des maths. Il est par ailleurs normal que ça n'intéresse pas tout le monde.
Cordialement.