Notas sobre lógica e a correspondência Curry-Howard

Todos fatos conhecidos, mas que eu estou entendendo um pouco melhor somente há pouco tempo. Senão vejamos: na lógica de primeira ordem a sintaxe é estratificada em duas camadas: termos e fórmulas. Os termos representam os valores sobre alguma estrutura sobre a qual se fala; as fórmulas tratam de propriedades sobre os termos. Pode-se interpretar a lógica intuicionista de primeira ordem no λ-cálculo tipado de primeira ordem: os termos são os valores (não necessariamente em sua forma normal, ou seja, não necessariamente avaliados) e as fórmulas são tipos, que são propriedades dos termos. Então um tipo é como se fosse um predicado sobre um termo, o que faz todo sentido. Isso é mais ou menos a essência da correspondência Curry-Howard.

Mas a coisa fica melhor. Na lógica de primeira ordem só podemos quantificar sobre variáveis, que são parte de termos. Na lógica de segunda ordem pode-se quantificar sobre predicados também. O correspondente no λ-cálculo é o Sistema F de Girard, que é um λ-calculo tipado de segunda ordem, no qual pode-se estabelecer abstrações de tipos e aplicações de tipos. Girard utilizou o Sistema F para estudar o PA₂, a aritmética de Peano de segunda ordem, e provar sua consistência. De forma similar temos a lógica de ordem superior e o Sistema F de ordem superior (Fω). A quantificação no caso da lógica é sobre predicados e predicados de predicados e por aí vai; no sistema Fω os tipos de ordem superior são como funções de tipos em tipos (no Sistema F de segunda ordem existem apenas funções de tipos em termos), em qualquer nível. Mais uma vez, Girard utilizou esse sistema para estudar o PA_ω, a aritmética de Peano de ordem superior, e provar sua consistência pela propriedade de normalização dos termos no sistema Fω.

Já na lógica de ordem superior a formulação mais utilizada é devida a Alonzo Church e, como esperado, envolve o λ-cálculo. É utilizado um cálculo tipado pois o cálculo sem tipos é inconsistente, graças ao paradoxo de Russell. Lógica de ordem superior também é utilizada como base para provadores de teoremas, por exemplo o sistema Isabelle/HOL. Um outro provador de teoremas famoso, o Coq, utiliza um cálculo baseado em tipos dependentes, que estabelecem uma conexão entre termos e tipos. Mas isso fica para outra hora.

Mônadas são valores

Lendo uma série de artigos sobre mônadas (os de Philip Wadler, especificamente). Atualmente estou no "Imperative Functional Programming" de Peyton-Jones e Wadler. Esse trecho bateu com o que eu já tinha redescoberto recentemente:

Notice the distinction between an action and its performance. Think of an action as a "script", which is performed by executing it. Actions themselves are first-class citizens.

As ações a que ele se refere, obviamente, são valores monádicos.

Outra idéia importante é que mônadas não necessariamente precisam exprimir ação. No geral, são um mecanismo para capturar diferentes estratégias de computação. Por exemplo, listas podem ser encaradas como mônadas que refletem uma estratégia de computação baseada no uso de vários valores por expressão, ao invés de apenas um. Isso também pode ser interpretado como não-determinismo. Aliás, existe um exemplo bem interessante de não-determinismo expresso por mônadas em "Comprehending Monads", de Wadler. Mas tratar uma lista como mônada, sem efeitos colaterais impuros, é bem diferente da mônada IO, que delimita partes do código que são imperativos. E isso se reflete no fato que é possível sair de uma mônada de lista, mas nunca de uma imperativa como IO ou State.