Ici tu confonds deux choses : la logique du premier et la logique intuitionniste. La première concerne les règles de formation des jugements, la seconde traite des règles d'inférences ou raisonnements.
Mmm après réflexion je dirai plutôt que je fais une erreur stupide : je confonds implication et déduction. Par définition, une logique s’intéresse aux règles de constructions et à la formation des jugements ... La non constructivité induit qu’il n’existe pas forcément de moyen de former un algorithme à partir du théorème ou de la formule, et c’est bien tout ... Je crois que tu confonds « formule de la logique du premier ordre » et « logique du premier ordre ». Ou alors c’est moi qui confond ... Parce que dans mon esprit, la logique du premier ordre est un système formel, donc comprend les règles de déduction : https://en.wikipedia.org/wiki/First-order_logic (et wp semble être d’accord avec moi) ou alors j’ai rien compris à ce que tu dis :) La logique intuitionniste est aussi un système de déduction, mais avec des règles de déduction différente. Ou alors tu voulais dire « la logique intuitionniste du premier ordre est l’archétype du typage dynamique » ?
Du coup je me fourvoyai effectivement, tu parlais à chaque fois de système de déduction intuitionnistes. Tu établis 'une correspondance preuve/programme qui ne fonctionne que pour ces système, et je pensai que tu associais un système non intuitionniste pour les langages dynamiques. Alors que tu établies plus une distinction théorie à variable typée/théorie à variable pas typée.
Cela dit j’ai quand même l’impression d’être grugé. Dans un cas, le connecteur « -> » est vu par correspondance de curry-howard comme le type d’une fonction, alors que dans l’autre pour un langage dynamique tu as complètement oublié cette correspondance implication/fonction et c’est le quantificateur qui joue ce rôle.
[^] # Re: Le cerveau n'est pas logique
Posté par thoasm . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4.
Mmm après réflexion je dirai plutôt que je fais une erreur stupide : je confonds implication et déduction. Par définition, une logique s’intéresse aux règles de constructions et à la formation des jugements ... La non constructivité induit qu’il n’existe pas forcément de moyen de former un algorithme à partir du théorème ou de la formule, et c’est bien tout ... Je crois que tu confonds « formule de la logique du premier ordre » et « logique du premier ordre ». Ou alors c’est moi qui confond ... Parce que dans mon esprit, la logique du premier ordre est un système formel, donc comprend les règles de déduction : https://en.wikipedia.org/wiki/First-order_logic (et wp semble être d’accord avec moi) ou alors j’ai rien compris à ce que tu dis :) La logique intuitionniste est aussi un système de déduction, mais avec des règles de déduction différente. Ou alors tu voulais dire « la logique intuitionniste du premier ordre est l’archétype du typage dynamique » ?
Du coup je me fourvoyai effectivement, tu parlais à chaque fois de système de déduction intuitionnistes. Tu établis 'une correspondance preuve/programme qui ne fonctionne que pour ces système, et je pensai que tu associais un système non intuitionniste pour les langages dynamiques. Alors que tu établies plus une distinction théorie à variable typée/théorie à variable pas typée.
Cela dit j’ai quand même l’impression d’être grugé. Dans un cas, le connecteur « -> » est vu par correspondance de curry-howard comme le type d’une fonction, alors que dans l’autre pour un langage dynamique tu as complètement oublié cette correspondance implication/fonction et c’est le quantificateur qui joue ce rôle.