5 février 2004
La notation mathématique a peu évolué depuis le début du 20ème siècle, et le paradigme dominant de la théorie des ensembles classique a occulté la notion traditionnelle de fonction comme procédé de calcul au profit de relations fonctionnelles réduites à un graphe extensionnel. L’invention du lambda-calcul par le logicien Church pour exprimer une théorie de la fonctionnalité où les fonctions sont des objets de première classe n’a donc pas eu d’impact sur la notation mathématique, alors que les langages de programmation allaient l’adopter comme formalisme noyau. La correspondance de Curry-Howard, qui donne un isomorphisme entre un espace de preuves formelles et un espace fonctionnel, nous permet maintenant de comprendre la notion de calcul comme l’élaboration d’une justification canonique à une spécification logique.
En parallèle, le développement des grammaires catégorielles en linguistique a montré que la syntaxe des langues avait pour noyau une logique linéaire non commutative, alors que les grammaires de Montague montrent qu’on peut prolonger ces structures syntaxiques en dénotations sémantiques de nature calculatoire. Les procédés anaphoriques, les ellipses, et plus généralement la structure rhétorique du discours, mais aussi la structure informationnelle du dialogue, peuvent être à leur tour formalisés dans des calculs fonctionnels de la théorie des types, et dans des calculs d’interaction de processus de la ludique.
Une grande unité conceptuelle se dégage ainsi des rapports mutuels entre informatique, logique et linguistique.
Vidéo indisponible
Télécharger le pdf de la présentation
