Teoria de tipo

Da Wikipédia, a enciclopédia livre
Ir para navegação Pular para pesquisar

Em matemática , lógica e ciência da computação , um sistema de tipos é um sistema formal em que cada termo tem um "tipo" que define seu significado e as operações que podem ser realizadas nele. A teoria dos tipos é o estudo acadêmico dos sistemas de tipos.

Algumas teorias de tipo servem como alternativas para a teoria dos conjuntos como base da matemática . Dois bem conhecidos tais teorias são Alonzo Church 's digitado λ-cálculo e Per Martin-Löf ' s teoria tipo intuitionistic .

A teoria dos tipos foi criada para evitar paradoxos em fundamentos anteriores, como a teoria dos conjuntos ingênua , lógicas formais e sistemas de reescrita .

A teoria de tipo está intimamente relacionada a, e em alguns casos se sobrepõe a, sistemas de tipos computacionais , que são um recurso de linguagem de programação usado para reduzir bugs e facilitar certas otimizações do compilador .

História

Entre 1902 e 1908, Bertrand Russell propôs várias "teorias do tipo" em resposta à sua descoberta de que a versão ingênua da teoria dos conjuntos de Gottlob Frege era afetada pelo paradoxo de Russell . Em 1908, Russell chegou a uma teoria "ramificada" dos tipos, juntamente com um " axioma da redutibilidade ", que figurou com destaque em Whitehead e Russell 's Principia Mathematicapublicado entre 1910 e 1913. Eles tentaram resolver o paradoxo de Russell criando primeiro uma hierarquia de tipos e, em seguida, atribuindo cada entidade matemática concreta (e possivelmente outra) a um tipo. Entidades de um determinado tipo são construídas exclusivamente a partir de entidades daqueles tipos que estão mais abaixo em sua hierarquia, evitando assim que uma entidade seja atribuída a si mesma.

Na década de 1920, Leon Chwistek e Frank P. Ramsey propuseram uma teoria dos tipos não ramificados, agora conhecida como a "teoria dos tipos simples" ou teoria dos tipos simples , que colapsou a hierarquia dos tipos na teoria ramificada anterior e, como tal, não exigia o axioma da redutibilidade.

O uso comum da "teoria dos tipos" é quando esses tipos são usados ​​com um sistema de reescrita de termos . O primeiro exemplo mais famoso é Alonzo Church 's cálculo lambda simplesmente tipado . A teoria dos tipos de Church [1] ajudou o sistema formal a evitar o paradoxo de Kleene-Rosser que afligia o cálculo lambda original não tipado. Church demonstrou que isso poderia servir de base para a matemática e foi referido como uma lógica de ordem superior .

Algumas outras teorias tipo incluem Per Martin-Löf 's teoria tipo intuitionistic , que tem sido a base utilizada em algumas áreas da matemática construtivas . O cálculo de construções de Thierry Coquand e seus derivados são a base usada por Coq , Lean e outros. O campo é uma área de pesquisa ativa, conforme demonstrado pela teoria dos tipos de homotopia .

Conceitos básicos

A apresentação contemporânea dos sistemas de tipos no contexto da teoria dos tipos foi sistematizada por uma estrutura conceitual introduzida por Henk Barendregt . [2]

Tipo, prazo, valor

Em um sistema de teoria de tipo, um termo se opõe a um tipo . Por exemplo, 4 , 2 + 2 esão todos termos separados com o tipo nat para números naturais. Tradicionalmente, o termo é seguido por dois pontos e seu tipo, como 2: nat - isso significa que o número 2 é do tipo nat . Além dessa oposição e sintaxe, pouco pode ser dito sobre os tipos nessa generalidade, mas frequentemente, eles são interpretados como algum tipo de coleção (não necessariamente conjuntos) dos valores que o termo pode avaliar. É comum denotar os termos por e e os tipos por τ . A forma como os termos e tipos são formados depende do sistema de tipo específico e é tornado preciso por alguma sintaxe e restrições adicionais de boa formação .

Ambiente de digitação, tipo de atribuição, tipo de julgamento

A digitação geralmente ocorre em algum contexto ou ambiente denotado pelo símbolo. Freqüentemente, um ambiente é uma lista de pares. Este par às vezes é chamado de atribuição . O contexto completa a oposição acima. Juntos, eles formam um julgamento denotado.

Reescrever regras, conversão, redução

As teorias de tipo têm computação explícita e são codificadas em regras para reescrever termos. Essas são chamadas de regras de conversão ou, se a regra funcionar apenas em uma direção, uma regra de redução . Por exemplo, e são termos sintaticamente diferentes, mas o primeiro se reduz ao segundo. Esta redução está escrita. Essas regras também estabelecem equivalências correspondentes entre os termos, por escrito.

O termo reduz a . Desde anão pode ser reduzida ainda mais, é chamada de forma normal . Vários sistemas de cálculo lambda tipado, incluindo o cálculo lambda simplesmente digitado , o Sistema F de Jean-Yves Girard e o cálculo de construções de Thierry Coquand estão fortemente normalizando . Em tais sistemas, uma verificação de tipo bem-sucedida implica em uma prova de rescisão do termo.

Regras do tipo

Com base nos julgamentos e equivalências, as regras de inferência de tipo podem ser usadas para descrever como um sistema de tipos atribui um tipo a construções sintáticas (termos), bem como na dedução natural . Para serem significativas, as regras de conversão e tipo geralmente estão intimamente relacionadas como, por exemplo, por uma propriedade de redução de assunto , que pode estabelecer uma parte da solidez de um sistema de tipo.

Problemas de decisão

Um sistema de tipos está naturalmente associado aos problemas de decisão de verificação de tipos , tipabilidade e ocupação de tipos . [3]

Verificação de tipo

O problema de decisão de verificação de tipo (abreviado por) é:

Dado um tipo de ambiente , um termo , e um tipo , decida se o termo pode ser atribuído o tipo no ambiente de tipo .

A capacidade de decisão da verificação de tipo significa que a segurança de tipo de qualquer texto de programa (código-fonte) pode ser verificada.

Typability

O problema de decisão de tipificação (abreviado por) é:

Dado um termo , decida se existe um tipo de ambiente e um tipo de modo que o termo pode ser atribuído o tipo no ambiente de tipo .

Uma variante da tipabilidade é a tipificação escrita. um ambiente de tipo (abreviado por), para o qual um ambiente de tipo faz parte da entrada. Se o termo fornecido não contiver referências externas (como variáveis ​​de termos livres), a tipabilidade coincide com a tipabilidade wrt. o ambiente de tipo vazio.

A tipabilidade está intimamente relacionada à inferência de tipo . Enquanto a tipabilidade (como um problema de decisão) aborda a existência de um tipo para um determinado termo, a inferência de tipo (como um problema de computação) requer que um tipo real seja calculado.

Tipo de habitação

O problema de decisão do tipo habitação (abreviado por) é:

Dado um tipo de ambiente e um tipo , decida se existe um termo que pode ser atribuído ao tipo no ambiente de tipo .

O paradoxo de Girard mostra que a habitação de tipos está fortemente relacionada à consistência de um sistema de tipos com a correspondência de Curry-Howard. Para ser sólido, tal sistema deve ter tipos desabitados.

A oposição de termos e tipos também pode ser vista como uma de implementação e especificação . Por síntese de programa (a contraparte computacional de) tipo de habitação (veja abaixo) pode ser usado para construir (todos ou partes de) programas a partir de especificações fornecidas na forma de informações de tipo. [4]

Interpretações da teoria dos tipos

A teoria dos tipos está intimamente ligada a muitos campos de pesquisa ativa. Mais especificamente, a correspondência Curry-Howard fornece um isomorfismo profundo entre a lógica intuicionista, cálculo lambda tipado e categorias fechadas cartesianas.

Lógica intuicionista

Ao lado da visão dos tipos como coleção de valores de um termo, a teoria dos tipos oferece uma segunda interpretação da oposição de termos e tipos. Os tipos podem ser vistos como proposições e os termos como provas . Nesta forma de ler uma digitação, um tipo de funçãoé visto como uma implicação , ou seja, como a proposição, que segue de .

Teoria da categoria

A linguagem interna da categoria fechada cartesiana é o cálculo lambda simplesmente digitado . Esta visualização pode ser estendida a outros cálculos lambda digitados. Certas categorias cartesianas fechadas, os topoi, foram propostas como um cenário geral para a matemática, em vez da teoria dos conjuntos tradicional.

Diferença da teoria dos conjuntos

Existem muitas teorias de conjuntos diferentes e muitos sistemas diferentes de teoria de tipos, portanto, o que se segue são generalizações.

  • A teoria dos conjuntos é construída sobre a lógica. Requer um sistema separado como lógica de predicados por baixo dele. Na teoria dos tipos, conceitos como "e" e "ou" podem ser codificados como tipos na própria teoria dos tipos.
  • Na teoria dos conjuntos, um elemento não está restrito a um conjunto. Na teoria dos tipos, os termos (geralmente) pertencem a apenas um tipo. (Onde um subconjunto seria usado, a teoria dos tipos tende a usar uma função de predicado que retorna verdadeiro se o termo estiver no subconjunto e retorna falso se o valor não estiver. A união de dois tipos pode ser definida como um novo tipo chamado de soma tipo , que contém novos termos.)
  • A teoria dos conjuntos geralmente codifica os números como conjuntos. (0 é o conjunto vazio, 1 é um conjunto contendo o conjunto vazio, etc. Consulte a definição teórica dos conjuntos de números naturais .) A teoria dos tipos pode codificar números como funções usando a codificação Church ou, mais naturalmente, como tipos indutivos . Os tipos indutivos criam novas constantes para a função sucessora e zero, semelhantes aos axiomas de Peano .
  • A teoria dos tipos tem uma conexão simples com a matemática construtiva por meio da interpretação de BHK . Ele pode ser conectado à lógica pelo isomorfismo de Curry-Howard . E algumas teorias de tipo estão intimamente ligadas à teoria das categorias .

Recursos opcionais

Tipos dependentes

Um tipo dependente é um tipo que depende de um termo ou outro tipo. Portanto, o tipo retornado por uma função pode depender do argumento da função.

Por exemplo, uma lista de s de comprimento 4 podem ser um tipo diferente de uma lista de s de comprimento 5. Em uma teoria de tipos com tipos dependentes, é possível definir uma função que recebe um parâmetro "n" e retorna uma lista contendo "n" zeros. Chamar a função com 4 produziria um termo com um tipo diferente do que se a função fosse chamada com 5.

Outro exemplo é o tipo que consiste nas provas de que o termo do argumento possui uma determinada propriedade, como o termo de tipo, por exemplo, um determinado número natural, é primo. Veja a correspondência de Curry-Howard .

Os tipos dependentes desempenham um papel central na teoria dos tipos intuicionista e no projeto de linguagens de programação funcionais como Idris , ATS , Agda e Epigram .

Tipos de igualdade

Muitos sistemas da teoria de tipos têm um tipo que representa a igualdade de tipos e de termos. Esse tipo é diferente da conversibilidade e costuma ser denotado como igualdade proposicional .

Na teoria do tipo intuicionista, o tipo de igualdade (também chamado de tipo de identidade) é conhecido como para identidade. Existe um tipo quando é um tipo e e são ambos os termos do tipo . Um termo do tipo é interpretado como significando que é igual a .

Na prática, é possível construir um tipo mas não existirá um termo desse tipo. Na teoria dos tipos intuicionista, novos termos de igualdade começam com reflexividade. Se é um termo do tipo , então existe um termo do tipo . Igualdades mais complicadas podem ser criadas criando um termo reflexivo e, em seguida, fazendo uma redução de um lado. Então se é um termo do tipo , então há um termo do tipo e, por redução, gerar um termo do tipo . Assim, neste sistema, o tipo de igualdade denota que dois valores do mesmo tipo são convertíveis por reduções.

Ter um tipo de igualdade é importante porque pode ser manipulado dentro do sistema. Normalmente não há julgamento para dizer que dois termos não são iguais; em vez disso, como na interpretação Brouwer-Heyting-Kolmogorov , mapeamos para , Onde é o tipo inferior sem valores. Existe um termo com tipo, mas não um do tipo.

A teoria dos tipos de homotopia difere da teoria dos tipos intuicionista principalmente por lidar com o tipo de igualdade.

Tipos indutivos

Um sistema de teoria de tipos requer alguns termos e tipos básicos para operar. Alguns sistemas os criam a partir de funções que usam codificação Church . Outros sistemas têm tipos indutivos : um conjunto de tipos básicos e um conjunto de construtores de tipo que geram tipos com propriedades bem comportadas. Por exemplo, certas funções recursivas chamadas em tipos indutivos têm o término garantido.

Os tipos coindutivos são tipos de dados infinitos criados por meio de uma função que gera o (s) próximo (s) elemento (s). Veja Coindução e Correcursão .

Indução-indução é um recurso para declarar um tipo indutivo e uma família de tipos que depende do tipo indutivo.

A recursão de indução permite uma gama mais ampla de tipos bem comportados, permitindo que o tipo e as funções recursivas que operam nele sejam definidas ao mesmo tempo.

Tipos universo

Tipos foram criados para evitar paradoxos, como o paradoxo de Russell . No entanto, os motivos que levam a esses paradoxos - ser capaz de dizer coisas sobre todos os tipos - ainda existem. Portanto, muitas teorias de tipo têm um "tipo de universo", que contém todos os outros tipos (e não ele mesmo).

Em sistemas onde você pode querer dizer algo sobre os tipos de universo, há uma hierarquia de tipos de universo, cada um contendo aquele abaixo dele na hierarquia. A hierarquia é definida como infinita, mas as declarações devem se referir apenas a um número finito de níveis do universo.

Universos de tipos são particularmente complicados na teoria de tipos. A proposta inicial da teoria dos tipos intuicionista sofreu com o paradoxo de Girard .

Componente computacional

Muitos sistemas da teoria dos tipos, como o cálculo lambda de tipo simples , a teoria dos tipos intuicionista e o cálculo de construções , também são linguagens de programação. Ou seja, dizem que têm um "componente computacional". O cálculo é a redução de termos da linguagem usando regras de reescrita .

Um sistema de teoria de tipo que tem um componente computacional bem comportado também tem uma conexão simples com a matemática construtiva por meio da interpretação de BHK .

A matemática não construtiva nesses sistemas é possível adicionando operadores em continuações, como chamada com continuação atual . No entanto, esses operadores tendem a quebrar propriedades desejáveis, como canonicidade e parametricidade .

Teorias do tipo

Principal

Menor

Ativo

Impacto prático

As linguagens de programação

Há ampla sobreposição e interação entre os campos da teoria dos tipos e os sistemas de tipos. Os sistemas de tipo são um recurso de linguagem de programação projetado para identificar bugs. Qualquer análise estática de programa , como os algoritmos de verificação de tipo na fase de análise semântica do compilador , tem uma conexão com a teoria de tipo.

Um bom exemplo é Agda , uma linguagem de programação que usa UTT (Teoria Unificada de Tipos Dependentes de Luo) para seu sistema de tipos. A linguagem de programação ML foi desenvolvida para manipular teorias de tipos (consulte LCF ) e seu próprio sistema de tipos foi fortemente influenciado por elas.

Fundamentos matemáticos

O primeiro assistente de prova de computador, chamado Automath , usou a teoria dos tipos para codificar matemática em um computador. Martin-Löf desenvolveu especificamente a teoria dos tipos intuicionista para codificar toda a matemática para servir como uma nova base para a matemática. Há pesquisas em andamento sobre os fundamentos matemáticos usando a teoria dos tipos de homotopia .

Os matemáticos que trabalham com a teoria das categorias já têm dificuldade em trabalhar com os fundamentos amplamente aceitos da teoria dos conjuntos de Zermelo-Fraenkel . Isso levou a propostas como a Teoria Elementar da Categoria de Conjuntos de Lawvere (ETCS). [5] A teoria dos tipos de homotopia continua nesta linha usando a teoria dos tipos. Os pesquisadores estão explorando conexões entre tipos dependentes (especialmente o tipo de identidade) e topologia algébrica (especificamente homotopia ).

Assistentes de prova

Grande parte da pesquisa atual na teoria dos tipos é conduzida por verificadores de prova , assistentes de prova interativos e provadores de teoremas automatizados . A maioria desses sistemas usa uma teoria dos tipos como base matemática para codificar as provas, o que não é surpreendente, dada a estreita conexão entre a teoria dos tipos e as linguagens de programação:

Muitas teorias de tipo são apoiadas por LEGO e Isabelle . Isabelle também apóia fundamentos além de teorias de tipo, como ZFC . Mizar é um exemplo de sistema de prova que suporta apenas a teoria dos conjuntos.

Lingüística

A teoria dos tipos também é amplamente usada em teorias formais de semântica de línguas naturais , especialmente a gramática de Montague e seus descendentes. Em particular, gramáticas categóricas e gramáticas pré - agrupadas usam construtores de tipo extensivamente para definir os tipos ( substantivo , verbo , etc.) de palavras.

A construção mais comum leva os tipos básicos e para indivíduos e valores de verdade , respectivamente, e define o conjunto de tipos recursivamente da seguinte forma:

  • E se e são tipos, então é ;
  • nada exceto os tipos básicos, e o que pode ser construído a partir deles por meio da cláusula anterior são tipos.

Um tipo complexo é o tipo de funções de entidades do tipo para entidades do tipo . Assim, temos tipos comoque são interpretados como elementos do conjunto de funções de entidades para valores de verdade, ou seja , funções indicadoras de conjuntos de entidades. Uma expressão de tipoé uma função de conjuntos de entidades para valores de verdade, ou seja, um (função indicadora de um) conjunto de conjuntos. Este último tipo é normalmente considerado o tipo de quantificadores de linguagem natural , como todos ou ninguém ( Montague 1973, Barwise e Cooper 1981).

Ciências sociais

Gregory Bateson introduziu uma teoria dos tipos lógicos nas ciências sociais; suas noções de double bind e níveis lógicos são baseadas na teoria dos tipos de Russell.

Relação à teoria da categoria

Embora a motivação inicial para a teoria das categorias estivesse muito distante do fundacionalismo, os dois campos revelaram ter conexões profundas. Como escreve John Lane Bell : "Na verdade, as próprias categorias podem ser vistas como teorias de tipos de um certo tipo; esse fato por si só indica que a teoria de tipos está muito mais intimamente relacionada à teoria das categorias do que à teoria dos conjuntos." Em resumo, uma categoria pode ser vista como uma teoria dos tipos considerando seus objetos como tipos (ou espécies), isto é, "Grosso modo, uma categoria pode ser pensada como uma teoria dos tipos desprovida de sua sintaxe." Uma série de resultados significativos seguem desta forma: [6]

A interação, conhecida como lógica categórica , tem sido um assunto de pesquisa ativa desde então; veja a monografia de Jacobs (1999), por exemplo.

Veja também

Notas

  1. ^ Church, Alonzo (1940). "Uma formulação da teoria simples dos tipos". The Journal of Symbolic Logic . 5 (2): 56–68. doi : 10.2307 / 2266170 . JSTOR  2266170 .
  2. ^ Barendregt, Henk (1991). "Introdução aos sistemas de tipos generalizados". Journal of Functional Programming . 1 (2): 125–154. doi : 10.1017 / s0956796800020025 . hdl : 2066/17240 . ISSN 0956-7968 . 
  3. ^ Henk Barendregt; Wil Dekkers; Richard Statman (20 de junho de 2013). Lambda Calculus with Types . Cambridge University Press. p. 66. ISBN 978-0-521-76614-2.
  4. ^ Heineman, George T .; Bessai, Jan; Düdder, Boris; Rehof, Jakob (2016). "Um longo e sinuoso caminho para a síntese modular". Aproveitando Aplicações de Métodos Formais, Verificação e Validação: Técnicas Fundamentais . ISoLA 2016. Notas de aula em Ciência da Computação. 9952 . Springer. pp. 303–317. doi : 10.1007 / 978-3-319-47166-2_21 .
  5. ^ ETCS em nLab
  6. ^ Bell, John L. (2012). "Tipos, conjuntos e categorias" (PDF) . Em Kanamory, Akihiro (ed.). Conjuntos e extensões no século XX . Manual da História da Lógica. 6 . Elsevier. ISBN  978-0-08-093066-4.

Referências

  • Farmer, William M. (2008). "As sete virtudes da teoria dos tipos simples". Journal of Applied Logic . 6 (3): 267–286. doi : 10.1016 / j.jal.2007.11.001 .

Leitura adicional

Ligações externas