Lógica variada

Lógica escrita jerárquica

La lógica multiclasificada puede reflejar formalmente nuestra intención de no manejar el universo como una colección homogénea de objetos, sino dividirlo de una manera similar a los tipos en la programación tipográfica . Tanto las " partes del discurso " funcionales como las asertivas en el lenguaje de la lógica reflejan esta partición tipográfica del universo, incluso en el nivel de sintaxis: la sustitución y el paso de argumentos sólo pueden realizarse en consecuencia, respetando los "géneros".

Existen diversas formas de formalizar la intención mencionada anteriormente; una lógica múltiple es cualquier paquete de información que la cumpla. En la mayoría de los casos, se da lo siguiente:

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

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

Ejemplo

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 multiordenada permite tener términos como , pero descartar términos como por estar sintácticamente mal formados. ${\displaystyle \mathrm {plant} }$ ${\displaystyle \mathrm {animal} }$ ${\displaystyle \mathrm {mother} \colon \mathrm {animal} \to \mathrm {animal} }$ ${\displaystyle \mathrm {mother} \colon \mathrm {plant} \to \mathrm {plant} }$ ${\displaystyle \mathrm {mother} (\mathrm {lassie} )}$ ${\displaystyle \mathrm {mother} (\mathrm {my\_favorite\_oak} )}$

Algebraización

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

Lógica ordenada por orden

Ejemplo de jerarquía de clasificación

Mientras que la lógica de orden múltiple requiere dos tipos distintos para tener conjuntos de universos separados, la lógica de orden ordenado permite que un tipo se declare como subtipo de otro tipo , generalmente mediante escritura o sintaxis similar. En el ejemplo de biología anterior, es deseable declarar ${\displaystyle s_{1}}$ ${\displaystyle 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}}}$,

etcétera; cf. imagen.

Siempre que se requiera un término de algún tipo , se puede proporcionar en su lugar un término de cualquier subtipo ( principio de sustitución de Liskov ). Por ejemplo, suponiendo una declaración de función y una declaración constante , el término es perfectamente válido y tiene el tipo . Para suministrar la información de que la madre de un perro es a su vez perro, podrá expedirse 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 se puede traducir a lógica no ordenada, utilizando un predicado unario para cada clasificación y un axioma para cada declaración de subclasificación . El enfoque inverso tuvo éxito en la demostración automatizada de teoremas: en 1985, Christoph Walther pudo resolver un problema entonces de referencia traduciéndolo a lógica ordenada, reduciéndolo así a un orden de magnitud, ya que muchos predicados unarios se convirtieron en géneros. ^[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 la lógica ordenada por orden en un demostrador de teoremas automatizado basado en cláusulas, es necesario un algoritmo de unificación ordenado por orden correspondiente , que requiere que para dos tipos declarados cualesquiera se declare también su intersección : si y son variables de ordenación 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 ordenada para permitir el polimorfismo paramétrico . ^{[3] [4]} En su marco, las declaraciones de subclasificación se propagan a expresiones de tipo complejo. 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, la relación se infiere automáticamente, lo que significa que cada lista de números enteros también es una lista de 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 por orden 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 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}}}$

Ver también

• Portal de filosofía

• Lógica categórica
• Lógica_de_primer-orden#Lógica_muchas-clasificadas

Referencias

1. Carlos Caleiro, Ricardo Gonçalves (2006). "Sobre la algebraización de lógicas variadas". Proc. 18º int. conf. sobre tendencias recientes en técnicas de desarrollo algebraico (WADT) (PDF) . Saltador. págs. 21–36. ISBN 978-3-540-71997-7.
2. Walther, Christoph (1985). "Una solución mecánica de la apisonadora de Schubert mediante resoluciones variadas" (PDF) . Artif. Intel . 26 (2): 217–224. doi :10.1016/0004-3702(85)90029-3.
3. Smolka, Gert (noviembre de 1988). "Programación lógica con tipos ordenados polimórficamente". En t. Taller de Programación Algebraica y Lógica . LNCS. vol. 343. Saltador. págs. 53–70.
4. Smolka, Gert (mayo de 1989), Programación lógica sobre tipos ordenados polimórficamente (tesis doctoral), Universidad de Kaiserslautern-Landau , Alemania
5. Schmidt-Schauß, Manfred (abril de 1988). Aspectos computacionales de una lógica ordenada por orden con declaraciones de términos . LNAI. vol. 395. Saltador.

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

• Wang, Hao (1952). "Lógica de teorías variadas". Revista de Lógica Simbólica . 17 (2): 105-116. doi :10.2307/2266241. JSTOR  2266241., recopilado en Computación, Lógica, Filosofía del autor . Una colección de ensayos , Beijing: Science Press; Dordrecht: Kluwer Académico, 1990.
• Gilmore, ordenador personal (1958). "Una adición a" Lógica de teorías variadas"" (PDF) . Composición Matemática . 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 ordenada y cuantificación restringida" (PDF) . Estudios Filosóficos . 23 (6): 400–404. doi :10.1007/bf00355532. S2CID  170303654.

enlaces externos

• "Lógica variada", el primer capítulo de Apuntes sobre procedimientos de decisión de Calogero G. Zarba