Logique multitriée - Many-sorted logic

La logique multitriée peut refléter formellement notre intention de ne pas traiter l'univers comme une collection homogène d'objets, mais de le partitionner d'une manière similaire aux types dans la programmation typée . Les « parties du discours » tant fonctionnelles qu'assertives dans le langage de la logique reflètent ce partitionnement typé de l'univers, même au niveau syntaxique : la substitution et le passage d'arguments ne peuvent se faire qu'en conséquence, en respectant les « sortes ».

Il existe différentes manières de formaliser l'intention évoquée ci-dessus ; une logique multitriée est tout paquet d'informations qui la remplit. Dans la plupart des cas, les éléments suivants sont indiqués :

• un ensemble de sortes, S
• une généralisation appropriée de la notion de signature pour pouvoir traiter les informations supplémentaires qui accompagnent les tris.

Le domaine du discours de toute structure de cette signature est alors fragmenté en sous-ensembles disjoints, un pour chaque sorte.

Exemple

Lorsqu'on raisonne sur les organismes biologiques, il est utile de distinguer deux sortes : et . Alors qu'une fonction a du sens, une fonction similaire n'en a généralement pas. La logique à plusieurs tris permet d'avoir des termes comme , mais de rejeter des termes comme comme syntaxiquement mal formés. ${\displaystyle \mathrm {plante} }$${\displaystyle \mathrm {animal} }$${\displaystyle \mathrm {mère} \colon \mathrm {animal} \to \mathrm {animal} }$${\displaystyle \mathrm {mère} \colon \mathrm {plante} \to \mathrm {plante} }$${\displaystyle \mathrm {mère} (\mathrm {lassie} )}$${\displaystyle \mathrm {mère} (\mathrm {mon\_favori\_chêne} )}$

Algébrisation

L'algébrisation de la logique multitriée est expliquée dans un article de Caleiro et Gonçalves, qui généralise la logique algébrique abstraite au cas multitrié , mais peut également être utilisé comme matériel d'introduction.

Logique triée par ordre

Alors que de nombreux triées logique nécessite deux types distincts d'avoir des ensembles d'univers disjoints, triées ordre logique permet une sorte d'être déclaré subsort d' une autre sorte , généralement par écrit ou syntaxe similaire. Dans l' exemple de biologie ci - dessus , il est souhaitable de déclarer ${\style d'affichage s_{1}}$${\style d'affichage s_{2}}$${\displaystyle s_{1}\subseteq s_{2}}$

${\displaystyle {\textit {chien}}\subseteq {\textit {carnivore}}}$,

${\displaystyle {\textit {chien}}\subseteq {\textit {mammifère}}}$,

${\displaystyle {\textit {carnivore}}\subseteq {\textit {animal}}}$,

${\displaystyle {\textit {mammifère}}\subseteq {\textit {animal}}}$,

${\displaystyle {\textit {animal}}\subseteq {\textit {organisme}}}$,

${\displaystyle {\textit {plante}}\subseteq {\textit {organisme}}}$,

etc; cf. photo.

Partout où un terme quelconque est requis, un terme de n'importe quelle sous-sorte de peut être fourni à la place ( principe de substitution de Liskov ). Par exemple, en supposant une déclaration de fonction , et une déclaration constante , le terme est parfaitement valide et a la sorte . Afin de fournir l'information que la mère d'un chien est à son tour un chien, une autre déclaration peut être délivrée ; c'est ce qu'on appelle la surcharge de fonction , similaire à la surcharge dans les langages de programmation . ${\style d'affichage s}$${\style d'affichage s}$${\displaystyle {\textit {mère}} :{\textit {animal}}\longrightarrow {\textit {animal}}}$${\displaystyle {\textit {lassie}} :{\textit {chien}}}$${\displaystyle {\textit {mère}}({\textit {lassie}})}$${\displaystyle {\textit {animal}}}$${\displaystyle {\textit {mère}} :{\textit {chien}}\longrightarrow {\textit {chien}}}$

La logique triée par ordre peut être traduite en logique non triée, en utilisant un prédicat unaire pour chaque sorte et un axiome pour chaque déclaration de sous-sort . L'approche inverse a réussi à prouver un théorème automatisé : en 1985, Christoph Walther a pu résoudre un problème de référence en le traduisant en logique triée par ordre, le réduisant ainsi d'un ordre de grandeur, car de nombreux prédicats unaires se sont transformés en sortes. ${\style d'affichage p_{i}(x)}$${\style d'affichage s_{i}}$${\displaystyle \forall x(p_{i}(x)\rightarrow p_{j}(x))}$${\displaystyle s_{i}\subseteq s_{j}}$

Afin d'incorporer une logique triée par ordre dans un démonstrateur de théorème automatisé basé sur des clauses, un algorithme d' unification trié par ordre correspondant est nécessaire, ce qui nécessite que pour deux sortes déclarées, leur intersection soit également déclarée : si et sont des variables de tri et , respectivement, l'équation a la solution , où . ${\style d'affichage s_{1},s_{2}}$${\displaystyle s_{1}\cap s_{2}}$${\style d'affichage x_{1}}$${\style d'affichage x_{2}}$${\style d'affichage s_{1}}$${\style d'affichage s_{2}}$${\displaystyle x_{1}{\stackrel {?}{=}}\,x_{2}}$${\displaystyle \{x_{1}=x,\;x_{2}=x\}}$${\displaystyle x:s_{1}\cap s_{2}}$

Smolka a généralisé la logique triée par ordre pour permettre le polymorphisme paramétrique . Dans son cadre, les déclarations de sous-sorts sont propagées vers des expressions de types complexes. À titre d'exemple de programmation, un tri paramétrique peut être déclaré (en étant un paramètre de type comme dans un modèle C++ ), et à partir d'une déclaration de sous-sort, la relation est automatiquement déduite, ce qui signifie que chaque liste d'entiers est également une liste de flottants. ${\displaystyle {\textit {list}}(X)}$${\style d'affichage X}$${\displaystyle {\textit {int}}\subseteq {\textit {float}}}$${\displaystyle {\textit {list}}({\textit {int}})\subseteq {\textit {list}}({\textit {float}})}$

Schmidt-Schauß a généralisé la logique triée par ordre pour permettre les déclarations de termes. Par exemple, en supposant des déclarations de sous-sort et , une déclaration de terme comme permet de déclarer une propriété d'addition d'entiers qui ne pourrait pas être exprimée par une surcharge ordinaire. ${\displaystyle {\textit {even}}\subseteq {\textit {int}}}$${\displaystyle {\textit {impair}}\subseteq {\textit {int}}}$${\displaystyle \forall i:{\textit {int}}.\;(i+i):{\textit {even}}}$

Voir également

• Logique catégorielle
• Logique du premier ordre à plusieurs tris#Logique à plusieurs tris

Les références

Les premiers articles sur la logique multitriée comprennent :

• Wang, Hao (1952). « La logique des théories multi-triées ». Journal de logique symbolique . 17 (2) : 105-116. doi : 10.2307/2266241 . JSTOR  2266241 ., rassemblés dans l'ouvrage de l'auteur sur le calcul, la logique et la philosophie. Une collection d'essais , Pékin : Science Press ; Dordrecht : Kluwer Academic, 1990.
• Gilmore, CP (1958). « Un ajout à « La logique des théories multiples » » (PDF) . Composition Mathématique . 13 : 277–281.
• A. Oberschelp (1962). "Untersuchungen zur mehrsortigen Quantorenlogik" . Mathematische Annalen . 145 (4) : 297-333. doi : 10.1007/bf01396685 . S2CID  123363080 . Archivé de l'original le 2015-02-20 . Récupéré le 2013-09-11 .
• F. Jeffry Pelletier (1972). « Quantification Sortal et quantification restreinte » (PDF) . Études philosophiques . 23 (6) : 400-404. doi : 10.1007/bf00355532 . S2CID  170303654 .

Liens externes

• "Many-sorted Logic" , le premier chapitre des Notes de cours sur les procédures de décision de Calogero G. Zarba