Lógica combinatoria

La lógica combinatoria es una rama de la lógica matemática que se ocupa de conceptos y métodos fundamentales (es decir, que no necesitan explicación y no se analizan) de sistemas lógicos formales o cálculos [1] [2] . En matemáticas discretas , la lógica combinatoria está estrechamente relacionada con el cálculo lambda , ya que describe procesos computacionales.

Desde sus inicios, la lógica combinatoria y el cálculo lambda se han clasificado como lógicas no clásicas . El punto es que la lógica combinatoria surgió en la década de 1920 y el cálculo lambda en la década de 1940 como una rama de las metamatemáticas con un propósito bastante bien definido: dar fundamentos a las matemáticas. Esto significa que habiendo construido la teoría matemática "aplicada" requerida, la teoría del sujeto, que refleja los procesos o fenómenos en el entorno externo real, uno puede usar la metateoría "pura" como un caparazón para aclarar las posibilidades y propiedades de la teoría del sujeto. . También pronto resultó que ambos sistemas podrían considerarse lenguajes de programación (ver también programación combinatoria ).

Hasta la fecha, ambos lenguajes no solo se han convertido en la base de toda la investigación en el campo de la informática , sino que también se utilizan ampliamente en la teoría de la programación. El crecimiento del poder de cómputo de las computadoras ha llevado a la automatización de una parte significativa del conocimiento teórico (lógico y matemático), y la lógica combinatoria, junto con el cálculo lambda, se reconoce como la base para el razonamiento en términos de objetos. .

Conceptos básicos

En lógica combinatoria, los conceptos básicos son una función de un lugar y la operación de aplicar una función a un argumento ( aplicación ). El concepto de función se toma como primario en relación con el concepto de conjunto . Una función se entiende de forma general y puede operar con objetos del mismo nivel que argumentos y valores. Dado que el argumento de una función puede ser una función, una función de muchos lugares se puede reducir a una función de un lugar [3] .

Un combinador es una función que satisface la igualdad $F$

fg_{1}g_{2}\puntos g_{n}=(\puntos ((fg_{1})g_{2})\puntos g_{n})=X,

donde ( ) son algunas funciones, X es un objeto construido a partir de funciones usando la aplicación [3] . $g_1, g_2, \puntos, g_n$ $n\geqslant 1$

Cualquier combinador se puede expresar en términos de dos combinadores S y K definidos por las siguientes igualdades [3] :

Sxyz=xz(yz)

( distribuidor ),

kxy=x

( delantero ).

Dada una expresión lambda, siempre puede crear una expresión aplicativa . Esto requiere solo dos combinadores: S y K . En forma de expresiones lambda: , . Es decir, la lógica combinatoria definida sobre estos objetos combinatorios puede considerarse como un modelo del cálculo lambda [4] . $K = \lambda x.\lambda yx$ $S=\lambda f.\lambda g.\lambda x.fx(gx)$

Otros ejemplos de combinadores (en la notación del cálculo lambda) son la función identidad , fácilmente expresada en términos de S y K [4] :

I = \lambda xx = SKK

y el combinador de punto fijo o combinador Y :

Y=\lambda h.((\lambda xh(xx))(\lambda xh(xx))).

Historia

En 1920, M. Sheinfinkel [6] introdujo originalmente los combinadores como entidades matemáticas especiales [5 ] . Unos años más tarde, fueron redescubiertos de forma independiente por H. Curry [7] , quien desde entonces ha realizado importantes avances en lógica combinatoria (aunque otros investigadores, como Rosser, también han contribuido a este trabajo en varias ocasiones). Casi al mismo tiempo, Church , Rosser y Kleene comenzaron el desarrollo de la conversión λ.

Desde la década de 1970, los combinadores se han utilizado de tres formas principales: primero, para construir sistemas lógicos basados en una notación abstracta de una operación; en segundo lugar, en la teoría de las pruebas como base para el registro de funciones constructivas de varios tipos; en tercer lugar, en la construcción y análisis de algunos lenguajes de programación en informática .

Lógica combinatoria categórica

En el marco de la lógica combinatoria, se construye una versión especial de la teoría de la computación, denominada máquina abstracta categórica . Para esto, se introduce en consideración un fragmento especial de lógica combinatoria: la lógica combinatoria categórica [8] . Está representado por un conjunto de combinadores, cada uno de los cuales tiene un valor independiente como instrucción de un sistema de programación. Por lo tanto, una aplicación más útil está integrada en la lógica combinatoria: un sistema de programación basado en una categoría cerrada cartesiana (fc). Esto le permite repensar la conexión entre el operador y el estilo de programación aplicativa una vez más en un nuevo nivel.

Lógica combinatoria ilativa

Utilizando el concepto de objetos como entidades matemáticas abstractas con ciertas propiedades de sustitución, es posible construir sistemas de razonamiento lógico . El más famoso de estos sistemas se basa en combinadores.

La lógica basada en combinadores, o lógica combinatoria ilativa , se construye a partir de la teoría de los combinadores o cálculo lambda, ampliada por constantes adicionales -constantes extra- junto con los correspondientes axiomas y reglas de inferencia, que proporcionan un medio de inferencia deductiva.

Véase también

Notas

↑ Edición. F. V. Konstantinova. Lógica combinatoria // Enciclopedia filosófica: en 5 volúmenes . - M. : Enciclopedia soviética, 1960-1970.
↑ Kondakov, 1971 .
↑ 1 2 3 MES, 1988 , pág. 275-276.
↑ 1 2 Field, Harrison, 1993 , pág. 291-293.
↑ Cardone F., Hindley J. R. History of lambda calculus and combinators ( Archivado el 10 de octubre de 2011 en Wayback Machine ), en Handbook of the History of Logic, Volume 5, DM Gabbay y J. Woods (eds) (Ámsterdam: Elsevier Co ., a aparecer).
↑ Schonfinkel M. Uber die Baustein der mathematischen Logik. - Matemáticas. Annalen, vol. 92, 1924, pág. 305-316.
↑ Curry H. B. Grundlagen der kombinatorischen Logik. Diario Americano de Matemáticas, 52:509-536, 789-834, 1930.
↑ Curien P.-L. Lógica combinatoria categórica. — LNCS, 194, 1985, pág. 139-151.

Literatura

Wolfenhagen VE Lógica combinatoria en programación. Cálculos con objetos en ejemplos y problemas. - 2ª ed. - M. : AO Center YurInfoR, 2003. - 204 p. — ISBN 5-89158-101-9 .
Kondakov N. I. Diccionario lógico / Gorsky D. P. - M . : Nauka, 1971. - 656 p.
Field A., Harrison P. Programación Funcional = Programación Funcional. — M .: Mir, 1993. — 637 p. — ISBN 5-03-001870-0 .
Diccionario enciclopédico matemático / Yu. V. Prokhorov. - M. : Enciclopedia soviética, 1988. - 847 p.
A. S. Kuzichev. Lógica combinatoria // Nueva Enciclopedia Filosófica : en 4 volúmenes / anterior. ed. científica consejo de V. S. Stepin . — 2ª ed., corregida. y adicional - M. : Pensamiento , 2010. - 2816 p.

diccionarios y enciclopedias	gran ruso
En catálogos bibliográficos	BNF : 119473722 TIERRA : 4164750-6 J9U : 987007543265905171 LCCN : sh85028814 SUDOC : 027430677