La lógica combinatoria es la lógica última y como tal puede ser un modelo simplificado del cómputo, usado en la teoría de computabilidad (el estudio de qué puede ser computado) y la teoría de la prueba (el estudio de qué se puede probar matemáticamente.)
La teoría, a causa de su simplicidad, captura las características esenciales de la naturaleza del cómputo. La lógica combinatoria (LC) es el fundamento del cálculo lambda, al eliminar el último tipo de variable de éste: la variable lambda. En LC las expresiones lambda (usadas para permitir la abstracción funcional) son substituidas por un sistema limitado de combinadores, las funciones primitivas que no contienen ninguna variable libre (ni ligada). Es fácil transformar expresiones lambda en expresiones combinatorias, y puesto que la reducción de un combinador es más simple que la reducción lambda, LC se ha utilizado como la base para la puesta en práctica de algunos lenguajes de programación funcionales no-estrictos en software y hardware.
No hay comentarios:
Publicar un comentario