Posté par kantien .
En réponse au journal À propos des certificats.
Évalué à -2.
Dernière modification le 02 février 2016 à 18:08.
Mais encore ? As-tu étudié leurs œuvres respectives ? Sur quoi te fondes-tu, en plus de ma remarque, pour aboutir à la conclusion : « Bienvenu dans le club de ceux qui ne comprennent pas le génie de Turing ! » ?
À mon corps défendant, je peux au moins verser au dossier de ma défense, ce commentaire où j'exposais de manière assez détaillée les principes de typage du \lambda-calcul1. Il est à noter que ce langage est Turing-complet, ce qui résulte trivialement de la Turing-complétude définie par Turing en référence au \lambda-calcul dans son article Computability and lambda-definability.
De son côté on doit à Gödel : les théorèmes d'incomplétude du calcul des prédicats et de l'arithmétique de Peano (qui ont pour corollaire trivial l'impossibilité de résoudre le problème de l'arrêt pour une machine de Turing), le théorème de complétude de la logique classique (qui est un désassembleur interractif) ainsi qu'une version pour la logique intuitionniste. Mais aussi de nombreux résultats de consistance relative en théorie des ensembles, et d'études sur la nature de la logique et des mathématiques.
Et je passe sous silence l'origine de ces résultats qui prend, en partie, racine dans des polémiques entre les tenants de l'école kantienne et l'école de Leibniz au sujet de la caractéristique universelle de celui-ci.
Néanmoins, je maintiens ce que j'ai dit sur les interrogations de Gödel qui me semblent plus fondamentales et plus profondes.
on peut noter que les principes ce cette théorie s'applique au typage de tout langage (C, C++, Java, Python...), c'est juste que la sémantique de leur langage de types est moins expressive. Et puisque le journal traite de protocole réseau, on pourra noter que le principe peut s'étendre au « typage » des protocoles : Formules valides, jeux et protocoles réseaux↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: What's the point ?
Posté par kantien . En réponse au journal À propos des certificats. Évalué à -2. Dernière modification le 02 février 2016 à 18:08.
Mais encore ? As-tu étudié leurs œuvres respectives ? Sur quoi te fondes-tu, en plus de ma remarque, pour aboutir à la conclusion : « Bienvenu dans le club de ceux qui ne comprennent pas le génie de Turing ! » ?
À mon corps défendant, je peux au moins verser au dossier de ma défense, ce commentaire où j'exposais de manière assez détaillée les principes de typage du \lambda-calcul1 . Il est à noter que ce langage est Turing-complet, ce qui résulte trivialement de la Turing-complétude définie par Turing en référence au \lambda-calcul dans son article Computability and lambda-definability.
De son côté on doit à Gödel : les théorèmes d'incomplétude du calcul des prédicats et de l'arithmétique de Peano (qui ont pour corollaire trivial l'impossibilité de résoudre le problème de l'arrêt pour une machine de Turing), le théorème de complétude de la logique classique (qui est un désassembleur interractif) ainsi qu'une version pour la logique intuitionniste. Mais aussi de nombreux résultats de consistance relative en théorie des ensembles, et d'études sur la nature de la logique et des mathématiques.
Il y a aussi cet échange avec Perthmâd juste au-dessus du message précédent.
Tu pourras aussi consulter le programme du master LMFI dont je suis sorti major de promotion.
Et je passe sous silence l'origine de ces résultats qui prend, en partie, racine dans des polémiques entre les tenants de l'école kantienne et l'école de Leibniz au sujet de la caractéristique universelle de celui-ci.
Néanmoins, je maintiens ce que j'ai dit sur les interrogations de Gödel qui me semblent plus fondamentales et plus profondes.
on peut noter que les principes ce cette théorie s'applique au typage de tout langage (C, C++, Java, Python...), c'est juste que la sémantique de leur langage de types est moins expressive. Et puisque le journal traite de protocole réseau, on pourra noter que le principe peut s'étendre au « typage » des protocoles : Formules valides, jeux et protocoles réseaux ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.