Skip to topic | Skip to bottom
Home
Linfo
Linfo.Histoirer1.1 - 14 Apr 2005 - 16:26 - NdeyeMarieTouretopic end

Start of topic | Skip to actions
La logique linéaire, introduite par Jean-Yves Girard vers 1986, est tout à la fois une branche de la théorie de la démonstration classique et une théorie mathématique de certains aspects de l'informatique .Cette forme de logique montre les propriétés constructives de la logique intuitionniste et les symétries de la logique classique. Girard s’est inspirée de plusieurs projets de scientifiques: - le Programme de Hilbert qui date des années 1920 et qui correspond à la vision formaliste des mathématiques, - le Projet de Brouwer qui a fondé l’intuitionnisme.

Depuis son apparition en 1986, elle s'est imposée , aussi bien comme un objet riche autorisant des développements internes, que comme un outil utilisé dans des domaines variés .Par exemple, elle est utilisée pour la théorie de la démonstration au lambda-calcul, à la conception de machines abstraites, à la théorie de la complexité , à la programmation logique pour la recherche de preuves (Prolog).La logique linéaire est aussi un outil commun à de nombreux travaux en sémantique des langages de programmation , notamment des langages fonctionnels, et en typage.

Elle est fondée sur une analyse fine de la sémantique de la logique intuitionniste et sur une analogie avec l'algèbre linéaire .Le plus souvent, les problèmes informatiques abordés par la logique linéaire sont l'évaluation des langages fonctionnels avec partage de calculs, ou la programmation logique et la modélisation de la concurrence. Cette forme de logique est utilisée comme un langage de spécification de processus. Ce sont les démonstrations elles-mêmes qui sont vues comme des processus, et le mécanisme de calcul est alors interne à la logique : l'élimination des coupures. Selon cette approche, les démonstrations sont elles-mêmes des programmes à évaluer.

La logique linéaire répond à 2 ambitions :

  • elle est constructive : toute preuve d'une formule passe forcément par le calcul d'un exemple; tout en possédant le principe du tiers exclus.
  • elle intègre une notion de ressource : un fait validé n'est pas utilisable un nombre arbitraire de fois.

(modifications en cours)

-- NdeyeMarieToure - 14 Apr 2005
to top


Copyright © 1999-2020 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding WIKIDeptinfo? Send feedback