Cadre logique vs théorie des types

Résumé. Un cadre logique est un méta-langage pour la formalisation des systèmes déductifs, où les déductions deviennent des objets syntaxiques.

Bien sûr, ce qui compte comme méta-langage est assez vague, et il est utile de comprendre le développement historique des cadres logiques. Le premier cadre logique a été l'Automath de Bruijn (1), qui est basé sur $\lambda$ -calculus. De nombreuses idées de la famille de langages Automath ont trouvé leur chemin dans les cadres logiques modernes. Les travaux de Martin-Löf sur les théories constructives des types, également basés sur $\lambda$ -calculi, ont également eu une influence.

$\lambda$ $A \rightarrow B$ $\Pi x^A. B$ $A \rightarrow B$ $\Pi x^A. B$

\frac{Γ ⊢ M : A \to B Γ ⊢ N : A}{Γ ⊢ M N : B} \frac{Γ ⊢ M : Π x^{A} . B Γ ⊢ N : A}{Γ ⊢ M N : B {N / x}}

$\newcommand{\TYPES}[3]{#1 \vdash #2 : #3} \newcommand{\SUBST}[2]{\{#1/#2\}} \frac{ \TYPES{\Gamma}{\color{red}{M}}{A \rightarrow B} \qquad \TYPES{\Gamma}{\color{red}{N}}{A} }{ \TYPES{\Gamma}{\color{red}{MN}}{B} } \qquad \frac{ \TYPES{\Gamma}{{\color{red}M}}{\Pi x^A. B} \qquad \TYPES{\Gamma}{\color{red}{N}}{A} }{ \TYPES{\Gamma}{{\color{red}{MN}}}{B\SUBST{{\color{red}N}}{x}} }$

À gauche, nous avons la règle pour le -calculus simplement tapé , à droite la règle qui généralise la gauche avec la dépendance de type. Nous voyons qu'une valeur «coule» dans le type dans la conclusion de droite. $\lambda$

Je pense que l'assistante de preuve interactive Isabelle utilise une logique intuitive du second ordre basée sur -calculus, sans aucun nombre ni type de données récursif comme cadre logique. Divers autres ont été proposés. $\lambda$

Un avantage de l'utilisation de -calculi comme cadre logique est que les constructions de liaison comme les quantificateurs universels peuvent être implémentées en utilisant le -binder du cadre. Notez que la plupart des cadres logiques sont expressivement faibles: les cadres prennent en charge le raisonnement au niveau objet, mais sont insuffisants pour effectuer beaucoup de raisonnement méta-théorique au-delà du fait qu'une déclaration particulière au niveau objet est un théorème. En fait, la logique métallique est généralement si faible qu'il est impossible de prouver le théorème de déduction pour une logique d'objet de style Hilbert. Bien sûr, rien ne vous empêche d'utiliser des théories de type plus puissantes comme cadre logique. $\lambda$ $\lambda$

Pour ces raisons pratiques et historiques, la plupart des cadres logiques utilisés aujourd'hui sont typés -calculi, c'est-à-dire les théories des types. Voir (3, 4) pour des discussions plus approfondies sur les cadres logiques. $\lambda$

N. de Bruijn: Le langage mathématique AUTOMATH, son utilisation et certaines de ses extensions.
RF Harper, F. Honsell, G. Plotkin: Un cadre pour définir la logique .
F. Pfenning: cadres logiques.
F. Pfenning: cadres logiques - brève introduction .

Martin Berger
la source

Connaissez-vous des livres d'introduction sur les assistants de preuve (cadres logiques) adaptés à quelqu'un qui connaît déjà les bases du calcul lambda simplement tapé et de la logique du premier ordre?

Trismegistos

@Trismegistos J'ai bien peur que non. Je suggère d'apprendre un assistant spécifique. Agda est le plus facile à utiliser car il s'agit essentiellement de Haskell, mais avec des types dépendants. D'après mon expérience, le cadre logique n'est pas aussi important que les autres dimensions des assistants de preuve. Par exemple, Isabelle est un prouveur générique que vous pouvez instancier avec différentes logiques, donc expose vraiment le cadre logique. Mais Isabelle / HOL est la seule instanciation utilisée en pratique. En effet, toutes les tactiques de preuve, tout le support du prouveur ont été écrits pour la logique d'objet HOL. Et l'utilisabilité d'un prouveur dépend de ceux-ci.

Martin Berger

Cadre logique vs théorie des types

Réponses: