Muchos lógica-ordenada puede reflejar formalmente nuestra intención de no manejar el universo como una homogénea colección de objetos, sino para crear particiones de una manera que es similar a los tipos de programación con tipo . Tanto las " partes del discurso " funcionales y 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 se pueden hacer en consecuencia, respetando los "géneros".
Hay varias formas de formalizar la intención mencionada anteriormente; una lógica de muchos ordenamientos es cualquier paquete de información que la satisfaga. En la mayoría de los casos, se proporciona lo siguiente:
- una serie de clases, S
- una adecuada generalización de la noción de firma para poder manejar la información adicional que acompaña a los géneros.
El dominio del discurso de cualquier estructura de esa firma se fragmenta en subconjuntos disjuntos, uno para cada tipo.
Ejemplo
Al razonar sobre organismos biológicos, es útil distinguir dos tipos: y . Mientras que una función tiene sentido, una función similar por lo general no lo hace. La lógica de muchos ordenamientos permite tener términos como, pero para descartar términos como como sintácticamente mal formado.
Algebraización
La algebraización de la lógica de muchos ordenamientos se explica en un artículo de Caleiro y Gonçalves, [1] que generaliza la lógica algebraica abstracta al caso de muchos ordenadas, pero también se puede utilizar como material introductorio.
Lógica ordenada por orden
Mientras que la lógica de muchos ordenamientos requiere dos tipos distintos para tener conjuntos de universos disjuntos, la lógica de ordenamiento permite un ser declarado un subgrupo de otro tipo , generalmente escribiendo o una sintaxis similar. En el ejemplo de biología anterior , es deseable declarar
- ,
- ,
- ,
- ,
- ,
- ,
y así; cf. imagen.
Dondequiera que un término de algún tipo se requiere, un término de cualquier subgrupo de en su lugar ( principio de sustitución de Liskov ). Por ejemplo, asumiendo una declaración de función, y una declaración constante , el termino es perfectamente válido y tiene el tipo . Para proporcionar la información de que la madre de un perro es un perro a su vez, otra declaraciónpuede emitirse; esto se llama sobrecarga de funciones , similar a la sobrecarga en los lenguajes de programación .
La lógica ordenada por orden se puede traducir a lógica no ordenada, utilizando un predicado unario para cada tipo y un axioma para cada declaración de subgrupo . El enfoque inverso tuvo éxito en la demostración automatizada de teoremas: en 1985, Christoph Walther pudo resolver un problema de referencia traduciéndolo en lógica ordenada, reduciéndolo a un orden de magnitud, ya que muchos predicados unarios se convirtieron en géneros. [2]
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 ordenada por orden correspondiente , que requiere para dos tipos declarados su intersección para ser declarado, también: si y son variables de tipo y , respectivamente, la ecuación tiene la solucion , dónde .
Smolka generalizó la lógica ordenada por orden para permitir el polimorfismo paramétrico . [3] [4] En su marco, las declaraciones de subgrupos se propagan a expresiones de tipos complejos. Como ejemplo de programación, una ordenación paramétrica puede ser declarado (con siendo un parámetro de tipo como en una plantilla de C ++ ), y de una declaración de subgrupo la relación se infiere automáticamente, lo que significa que cada lista de enteros también es una lista de flotantes.
Schmidt-Schauß generalizó la lógica ordenada por orden para permitir declaraciones de términos. [5] Como ejemplo, asumiendo declaraciones de subgrupos 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.
Ver también
Referencias
- ^ Carlos Caleiro, Ricardo Gonçalves (2006). "Sobre la algebraización de lógicas de muchos ordenamientos". Proc. XVIII int. conf. sobre Tendencias recientes en técnicas de desarrollo algebraico (WADT) (PDF) . Saltador. págs. 21–36. ISBN 978-3-540-71997-7.
- ^ Walther, Christoph (1985). "Una solución mecánica de la apisonadora de Schubert por resolución variada" (PDF) . Artif. Intell . 26 (2): 217–224. doi : 10.1016 / 0004-3702 (85) 90029-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. 343 . Saltador. págs. 53–70.
- ^ Smolka, Gert (mayo de 1989), Programación lógica sobre tipos ordenados polimórficamente , Univ. Kaiserslautern, Alemania
- ^ Schmidt-Schauß, Manfred (abril de 1988). Aspectos computacionales de una lógica ordenada por orden con declaraciones a plazo . LNAI. 395 . Saltador.
Los primeros artículos sobre lógica de muchos ordenamientos incluyen:
- Wang, Hao (1952). "Lógica de teorías polifacéticas". Revista de lógica simbólica . 17 (2): 105-116. doi : 10.2307 / 2266241 . JSTOR 2266241 ., recogido en Computación, Lógica, Filosofía del autor . Una colección de ensayos , Beijing: Science Press; Dordrecht: Kluwer Academic, 1990.
- Gilmore, PC (1958). "Una adición a" Lógica de teorías variadas " " (PDF) . Compositio Mathematica . 13 : 277-281.
- A. Oberschelp (1962). "Untersuchungen zur mehrsortigen Quantorenlogik" . Mathematische Annalen . 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 clasificación y cuantificación restringida" (PDF) . Estudios filosóficos . 23 (6): 400–404. doi : 10.1007 / bf00355532 . S2CID 170303654 .
enlaces externos
- "Lógica de muchos ordenamientos" , primer capítulo de las notas de la conferencia sobre procedimientos de decisión de Calogero G. Zarba