Sujet de thèse / PhD thesis (autres sujets)

Interprétations catégoriques de la logique linéaire du premier ordre
— applications aux aspects ontologiques de la sémantique lexicale

Categorical interpretations of first order linear logic
— with application to ontological aspects of lexical semantics

 

Christian Retoré Jean Gillibert

christian.retore@labri.fr Jean.Gillibert@math.u-bordeaux1.fr

Sujet attribué à Ivano Ciardelli (Université Bordeaux 1 - Università di Bologna)

(English description below)

Interprétations catégoriques de la logique linéaire du premier ordre
— applications aux aspects ontologiques de la sémantique lexicale

Mots-clés: logique, théorie des types, théorie des catégories, linguistique informatique, philosophie du langage, lexique

Contexte

Les modèles de la logique classique du premier ordre sont bien connus et le théorème de complétude montre que F est vraie dans tout modèle si et seulement si F est démontrable. En revanche, il n'y a pas d'interprétation simple des démonstrations formelles de la logique classique.

Pour la logique intuitionniste, la situation est inversée. Il est relativement facile d'interpréter une formule comme l'ensemble de ses démonstrations potentielles, et les démonstrations de A=>B sont les fonctions des démonstrations de A dans les démonstrations de B. Les modèles sont en revanche plus compliqués, ce sont des faisceaux de modèles classiques (sur un espace topologique ou sur une prétopologie de Grothendieck) et la notion de validité est à remplacer par une notion de forcing. Le théorème de complétude est alors vérifié. On sait même, grâce aux travaux de Lawvere, relier les modèles du premier ordre et les interprétations des démonstrations.

La logique linéaire est un raffinement de la logique intutionniste qui analyse les mécanismes de calcul sous-jacents à cette dernière. Ce raffinement permet en outre de gérer les ressources lors d'un calcul, de partager les calculs qui peuvent l'être, de spécificier des programmes suffisamment précisément pour borner leur complexité. En linguistique, la logique linéaire peut modéliser certains aspects de la syntaxe, de la sémantique et de leur relation mutuelle, à la suite des travaux sur les grammaires catégorielles ou la sémantique de LFG. Néanmoins elle souffre de l'absence de modèles naturels du premier ordre qui, dans toutes les applications évoquées, seraient fort bienvenus.

Objectif

Du point de vue fondamental, cette thèse a pour ambition l'étude de modèles non ad hoc de la logique linéaire du premier ordre, par exemple issus de la géométrie, et de leur combinaison avec la sémantique des preuves, comme les espaces cohérents. Si cela s'avère possible on essaiera aussi de comprendre le lien avec la dynamique des preuves exprimée par la ludique.

Du point de vue applicatif, on étudiera la logique linéaire pour spécifier les facettes du sens d'un mot et l'ontologie du lexique qui n'est pas forcément celle du monde. On tâchera de rendre compte de la possibilité d'accéder à certains aspects du sens d'un mot, d'appliquer simultanément plusieurs prédicats à différentes facettes d'un même mot.

Prérequis

Un niveau master 1 en mathématiques est indispensable. Une connaissance de la logique mathématique ou de la théorie des catégories sera appréciée. Les aspects applicatifs, linguistiques ou philosophiques, seront découverts pendant la thèse.

Categorical interpretations of first order linear logic
— with application to ontological aspects of lexical semantics

Keywords: logic, category theory, type theory, computational linguistics, philosophy of language, lexicon,

Context

Models of first-order classical logic are well-known and the completeness theorem shows that F is true in every model if and only if it is provable. But there is no simple interpretation of classical proofs.

The situation is reversed for intuitionistic logic. It is relatively easy to interpret a formula as the set of its possible proofs, and the proofs of A=>B map proofs of A on proofs of B. Models are more complex, they are sheaves of classical models (over a topological space or a Grothendieck's pretopology) and a forcing notion is used for validity and completeness holds. Thanks to Lawvere's work, it is ossible to connect the interpretation of proofs with first order models.

Linear logic is refinement of intuitionistic logic, which analyses the computational contents of the later. This refinement allows resource management and process sharing or to specify programs as precisely as to bound their algorithmic complexity. Linear logic can also model some aspects of natural language syntax, semantics and their interconnection, following the work on categorial grammars or on LFG semantics. Nevertheless linear logic lacks a natural notion of model for first-order formulae, while it would be most welcome for the aforementioned applications.

Objective

The theoretical objective is to find non ad hoc models of first order linear logic, for instance issued from geometry, and their combination with proof semantics like coherence spaces. If it looks possible, a second objective will be a better understanding of the relation with proof computations as expressed by ludics.

The privileged application of first order linear logic will be the facets of the meanings of a given word, the ontology inherent to the lexicon (which need not coincide with the world's ontology). The possibility to access to the various facets of a word meaning, or to apply simultaneously several predicates to different facets will be explored.

Prerequisites

A graduate level in mathematics is mandatory. Some background in mathematical logic or category theory is welcome. Applicative aspects, linguistic and philosophic, will be discovered during the thesis.

Bibliographie / bibliography