Cálculo lambda simplesmente tipado

O cálculo lambda simplesmente tipado ($\lambda ^{\to }$), ou cálculo lambda com tipagem simples, é um modelo da teoria dos tipos que adiciona o conceito de tipagem ao cálculo lambda. Isso é possível com adição de apenas um elemento (o construtor de tipos: $\to$) para construir tipos de funções. Esse é o exemplo mais simples e canônico de um cálculo lambda com tipagem. O cálculo lambda simplesmente tipado foi introduzido originalmente por Alonzo Church em 1940 como uma tentativa de evitar o uso paradoxal do lambda cálculo não tipado, o qual mostrou várias propriedades interessantes e desejadas.

O termo tipo simples também é utilizado para se referir à extensões do cálculo lambda simplesmente tipado como produtos, coprodutos, números naturais (Sistema T) ou até recursão completa. Em contraste, sistemas que introduzem tipos polimórficos (como o Sistema F) ou tipos dependentes não são considerados simplesmente tipados. O cálculo lambda simplesmente tipado é considerado simples por conta da Codificação de Church de suas estruturas que pode ser feita usando apenas o símbolo $\to$ e variáveis de tipos adequadas, enquanto polimorfismo e dependência não podem.

Sintaxe

Para definir os tipos, começa-se determinando um conjunto de tipos base, $B$. Esses tipos são chamados tipos atômicos ou constantes de tipos. Tendo-os determinado, a sintaxe dos tipos pode ser exemplificada da seguinte forma:

$\tau =\tau \to \tau \mid T\quad \mathrm {onde} \;T\in B$.

Neste artigo serão utilizados $\sigma$ e $\tau$ para representação dos tipos. Informalmente, o tipo de função $\sigma \to \tau$ se refere a um conjunto de funções que, dado uma entrada do tipo $\sigma$, produz uma saída do tipo $\tau$. Por convenção, $\to$ associa à direita, ou seja, $\sigma \to \tau \to \rho$ é lido como $\sigma \to (\tau \to \rho )$.

Os termos constantes também são fixos para os tipos base. Por exemplo, assume-se que o tipo base nat, e as constantes de termo podem ser os números naturais. Na representação original, Church utilizou apenas dois tipos base: $o$ para os tipos de proposições e $\iota$ para os tipos de indivíduos. O tipo $o$ não contém constantes de termo, enquanto que $\iota$ contém uma constante de termo. Frequentemente apenas o cálculo com um tipo base é considerado (normalmente $o$).

A sintaxe do cálculo lambda simplesmente tipado é essencialmente a mesma do cálculo lambda. A sintaxe dos termos utilizados neste artigo é mostrada a seguir:

$e=x\mid \lambda x\!:\!\tau .e\mid e\,e\mid c$

onde $c$ é uma constante de termo.

Isto é, variável de referência, abstrações, aplicação e constante. A variável de referência $x$ é ligada se estiver dentro de uma abstração ligando $x$. Um termo é fechado se não existir variáveis não ligadas.

Compare com a sintaxe do cálculo lambda não tipado:

$e=x\mid \lambda x.e\mid e\,e$

É possível verificar que no cálculo lambda tipado toda função (abstração) deve especificar o tipo de seus argumentos.

Regras de tipagem

Para definir o conjunto de lambda termos bem tipados para um dado tipo é necessário definir a relação de tipagem entre termos e tipos. Primeiro será introduzido os contextos de tipagem $\Gamma ,\Delta ,\dots$, que são conjuntos de suposições de tipagem. Uma suposição de tipagem tem forma $x:\sigma$, que significa $x$ tem tipo $\sigma$.

A relação de tipagem $\Gamma \vdash e:\sigma$ indica que $e$ é um termo do tipo $\sigma$ no contexto $\Gamma$. Isto é o mesmo que dizer que "$e$ é bem-tipado (em $\sigma$)". Instâncias de uma relação de tipagem são chamadas sentenças de tipagem. A validade de uma sentença de tipagem é mostrada provando-se a derivação de tipagem, construída usando as seguintes regras de tipagem (em que as premissas acima da linha permitem derivar a conclusão abaixo da linha):

${x:\sigma \in \Gamma } \over {\Gamma \vdash x:\sigma }$ (1)      ${c{\textrm {~uma~constante~do~tipo~}}T} \over {\Gamma \vdash c:T}$ (2)

${\Gamma ,x:\sigma \vdash e:\tau } \over {\Gamma \vdash \lambda x:\sigma .~e:\sigma \to \tau }$ (3)      ${\Gamma \vdash e_{1}:\sigma \to \tau \quad \Gamma \vdash e_{2}:\sigma } \over {\Gamma \vdash e_{1}~e_{2}:\tau }$ (4)

Em outras palavras,

1. Se $x$ tem tipo $\sigma$ no contexto, sabe-se que $x$ tem tipo $\sigma$.
2. Constantes de termos tem o tipo base apropriado.
3. Se, em um determinado contexto com $x$ tendo tipo $\sigma$, $e$ tem tipo $\tau$, então, no mesmo contexto sem $x$, $\lambda x:\sigma .~e$ tem tipo $\sigma \to \tau$.
4. Se, em um determinado contexto, $e_{1}$ tem tipo $\sigma \to \tau$, e $e_{2}$ tem tipo $\sigma$, então $e_{1}~e_{2}$ tem tipo $\tau$.

Exemplos de termos fechados, isto é termos tipáveis em um contexto vazio:

• Para todo tipo $\tau$, um termo $\lambda x:\tau .x:\tau \to \tau$ (o combinador I/função identidade),
• Para tipos $\sigma ,\tau$, um termo $\lambda x:\sigma .\lambda y:\tau .x:\sigma \to \tau \to \sigma$ (o combinador K), e
• Para tipos $\tau ,\tau ',\tau ''$, um termo $\lambda x:\tau \to \tau '\to \tau ''.\lambda y:\tau \to \tau '.\lambda z:\tau .xz(yz):(\tau \to \tau '\to \tau '')\to (\tau \to \tau ')\to \tau \to \tau ''$ (o combinador S).

Essas são as representações no lambda cálculo tipado dos combinadores básicos da lógica combinatória.

Para cada tipo $\tau$ é atribuído uma ordem, um número $o(\tau )$. Para os tipos base, $o(T)=0$; para tipos de função, $o(\sigma \to \tau )={\mbox{max}}(o(\sigma )+1,o(\tau ))$. Isto é, a ordem de um tipo mede a profundidade da seta aninhada mais à esquerda. Logo:

$o(\iota \to \iota \to \iota )=1$

$o((\iota \to \iota )\to \iota )=2$

Semântica

Estilo Church vs estilo Curry

De um modo geral, existem duas maneiras de atribuição de significado para o cálculo lambda simplesmente tipado, às vezes chamado intrínseco vs extrínseco, ou estilo Church vs. estilo Curry. Uma semântica estilo Church apenas atribui significado à termos bem tipados, ou mais precisamente, atribui significado diretamente por derivações de tipagem. O efeito disso é que é possível se atribuir significados diferentes à termos que se diferenciam apenas por anotações de tipos. Por exemplo, o termo identidade nos inteiros ($\lambda x:{\texttt {int}}.~x$) e o termo identidade nos booleanos ($\lambda x:{\texttt {bool}}.~x$) podem significar coisas diferentes. Entretanto, uma semântica estilo Curry atribui significado para termos independente da tipagem, como seriam interpretados em uma linguagem não tipada. Nesta visão, $\lambda x:{\texttt {int}}.~x$ e $\lambda x:{\texttt {bool}}.~x$ significam a mesma coisa (isto é, $\lambda x.~x$).

A distinção entre semântica intrínseca e extrínseca é às vezes associada a presença ou não de anotações nas abstrações lambda, mas estritamente falando esse uso é impreciso. É possível se definir uma semântica estilo Curry em termos anotados simplesmente ignorando os tipos (através da remoção de tipos, como também é possível prover uma semântica estilo Church a termos não anotados quando os tipos podem ser deduzidos do contexto (através da inferência de tipos). A diferença essencial entre essas duas abordagens é apenas como as regras de tipagem são vistas na definição da linguagem, ou como um formalismo para verificação de propriedades de uma linguagem fundamental mais primitiva. Maior parte da diferença das interpretações semânticas discutidas abaixo podem ser vistas sob uma ótica Church ou Curry.

Teoria equational

O cálculo lambda simplesmente tipado tem a mesma teoria da $\beta \eta$-equivalência do cálculo lambda não tipado, mas sujeito à retrições de tipos. A equação $(\lambda x:\sigma .t)\,u=_{\beta }t[x:=u]$ é verdadeira em um contexto $\Gamma$ sempre que $\Gamma ,x:\sigma \vdash t:\tau$ e $\Gamma \vdash u:\sigma$, enquanto a equação $t=_{\eta }\lambda x:\sigma .t\,x$ é verdadeira sempre que $\Gamma \vdash t:\sigma \to \tau$.

Semântica operacional

De modo semelhante, a semântica operacional do cálculo lambda simplesmente tipado pode ser determinada como a do cálculo lambda não tipado, utilizando-se chamada por valor, ou outra estratégia de avaliação. Assim como para qualquer linguagem tipada, segurança de tipos é uma propriedade fundamental para todas essas estratégias de avaliação. Adicionalmente, a propriedade da normalização forte implica que qualquer estratégia de avaliação irá terminar em todos os termos simplesmente tipados.

Semântica categórica

O cálculo lambda simplesmente tipado (com $\beta \eta$-equivalência) é a linguagem interna da Categoria Cartesiano Fechado (CCCs), como foi observado primeiro por Joachim Lambek.

Semântica prova-teórica

O cálculo lambda simplesmente tipado é intimamente relacionado ao fragmento implicacional da lógica intuicionista proposicional (lógica minimal) através do Isomorfismo de Curry-Howard: termos correspondem precisamente à provas em dedução natural.

Sintaxes alternativas

A representação utilizada acima não é a única forma de se definir a sintaxe do cálculo lambda simplesmente tipado. Uma das alternativas é remover as anotações de tipo completamente (dessa forma, a sintaxe é idêntica à do cálculo lambda não tipado), garantindo que os termos são bem tipados pela inferência de tipos de Hindley-Milter. O algoritmo de inferência termina, é seguro e completo: sempre que um termo for tipável, o algoritmo computará seu tipo. Mais precisamente, o algoritmo computa o tipo principal do termo, uma vez que frequentemente um termo não anotado (como $\lambda x.~x$) pode ter mais de um tipo (${\texttt {int}}\to {\texttt {int}}$, ${\texttt {bool}}\to {\texttt {bool}}$, etc., sendo todos esses instâncias do tipo principal $\alpha \to \alpha$).

Outra representação alternativa do cálculo lambda simplesmente tipado é baseada na checagem de tipos bidirecional, que requer mais anotações de tipos que a inferência de Hindley-Milner mas é mais fácil de descrever. O sistema de tipos é dividido em duas sentenças, uma representando a checagem e a outra a síntese, sendo $\Gamma \vdash e\Leftarrow \tau$ e $\Gamma \vdash e\Rightarrow \tau$, respectivamente. Operacionalmente, os três componentes $\Gamma$, $e$, e $\tau$ são todos entradas para a sentença de checagem $\Gamma \vdash e\Leftarrow \tau$, enquanto a sentença de síntese $\Gamma \vdash e\Rightarrow \tau$ toma apenas $\Gamma$ e $e$ como entradas, produzindo o tipo $\tau$ como saída. Essas sentenças são derivadas pelas seguintes regras:

${x:\sigma \in \Gamma } \over {\Gamma \vdash x\Rightarrow \sigma }$ [1]      ${c{\textrm {~uma~constante~do~tipo~}}T} \over {\Gamma \vdash c\Rightarrow T}$ [2]

${\Gamma ,x:\sigma \vdash e\Leftarrow \tau } \over {\Gamma \vdash \lambda x.~e\Leftarrow \sigma \to \tau }$ [3]      ${\Gamma \vdash e_{1}\Rightarrow \sigma \to \tau \quad \Gamma \vdash e_{2}\Leftarrow \sigma } \over {\Gamma \vdash e_{1}~e_{2}\Rightarrow \tau }$ [4]

${\Gamma \vdash e\Rightarrow \tau } \over {\Gamma \vdash e\Leftarrow \tau }$ [5]      ${\Gamma \vdash e\Leftarrow \tau } \over {\Gamma \vdash (e:\tau )\Rightarrow \tau }$ [6]

Observe que as regras [1]-[4] são praticamente idênticas às regras (1)-(4) acima, exceto pela cautelosa escolha das sentenças de checagem e síntese. Essas escolhas podem ser explicadas da seguinte forma:

1. Se $x:\sigma$ está no contexto, pode-se sintetizar o tipo $\sigma$ para $x$.
2. Os tipos das constantes de termos são fixos e podem ser sintetizados.
3. Para checar que $\lambda x.~e$ tem tipo $\sigma \to \tau$ em algum contexto, pode-se estender o contexto com $x:\sigma$ e checar que $e$ tem o tipo $\tau$.
4. Se $e_{1}$ sintetiza o tipo $\sigma \to \tau$ (em algum contexto), e $e_{2}$ e se verifica contra o tipo $\sigma$ (em algum contexto), então $e_{1}~e_{2}$ sintetiza o tipo $\tau$.

Observe que as regras para síntese são lidas de cima para baixo, enquanto as regras para checagem são lidas de baixo para cima. Note em particular que não é necessário qualquer anotação na abstração lambda na regra [3], porque o tipo da variável ligada pode ser deduzido através do tipo que é checado da função. Finalmente, as regras [5] e [6] podem ser explicadas da seguinte forma:

5. Para checar que $e$ tem tipo $\tau$, é suficiente para sintetizar o tipo $\tau$.
6. Se verifica-se $e$ contra o tipo $\tau$, então o termo explicitamente anotado $(e:\tau )$ sintetiza $\tau$.

Por conta dessas duas últimas regras coagindo entre síntese e checagem, é fácil perceber que qualquer termo bem tipado mas não anotado pode ser checado no sistema bidirecional, enquanto se puder inserir anotações de tipos "suficientes". E de fato, anotações são necessárias apenas para redexes $\beta$.

Observações gerais

Dadas as semânticas padrões, o cálculo lambda simplesmente tipado é fortemente normalizável: isto é, termos bem tipados sempre reduzem para um valor (uma abstração $\lambda$). Isso acontece porque recursão não é permitida pelas regras de tipagem: é impossível encontrar tipos para combinadores de ponto fixo e termos de looping como por exemplo $\Omega =(\lambda x.~x~x)(\lambda x.~x~x)$. Recursão pode ser adicionada à linguagem tendo um operador especial ${\texttt {fix}}_{\alpha }$do tipo $(\alpha \to \alpha )\to \alpha$ ou adicionando tipos recursivos gerais, porém ambos eliminam a normalização forte.

Resultados importantes

• Tait mostrou em 1967 que a redução $\beta$ é fortemente normalizável. Como corolário a equivalência $\beta$ é decidível. Statman mostrou em 1977 que o problema da normalização não é recursivo elementar.
• O problema da unificação para equivalência $\beta \eta$ é indecidível. Huet mostrou em 1973 que a unificação de terceira ordem é indecidível e isso foi melhorado posteriormente por Baxter em 1978 e depois por Goldfarb em 1981 mostrando que a unificação de segunda ordem é indecidível. Enquanto a correspondência de alta ordem (unificações onde apenas um termo contém variáveis existenciais) é decidível e ainda em aberto. [2006: Colin Stirling, Edinburgh, publicou um esboço da prova que ele alega que o problema é decidível; entretanto, a versão completa da prova ainda não foi publicada]
• É possível codificar números naturais por termos do tipo $(o\to o)\to (o\to o)$ (numerais de Church). Schwichtenberg mostrou em 1976 que em exatamente $\lambda ^{\to }$ os polinômios estendidos são representáveis como funções sobre os numerais de Church; esses são grosseiramente os polinômios fechados sobre o operador condicional.

Referências

• A. Church: A Formulation of the Simple Theory of Types, JSL 5, 1940
• W.W.Tait: Intensional Interpretations of Functionals of Finite Type I, JSL 32(2), 1967
• G.D. Plotkin: Lambda-definability and logical relations, Technical report, 1973
• G.P. Huet: The Undecidability of Unification in Third Order Logic Information and Control 22(3): 257-267 (1973)
• H. Friedman: Equality between functionals. LogicColl. '73, pages 22-37, LNM 453, 1975.
• H. Schwichtenberg: Functions definable in the simply-typed lambda calculus, Arch. Math Logik 17 (1976) 113-114.
• R. Statman: The Typed lambda-Calculus Is not Elementary Recursive FOCS 1977: 90-94
• W. D. Goldfarb: The undecidability of the 2nd order unification problem, TCS (1981), no. 13, 225- 230.
• R. Statman. $\lambda$-definable functionals and $\beta \eta$ conversion. Arch. Math. Logik, 23:21--26, 1983.
• J. Lambek: Cartesian Closed Categories and Typed Lambda-calculi. Combinators and Functional Programming Languages 1985: 136-175
• U. Berger, H. Schwichtenberg: An Inverse of the Evaluation Functional for Typed lambda-calculus LICS 1991: 203-211
• Jung, A.,Tiuryn, J.:A New Characterization of Lambda Definability, TLCA 1993
• R. Loader: The Undecidability of λ-definability, appeared in the Church Festschrift, 2001
• H. Barendregt, Lambda Calculi with Types, Handbook of Logic in Computer Science, Volume II, Oxford University Press, 1993. ISBN 0-19-853761-1.
• L. Baxter: The undecidability of the third order dyadic unification problem, Information and Control 38(2), 170-178 (1978)

Ver também

• Cálculo lambda
• Forma normal beta

Ligações externas

• Loader, Ralph (1998). «Notes on Simply Typed Lambda Calculus»