Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Logique linéaire
Résumé
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).
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.