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).
Para evaluar el cuadrado para un argumento particular, digamos 3, lo insertamos en la definición en lugar del parámetro formal: El cuadrado de 3 es 3*3 para evaluar la expresión que resulta 3*3, tendríamos que recurrir a nuestro conocimiento de la multiplicación y del número 3.
Según la tesis de Church-Turing, ambos modelos pueden expresar cualquier cómputo posible.
Quizás parezca sorprendente que el cálculo lambda pueda representar cualquier cómputo concebible usando solamente las nociones simples de abstracción funcional y aplicación basado en la substitución textual simple de términos por variables.
La Lógica Combinatoria es un modelo del cómputo equivalente al cálculo lambda, pero sin la abstracción.
El ejemplo más simple de un combinador es I, el combinator identidad, definido por para todos los términos x. otro combinator simple es K, que produce funciones constantes: (K x) es la función que, para cualquier argumento, devuelve x, así que decimos para todos los términos x e y.
Utilizaremos la palabra equivalente para indicar la igualdad extensional, reservando igual para los términos combinatorios idénticos.
Es, quizás, un hecho asombroso que S y K se puedan componer para producir los combinadores que son extensionalmente iguales a cualquier término lambda, y por lo tanto, por la tesis de Church, a cualquier función computable.
La prueba es presentar una transformación, T[ ], que convierte un término arbitrario lambda en un combinador equivalente.
Dos casos especiales, reglas 3 y 4, son triviales: λx.x es claramente equivalente a I, y λx.E es claramente equivalente a (K E) si x no aparece libre en E.
Las primeras dos reglas son también simples: Las variables se convierten en sí mismas, y las aplicaciones permitidas en términos combinatorios, son convertidas los combinadores simplemente convirtiendo el aplicando y el argumento a combinadores.
(E1E2) es una función que toma un argumento, digamos a, y lo substituye en el término lambda (E1 E2) en lugar de x, dando (E1 E2)[a/x].
(E1 E2), es suficiente encontrar un combinador equivalente a (S λx.E1 λx.E2), y evidentemente cumple el objetivo.
Los combinadores generados por la transformación T[ ] pueden ser hechos más pequeños si consideramos la regla de η-reducción: λx.
En Lógica combinatoria T. I, Se ha vuelto a S, K pero se muestra, (vía algoritmos de Markov) que el uso de B y C pueden simplificar muchas reducciones.
Esto parece haberse utilizado mucho después por David Turner, cuyo nombre ha quedado ligado a su uso computacional.
No obstante, una prueba directa es como sigue: Primero, obsérvese que el término no tiene forma normal, porque se reduce a sí mismo en tres pasos, como sigue: y claramente ningún otro orden de reducción puede hacer la expresión más corta.
Por tanto, el hipotético combinador de forma normal N no puede existir.