Question d'origine :
Pourquoi la linguistique contemporaine n'utilise-t-elle pas des logiques de description (description logic) telles qu'utilisées en modélisation de l'information en intelligence artificielle (knowledge representation) pour modéliser la variété de sens des mots en complémentarité de la théorie des types ? Merci !
Réponse du Guichet
gds_et
- Département : Équipe du Guichet du Savoir
Le 14/12/2020 à 12h06
Bonjour,
Commençons par préciser ce que sont les logiques de description et dans quels cadres elles s’appliquent :
«3.1 Origines et applications des logiques de description
Les logiques de description ont été conçues à partir des réseaux sémantiques de Quillian [Qui88] qui sont des graphes orientés étiquetés dans lesquels on associe des concepts aux noeuds et des relations aux arcs. Elles sont également influencées par la sémantique des cadres de Minsky [Min74] dans laquelle les concepts sont représentés par des cadres caractérisés par un certain nombre d'attributs (appelés aussi slots).
Les logiques de description forment une famille de langages de représentation de connaissances qui peuvent être utilisées pour représenter la connaissance terminologique d'un domaine d'application d'une façon structurée et formelle. Le nom "logique de description" peut être interprété de deux manières. D'une part ces langages ont étés élaborés pour écrire la "description" des concepts pertinents d'un domaine d'application. D'autre part, une caractéristique cruciale de ces langages est qu'ils ont une sémantique formelle définie en logique du première ordre (à la différence des propositions précédentes comme les cadres de Minsky). Dans ce sens, nous pouvons dire que les LDs ont une sémantique "descriptive" formelle.
3. Logiques de description
Les logiques de descriptions sont utilisées pour de nombreuses applications (voir International Work-shop on Description Logics[Hor05] et Workshop on Applications of Description Logics [Bec04] ) comme par exemple :
- Le web sémantique (e.g., représentation d'ontologies et recherche d'information basée sur la logique)
- La médecine/bioinformatique (e.g., représenter et gérer des ontologies biomédicales)
- Le traitement automatique des langues
- L'ingénierie de processus (e.g., représenter des descriptions de service)
- L'ingénierie de la connaissance (e.g., représenter des ontologies)
- L'ingénierie logicielle (e.g., représenter la sémantique des diagrammes de classe UML)
3.2 Définition des Logiques de Description
La plupart des logiques de descriptions divisent la connaissance en deux parties contenants :
- les informations terminologiques: définition des notions basiques ou dérivées et des relations entre ces notions. Ces informations sont "génériques" ou "globales", vraies dans tous les modèles et pour tous les individus.
- les informations sur les assertions: ces informations sont "spécifiques" ou "locales", vraies pour certains individus particuliers.
L'ensemble des informations est modélisé par un couple〈T, A〉, où T est un ensemble de formules relatives aux informations terminologiques (la T-Box) et A est un ensemble de formules relatives aux informations sur les assertions (la A-Box).
Une autre manière de voir la séparation entre ces informations, est d'associer la T-Box aux règles qui régissent notre monde (e.g., la physique, la chimie, la biologie, ...), et d'associer les individus de notre monde à la A-Box (e.g., Jean, Marie, un chat, ...). »
Source : Implication textuelle et logiques de description, Paul Bedaride
Ainsi que la théorie des types :
« En mathématiques, logique et informatique, une théorie des types est une classe de systèmes formels, dont certains peuvent servir d'alternatives à la théorie des ensembles comme fondation des mathématiques. Grosso modo, un type est une « caractérisation » des éléments qu'un terme qualifie. En théorie des types, chaque terme possède un type et les opérations décrites par le système imposent des restrictions sur le type des termes qu'elles combinent.
La théorie des types est très liée à (et recoupe parfois) l'étude des systèmes de types qui sont utilisés dans certains langages de programmation afin d'éviter certains bugs. Cependant, historiquement les théories des types ont été introduites pour empêcher des paradoxes de la logique formelle et l'expression « théorie des types » renvoie souvent à ce contexte plus large.
Deux théories des types qui émergent peuvent servir de fondations pour les mathématiques ; ce sont le λ-calcul typé d'Alonzo Church et la théorie des types intuitionniste de Per Martin-Löf. Quoi qu'il en soit, les théories des types créées par les logiciens trouvent une application majeure comme systèmes axiomatiques de la majorité des assistants de preuve du fait de la correspondance de Curry-Howard liant démonstrations et programmes.
Histoire
D'un point de vue de la théorie mathématique : les types ont été pour la première fois théorisés par Bertrand Russell comme réponse à sa découverte du paradoxe ébranlant la théorie naïve des ensembles de Gottlob Frege. Cette théorie des types est développée dans l'ouvrage Principia Mathematica de Russell et Whitehead. Elle permet de contourner le paradoxe de Russell en introduisant tout d'abord une hiérarchie de types, puis en assignant un type à chaque entité mathématique. Les objets d'un certain type ne peuvent être construits qu'à partir d'objets leur pré-existant (situés plus bas dans la hiérarchie), empêchant ainsi les boucles infinies et les paradoxes de surgir et de casser la théorie.
Pour ce qui concerne le sous-domaine des mathématiques nommé la logique mathématique — mais c'est aussi très utile dans le domaine de l'informatique, dans des sous-domaines nommés théorie des grammaires, théorie de la compilation, et système de réécriture, voire plus récemment dans le domaine de la transcompilation — on utilise les types dans le cadre de la théorie des types.
Dans le langage courant, « théorie des types » est à comprendre dans le contexte des systèmes de réécriture. L'exemple le plus connu est le lambda calcul d'Alonzo Church. Sa Theory of Types a permis de passer du calcul non-typé originel, incohérent du fait du paradoxe de Kleene-Rosser (en), à un calcul correct. Church a démontré que ce système pouvait servir de fondement des mathématiques ; on le décrit comme une logique d'ordre supérieur.
D'autres théories des types marquantes sont la théorie des types intuitionniste de Per Martin-Löf qui est utilisée comme fondement dans certaines branches des mathématiques constructivistes et pour des assistants de preuve tels que Agda (en) ou Idris. Le calcul des constructions de Thierry Coquand et ses extensions sont utilisés notamment par Coq et Matita (en). Il s'agit d'une recherche active, comme le démontrent les récents développements en théorie des types homotopiques.
Une première théorie des types (dite « ramifiée ») a été créée par Bertrand Russell pour résoudre les paradoxes logiques, comme celui du menteur et ceux de la théorie des ensembles ; lourde d'emploi, elle a d'abord été simplifiée par Ramsey puis supplantée par la théorie de Zermelo-Frankel en 1922 (socle axiomatique utilisé par tous les mathématiciens, l'autre théorie NF conçue par Quine en 1937 et perfectionnée en NFU en 1969 par Ronald Jensen n'étant pas utilisée par les mathématiciens malgré les possibilités simplificatrices qu'elle offre, voir New Foundations), et aussi reconsidérée pour des objets plus élémentaires après la découverte du lambda-calcul et de la logique combinatoire. Bien que ces théories soient cohérentes dans leurs versions originelles, qui sont non typées, il est intéressant d'en étudier des formulations avec types.
Dans ces derniers cas, les entités mathématiques sont construites à l'aide de fonctions, où chaque fonction a un type qui décrit le type de ses arguments et le type de la valeur retournée. Les entités sont bien formées lorsque les fonctions sont appliquées à des entités ayant le type que la fonction attend.
Applications
Le concept de type a plusieurs domaines d'applications :
• les théories des ensembles qui, suivant l'intuition de Russell, classent les ensembles en différents types ;
• la logique pour laquelle on cherche à donner un contenu calculatoire aux propositions et aux démonstrations par la correspondance de Curry-Howard ;
• la théorie des modèles, où un type est un ensemble de formules particulier ;
• les langages de programmation, surtout les langages fonctionnels typés ;
• les systèmes de démonstration sur ordinateur ;
• la linguistique, à travers le concept de catégorie syntaxique.
Source : Wikipedia
Nos connaissances très rudimentaires dans les domaines concernés ne nous permettent pas de vous apporter directement des éléments de réponse. Néanmoins nous vous proposons ci-dessous quelques références qui vous aideront peut-être à avancer dans votre réflexion :
- Habert, Benoît. « Outiller la linguistique : de l'emprunt de techniques aux rencontres de savoirs », Revue française de linguistique appliquée, vol. vol. ix, no. 1, 2004, pp. 5-24.
- La langue commune au cœur du raisonnement, notamment mathématique, Christian Retoré
- Conception et implantation d’un modèle de raisonnement sur les contextes basée sur une théorie des types et utilisant une ontologie de domaine, Patrick Barlatier
- Logique de la détermination d’objets (ldo) : une logique pour l’analyse des langues naturelles, Jean-Pierre Desclés, Anca Pascu
- Monnin, Alexandre. « L’ingénierie philosophique de Rudolf Carnap. De l’IA au Web sémantique », Cahiers philosophiques, vol. 141, no. 2, 2015, pp. 27-53.
Bonne journée.
Commençons par préciser ce que sont les logiques de description et dans quels cadres elles s’appliquent :
«
Les logiques de description ont été conçues à partir des réseaux sémantiques de Quillian [Qui88] qui sont des graphes orientés étiquetés dans lesquels on associe des concepts aux noeuds et des relations aux arcs. Elles sont également influencées par la sémantique des cadres de Minsky [Min74] dans laquelle les concepts sont représentés par des cadres caractérisés par un certain nombre d'attributs (appelés aussi slots).
Les logiques de description forment une famille de langages de représentation de connaissances qui peuvent être utilisées pour représenter la connaissance terminologique d'un domaine d'application d'une façon structurée et formelle. Le nom "logique de description" peut être interprété de deux manières. D'une part ces langages ont étés élaborés pour écrire la "description" des concepts pertinents d'un domaine d'application. D'autre part, une caractéristique cruciale de ces langages est qu'ils ont une sémantique formelle définie en logique du première ordre (à la différence des propositions précédentes comme les cadres de Minsky). Dans ce sens, nous pouvons dire que les LDs ont une sémantique "descriptive" formelle.
3. Logiques de description
Les logiques de descriptions sont utilisées pour de nombreuses applications (voir International Work-shop on Description Logics[Hor05] et Workshop on Applications of Description Logics [Bec04] ) comme par exemple :
- Le web sémantique (e.g., représentation d'ontologies et recherche d'information basée sur la logique)
- La médecine/bioinformatique (e.g., représenter et gérer des ontologies biomédicales)
- Le traitement automatique des langues
- L'ingénierie de processus (e.g., représenter des descriptions de service)
- L'ingénierie de la connaissance (e.g., représenter des ontologies)
- L'ingénierie logicielle (e.g., représenter la sémantique des diagrammes de classe UML)
La plupart des logiques de descriptions divisent la connaissance en deux parties contenants :
- les informations terminologiques: définition des notions basiques ou dérivées et des relations entre ces notions. Ces informations sont "génériques" ou "globales", vraies dans tous les modèles et pour tous les individus.
- les informations sur les assertions: ces informations sont "spécifiques" ou "locales", vraies pour certains individus particuliers.
L'ensemble des informations est modélisé par un couple〈T, A〉, où T est un ensemble de formules relatives aux informations terminologiques (la T-Box) et A est un ensemble de formules relatives aux informations sur les assertions (la A-Box).
Une autre manière de voir la séparation entre ces informations, est d'associer la T-Box aux règles qui régissent notre monde (e.g., la physique, la chimie, la biologie, ...), et d'associer les individus de notre monde à la A-Box (e.g., Jean, Marie, un chat, ...). »
Source : Implication textuelle et logiques de description, Paul Bedaride
Ainsi que la théorie des types :
« En mathématiques, logique et informatique, une théorie des types est une classe de systèmes formels, dont certains peuvent servir d'alternatives à la théorie des ensembles comme fondation des mathématiques. Grosso modo, un type est une « caractérisation » des éléments qu'un terme qualifie. En théorie des types, chaque terme possède un type et les opérations décrites par le système imposent des restrictions sur le type des termes qu'elles combinent.
La théorie des types est très liée à (et recoupe parfois) l'étude des systèmes de types qui sont utilisés dans certains langages de programmation afin d'éviter certains bugs. Cependant, historiquement les théories des types ont été introduites pour empêcher des paradoxes de la logique formelle et l'expression « théorie des types » renvoie souvent à ce contexte plus large.
Deux théories des types qui émergent peuvent servir de fondations pour les mathématiques ; ce sont le λ-calcul typé d'Alonzo Church et la théorie des types intuitionniste de Per Martin-Löf. Quoi qu'il en soit, les théories des types créées par les logiciens trouvent une application majeure comme systèmes axiomatiques de la majorité des assistants de preuve du fait de la correspondance de Curry-Howard liant démonstrations et programmes.
D'un point de vue de la théorie mathématique : les types ont été pour la première fois théorisés par Bertrand Russell comme réponse à sa découverte du paradoxe ébranlant la théorie naïve des ensembles de Gottlob Frege. Cette théorie des types est développée dans l'ouvrage Principia Mathematica de Russell et Whitehead. Elle permet de contourner le paradoxe de Russell en introduisant tout d'abord une hiérarchie de types, puis en assignant un type à chaque entité mathématique. Les objets d'un certain type ne peuvent être construits qu'à partir d'objets leur pré-existant (situés plus bas dans la hiérarchie), empêchant ainsi les boucles infinies et les paradoxes de surgir et de casser la théorie.
Pour ce qui concerne le sous-domaine des mathématiques nommé la logique mathématique — mais c'est aussi très utile dans le domaine de l'informatique, dans des sous-domaines nommés théorie des grammaires, théorie de la compilation, et système de réécriture, voire plus récemment dans le domaine de la transcompilation — on utilise les types dans le cadre de la théorie des types.
Dans le langage courant, « théorie des types » est à comprendre dans le contexte des systèmes de réécriture. L'exemple le plus connu est le lambda calcul d'Alonzo Church. Sa Theory of Types a permis de passer du calcul non-typé originel, incohérent du fait du paradoxe de Kleene-Rosser (en), à un calcul correct. Church a démontré que ce système pouvait servir de fondement des mathématiques ; on le décrit comme une logique d'ordre supérieur.
D'autres théories des types marquantes sont la théorie des types intuitionniste de Per Martin-Löf qui est utilisée comme fondement dans certaines branches des mathématiques constructivistes et pour des assistants de preuve tels que Agda (en) ou Idris. Le calcul des constructions de Thierry Coquand et ses extensions sont utilisés notamment par Coq et Matita (en). Il s'agit d'une recherche active, comme le démontrent les récents développements en théorie des types homotopiques.
Une première théorie des types (dite « ramifiée ») a été créée par Bertrand Russell pour résoudre les paradoxes logiques, comme celui du menteur et ceux de la théorie des ensembles ; lourde d'emploi, elle a d'abord été simplifiée par Ramsey puis supplantée par la théorie de Zermelo-Frankel en 1922 (socle axiomatique utilisé par tous les mathématiciens, l'autre théorie NF conçue par Quine en 1937 et perfectionnée en NFU en 1969 par Ronald Jensen n'étant pas utilisée par les mathématiciens malgré les possibilités simplificatrices qu'elle offre, voir New Foundations), et aussi reconsidérée pour des objets plus élémentaires après la découverte du lambda-calcul et de la logique combinatoire. Bien que ces théories soient cohérentes dans leurs versions originelles, qui sont non typées, il est intéressant d'en étudier des formulations avec types.
Dans ces derniers cas, les entités mathématiques sont construites à l'aide de fonctions, où chaque fonction a un type qui décrit le type de ses arguments et le type de la valeur retournée. Les entités sont bien formées lorsque les fonctions sont appliquées à des entités ayant le type que la fonction attend.
Le concept de type a plusieurs domaines d'applications :
• les théories des ensembles qui, suivant l'intuition de Russell, classent les ensembles en différents types ;
• la logique pour laquelle on cherche à donner un contenu calculatoire aux propositions et aux démonstrations par la correspondance de Curry-Howard ;
• la théorie des modèles, où un type est un ensemble de formules particulier ;
• les langages de programmation, surtout les langages fonctionnels typés ;
• les systèmes de démonstration sur ordinateur ;
• la linguistique, à travers le concept de catégorie syntaxique.
Source : Wikipedia
Nos connaissances très rudimentaires dans les domaines concernés ne nous permettent pas de vous apporter directement des éléments de réponse. Néanmoins nous vous proposons ci-dessous quelques références qui vous aideront peut-être à avancer dans votre réflexion :
- Habert, Benoît. « Outiller la linguistique : de l'emprunt de techniques aux rencontres de savoirs », Revue française de linguistique appliquée, vol. vol. ix, no. 1, 2004, pp. 5-24.
- La langue commune au cœur du raisonnement, notamment mathématique, Christian Retoré
- Conception et implantation d’un modèle de raisonnement sur les contextes basée sur une théorie des types et utilisant une ontologie de domaine, Patrick Barlatier
- Logique de la détermination d’objets (ldo) : une logique pour l’analyse des langues naturelles, Jean-Pierre Desclés, Anca Pascu
- Monnin, Alexandre. « L’ingénierie philosophique de Rudolf Carnap. De l’IA au Web sémantique », Cahiers philosophiques, vol. 141, no. 2, 2015, pp. 27-53.
Bonne journée.
DANS NOS COLLECTIONS :
Ça pourrait vous intéresser :
Commentaires 0
Connectez-vous pour pouvoir commenter.
Se connecter