Codificação de Church

Em matemática, a codificação de Church é uma forma de incorporar dados e operadores ao cálculo lambda, a forma mais conhecida dos numerais de Church, uma representação dos números naturais usando a notação lambda. O método é conhecido como Alonzo Church, que foi o primeiro a codificar os dados no cálculo lambda desta forma. Termos que são geralmente considerados primitivos em outras notações (com inteiros, booleanos e pares, por exemplo) são mapeados para funções de ordem superior na codificação de Church. A tese de Church-Turing afirma que qualquer operador computável (e seus operandos) pode ser representado sob a codificação de Church. Muitos estudantes de matemática estão familiarizados com a numeração de Gödel de elementos de um conjunto. A codificação de Church é uma operação equivalente, definida sob lambda-abstrações, o invés de números naurais.