Teoria dos tipos intuicionista

Teoria dos tipos intuicionista, ou Teoria dos tipos construtiva, ou Teoria dos tipos de Martin-Löf é uma teoria dos tipos e uma alternativa para os fundamentos da matemática baseados nos princípios do construtivismo matemático. A teoria de tipos intuicionista foi introduzida por Per Martin-Löf, um matemático e filósofo sueco, em 1972. Martin-Löf modificou sua proposta algumas vezes; sua formulação impredicativa de 1971 era inconsistente, como demonstrado pelo paradoxo de Girard. As próximas formulações eram predicativas. Ele propôs tanto uma variante intensional quanto uma variante extensional da teoria.

A teoria dos tipos intuicionista é baseada em uma certa lógica ou isomorfismo entre proposições e tipos: uma proposição é identificada com o tipo de suas provas. Essa identificação é usualmente chamada de isomorfismo de Curry-Howard, que originalmente foi formulado para a lógica intuicionista e para o cálculo lambda simplesmente tipado. A Teoria dos Tipos estende sua identificação para a lógica de predicados através da introdução de tipos dependentes, que são tipos que contêm valores. A Teoria dos Tipos internaliza a interpretação da lógica intuicionista proposta por Brouwer, Heyting e Kolmogorov, também chamada de interpretação BHK. Os tipos da Teoria dos Tipos possuem um papel similar aos conjuntos da teoria dos conjuntos, mas as funções definidas na Teoria dos Tipos são sempre computáveis.

Conectivos da Teoria dos Tipos

No contexto da Teoria de Tipos um conectivo é uma forma de construir tipos, possivelmente utilizando tipos já dados. Os conectivos básicos da Teoria dos Tipos são:

Tipos Π

Tipos $\Pi$, também chamados de tipos dependentes do produto, são análogos aos produtos indexados de conjuntos. Como tais, eles generalizam o usual espaço de funções para modelar funções cujo tipo resultante pode variar em sua entrada. Exemplo: escrevendo ${\mbox{Vec}}({\mathbb {R} },n)$ para o tipo de n-tuplas de números reais e ${\mathbb {N} }$ para o tipo de números naturais.

$\Pi n:{\mathbb {N} }.{\mbox{Vec}}({\mathbb {R} },n)$

significa o tipo de função que, dado um número natural n, retorna uma n-tupla de números reais. A operação de espaço de funções surge como um caso especial quando o espaço do tipo na realidade não depende da entrada, exemplo, $\Pi n:{\mathbb {N} }.{\mathbb {R} }$ é o tipo de funções dos números naturais para os números reais, que pode ser escrito também como ${\mathbb {N} }\to {\mathbb {R} }$.

Utilizar o isomorfismo de Curry-Howard tipos $\Pi$ também serve para modelos de implicação e quantificadores universais, exemplo, o termo residindo em $\Pi m,n:{\mathbb {N} }.m+n=n+m$ é uma função que atribui a qualquer par de números naturais a prova de que a adição é comutativa para o par e logo pode ser considerada como a prova de que a adição é comutativa para todos os números naturais. (Aqui usamos o tipo igualdade $m+n=n+m$ explicado abaixo.)

Tipos Σ

Tipos $\Sigma$, também chamados de tipos dependentes da soma, são análogos às uniões indexadas de conjuntos disjuntos. Como tal, eles generalizam o produto cartesiano usual para modelar pares onde o tipo do segundo componente depende do do primeiro. Por exemplo, o tipo $\Sigma n:{\mathbb {N} }.{\mbox{Vec}}({\mathbb {R} },n)$ simboliza o tipo de pares de um número natural e uma $n$-tupla de números reais, isto é, esse tipo pode ser usado para modelar sequências de tamanho arbitrário, porém finito (usualmente chamado de listas). O tipo convencional do produto cartesiano surge como um caso especial quando o tipo do segundo componente não depende na realidade do primeiro componente, exemplo, $\Sigma n:{\mathbb {N} }.{\mathbb {R} }$ é o tipo de pares de um número natural e um número real, que pode ser escrito também como ${\mathbb {N} }\times {\mathbb {R} }$.

Mais uma vez, usando o isomorfismo de Curry-Howard, Tipos $\Sigma$ também servem de modelo para conjunções e quantificadores existenciais.

Tipos finitos

De especial importância são 0 ou ⊥ (o tipo vazio), 1 ou ⊤ (o tipo unitário) e 2 (o tipo de Booleanos ou de valores verdadeiros clássicos). Invocando o isomorfismo de Curry-Howard novamente, ⊥ simboliza Falso e ⊤ Verdadeiro.

Usando tipos finitos podemos definir negação como $\neg A=A\to \bot$.

Tipo igualdade

Dado $a,b:A$ então $a=b$ é o tipo de igualdade, prova de que $a$ é igual a $b$. Só existe um habitante (canônico) de $a=a$ e essa é a prova da reflexibilidade ${\mbox{refl}}:\Pi a:A.a=a$.

A análise das propriedades do tipo igualdade leva à teoria homotópica de tipos.

Tipos indutivos

Um dos primeiros exemplos de um tipo indutivo é o tipo de números naturais $\mathbb {N}$ que é gerado por $0:{\mathbb {N} }$ e ${\mbox{succ}}:{\mathbb {N} }\to {\mathbb {N} }$. Uma importante aplicação do princípio proposições como tipos é a identificação de uma recursão primitiva (dependente) e indução por uma constante de eliminação: ${\mathbb {N} }{\mbox{-elim}}:P(0)\to (\Pi n:{\mathbb {N} }.P(n)\to P({\mbox{succ}}(n)))\to \Pi n:{\mathbb {N} }.P(n)$ para qualquer tipo dado indexado por $P(n)$ indexado por $n:{\mathbb {N} }$. Em geral os tipos indutivos podem ser definidos em termos de tipos W, o tipo de árvores bem-formadas.

Uma importante classe de tipos indutivos são famílias indutivas, como o tipo de vetores ${\mbox{Vec}}(A,n)$ mencionado acima, que é indutivamente gerado pelos construtores ${\mbox{vnil}}:{\mbox{Vec}}(A,0)$ e ${\mbox{vcons}}:A\to \Pi n:{\mathbb {N} }.{\mbox{Vec}}(A,n)\to {\mbox{Vec}}(A,{\mbox{succ}}(n))$. Aplicando o isomorfismo de Curry–Howard mais uma vez, famílias indutivas correspondem a relações indutivamente definidas. Dybjer sugeriu estender tipos indutivos com indução-recursão.

Universos

Um exemplo de universo é $U_{0}$, o universo de todos os tipos pequenos, que contém nomes para todos os tipos introduzidos até agora. Para todo nome $a:U_{0}$ nós associamos ao tipo $El(a)$, sua extensão ou significado. Isso é padrão para assumir uma hierarquia predicativa dos universos: $U_{n}$ para cada número natural $n:{\mathbb {N} }$, no qual o universo $U_{n+1}$ contém o código para o universo anterior, isto é, nós temos $u_{n}:U_{n+1}$ com $El(u_{n})=U_{n}$. (Uma hierarquia com essa propriedade é chamada "cumulativa".)

Princípios mais fortes de universos vêm sendo investigados, isto é, super universos e o universo Mahlo. Em 1992 Huet e Coquand introduziram o cálculo de construções, uma teoria de tipos com um universo impredicativo, desta forma combinaram a Teoria do Tipos com o Sistema F de Girard. Essa extensão não é universalmente aceita por intuicionistas porque permite impredicatividade, isto é, construções circulares que são frequentemente identificadas com lógica clássica.

Formalização da Teoria dos Tipos

Essa formalização é baseada na discussão de Nordström, Petersson, e Smith. A teoria formal trabalha com tipos e objetos. Um tipo é declarado como:

• $A\,{\mbox{Tipo}}$

Um objeto existe e está em um tipo se:

• $a\in A$

Objetos podem ser iguais

• $a=b$

e tipos podem ser iguais

• $A=B$

Um tipo que depende de um objeto de um outro tipo é declarado

• $(x\in A)B$

e removido por substituição

• $B[x\leftarrow a]$, repondo a variável $x$ com o objeto $a$ em $B$.

Um objeto que depende de um objeto de um outro tipo pode ser feito de duas formas. Se o objeto é "abstrato", então é escrito

• $[x]b$

e removido por substituição

• $b[x\leftarrow a]$, repondo a variável $x$ com o objeto $a$ em $b$.

O objeto dependente do outro objeto pode também ser declarado como uma constante de um tipo recursivo. Um exemplo de um tipo recursivo é:

• $0\in nat$
• $succ\in nat\to nat$

Aqui, $succ$ é uma constante de um objeto que depende de um objeto. Não é associada com uma abstração. Constantes como $succ$ podem ser removidas através da definição de uma igualdade. Aqui a relação com a adição é definida usando uma igualdade e usando um padrão de correspondência para tratar o aspecto recursivo de $succ$.

• $add(0,b)=b$
• $add(succ(a),b)=succ(add(a,b))$

$succ$ é manipulado como uma constate opaca - ela não tem estrutura interna para substituição.

Então, objetos e tipos e essas relações são usados par expressar fórmulas na teoria. Os estilos de sentenças seguintes são usados para criar novos objetos, tipos e relações a partir de outros já existentes.

• $\Gamma \vdash \sigma \,{\mbox{Type}}$, $\sigma$ é um tipo bem-formado no contexto $\Gamma$.
• $\Gamma \vdash t:\sigma$, $t$ é um termo bem-formado do tipo $\sigma$ no contexto $\Gamma$.
• $\Gamma \vdash \sigma \equiv \tau$, $\sigma$ e $\tau$ são tipos iguais no contexto $\Gamma$.
• $\Gamma \vdash t\equiv u:\sigma$, $t$ e $u$ são termos iguais do tipo $\sigma$ no contexto $\Gamma$.
• $\vdash \Gamma \,{\mbox{Context}}$, $\Gamma$ é um contexto bem-formado de sentenças de tipos.

Por convenção, tem um tipo que representa todos os outros tipos. É chamado $U$ (ou $Set$). Como $U$ é um tipo, seus membros são objetos. Há um tipo dependente $El$ que mapeia cada objeto ao seu tipo correspondente. Na maioria dos textos $El$ nunca é escrito. No contexto da sentença, um leitor pode quase sempre dizer se $A$ se refere a um tipo, ou se refere-se ao objeto em $U$ que corresponde ao tipo.

Esse é o fundamento completo da teoria. Todo o resto é derivado.

Para implementar a lógica, para cada proposição é dado seu próprio tipo. Os objetos nesses tipos representam as diferentes possibilidades de formas para provar a proposição. Obviamente, se não há prova para a proposição, então o tipo não tem objetos. Operadores como "e" ou "ou" que estão presentes em proposições introduzem novos tipos e novos objetos. Então $A\land B$ é um tipo que depende do tipo $A$ e do tipo $B$. Os objetos nesse tipo dependente são definidos para existirem para cada par de objetos em $A$ e $B$. Obviamente, se $A$ ou $B$ não possui uma prova e é um tipo vazio, então o novo tipo representado por $A\land B$ também é vazio.

Isso pode ser aplicado em outros tipo (booleanos, números naturais, etc.) e em seus operadores.

Modelos Categóricos da Teoria dos Tipos

Usando a linguagem da teoria das categorias, R.A.G. Seely introduziu a notação de uma categoria fechada no plano cartesiano (LCCC - Locally Cartesian Closed Category) como um tipo básico do modelo da Teoria dos Tipos. Isso vem sido refinado por Hofmann e Dybjer na obra Categorias com Famílias ou Categorias com Atributos baseado em um trabalho anterior de Cartmell. Uma categoria com famílias é uma categoria C de contextos (no qual os objetos são contextos, e o contexto mórfico são substituições), juntos com um functor T : Cop → Fam(Set). Fam(Set) é a categoria de famílias de conjuntos, no qual objetos são pares (A,B) de um "conjunto indexado" A e uma função B: X → A, e os morfismos são pares de funções f : A → A' e g : X → X' , tais que B' ° g = f ° B - em outras palavras, f mapeia Ba para B'g(a). O functor T atribui a um contexto G um conjunto Ty(G) de tipos, e para cada A : Ty(G), um conjunto Tm(G,A) de termos. Os axiomas para uma functor requer que eles funcionem harmonicamente com substituição. Substituição é usualmente escrita da forma Af ou af, onde A é um tipo em Ty(G) e a é um termo em Tm(G,A), e f é uma substituição de D para G. Aqui Af : Ty(D) e af : Tm(D,Af). A categoria C deve conter um objeto terminal (o contexto vazio), e um objeto final para uma forma de produto chamado alcance, ou extensão do contexto, no qual o elemento da direita é um tipo no contexto do elemento da esquerda. Se G é um contexto, e A : Ty(G), então deve haver um objeto (G,A) final dentre os contextos D com mapeamentos p : D → G, q : Tm(D,Ap). Um framework lógico, como o de Martin-Löf's é da forma de condições de parada no contexto de conjuntos dependentes de tipos e termos: deve haver um tipo chamado Set, e para cada tipo estabelecido, os tipos devem ser fechados sob as operações de soma e produto dependentes, e assim em diante. Uma teoria como essa teoria de conjuntos predicativos expressa condições de fechamento nos tipos de conjuntos e seus elementos: eles devem ser fechados sob operações que refletem a soma e produto dependentes e sob várias formas de definições indutivas.

Extensional versus Intensional

Uma distinção fundamental é a da Teoria dos Tipos Extensional vs Intensional. Na Teoria dos Tipos Extensional igualdade de definição (isto é, de computação) não é distinguida da igualdade proposicional, que requer uma prova. Como consequência a checagem dos tipos torna-se indecidível na teoria dos tipos extensional. Isso porque contar com a igualdade de computação significa que a igualdade depende de computações que podem ser Turing completas em geral e assim a igualdade em si é indecidível devido ao problema da parada. Alguns tipos de teorias aplicam a restrição que todas as computações devem ser decidíveis para que essa igualdade de definição possa ser usada.

Em contraste na Teoria dos Tipos Intensional a checagem de tipos é decidível, mas a representação do conceito matemático padrão é complexa, já que a lógica de extensão requer o uso de igualdade de conjuntos ou construções similares. Isso é um assunto em discussão corrente se essa troca é inevitável ou se a falta de princípios de extensão na Lógica dos Tipos Intuicionistas é uma característica ou um bug.

Implementações da Teorias dos Tipos

A Teoria dos Tipos tem tido sido base de várias provas auxiliares, tais como NuPRL, LEGO e Coq. Recentemente, tipos dependentes também são características do design de linguagens de programação tais como ATS, Cayenne, Epigram e Agda.

Ver também

• Lógica Intuicionista
• Per Martin-Löf
• Teoria dos Tipos

Referências

• Per Martin-Löf (1984). Intuitionistic Type Theory Bibliopolis. ISBN 88-7088-105-9.

Leituras Adicionais

• Bengt Nordström; Kent Petersson; Jan M. Smith (1990). Programming in Martin-Löf's Type Theory. Oxford University Press. The book is out of print, but a free version can be picked up from here.
• Thompson, Simon (1991). Type Theory and Functional Programming Addison-Wesley. ISBN 0-201-41667-0.
• Granström, Johan G. (2011). Treatise on Intuitionistic Type Theory Springer. ISBN 978-94-007-1735-0.

Ligações Externas

• EU Types Project: Tutorials - notas e slides das aulas de Types Summer School 2005
• n-Categories - Sketch of a Definition - carta de John Baez e James Dolan para Ross Street, 29 de novembro de 1995