La lógica no conmutativa es una extensión de la lógica lineal que combina las conectivas conmutativas de la lógica lineal con las conectivas multiplicativas no conmutativas del cálculo de Lambek . Su cálculo secuencial se basa en la estructura de las variedades de orden (una familia de órdenes cíclicos que pueden verse como una especie de estructura ), y el criterio de corrección para sus redes de prueba se da en términos de permutaciones parciales . También tiene una semántica denotacional en la que las fórmulas son interpretadas por módulos sobre algunas álgebras de Hopf específicas .
No conmutatividad en lógica
Por extensión, el término lógica no conmutativa también es utilizado por varios autores para referirse a una familia de lógicas subestructurales en las que la regla del intercambio es inadmisible . El resto de este artículo está dedicado a una presentación de esta aceptación del término.
La lógica no conmutativa más antigua es el cálculo de Lambek , que dio lugar a la clase de lógicas conocidas como gramáticas categóricas . Desde la publicación de Jean-Yves Girard 's lógica lineal Ha habido varias nuevas lógicas no conmutativos propuestas, a saber, la lógica lineal cíclico de David Yetter, la lógica pomset de Cristiano retore, y las lógicas no conmutativos BV y NEL .
La lógica no conmutativa a veces se denomina lógica ordenada, ya que es posible con la mayoría de las lógicas no conmutativas propuestas imponer un orden total o parcial a las fórmulas en las secuencias. Sin embargo, esto no es completamente general, ya que algunas lógicas no conmutativas no admiten tal orden, como la lógica lineal cíclica de Yetter. Aunque la mayoría de las lógicas no conmutativas no permiten el debilitamiento o la contracción junto con la no conmutatividad, esta restricción no es necesaria.
El cálculo de Lambek
Joachim Lambek propuso la primera lógica no conmutativa en su artículo de 1958 Matemáticas de la estructura de la oración para modelar las posibilidades combinatorias de la sintaxis de los lenguajes naturales. [1] Su cálculo se ha convertido así en uno de los formalismos fundamentales de la lingüística computacional .
Lógica lineal cíclica
David N. Yetter propuso una regla estructural más débil en lugar de la regla de intercambio de la lógica lineal, produciendo una lógica lineal cíclica. [2] Las secuencias de lógica lineal cíclica forman un anillo, por lo que son invariantes bajo rotación, donde las reglas multipremise unen sus anillos en las fórmulas descritas en las reglas. El cálculo admite tres modalidades estructurales, una modalidad auto-dual que permite el intercambio, pero sigue siendo lineal, y las exponenciales habituales (? Y!) De la lógica lineal, que permite utilizar reglas estructurales no lineales junto con el intercambio.
Lógica de Pomset
La lógica de Pomset fue propuesta por Christian Retoré en un formalismo semántico con dos operadores secuenciales duales que existen junto con el producto tensorial habitual y los operadores par de la lógica lineal, la primera lógica propuesta para tener operadores conmutativos y no conmutativos. [3] Se proporcionó un cálculo secuencial para la lógica, pero carecía de un teorema de eliminación de cortes ; en cambio, el sentido del cálculo se estableció a través de una semántica denotacional.
BV y NEL
Alessio Guglielmi propuso una variación del cálculo de Retoré, BV, en el que las dos operaciones no conmutativas se colapsan en un operador único, auto-dual, y propuso un cálculo de prueba novedoso, el cálculo de estructuras para acomodar el cálculo. La principal novedad del cálculo de estructuras fue su uso generalizado de la inferencia profunda , que se argumentó es necesaria para los cálculos que combinan operadores conmutativos y no conmutativos; esta explicación coincide con la dificultad de diseñar sistemas secuenciales para la lógica de pomset que tienen eliminación de cortes.
Lutz Strassburger ideó un sistema relacionado, NEL, también en el cálculo de estructuras en el que la lógica lineal con la regla de mezcla aparece como un subsistema.
Structads
Los Structads son un acercamiento a la semántica de la lógica que se basan en generalizar la noción de secuenciante a lo largo de las líneas de la especie combinatoria de Joyal , permitiendo el tratamiento de lógicas más drásticamente no estándar que las descritas anteriormente, donde, por ejemplo, el ',' del el cálculo secuencial no es asociativo.
Ver también
Referencias
- ^ Lambek, Joachim (1958). "Las matemáticas de la estructura de la oración". The American Mathematical Monthly . 65 (3): 154-170. CiteSeerX 10.1.1.538.885 . doi : 10.2307 / 2310058 . ISSN 0002-9890 . JSTOR 2310058 .
- ^ Yetter, David N. (1990). "Quantales y (no conmutativa) lógica lineal" (PDF) . El diario de la lógica simbólica . 55 (1): 41–64. doi : 10.2307 / 2274953 . hdl : 10338.dmlcz / 140417 . ISSN 0022-4812 . JSTOR 2274953 .
- ^ Retoré, Christian (2 de abril de 1997). "Lógica de Pomset: una extensión no conmutativa de la lógica lineal clásica". En Philippe de Groote; J. Roger Hindley (eds.). Cálculos y aplicaciones Lambda mecanografiados . Apuntes de conferencias en informática. 1210 . Springer Berlín Heidelberg. págs. 300–318. CiteSeerX 10.1.1.47.2354 . doi : 10.1007 / 3-540-62688-3_43 . ISBN 978-3-540-62688-6.
enlaces externos
- Lógica no conmutativa I: el fragmento multiplicativo de V. Michele Abrusci y Paul Ruet, Annals of Pure and Applied Logic 101 (1), 2000.
- Aspectos lógicos de la lingüística computacional (PS) por Patrick Blackburn, Marc Dymetman, Alain Lecomte, Aarne Ranta, Christian Retoré y Eric Villemonte de la Clergerie.
- Artículos sobre lógica lineal conmutativa / no conmutativa en el cálculo de estructuras : una página de inicio de investigación en la que están disponibles los artículos que proponen BV y NEL.