Une question sur la logique et la correspondance de Curry-Howard

Question

Pourriez-vous m'expliquer quelle est la connexion de base entre les principes fondamentaux de la programmation logique et le phénomène de similarité syntaxique entre les systèmes de types et la logique conventionnelle?

Answer 1

La correspondance de Curry-Howard ne concerne pas la programmation logique, mais la programmation fonctionnelle. Le mécanisme fondamental de Prolog est justifié dans la théorie de la preuve par resolution technique de John Robinson, qui montre comment il est possible de vérifier si les formules logiques exprimées en clauses de cor sont satisfiable, c'est-à-dire si vous pouvez trouver des termes pour leurs variables logiques qui les rendent vrai.

Ainsi, la programmation logique consiste à spécifier des programmes en tant que formules logiques, et le calcul du programme est une forme d'inférence de preuve, en résolution Prolog, comme je l'ai dit. En revanche, la correspondance de Curry-Howard montre comment les preuves dans une formule spéciale de la logique, appelées natural deduction, correspondent à des programmes dans le lambda-calcul, avec le type du programme correspondant à la formule que la preuve prouve; Le calcul dans le lambda-calcul correspond à un phénomène important dans la théorie de la preuve appelée normalisation, qui transforme les preuves en de nouvelles preuves plus directes. Ainsi, la programmation logique et la programmation fonctionnelle correspondent à différents niveaux dans ces logiques: les programmes logiques correspondent aux formules d'une logique, alors que les programmes fonctionnels correspondent à des preuves de formules.

Il y a une autre différence: les logiques utilisées sont généralement différentes. La programmation logique utilise généralement des logiques plus simples — comme je l'ai dit, Prolog est fondée sur des clauses Horn, qui sont une classe très restreinte de formules où les implications ne peuvent pas être imbriquées, et il n'y a pas de disjonction, bien que Prolog récupère toute la logique classique. couper la règle. En revanche, les langages de programmation fonctionnels tels que Haskell font un usage intensif des programmes dont les types ont des implications imbriquées, et sont décorés par toutes sortes de formes de polymorphisme. Ils sont également basés sur la logique intuitionniste, une classe de logiques qui interdit l'utilisation du principe du tiers exclu, sur lequel repose le mécanisme de calcul de Robinson.

Quelques autres points:

1. Il est possible de programmation logique de base sur des logiques plus sophistiquées que les clauses de Horn; par exemple, Lambda-prolog est basé sur une logique intuitionniste, avec un mécanisme de calcul différent de la résolution.
2. Dale Miller a appelé le paradigme de la preuve derrière la logique de programmation théorétique la recherche de la preuve que la programmation métaphore, en contraste avec les preuves que les programmes métaphore qui est un autre terme utilisé pour la correspondance de Curry-Howard.

Answer 2

La programmation logique repose fondamentalement sur la recherche orientée objectif pour les preuves. La relation structurelle entre les langages dactylographiés et la logique implique généralement des langages fonctionnels, bien que parfois impératifs et d'autres langages - mais pas des langages de programmation logiques directement. Cette relation relie les preuves aux programmes. Ainsi, la recherche de preuve de programmation logique peut être utilisée pour trouver des preuves qui sont ensuite interprétées comme des programmes fonctionnels. Cela semble être la relation la plus directe entre les deux (comme vous l'avez demandé).

Construire des programmes entiers de cette façon n'est pas pratique, mais cela peut être utile pour remplir des détails fastidieux dans les programmes, et il y a quelques exemples importants dans la pratique. Un exemple de base est le sous-typage structurel - qui consiste à remplir quelques étapes de preuve via une simple preuve d'implication.Un exemple beaucoup plus sophistiqué est le système de classes de types de Haskell, qui implique un type particulier de recherche orientée vers un but - à l'extrême, cela implique une forme de Turing-complete de programmation logique au moment de la compilation.