Courry Howard Correspondence et Thèse de l'église

Question

La correspondance Curry-Howard indique l'équivalence entre la logique / la déduction et les types / programmes.

La thèse de l'église énonce l'équivalence de certains modèles de calcul. Plus précisément, toutes les fonctions calculables peuvent être écrites à la fois sur une machine Turing et dans le calcul Lambda.

Toutes les logiques ne sont cependant pas équivalentes. Logique du 2e ordre peut quantifier sur les ensembles pendant 1ère commande ne peut pas.

Quelqu'un peut-il expliquer la dissonance? Certaines fonctions calculables peuvent-elles être exprimées à un "niveau supérieur" mais pas à un "niveau plus simple"?

CLARIFICATION

Si je définis un modèle de calcul, disons la logique du 2e ordre tandis que la machine Turing est un modèle pour la logique du premier ordre, cela signifie-t-il que mon langage hypothétique peut calculer les fonctions "non ordinables"? Il me semble que la logique du 2e ordre est plus puissante que la logique du premier ordre. Ceci est clairement absurde car Haskell est basé sur une saveur de logique à 2 commandes (système F avec des extensions) mais n'est pas plus puissant que disons C: Tout programme réalisable dans Haskell est réalisable dans C. La cartographie (ou l'équivalence) entre la logique et Le calcul ne semble pas préserver la notion de résistance: la logique du 2e ordre est plus forte que la logique du 1er ordre mais les langages de programmation hors de la logique 2e et 1er ordre ont la même force. Cela a-t-il du sens?

La seule conclusion à laquelle je peux arriver est que la relation entre la logique et les types n'est pas une cartographie simple. La machine Turing n'est pas basée sur une logique spécifique et que tout système logique / déductif peut être mappé sur la machine Turing. Pouvez-vous confirmer?

Mots de clôture

Je pense que mon erreur est de ne pas réaliser qu'il existe un grand fossé entre le «programme» familier et les programmes dans le contexte des types.

Haskell qui est basé sur un système de type plus fort et plus expressif fournit en effet des programmes plus forts et plus expressifs. Ces programmes sont plus forts dans le sens où davantage peut être garanti à leur sujet (dans le même sens que «type de sécurité»). Cela ne signifie pas que Haskell peut «calculer» plus; Il est encore simplement complet.