Lógica de múltiples tipos

La lógica multisortada puede reflejar formalmente nuestra intención de no tratar el universo como una colección homogénea de objetos, sino de particionarlo de una manera similar a los tipos en la programación tipada . Tanto las " partes del discurso " funcionales como las asertivas en el lenguaje de la lógica reflejan esta partición tipada del universo, incluso a nivel sintáctico: la sustitución y el paso de argumentos solo pueden realizarse de acuerdo con los "tipos".

Existen diversas maneras de formalizar la intención mencionada anteriormente; una lógica multisortada es cualquier conjunto de información que la cumple. En la mayoría de los casos, se proporcionan los siguientes elementos:

• un conjunto de algún tipo, S
• una generalización apropiada de la noción de firma para poder manejar la información adicional que viene con los tipos.

El dominio del discurso de cualquier estructura de esa firma se fragmenta entonces en subconjuntos disjuntos, uno para cada tipo.

Al razonar sobre los organismos biológicos, es útil distinguir dos tipos:${\displaystyle \mathrm {planta} }$y${\displaystyle \mathrm {animal} }$. Mientras que una función${\displaystyle \mathrm {madre} \colon \mathrm {animal} \to \mathrm {animal} }$Tiene sentido, una función similar${\displaystyle \mathrm {madre} \colon \mathrm {planta} \to \mathrm {planta} }$Por lo general, no. La lógica de múltiples tipos permite tener términos como${\displaystyle \mathrm {madre} (\mathrm {lassie} )}$pero descartar términos como${\displaystyle \mathrm {madre} (\mathrm {mi\_favorito\_oak} )}$como sintácticamente mal formado.

La algebrización de la lógica de múltiples clases se explica en un artículo de Caleiro y Gonçalves, ^{[ 1 ]} que generaliza la lógica algebraica abstracta al caso de múltiples clases, pero que también puede utilizarse como material introductorio.

Mientras que la lógica de múltiples tipos requiere que dos tipos distintos tengan conjuntos de universos disjuntos, la lógica de orden permite un solo tipo.${\displaystyle s_{1}}$ser declarado un subtipo de otro tipo${\displaystyle s_{2}}$, generalmente por escrito${\displaystyle s_{1}\subsetequ s_{2}}$o sintaxis similar. En el ejemplo de biología anterior , es deseable declarar

${\displaystyle {\text{perro}}\subsetequ {\text{carnívoro}}}$,

${\displaystyle {\text{perro}}\subsetequ {\text{mamífero}}}$,

${\displaystyle {\text{carnívoro}}\subseteteq {\text{animal}}}$,

${\displaystyle {\text{mamífero}}\subsetequ {\text{animal}}}$,

${\displaystyle {\text{animal}}\subseteq {\text{organismo}}}$,

${\displaystyle {\text{planta}}\subseteq {\text{organismo}}}$,

y así sucesivamente; véase la imagen.

Dondequiera que un término de algún tipo${\displaystyle s}$se requiere, un término de cualquier subtipo de${\displaystyle s}$En su lugar, se puede proporcionar ( principio de sustitución de Liskov ). Por ejemplo, suponiendo una declaración de función${\displaystyle {\text{madre}}:{\text{animal}}\longrightarrow {\text{animal}}}$y una declaración constante${\displaystyle {\text{lassie}}:{\text{perra}}}$, el término ${\displaystyle {\text{madre}}({\text{lassie}})}$es perfectamente válido y tiene el tipo${\displaystyle {\text{animal}}}$. Para proporcionar la información de que la madre de un perro es a su vez un perro, otra declaración ${\displaystyle {\text{madre}}:{\text{perro}}\longrightarrow {\text{perro}}}$puede emitirse; esto se llama sobrecarga de funciones , similar a la sobrecarga en los lenguajes de programación .

La lógica ordenada puede traducirse a lógica no ordenada, utilizando un predicado unario.${\displaystyle p_{i}(x)}$para cada tipo${\displaystyle s_{i}}$y un axioma${\displaystyle \forall x(p_{i}(x)\rightarrow p_{j}(x))}$para cada declaración de suborden${\displaystyle s_{i}\subseteq s_{j}}$El enfoque inverso tuvo éxito en la demostración automatizada de teoremas : en 1985, Christoph Walther pudo resolver un problema de referencia en aquel entonces traduciéndolo a lógica ordenada, reduciéndolo así en un orden de magnitud, ya que muchos predicados unarios se convirtieron en tipos. ^{[ 2 ]}

Para incorporar lógica de ordenación en un demostrador de teoremas automatizado basado en cláusulas, es necesario un algoritmo de unificación de ordenación correspondiente, que requiere para cualesquiera dos tipos declarados${\displaystyle s_{1},s_{2}}$su intersección${\displaystyle s_{1}\cap s_{2}}$que también debe declararse: si${\displaystyle x_{1}}$y${\displaystyle x_{2}}$son variables de tipo${\displaystyle s_{1}}$y${\displaystyle s_{2}}$, respectivamente, la ecuación${\displaystyle x_{1}{\stackrel {?}{=}}\,x_{2}}$tiene la solución${\displaystyle \{x_{1}=x,\;x_{2}=x\}}$, dónde${\displaystyle x:s_{1}\cap s_{2}}$.

Smolka generalizó la lógica de ordenación para permitir el polimorfismo paramétrico . ^{[ 3 ] [ 4 ]} En su marco, las declaraciones de subordenación se propagan a expresiones de tipo complejas. Como ejemplo de programación, una ordenación paramétrica${\displaystyle {\text{lista}}(X)}$puede ser declarado (con${\displaystyle X}$siendo un parámetro de tipo como en una plantilla de C++ ), y de una declaración de suborden${\displaystyle {\text{int}}\subsetequ {\text{float}}}$la relación${\displaystyle {\text{list}}({\text{int}})\subseteq {\text{list}}({\text{float}})}$Se infiere automáticamente, lo que significa que cada lista de números enteros es también una lista de números de coma flotante.

Schmidt-Schauß generalizó la lógica de ordenación para permitir declaraciones de términos. ^{[ 5 ]} Como ejemplo, suponiendo declaraciones de suborden${\displaystyle {\text{even}}\subsetequ {\text{int}}}$y${\displaystyle {\text{impar}}\subsetequ {\text{int}}}$, una declaración de términos como${\displaystyle \forall i:{\text{int}}.\;(i+i):{\text{even}}}$permite declarar una propiedad de la suma de enteros que no podría expresarse mediante la sobrecarga ordinaria.

• Lógica categórica
• Lógica de primer orden §  Lógica de múltiples tipos

Entre los primeros trabajos sobre lógica de múltiples tipos se incluyen:

• Wang, Hao (1952). "Lógica de teorías de múltiples clases". Journal of Symbolic Logic . 17 (2): 105– 116. doi : 10.2307/2266241 . JSTOR 2266241 . , recopilados en la obra del autor Computation, Logic, Philosophy. A Collection of Essays , Pekín: Science Press; Dordrecht: Kluwer Academic, 1990.
• Gilmore, PC (1958). "Una adición a "Lógica de teorías de muchos tipos"" (PDF) . Compositio Mathematica . 13 : 277–281 .
• A. Oberschelp (1962). "Untersuchungen zur mehrsortigen Quantorenlogik" . Annalen Matemáticas . 145 (4): 297– 333. doi : 10.1007/bf01396685 . S2CID 123363080 . Archivado desde el original el 20 de febrero de 2015 . Consultado el 11 de septiembre de 2013 . 
• F. Jeffry Pelletier (1972). "Cuantificación Sortal y Cuantificación Restringida" (PDF) . Estudios Filosóficos . 23 (6): 400– 404. doi : 10.1007/bf00355532 . S2CID 170303654 . 

• "Lógica de múltiples clases", primer capítulo de las Notas de clase sobre procedimientos de decisión de Calogero G. Zarba.