Type d'habitation - Type inhabitation

Dans la théorie des types , branche de la logique mathématique , dans un calcul typé donné, le problème d' habitation de type pour ce calcul est le problème suivant: étant donné un type et un environnement de typage , existe-t-il un -terme M tel que ? Avec un environnement de type vide, un tel M est dit être un habitant de . ${\ displaystyle \ tau}$ ${\ displaystyle \ Gamma}$${\ displaystyle \ lambda}$${\ displaystyle \ Gamma \ vdash M: \ tau}$${\ displaystyle \ tau}$

Relation à la logique

Dans le cas du calcul lambda simplement typé , un type a un habitant si et seulement si sa proposition correspondante est une tautologie de logique implicative minimale. De même, un type System F a un habitant si et seulement si sa proposition correspondante est une tautologie de logique du second ordre .

Le paradoxe de Girard montre que l'habitation de type est fortement liée à la cohérence d'un système de types avec la correspondance Curry-Howard. Pour être sain, un tel système doit avoir des types inhabités.

Propriétés formelles

Pour la plupart des calculs typés, le problème de l'habitation de type est très difficile . Richard Statman a prouvé que pour le calcul lambda simplement typé, le problème d' habitation de type est PSPACE-complet . Pour d'autres calculs, comme le système F , le problème est même indécidable .

Voir également

• Isomorphisme de Curry-Howard

Références

${\ displaystyle \ Gamma \ vdash x: {\ text {Int}}}$

Cet article sur la théorie du langage de programmation ou la théorie des types est un bout . Vous pouvez aider Wikipédia en le développant .

• v
• t
• e