A Biblioteca Impossível: do Paradoxo de Russell ao Cálculo Lambda Tipado

Imagine uma biblioteca, vasta e silenciosa. O mais importante repositório do conhecimento humano, mesmo hoje, em tempos de internet, nada se compara ao folhear de um livro. No entanto, só é realmente útil se os livros puderem ser consultados. Nessa nossa biblioteca, de sonhos e lembranças boas, os livros estão organizados em prateleiras e estas em seções. Entre tantas, há uma seção especial. Onde estão os livros puros, humildes, os livros que não se referem a si mesmos.

Nossa bibliotecária, de olhos negros, grandes e profundos, escondidos atrás de óculos de vidro grosso que lhe disfarçam a beleza criando um ar de mistério e erudição, precisa de um catálogo. Justamente da seção dos livros que não citam a si mesmos. Este livro, este catálogo, deve ficar na própria seção. Feita a encomenda do catálogo, o autor do catálogo, arde em dúvidas e pergunta-se repetidamente: o catálogo lista a si mesmo?

O catálogo desta seção deve listar todos os livros que não se referem a si mesmos. Se o catálogo se referir a si mesmo, ele não pertence à seção especial e, portanto, não deve listar-se. Mas se o catálogo não se referir a si mesmo, então ele pertence à seção especial e deve listar-se. Isto é uma contradição.

Pobre da literatura, se perde nos meandros da lógica e da matemática. Talvez possamos entender o problema do escritor do catálogo se abandonarmos a literatura e abraçarmos a matemática. Foi o que Russell fez.

Este artigo percorre o caminho que sai daquela prateleira e chega, umas quatro décadas e dois continentes depois, nas linguagens de programação que a atenta leitora usa hoje. O trajeto tem três estações. Primeiro, o paradoxo e a hierarquia de tipos que Russell construiu para desarmá-lo. Depois, o cálculo lambda de Church, uma tentativa independente de fundamentar a matemática que adoeceu exatamente da mesma doença. Por fim, a cura: tipos aplicados a funções, e a descoberta, tardia e espantosa, de que tipos e proposições lógicas são a mesma coisa vista de dois ângulos.

1. O Teorema de Cantor, ou por que sempre há mais prateleiras que livros

Russell percebeu a contradição analisando um teorema de Cantor que diz que nenhum mapeamento $F:X \rightarrow \text{Pow}(X)$ pode ser sobrejetivo. Isto é, $F$ não pode ser tal que cada membro $b$ de $\text{Pow}(X)$ seja igual a $F(a)$ para algum elemento $a$ de $X$. Isso pode ser expresso intuitivamente como o fato de haver mais subconjuntos de $X$ do que elementos de $X$. Pensa em um parágrafo complicado.

Antes de destrinchá-lo, dois objetos precisam de definição. O símbolo $\text{Pow}(X)$ refere-se ao conjunto potência de um conjunto $X$. Esse conjunto potência contém todos os subconjuntos possíveis de $X$, incluindo o próprio conjunto $X$ e o conjunto vazio:

Por exemplo, se $X = {1, 2}$, então $\text{Pow}(X) = {\emptyset, {1}, {2}, {1, 2}}$. Repare no tamanho: $X$ tem dois elementos, $\text{Pow}(X)$ tem quatro. Em geral, um conjunto finito com $n$ elementos gera um conjunto potência com $2^n$ elementos, porque cada elemento entra ou não entra em cada subconjunto, duas escolhas independentes repetidas $n$ vezes. Para conjuntos finitos, portanto, o teorema de Cantor é aritmética de escola: $2^n > n$ para todo $n \geq 0$. A graça está em provar o mesmo quando $n$ é infinito, onde a intuição de tamanho não serve para nada e a aritmética menos ainda.

O segundo objeto é a sobrejeção. Talvez você consiga fechar o conceito se lembrar que os termos função sobrejetiva e função sobrejetora referem-se à mesma coisa. Uma função é chamada de sobrejetiva quando cada elemento do codomínio é a imagem de pelo menos um elemento do domínio. Formalmente, para $f: A \rightarrow B$, se para todo $b \in B$ existe algum $a \in A$ tal que $f(a) = b$, então a função é sobrejetiva.

Vamos ao concreto. Dados o domínio $A = {1, 2, 3}$ e o codomínio $B = {4, 5}$, defina $f: A \rightarrow B$ por $f(1) = 4$, $f(2) = 5$ e $f(3) = 4$. Cada elemento de $B$ é atingido: o $4$ pelos elementos $1$ e $3$, o $5$ pelo elemento $2$. A função $f$ é sobrejetiva. Agora, para garantir que veremos tudo em contraste, mantenha $A = {1, 2, 3}$, mas tome $B = {4, 5, 6}$ e defina $g(1) = 4$, $g(2) = 4$ e $g(3) = 5$. O elemento $6$ de $B$ ficou órfão, sem nenhuma origem em $A$, e por isso $g$ não é sobrejetiva. A sobrejeção, em suma, é a promessa de que nada no destino fica de fora.

Com as duas definições na mão, a prova do teorema de Cantor cabe em três linhas. Suponha, buscando a contradição, que exista uma $F: X \rightarrow \text{Pow}(X)$ sobrejetiva. Considere o subconjunto

que reúne exatamente os elementos que não pertencem ao conjunto ao qual são mapeados. Como $A \subseteq X$, temos $A \in \text{Pow}(X)$ e, pela sobrejetividade suposta, deve existir algum $a \in X$ com $A = F(a)$. Pergunte então se $a \in A$. Pela definição de $A$, $a \in A$ se e somente se $a \notin F(a)$; mas $F(a)$ é o próprio $A$, logo $a \in A \iff a \notin A$. Contradição. Não existe $F$ sobrejetiva, e o conjunto potência é sempre estritamente maior que o conjunto.

Três linhas de álgebra escondem uma imagem muito simples, e a Figura 1 a revela. Com $X = {a, b, c, d}$, cada linha da tabela é o conjunto $F(x)$ e cada coluna pergunta se um elemento pertence a ele. O conjunto $A$ é construído invertendo, uma a uma, as células da diagonal; por construção, ele discorda de $F(x)$ exatamente na coluna $x$, e por isso não pode coincidir com nenhuma linha.

Figura 1: O conjunto $A$ discorda de $F(x)$ exatamente na coluna $x$ e por isso difere de todas as quatro linhas. Aqui $A = {d}$, que não é $F(a)$, nem $F(b)$, nem $F(c)$, nem $F(d)$.

O método usado aqui chama-se diagonalização, e a atenta leitora que quiser a história completa da técnica, incluindo o fato incômodo de que Cantor não a inventou para provar a não enumerabilidade dos reais e sequer foi o primeiro a usá-la, encontra a tradução dos artigos originais em Em Busca da Diagonalização de Cantor. Para o que nos interessa agora, basta o esqueleto: suponha um mapeamento de $X$ em $Y$, construa em $Y$ um elemento que difere de $F(x)$ precisamente no ponto $x$, para todo $x$, e observe que esse elemento não pode ter origem. O conjunto $A$ acima é esse elemento: ele discorda de $F(a)$ quanto à pertinência de $a$, seja qual for $a$. Duas notas técnicas, que não custam nada e evitam mal-entendidos. A prova não usa a lei do terceiro excluído, portanto vale também na matemática intuicionista. E a técnica já aparecia, antes de Cantor, no trabalho de du Bois-Reymond, que a usava para construir funções reais crescendo mais rápido que qualquer função de uma sequência dada.

2. Do catálogo ao conjunto

Russell fez a pergunta óbvia e devastadora: o que acontece se aplicarmos o teorema de Cantor ao caso em que $X$ é a classe de todas as classes? Se tal classe existe, então cada uma de suas subclasses é também uma classe, ou seja, um de seus elementos. O mapeamento $F$ seria a identidade, trivialmente sobrejetivo. E o teorema acabou de provar que isso é impossível.

Traduzindo o subconjunto diagonal $A$ para esse caso particular, $F(x) = x$ e o conjunto crítico vira a classe das classes que não pertencem a si mesmas:

Então, pergunte-se: $R$ pertence a si mesmo? Substituindo $w$ por $R$ na definição:

A afirmação é contraditória: diz que $R$ pertence a si mesmo se e somente se $R$ não pertence a si mesmo. É o catálogo, com outra roupa. A biblioteca é o universo das classes, os livros são os elementos, a seção especial é $R$ e a pergunta do pobre autor do catálogo é a pergunta sobre $R \in R$. A metáfora não é ilustração decorativa do argumento; é o argumento, escrito com substantivos em vez de símbolos. Cantor, ao que tudo indica, já suspeitava que a classe de todos os conjuntos não podia ser tratada como um conjunto, mas foi Russell quem transformou a suspeita em contradição explícita, publicada e impossível de ignorar.

3. A carta que derrubou um sistema

Em junho de 1902, Russell escreveu a Gottlob Frege contando o problema. A carta, junto com a resposta de Frege, está reproduzida em van Heijenoort (1967) e é leitura obrigatória para quem gosta de ver um matemático receber a notícia de que trinta anos de trabalho acabaram de rachar. Frege respondeu com uma dignidade quase dolorosa, e o segundo volume dos Grundgesetze der Arithmetik, já no prelo, ganhou um apêndice reconhecendo a falha.

É importante perceber que a formulação de Russell não se aplica diretamente ao sistema de Frege. Como o próprio Frege observou na resposta, a expressão um predicado é predicado de si mesmo não é exata no sistema dele. Frege distinguia predicados, ou conceitos, de objetos: um predicado de primeira ordem se aplica a um objeto e não pode receber outro predicado como argumento. Nesse arranjo, escrever $w \notin w$ é simplesmente agramatical, e o paradoxo, na forma ingênua, nem chega a ser enunciável.

O que permite reconstruí-lo é a noção de extensão de um predicado $P$, escrita $\varepsilon P$. A extensão é o objeto que reúne tudo aquilo de que $P$ é verdadeiro, e, sendo objeto, pode ser argumento de predicados. É a ponte entre os dois andares. O Axioma V governa essa ponte:

Em português: duas extensões são idênticas exatamente quando os predicados correspondentes são materialmente equivalentes, isto é, verdadeiros dos mesmos objetos. Parece inofensivo. Parece, aliás, quase uma definição. É a viga que Russell derrubou.

Basta definir o predicado

que se lê: $x$ é a extensão de algum predicado $P$ do qual $x$ não é caso. Aplicando $R$ à sua própria extensão e usando o Axioma V para identificar quando duas extensões coincidem, obtém-se

e a contradição reaparece, agora dentro do sistema de Frege. Note que, para definir $R$, foi necessária uma quantificação existencial sobre predicados, $\exists P$, na qual $R$ é ele próprio um dos predicados quantificados. Esse tipo de definição, que caracteriza um objeto por referência a uma totalidade que o inclui, chama-se impredicativa, e é a raiz do problema. Vale registrar que fragmentos predicativos do sistema de Frege, obtidos justamente proibindo esse movimento, são consistentes, como mostraram Heck (1996) e, com refinamentos, Ferreira e Wehmeier (2002). O sistema não estava podre; estava aberto num ponto específico.

Fica claro, desta história, que uma ideia de tipos já existia no trabalho de Frege: objetos, predicados de objetos, predicados de predicados, e assim por diante, cada andar recusando-se a receber inquilinos do próprio andar. Russell (1959) chamaria essa estratificação de hierarquia extensional e reconheceria que a necessidade dela era consequência direta do paradoxo. O que faltava, e que Russell forneceu, era transformar a distinção informal em regra sintática, obrigatória e sem exceções.

4. Prateleiras: a teoria dos tipos

Russell discutiu o paradoxo no Apêndice B, The Doctrine of Types, dos Principles of Mathematics, de 1903, e desenvolveu a solução ao longo da década seguinte, culminando nos Principia Mathematica escritos com Whitehead entre 1910 e 1913. A ideia central é simples de enunciar e trabalhosa de executar: separar os objetos em níveis, como prateleiras distintas em uma biblioteca, e permitir que um objeto de um nível se refira apenas a objetos de níveis inferiores.

Formalmente, atribui-se um tipo a cada objeto. Indivíduos têm tipo $0$. Conjuntos de indivíduos têm tipo $1$. Conjuntos de conjuntos de indivíduos têm tipo $2$, e assim por diante. A relação $x \in y$ só é uma fórmula bem formada quando o tipo de $y$ é exatamente o tipo de $x$ mais um. Sob essa regra, a expressão $w \notin w$ exigiria que o tipo de $w$ fosse simultaneamente $n$ e $n+1$, o que nenhum número natural faz. A classe $R$ não é falsa nem verdadeira: ela não pode nem ser escrita. E o paradoxo não é resolvido, é impedido de nascer, que é uma forma bem mais definitiva de resolver problemas.

À luz da nossa linda metáfora, os livros são objetos de um tipo inferior e o catálogo é um objeto de um tipo superior. A questão de se o catálogo se cita ou não perde o sentido, do mesmo modo que perguntar a cor de um número. Um catálogo, sendo de tipo superior, não pode conter ou referir-se a um objeto do próprio tipo, e portanto não pode conter a si mesmo. A hierarquia impede a formação do paradoxo restringindo as relações que podem existir entre os objetos. A bibliotecária, é claro, terá que escrever um catálogo dos catálogos, e depois um catálogo dos catálogos dos catálogos, mas cada um deles morará numa prateleira mais alta e nenhum deles vai enlouquecer o autor. A Figura 2 desenha essas prateleiras e, ao lado, o que a regra torna inexprimível.

Figura 2: Escrever $w \in w$ exigiria que o mesmo $w$ tivesse tipo $n$, como elemento, e tipo $n+1$, como o conjunto que o contém. A hierarquia não responde à pergunta do catálogo; ela torna a pergunta inexprimível.

Russell foi além, e foi longe demais. Preocupado também com paradoxos semânticos, como o do mentiroso, ele estratificou não apenas os objetos mas também as fórmulas, criando a teoria ramificada de tipos, na qual uma propriedade definida por quantificação sobre propriedades de nível $n$ tem, obrigatoriamente, nível $n+1$. O remédio funcionou e quase matou o paciente: a análise matemática comum, que define o supremo de um conjunto quantificando sobre cotas superiores, tornou-se indefinível. Para recuperá-la, Russell e Whitehead introduziram o axioma da redutibilidade, que postula, para toda propriedade de nível alto, uma propriedade equivalente de nível mínimo. Como o axioma desfaz precisamente aquilo que a ramificação impunha, ele foi recebido com o entusiasmo que se dedica a um curativo feito com a própria ferida. A teoria simples de tipos, que abandona a ramificação e mantém só a hierarquia de objetos, acabou prevalecendo, e é dela que descende tudo que veremos a partir da Seção 8.

A contradição é clara. A solução é lógica. A biblioteca é silenciosa novamente, mas a questão permanece. A matemática é simples, a realidade complexa. Uma contradição levou a uma nova compreensão. E a biblioteca permanece lá, intacta, mas mudada. Agora os livros têm tipos diferentes.

Só não consegui incluir a bibliotecária de olhos negros e profundos. Ninguém é perfeito!

5. Outro caminho para a mesma montanha

Enquanto Russell e Whitehead empilhavam prateleiras em Cambridge, Alonzo Church, em Princeton, atacava o mesmo problema por um ângulo diferente. Em vez de tomar o conjunto como noção primitiva e depois disciplinar a pertinência, Church tomou a função como noção primitiva e tentou construir a lógica inteira em cima dela. O resultado, publicado em 1932 e 1933 sob o título A Set of Postulates for the Foundation of Logic, é o cálculo lambda.

A escolha não é arbitrária. Na matemática usual, uma função é um conjunto de pares ordenados, o que a torna cidadã de segunda classe: para falar de funções é preciso primeiro falar de conjuntos. Church inverteu a hierarquia. No cálculo lambda não há números, não há conjuntos, não há booleanos, não há pares. Há funções, aplicadas a funções, retornando funções. Tudo o mais é codificação, como veremos na Seção 6, e a leitora que achar isso um exagero ascético está em boa companhia, porque era exatamente esse o ponto.

5.1 A sintaxe, que cabe em três linhas

O conjunto $\Lambda$ dos termos lambda é definido indutivamente sobre um conjunto infinito e enumerável $V$ de variáveis. Um termo é uma de três coisas:

1. Variável: se $x \in V$, então $x \in \Lambda$.
2. Abstração: se $x \in V$ e $M \in \Lambda$, então $(\lambda x . M) \in \Lambda$. Lê-se “a função que, dado $x$, devolve $M$”.
3. Aplicação: se $M \in \Lambda$ e $N \in \Lambda$, então $(M\ N) \in \Lambda$. Lê-se “a função $M$ aplicada ao argumento $N$”.

É toda a gramática. Em notação compacta, $M ::= x \mid \lambda x . M \mid M\ M$. A abstração é a única construtora de funções e a aplicação é a única forma de usá-las. Duas convenções poupam parênteses e serão usadas o tempo todo: a aplicação associa à esquerda, de modo que $M\ N\ P$ significa $((M\ N)\ P)$; e o corpo de uma abstração se estende o máximo possível para a direita, de modo que $\lambda x . M\ N$ significa $\lambda x . (M\ N)$ e não $(\lambda x . M)\ N$. A diferença entre essas duas leituras é a diferença entre um programa e outro, e trocar uma pela outra é o erro mais barato e mais frequente de quem está começando.

A função identidade é $\mathbf{I} = \lambda x . x$. A função que ignora o segundo argumento e devolve o primeiro é $\mathbf{K} = \lambda x . \lambda y . x$. O distribuidor, $\mathbf{S} = \lambda x . \lambda y . \lambda z . x\ z\ (y\ z)$, aplica $x$ e $y$ ao mesmo argumento $z$ e depois combina os resultados. Guarde $\mathbf{K}$, em particular: ele voltará na Seção 10 disfarçado de axioma da lógica proposicional.

5.2 Variáveis livres e ligadas

Em $\lambda x . x\ y$, o $x$ está ligado pelo lambda que o precede, ao passo que $y$ não está ligado a nada e depende do ambiente externo para significar alguma coisa. Variáveis nessa segunda situação chamam-se livres. A distinção é a mesma que existe entre o $i$ de um somatório $\sum_{i=1}^{n} a_i$, que é interno, e o $n$, que vem de fora.

O conjunto $FV(M)$ das variáveis livres de $M$ define-se por recursão sobre a estrutura do termo:

A terceira cláusula é onde a ação acontece: a abstração remove $x$ do conjunto, porque o lambda captura todas as ocorrências livres de $x$ em $M$. Assim, $FV(\lambda x . x\ y) = {y}$, e $FV(\lambda x . \lambda y . x\ y) = \emptyset$. Termos sem variáveis livres chamam-se fechados, ou combinadores, e são os únicos que fazem sentido isoladamente. Os três termos da subseção anterior são combinadores.

5.3 Alfa-conversão, ou o nome não importa

O nome de uma variável ligada é decoração. As funções $\lambda x . x$ e $\lambda z . z$ são a mesma função, escrita com tintas diferentes, e o cálculo trata termos que diferem apenas por renomeação de variáveis ligadas como idênticos. Essa relação chama-se alfa-conversão, escreve-se $\lambda x . M =_\alpha \lambda y . M[x := y]$, e vale desde que $y$ não ocorra livre em $M$.

A ressalva final não é burocracia. Renomear $x$ para $y$ em $\lambda x . \lambda y . x$ produziria $\lambda y . \lambda y . y$, um termo em que o argumento externo foi engolido pelo interno, e que devolve o segundo argumento em vez do primeiro. A operação teria mudado a função, que é exatamente o que a alfa-conversão promete não fazer. A restrição existe para manter a promessa.

5.4 Substituição, e a captura que ela precisa evitar

A substituição $M[x := N]$ troca toda ocorrência livre de $x$ em $M$ por $N$. Sua definição, também por recursão na estrutura, tem cinco casos:

O quarto caso registra que um lambda interno com a mesma variável bloqueia a substituição: aquelas ocorrências de $x$ já pertencem a outro dono. O quinto caso carrega a condição crítica, $y \notin FV(N)$. Sem ela, substituir $x$ por $y$ em $\lambda y . x$ produziria $\lambda y . y$, transformando a função constante que devolve $y$ na função identidade. O $y$ que era livre, e portanto significava algo do mundo externo, foi capturado pelo lambda e passou a significar o argumento local. Quando a condição falha, a saída é aplicar alfa-conversão ao termo interno antes de substituir, renomeando $y$ para uma variável fresca. É um cuidado sintático chato de implementar e responsável por uma fração generosa dos bugs de quem escreve interpretadores pela primeira vez.

5.5 Beta-redução: a única regra de computação

Tudo o que o cálculo lambda faz, ele faz com uma regra:

Um termo da forma $(\lambda x . M)\ N$ chama-se redex, contração de reducible expression. Reduzir é substituir. Computar é reduzir até não haver mais redexes, momento em que o termo está na forma normal. Um exemplo mínimo, com a identidade aplicada a si mesma:

Outro, com o $\mathbf{K}$, mostrando que ele de fato descarta o segundo argumento:

Um termo pode conter vários redexes, e a ordem de redução é uma escolha. O Teorema de Church-Rosser garante que a escolha não altera o destino: se $M$ reduz a $P$ e também a $Q$, então existe um $T$ ao qual tanto $P$ quanto $Q$ reduzem. Essa propriedade, chamada confluência, implica que a forma normal, quando existe, é única a menos de alfa-conversão. A ressalva “quando existe” é o assunto da Seção 7, e é onde o paradoxo volta a bater na porta.

Há ainda uma segunda regra, mais fraca e opcional, a eta-conversão: $\lambda x . (M\ x) \longrightarrow_\eta M$, desde que $x \notin FV(M)$. Ela formaliza a ideia de que uma função que apenas repassa seu argumento para $M$ é indistinguível de $M$. Em Haskell, é a diferença entre f x = g x e f = g, e a comunidade dá a isso o nome de point-free style, ou, nos dias ruins, pointless style.

6. Tudo é função

O cálculo lambda não tem números. Church precisava deles, e resolveu o problema da única maneira disponível: definindo o número $n$ como a operação de fazer alguma coisa $n$ vezes. Os numerais de Church são

O numeral $\overline{n}$ recebe uma função $f$ e um ponto de partida $x$, e aplica $f$ ao resultado $n$ vezes. O número deixa de ser uma quantidade e passa a ser um padrão de iteração. Não é uma representação de número; para o cálculo, é o número.

Com essa escolha, a aritmética sai por dedução. O sucessor precisa aplicar $f$ uma vez a mais que $n$ já aplica:

A soma precisa aplicar $f$ um total de $m + n$ vezes, o que se consegue usando o resultado de $n$ como ponto de partida de $m$:

A multiplicação é mais bonita. Se $n\ f$ é “aplicar $f$ $n$ vezes”, então aplicar essa operação $m$ vezes aplica $f$ um total de $m \cdot n$ vezes, e nem é preciso mencionar $x$:

A exponenciação chega ao limite do minimalismo, dispensando também o $f$:

Vale conferir na unha, para que a atenta leitora não precise acreditar em mim. Calculemos $\mathbf{plus}\ \overline{2}\ \overline{1}$, com $\overline{2} = \lambda f . \lambda x . f (f x)$ e $\overline{1} = \lambda f . \lambda x . f x$:

Os booleanos seguem a mesma filosofia: um valor de verdade é aquilo que ele faz, e o que ele faz é escolher entre duas alternativas.

O $\mathbf{true}$ é o nosso velho $\mathbf{K}$, reaparecendo com outro chapéu. Como cada booleano já é a própria decisão, o condicional é trivial, $\mathbf{if} = \lambda p . \lambda a . \lambda b . p\ a\ b$, e a conjunção sai de graça: $\mathbf{and} = \lambda p . \lambda q . p\ q\ p$, que devolve $q$ se $p$ for verdadeiro e devolve $p$, isto é, falso, caso contrário.

Pares ordenados usam o mesmo truque, guardando os componentes dentro de uma função que espera saber qual deles entregar:

De fato, $\mathbf{fst}\ (\mathbf{pair}\ M\ N) \longrightarrow_\beta (\mathbf{pair}\ M\ N)\ \mathbf{true} \longrightarrow_\beta \mathbf{true}\ M\ N \longrightarrow_\beta M$. Repare que a estrutura de dados e a operação de acesso são a mesma coisa: o par é a função que sabe entregar seus componentes, e o seletor apenas informa qual. Não há memória, não há campos, não há ponteiros. Há aplicação.

Em Haskell, que descende diretamente dessa linhagem, a codificação inteira se escreve quase sem tradução:

{-# LANGUAGE RankNTypes #-}

-- Um numeral de Church: para qualquer tipo a, dado f :: a -> a e x :: a,
-- aplica f a x exatamente n vezes.
type Church = forall a. (a -> a) -> a -> a

zero :: Church
zero  = \_ x -> x

suc :: Church -> Church
suc n = \f x -> f (n f x)

plus, mult :: Church -> Church -> Church
plus m n = \f x -> m f (n f x)
mult m n = \f -> m (n f)

-- Traduz de volta para Int, aplicando (+1) a partir de 0.
toInt :: Church -> Int
toInt n = n (+1) 0

-- toInt (plus (suc (suc zero)) (suc zero)) == 3

A anotação forall a não é enfeite. Ela diz que o numeral funciona para qualquer tipo, e é justamente o tipo de polimorfismo que o cálculo lambda simplesmente tipado da Seção 8 não possui, o que nos obrigará a uma conversa desagradável sobre o preço dos tipos.

7. O catálogo que lê a si mesmo

Church construiu o cálculo lambda para servir de fundamento à lógica, e não como uma teoria da computação. A ambição era a mesma de Frege e de Russell: uma base única a partir da qual toda a matemática pudesse ser derivada. E o desfecho também foi o mesmo, com um atraso de três anos e a mesma causa mortis.

Volte à sintaxe da Seção 5.1 e procure onde está proibido aplicar um termo a si mesmo. Não está. A gramática permite $M\ N$ para quaisquer $M$ e $N$, inclusive quando $M$ e $N$ são o mesmo termo. Considere então o termo de autoaplicação $\omega = \lambda x . x\ x$, que recebe algo e o aplica a si próprio, e o aplique a si mesmo:

Reduzindo, com $M = \lambda x . x\ x$, a substituição devolve $x\ x$ com $x$ trocado por $M$, ou seja, $M\ M$, que é o próprio $\Omega$:

O termo se reduz a si mesmo, indefinidamente. Não há forma normal. É o primeiro programa que nunca termina da história da computação, escrito em 1932, e cabe em vinte caracteres. A confluência de Church-Rosser continua valendo, veja bem; ela promete que se houver um destino, ele é único, e não promete que haja destino.

Um passo adiante, e a não terminação vira ferramenta. O combinador de ponto fixo de Curry,

satisfaz $\mathbf{Y}\ F \longrightarrow_\beta F\ (\mathbf{Y}\ F)$ para qualquer $F$, o que se verifica em dois passos de beta-redução. Isto é, $\mathbf{Y}\ F$ é um ponto fixo de $F$: aplicar $F$ a ele devolve ele mesmo, envolto em mais uma camada de $F$. Como o cálculo lambda não tem nomes e portanto não pode definir uma função que se chame recursivamente, $\mathbf{Y}$ é o que fornece a recursão. Um fatorial escrito como funcional que recebe “a si mesmo” como primeiro argumento vira, sob $\mathbf{Y}$, o fatorial de verdade. Foi por esse caminho que o cálculo lambda alcançou toda função computável, resultado que Turing (1937) fechou ao provar a equivalência entre lambda-definibilidade e computabilidade por máquinas.

E foi por esse mesmo caminho que o sistema desabou. Em 1935, Kleene e Rosser provaram que a lógica original de Church era inconsistente: nela, toda fórmula é demonstrável, o que é a forma técnica de dizer que ela não distingue verdade de mentira. Curry (1942) destilou o argumento até deixá-lo com o tamanho de um cartão-postal, e a versão dele merece ser vista de perto, porque é o catálogo da bibliotecária de novo.

Suponha uma lógica com implicação, na qual seja possível construir, para uma proposição qualquer $X$, uma proposição $A$ que afirme “se eu for verdadeira, então $X$”. Formalmente, $A \iff (A \rightarrow X)$. O ponto fixo $\mathbf{Y}$ é exatamente a máquina que fabrica esse $A$. Agora observe:

1. Suponha $A$. Da equivalência, $A \rightarrow X$. Com a suposição $A$ e modus ponens, obtém-se $X$.
2. O passo anterior partiu de $A$ e chegou a $X$, portanto está provado $A \rightarrow X$, agora sem suposições.
3. Da equivalência, na outra direção, $A \rightarrow X$ dá $A$. Está provado $A$.
4. De $A \rightarrow X$ e $A$, modus ponens dá $X$.

E $X$ era uma proposição qualquer. A lógica prova tudo, inclusive $0 = 1$, e serve tanto para fundamentar a matemática quanto um mapa que marca todos os lugares com um X.

A leitora atenta já reconheceu o padrão. A doença é a mesma que matou o sistema de Frege: a autorreferência irrestrita. Onde Russell escreveu $w \in w$, Church escreveu $x\ x$. Onde o catálogo tentava listar a si mesmo, o termo tenta aplicar-se a si mesmo. Só mudou o vocabulário. A biblioteca ganhou prateleiras infinitas e nenhuma regra sobre quem pode citar quem, e o resultado é sempre um bibliotecário desempregado.

O que sobrou dos escombros foi o cálculo lambda puro, sem as pretensões lógicas: um sistema de reescrita de termos, Turing-completo, magnificamente simples e completamente inútil como fundamento da matemática. Church, que era um homem prático dentro dos padrões da lógica dos anos 1930, tirou a lição óbvia. Se prateleiras salvaram os conjuntos, prateleiras salvariam as funções.

8. Prateleiras para funções

Em 1940, Church publicou A Formulation of the Simple Theory of Types, aplicando ao seu próprio cálculo a solução que Russell dera à teoria dos conjuntos. O resultado é o cálculo lambda simplesmente tipado, que a literatura abrevia como STLC, de simply typed lambda calculus.

A gramática dos tipos tem duas cláusulas, e é a hierarquia de Russell escrita para funções:

na qual $o$ é um tipo base qualquer, digamos o dos indivíduos, e $\tau_1 \rightarrow \tau_2$ é o tipo das funções que recebem um argumento de tipo $\tau_1$ e devolvem um resultado de tipo $\tau_2$. A seta associa à direita, de modo que $\sigma \rightarrow \tau \rightarrow \rho$ significa $\sigma \rightarrow (\tau \rightarrow \rho)$, convenção que combina com a aplicação associando à esquerda para que os argumentos sejam consumidos um a um, na ordem.

Termos passam a carregar tipos, e a atribuição depende do que se assume sobre as variáveis livres. Um contexto $\Gamma$ é uma lista de suposições da forma $x : \sigma$, e o julgamento $\Gamma \vdash M : \tau$ lê-se “sob as suposições $\Gamma$, o termo $M$ tem tipo $\tau$”. Três regras bastam:

A regra (var) consulta o contexto. A regra (abs) diz que, se assumindo $x$ de tipo $\sigma$ o corpo tem tipo $\tau$, então a função inteira leva $\sigma$ em $\tau$. A regra (app) é a única que faz exigências: só é permitido aplicar $M$ a $N$ quando o tipo do argumento que $M$ espera coincide, exatamente, com o tipo que $N$ tem. É a prateleira. É o “$y$ tem que ser do tipo de $x$ mais um” de Russell, reescrito para funções.

Vejamos o que a regra (app) faz com o vilão da seção anterior. Tentemos tipar $\lambda x . x\ x$. Pela regra (abs), é preciso assumir $x : \sigma$ para algum $\sigma$ e tipar o corpo $x\ x$. Pela regra (app), o $x$ da posição de função precisa ter tipo $\alpha \rightarrow \beta$, e o $x$ da posição de argumento precisa ter tipo $\alpha$. Mas os dois $x$ são a mesma variável, com o mesmo tipo $\sigma$ vindo do mesmo contexto. Logo,

Um tipo teria de ser igual a um tipo estritamente maior que ele. Que isso é impossível se prova contando seta por seta: defina $\vert o\vert = 0$ e $\vert \sigma \rightarrow \tau \vert = \vert \sigma \vert + \vert \tau \vert + 1$, o número de setas do tipo. Então $\vert \sigma \rightarrow \beta \vert = \vert \sigma \vert + \vert \beta \vert + 1 \geq \vert \sigma \vert + 1 > \vert \sigma \vert$, e dois tipos com números diferentes de setas não são o mesmo tipo. A equação não tem solução, $\lambda x . x\ x$ não é tipável, $\Omega$ não existe, $\mathbf{Y}$ não existe, e o paradoxo de Curry não pode nem ser enunciado. A biblioteca é silenciosa de novo, agora do lado das funções.

A Figura 3 põe as duas exigências lado a lado, para deixar visível o que a álgebra faz em silêncio: elas nascem de posições sintáticas diferentes, mas recaem sobre a mesma variável, à qual a regra (abs) já atribuiu um único tipo.

Figura 3: A posição de função exige $x : \alpha \rightarrow \beta$; a posição de argumento exige $x : \alpha$. Como as duas ocorrências herdam o mesmo $\sigma$ do ligador, sobra $\sigma = \sigma \rightarrow \beta$, e contar setas mostra que nenhum tipo satisfaz isso.

Isso não é um acidente feliz que vale para $\Omega$ em particular. O Teorema da Normalização Forte, provado por Tait em 1967 com uma técnica de candidatos de redutibilidade que se tornou padrão na área, garante que todo termo bem tipado do STLC atinge sua forma normal, por qualquer sequência de reduções, em um número finito de passos. Não existe divergência. Não existe laço infinito. Todo programa termina.

9. O preço da felicidade

A leitora com alguma experiência em computação deve ter estremecido no parágrafo anterior, e com razão. Uma linguagem em que todo programa termina não pode ser Turing-completa, porque o problema da parada nela é trivial: a resposta é sempre “sim”. Se decidir a parada fosse possível para uma linguagem que expressa todas as funções computáveis, a diagonalização de Turing, prima em primeiro grau da diagonalização de Cantor da Seção 1, produziria uma contradição. Como não há contradição, o que se perdeu foi expressividade.

E perdeu-se muita. Sobre os numerais de Church, com um tipo fixo $N = (o \rightarrow o) \rightarrow o \rightarrow o$, as funções definíveis no STLC são exatamente os polinômios estendidos: polinômios com coeficientes naturais, acrescidos da função de teste de zero. Esse é o resultado de Schwichtenberg (1975), e ele é bem menos generoso do que parece. A soma está lá, a multiplicação está lá, a exponenciação com expoente fixo está lá. Já a subtração truncada, a divisão, o fatorial, a função de Ackermann e, mais relevante para quem programa, qualquer função definida por recursão sobre uma lista de tamanho arbitrário: nada disso é definível. O sistema que Church construiu para salvar a lógica sacrificou a computação inteira no processo.

Há uma segunda má notícia, menos citada e mais engraçada. Embora todo termo tipado normalize, o número de passos até a forma normal não é limitado por nenhuma torre de exponenciais de altura fixa. Statman (1979) provou que decidir se dois termos do STLC são beta-equivalentes é um problema não elementar. Portanto, “sempre termina” e “termina a tempo de você ver” são afirmações diferentes, e o STLC satisfaz apenas a primeira. Um engenheiro de compiladores dirá que isso é irrelevante na prática, e ele estará certo, o que não torna o fato menos divertido.

Nada disso condenou a ideia; apenas mostrou que a hierarquia simples era rígida demais, exatamente como a teoria ramificada de Russell fora rígida demais. As três saídas encontradas desde então são todas formas de afrouxar a prateleira sem derrubá-la, e todas estão vivas em linguagens de produção. A primeira é admitir recursão como construção primitiva, com um operador $\mathbf{fix}$ de tipo $(\tau \rightarrow \tau) \rightarrow \tau$: recupera-se a Turing-completude e devolve-se a possibilidade de não terminar, troca que qualquer linguagem de programação faz sem hesitar. A segunda é o polimorfismo paramétrico, que permite quantificar sobre tipos, $\forall \alpha . \tau$, e que Girard (1972) e Reynolds (1974) descobriram de forma independente sob os nomes de Sistema F e cálculo lambda polimórfico; é o forall a que apareceu no código Haskell da Seção 6, e nele os numerais de Church voltam a somar, multiplicar e iterar sobre qualquer coisa. A terceira é a restrição de Hindley-Milner (Hindley, 1969; Milner, 1978), um fragmento do Sistema F escolhido com precisão cirúrgica para que a inferência de tipos seja decidível e eficiente na prática, e que é a razão pela qual em ML, OCaml e Haskell a leitora pode escrever funções inteiras sem anotar tipo nenhum e mesmo assim receber erro de compilação quando soma um inteiro com uma string.

10. Tipos são proposições

Falta a parte espantosa. Compare o tipo do combinador $\mathbf{K} = \lambda x . \lambda y . x$ com o primeiro axioma da lógica proposicional intuicionista. Derivando pelas regras da Seção 8, com $x : A$ e $y : B$, o corpo tem tipo $A$, a abstração interna tem tipo $B \rightarrow A$ e o termo inteiro tem tipo

O axioma diz: se $A$, então, se $B$, então $A$. São a mesma fórmula. Não são parecidas, não são análogas: são a mesma sequência de símbolos, com a seta lida como “função de” em um caso e como “implica” no outro. O mesmo vale para o distribuidor $\mathbf{S}$, cujo tipo $(A \rightarrow B \rightarrow C) \rightarrow (A \rightarrow B) \rightarrow A \rightarrow C$ é o segundo axioma do mesmo sistema.

A coincidência não é coincidência. Ela foi notada por Curry em 1934, ao observar que os tipos dos combinadores eram exatamente os axiomas da lógica implicacional, e formulada em toda a sua extensão por Howard em 1969, num manuscrito que circulou por onze anos antes de ser publicado em 1980. O que a correspondência de Curry-Howard afirma é uma tradução completa, nos dois sentidos, entre dois mundos que ninguém esperava que se falassem:

Escrever um programa é construir uma prova; executá-lo é simplificar a prova. A última linha é a mais surpreendente das doze: a normalização de Gentzen, que elimina os passos redundantes de uma demonstração, e a beta-redução, que executa um programa, são o mesmo procedimento sob dois nomes, inventados em continentes diferentes por pessoas que não sabiam uma da outra.

A correspondência também explica, retroativamente, por que o STLC precisa terminar. Um sistema lógico é consistente quando não prova $\bot$; do lado computacional, isso significa que o tipo vazio não tem nenhum termo. Se existisse um termo divergente de tipo arbitrário, como $\mathbf{Y}$ teria dado a qualquer tipo pela sua assinatura $(\tau \rightarrow \tau) \rightarrow \tau$, ele habitaria também o tipo vazio, e a lógica correspondente provaria o falso. A normalização forte da Seção 8 é a consistência da lógica, traduzida. E o paradoxo de Curry da Seção 7 era a mesma inconsistência, também traduzida: $\mathbf{Y}$ tipado é a prova de que tudo é demonstrável. Três resultados, uma única ideia, e a suspeita crescente de que a lógica e a computação são a mesma disciplina estudada por dois departamentos que não se falam.

11. Onde as prateleiras moram hoje

Nada disso é arqueologia. A correspondência de Curry-Howard é a razão de existir de duas famílias inteiras de ferramentas que a leitora provavelmente já usou ou vai usar.

Do lado das linguagens de programação, o sistema de tipos deixou de ser um mecanismo de detecção de erros de digitação e passou a ser um mecanismo de especificação. Quando o tipo de uma função é uma proposição, escolher o tipo certo é escrever o teorema que a implementação precisa provar. Em Haskell, uma assinatura suficientemente restrita chega a determinar a implementação:

{-# LANGUAGE EmptyCase #-}
import Data.Void (Void)

-- Só existe uma função total com este tipo: a identidade.
-- O tipo é a proposição "A implica A", e sua única prova é trivial.
ident :: a -> a
ident x = x

-- Só existe uma função total com este tipo: fst.
-- O tipo é o combinador K, isto é, o axioma A -> (B -> A).
konst :: a -> b -> a
konst x _ = x

-- Curry-Howard aplicado: o tipo Void não tem habitantes,
-- portanto é a proposição falsa. Uma função a -> Void é a prova
-- de que 'a' também não tem habitantes.
absurdo :: Void -> a
absurdo v = case v of {}

A parametricidade que torna isso possível, isto é, o fato de que uma função polimórfica não pode inspecionar o tipo com que foi instanciada e portanto tem opções severamente limitadas, é consequência direta do Sistema F, e Wadler (1989) mostrou como extrair teoremas gratuitos a partir de tipos apenas, num artigo cujo título, Theorems for Free!, resume a piada melhor do que eu conseguiria.

Do lado dos assistentes de prova, a estrada segue até o fim. Se tipos são proposições e programas são provas, então um verificador de tipos é um verificador de provas, e basta enriquecer os tipos o bastante para que eles expressem matemática de verdade. Foi o que fez Martin-Löf (1984) com a teoria de tipos intuicionista, na qual tipos podem depender de valores: o tipo Vetor n das listas de exatamente $n$ elementos é uma proposição sobre $n$, e uma função que concatena Vetor m com Vetor n devolvendo Vetor (m + n) é a demonstração de um lema aritmético que o compilador confere. Coquand e Huet (1988) levaram a ideia ao Cálculo de Construções, que é o motor do Coq, hoje Rocq, no qual foram verificados o Teorema das Quatro Cores e um compilador C inteiro, o CompCert. Agda e Lean seguem a mesma linhagem, e a biblioteca matemática do Lean já formalizou uma fração respeitável do currículo de graduação.

A hierarquia continua lá, aliás, com os mesmos problemas de sempre. Assistentes de prova modernos precisam de universos, $\mathsf{Type}_0 : \mathsf{Type}_1 : \mathsf{Type}_2 : \cdots$, porque supor $\mathsf{Type} : \mathsf{Type}$ reintroduz uma contradição, o paradoxo de Girard, que é o paradoxo de Russell vestido para a ocasião. Cento e vinte anos depois do Apêndice B, o catálogo continua sem poder listar a si mesmo.

Vale olhar o percurso inteiro de uma vez. A Figura 4 alinha os oito marcos que este artigo atravessou, e o que salta aos olhos é o compasso binário: a autorreferência derruba um sistema, a hierarquia o reergue, e a plateia troca de continente sem trocar de argumento.

Figura 4: Os pares 1902-1903 e 1935-1940 têm a mesma forma: alguém mostra que o sistema se refere a si mesmo, e alguém responde separando os objetos em níveis. O intervalo entre a doença e a cura foi de um ano na teoria dos conjuntos e de cinco no cálculo lambda.

12. A biblioteca, de novo

Volte à prateleira. A bibliotecária de olhos negros, grandes e profundos, escondidos atrás de óculos de vidro grosso, recebeu, afinal, o seu catálogo. Não é o catálogo que ela encomendou, porque aquele não existe e nunca existiu. É um catálogo de tipo superior, morando numa prateleira acima dos livros que lista, incapaz de mencionar a si mesmo e, por isso mesmo, capaz de existir.

O autor, que ardia em dúvidas, aprendeu a lição mais dura da lógica do século XX: nem toda pergunta bem formulada em português é uma pergunta. Algumas são apenas ruído com boa gramática. A teoria dos tipos não responde “o catálogo lista a si mesmo?”, ela mostra que a frase, apesar do sujeito, do verbo e do complemento, não diz nada. E ao fazer isso, ela devolve a biblioteca ao silêncio, com uma regra a mais e um paradoxo a menos.

O que ninguém previa, em 1903, é que a mesma regra reapareceria quarenta anos depois disciplinando funções em vez de conjuntos, e outros trinta depois disso rodando dentro de compiladores. Russell queria salvar a aritmética. Church queria salvar a lógica. O que ambos construíram, sem saber, foi a infraestrutura conceitual de todo sistema de tipos que a leitora já viu, do int do C ao Vetor n do Agda. Toda vez que um compilador recusa o seu código, ele está repetindo, com outras palavras e menos elegância, que o catálogo não pode listar a si mesmo.

A simplicidade, no fim, era mesmo o segredo da felicidade. Só não era a simplicidade de deixar tudo se referir a tudo, que é a simplicidade preguiçosa das coisas que não funcionam. Era a simplicidade de admitir que existem andares, e que ninguém sobe pela escada que está carregando.

Referências

CANTOR, G. Über eine elementare Frage der Mannigfaltigkeitslehre. Jahresbericht der Deutschen Mathematiker-Vereinigung, v. 1, p. 75–78, 1891.

CHURCH, A. A Set of Postulates for the Foundation of Logic. Annals of Mathematics, v. 33, n. 2, p. 346–366, 1932.

CHURCH, A. A Set of Postulates for the Foundation of Logic (Second Paper). Annals of Mathematics, v. 34, n. 4, p. 839–864, 1933.

CHURCH, A. A Formulation of the Simple Theory of Types. The Journal of Symbolic Logic, v. 5, n. 2, p. 56–68, 1940.

COQUAND, T.; HUET, G. The Calculus of Constructions. Information and Computation, v. 76, n. 2–3, p. 95–120, 1988.

CURRY, H. B. Functionality in Combinatory Logic. Proceedings of the National Academy of Sciences, v. 20, n. 11, p. 584–590, 1934.

CURRY, H. B. The Inconsistency of Certain Formal Logics. The Journal of Symbolic Logic, v. 7, n. 3, p. 115–117, 1942.

FERREIRA, F.; WEHMEIER, K. F. On the Consistency of the $\Delta^1_1$-CA Fragment of Frege’s Grundgesetze. Journal of Philosophical Logic, v. 31, n. 4, p. 301–311, 2002.

FREGE, G. Grundgesetze der Arithmetik, v. II. Jena: Hermann Pohle, 1903.

GIRARD, J.-Y. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Tese de doutorado, Université Paris VII, 1972.

HECK, R. G. The Consistency of Predicative Fragments of Frege’s Grundgesetze der Arithmetik. History and Philosophy of Logic, v. 17, n. 4, p. 209–220, 1996.

HINDLEY, R. The Principal Type-Scheme of an Object in Combinatory Logic. Transactions of the American Mathematical Society, v. 146, p. 29–60, 1969.

HOWARD, W. A. The Formulae-as-Types Notion of Construction. In: SELDIN, J. P.; HINDLEY, J. R. (eds.). To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. London: Academic Press, 1980. p. 479–490.

KLEENE, S. C.; ROSSER, J. B. The Inconsistency of Certain Formal Logics. Annals of Mathematics, v. 36, n. 3, p. 630–636, 1935.

MARTIN-LÖF, P. Intuitionistic Type Theory. Napoli: Bibliopolis, 1984.

MILNER, R. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences, v. 17, n. 3, p. 348–375, 1978.

QUINE, W. V. O. Mathematical Logic. Cambridge: Harvard University Press, 1940.

REYNOLDS, J. C. Towards a Theory of Type Structure. In: Programming Symposium, Lecture Notes in Computer Science, v. 19. Berlin: Springer, 1974. p. 408–425.

RUSSELL, B. The Principles of Mathematics. Cambridge: Cambridge University Press, 1903. Disponível em: https://people.umass.edu/klement/pom/.

RUSSELL, B. My Philosophical Development. London: George Allen and Unwin, 1959.

SCHWICHTENBERG, H. Definierbare Funktionen im $\lambda$-Kalkül mit Typen. Archiv für mathematische Logik und Grundlagenforschung, v. 17, n. 3–4, p. 113–114, 1975.

STATMAN, R. The Typed $\lambda$-Calculus Is Not Elementary Recursive. Theoretical Computer Science, v. 9, n. 1, p. 73–81, 1979.

TAIT, W. W. Intensional Interpretations of Functionals of Finite Type I. The Journal of Symbolic Logic, v. 32, n. 2, p. 198–212, 1967.

TURING, A. M. Computability and $\lambda$-Definability. The Journal of Symbolic Logic, v. 2, n. 4, p. 153–163, 1937.

VAN HEIJENOORT, J. (ed.). From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931. Cambridge: Harvard University Press, 1967.

WADLER, P. Theorems for Free!. In: Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture. New York: ACM, 1989. p. 347–359.

WHITEHEAD, A. N.; RUSSELL, B. Principia Mathematica. 3 v. Cambridge: Cambridge University Press, 1910–1913.