Lógica de múltiples ordenaciones

La lógica de ordenación múltiple puede reflejar formalmente nuestra intención de no manejar el universo como una colección homogénea de objetos, sino de dividirlo de una manera similar a los tipos en la programación de tipos . Tanto las " partes del discurso " funcionales como las asertivas en el lenguaje de la lógica reflejan esta división de tipos del universo, incluso en el nivel de sintaxis: la sustitución y el paso de argumentos se pueden hacer solo en consecuencia, respetando los "tipos".

Existen diversas formas de formalizar la intención mencionada anteriormente; una lógica polisémica es cualquier paquete de información que la cumpla. En la mayoría de los casos se dan las siguientes:

• un conjunto de clases, 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 organismos biológicos, es útil distinguir dos tipos: y . Si bien una función tiene sentido, una función similar normalmente no lo tiene. La lógica de múltiples tipos permite tener términos como , pero descartar términos como por estar mal formados sintácticamente. ${\displaystyle \mathrm {planta}}$${\displaystyle \mathrm {animal}}$${\displaystyle \mathrm {madre} \colon \mathrm {animal} \a \mathrm {animal} }$${\displaystyle \mathrm {madre} \colon \mathrm {planta} \to \mathrm {planta} }$${\displaystyle \mathrm {madre} (\mathrm {muchacha} )}$${\displaystyle \mathrm {madre} (\mathrm {mi\_roble\_favorito} )}$

La algebrización de la lógica multiordenada se explica en un artículo de Caleiro y Gonçalves, ^[1] que generaliza la lógica algebraica abstracta al caso multiordenado, pero también puede usarse como material introductorio.

Mientras que la lógica de orden múltiple requiere que dos tipos distintos tengan conjuntos de universos disjuntos, la lógica de ordenación permite que un tipo se declare como un subtipo de otro tipo , generalmente mediante la escritura o una sintaxis similar. En el ejemplo de biología anterior, es deseable declarar $estilo de visualización s_{1}$$estilo de visualización s_{2}$${\displaystyle s_{1}\subseteq s_{2}}$

${\displaystyle {\text{dog}}\subseteq {\text{carnivore}}}$,

${\displaystyle {\text{dog}}\subseteq {\text{mammal}}}$,

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

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

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

${\displaystyle {\text{plant}}\subseteq {\text{organism}}}$,

y así sucesivamente; cf. imagen.

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

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

Para incorporar lógica ordenada en un demostrador de teoremas automatizado basado en cláusulas, es necesario un algoritmo de unificación ordenado correspondiente, que requiere que para dos tipos declarados, también se declare su intersección : si y son variables de tipo y , respectivamente, la ecuación tiene la solución , donde . ${\displaystyle s_{1},s_{2}}$${\displaystyle s_{1}\cap s_{2}}$${\displaystyle x_{1}}$${\displaystyle x_{2}}$${\displaystyle s_{1}}$${\displaystyle s_{2}}$${\displaystyle x_{1}{\stackrel {?}{=}}\,x_{2}}$${\displaystyle \{x_{1}=x,\;x_{2}=x\}}$${\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 subclasificación se propagan a expresiones de tipo complejas. Como ejemplo de programación, se puede declarar una clasificación paramétrica ( siendo un parámetro de tipo como en una plantilla de C++ ), y a partir de una declaración de subclasificación se infiere automáticamente la relación , lo que significa que cada lista de números enteros es también una lista de números flotantes. ${\displaystyle {\text{list}}(X)}$${\displaystyle X}$${\displaystyle {\text{int}}\subseteq {\text{float}}}$${\displaystyle {\text{list}}({\text{int}})\subseteq {\text{list}}({\text{float}})}$

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

• Lógica categórica
• Lógica de primer orden#Lógica de múltiples ordenaciones

Los primeros artículos sobre lógica multiclasificada incluyen:

• Wang, Hao (1952). "Lógica de teorías de múltiples tipos". Revista de lógica simbólica . 17 (2): 105–116. doi :10.2307/2266241. JSTOR  2266241., recopilado en Computación, lógica y filosofía. Una colección de ensayos , Beijing: Science Press; Dordrecht: Kluwer Academic, 1990.
• Gilmore, PC (1958). "Una adición a 'Lógica de teorías de múltiples 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 de Sortal y cuantificación restringida" (PDF) . Estudios filosóficos . 23 (6): 400–404. doi :10.1007/bf00355532. S2CID  170303654.

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