Logique linéaire

vignette|Arbre de résolution linéaire En logique mathématique et plus précisément en théorie de la démonstration, la logique linéaire est un système formel inventé par le logicien Jean-Yves Girard en 1987. Du point de vue logique, la logique linéaire décompose et analyse les logiques classique et intuitionniste. Du point de vue calculatoire, elle est un système de type pour le lambda-calcul permettant de spécifier certains usages des ressources. La logique classique n'étudie pas les aspects les plus élémentaires du raisonnement. Sa structure peut être décomposée dans des systèmes formels plus élémentaires qui décrivent des étapes plus fines de la déduction ; en particulier, il est possible de s'intéresser à des logiques où certaines règles de la logique classique n'existent pas. De telles logiques sont appelées des logiques sous-structurelles. L'une de ces logiques sous-structurelles est la logique linéaire ; il lui manque en particulier la règle de contraction de la logique classique qui dit en gros que si on peut faire un raisonnement avec une même hypothèse invoquée deux fois, on peut faire le même raisonnement sans dupliquer cette hypothèse et la règle daffaiblissement qui permet d'éliminer de l'ensemble des hypothèses une hypothèse inutilisée dans le raisonnement. La logique linéaire peut se comprendre au travers de la correspondance de Curry-Howard comme un système de typage des programmes d'ordre supérieur (lambda-calcul typé) permettant d'exprimer la manière dont ceux-ci gèrent leurs ressources, et notamment le fait qu'une ressource soit consommée linéairement, c'est-à-dire une et une seule fois pendant l'exécution du programme. La logique linéaire promeut une vision « géométrique » des syntaxes formelles en cultivant l'analogie avec l'algèbre linéaire (espaces cohérents) et en introduisant de nouvelles représentations des preuves/programmes utilisant des graphes (réseaux de preuves), voire des opérateurs (géométrie de l'interaction). Elle a également permis à Girard de proposer une approche logique de la complexité algorithmique (logique linéaire légère et élémentaire).