Les logiques : notes en vrac

Il n’existe pas qu’une logique du lambda calcul, mais plusieurs. Il existe une logique pour chacune de ses variantes concernant les types. On distingue principalement :

• Lambda calcul non‑typé, qui donne la logique des propositions du premier ordre, FOL ;
• simplement typé, qui donne la logique d’ordre supérieur, HOL ;
• simplement typé avec fixed‑point combinator (je ne sais pas comment on le traduit en français) ;
• typé avec polymorphisme (System F) ;
• typé avec polymorphisme d’ordre supérieur (System Fω).

Cette liste n’est pas exhaustive, mais le plus important y est mentionné.

De plus, mais c’est moins important pour la logique je crois, il existe deux familles de typage du lambda calcul : à la Curry, “ lambda calculus with type assignment ”, où le type est explicite, et à la Church, “ type lambda calculus ”, où le type est implicite.

Une question que je me pose : il a été démontré depuis longtemps, que le lambda calcul non‑typé permet de représenté toutes les fonctions calculables, mais est‑ce le cas aussi des lambda calculs typés ?

Dans la logique du premier ordre au moins, la formule S ⊨ F se lit comme ayant n’importe laquelle de ces significations :

• F est vrai dans S ;
• S satisfait F ;
• S est un modèle de F.

Ce n’est pas tout à fait une conséquence dans ce cas, mais plutôt un jugement.

Au passage, on a là une définition de ce qu’est un modèle.

Appliqués dans une même logique, le calcul des séquents, la déduction naturelle et les systèmes à la Hilbert, sont équivalents pour ce qui est de la démonstrabilité, ils ne différent que par des aspects pratiques.

Il existe une importe opposition entre sémantique dénotationnelle et sémantique opérationnelle. Même si je crois que ce qui est compréhensible dans l’une l’est aussi dans l’autre, il y doit y avoir des différences pratiques.

La sémantique opérationnelle, est celle d’une machine virtuelle, la sémantique dénotationnelle, est celle des objet mathématique.

Je me demande si le lambda calcul a les deux sémantiques ou une seule des deux et laquelle. Même question pour SML.

Il existe assez une opposition entre théorie des types et théorie des ensembles, d’un part, et entre théorie des catégories et théorie des ensembles, d’une autre part.

Il existe quand‑même une petite superposition entre théorie des types et théorie des ensembles. J’ignore s’il existe aussi une petite superposition entre théorie des catégories et théorie des ensembles.

Je me demande si les types quotient sont considérés comme des types algébriques. Je ne crois pas, mais leur nom peut le faire penser.

Un format permettant d’échanger de preuves entre des assistants de preuves, peut être vu comme un certificat de preuve. C’est le cas du format OpenTheory.

Il me semble que ces quatre expressions désignent la même chose :

• Dependent types theory, DTT (théorie des types dépendants) ;
• Martin‑Löf type theory, MLTT (théorie des types de Martin‑Löf) ;
• Constructive type theory, CTT (théorie constructive des types) ;
• Intuitionistic type theory, ITT (théorie intuitioniste des types).

La première expressions, les types dépendants, est la plus répandue dans la littérature où la logique est appliquée à l’informatique.

Une règle des système de typage.

Si une expression E1 a un type T, si l’expression E1 peut s’évaluer en l’expression E2, alors E2 doit avoir aussi le type T (en notant qu’une expression peut éventuellement être de plusieurs types). Cette condition est requise pour qu’un système de typage soit correcte (sa soundness).

C’est le principe de la préservation du type, ou type preservation.