Nos ramos da lógica matemática conhecidos como teoria da prova e teoria dos tipos, um sistema de tipos puro (PTS), anteriormente conhecido como sistema de tipos generalizado (GTS), é uma forma de cálculo lambda tipado que permite um número arbitrário de sortes e dependências entre quaisquer delas. O arcabouço pode ser visto como uma generalização do cubo lambda de Barendregt, no sentido de que todos os cantos do cubo podem ser representados como instâncias de um PTS com apenas duas sortes. De fato, Barendregt (1991) formulou seu cubo neste cenário. Sistemas de tipos puros podem obscurecer a distinção entre tipos e termos e colapsar a hierarquia de tipos, como é o caso do cálculo das construções, mas isso não é geralmente o caso, por exemplo, o cálculo lambda simplesmente tipado permite apenas que termos dependam de termos.
Sistemas de tipos puros foram introduzidos independentemente por Stefano Berardi (1988) e Jan Terlouw (1989). Barendregt os discutiu extensivamente em seus artigos subsequentes. Em sua tese de doutorado, Berardi definiu um cubo de lógicas construtivas análogo ao cubo lambda (essas especificações são não-dependentes). Uma modificação deste cubo foi posteriormente chamada de L-cubo por Herman Geuvers, que em sua tese de doutorado estendeu a correspondência de Curry–Howard a este cenário. Baseando-se nessas ideias, G. Barthe e outros definiram sistemas de tipos puros clássicos (CPTS) adicionando um operador de dupla negação. Similarmente, em 1998, Tijn Borghuis introduziu os sistemas de tipos puros modais (MPTS). Roorda discutiu a aplicação de sistemas de tipos puros à programação funcional; e Roorda e Jeuring propuseram uma linguagem de programação baseada em sistemas de tipos puros. A tese de mestrado de Roorda (linkada a partir da página citada) também contém uma introdução geral aos sistemas de tipos puros.
Os sistemas do cubo lambda são todos conhecidos por serem fortemente normalizantes. Sistemas de tipos puros em geral não precisam ser, por exemplo, o Sistema U do paradoxo de Girard não é. (Grosso modo, Girard encontrou sistemas puros nos quais se pode expressar a sentença "os tipos formam um tipo"). Além disso, todos os exemplos conhecidos de sistemas de tipos puros que não são fortemente normalizantes também não são (fracamente) normalizantes: eles contêm expressões que não têm formas normais, assim como o cálculo lambda não tipado
. É um grande problema em aberto na área se este é sempre o caso, isto é, se um PTS (fracamente) normalizante sempre tem a propriedade de normalização forte. Isso é conhecido como a conjectura de Barendregt–Geuvers–Klop (em homenagem a Henk Barendregt, Herman Geuvers e Jan Willem Klop).
Definição Um sistema de tipos puro é definido por um triplo onde é o conjunto de sortes, é o conjunto de axiomas, e é o conjunto de regras. A tipagem em sistemas de tipos puros é determinada pelas seguintes regras, onde é qualquer sorte:
Implementações As seguintes linguagens de programação têm sistemas de tipos puros: SAGESAGE YarrowYarrow Henk 2000Henk 2000 Haskell desde a versão 8 do GHC.Weirich et al., System FC with Explicit Kind Equality, ICFP '13: "Portanto, seguimos sistemas de tipos puros (Barendregt 1992) e unificamos a sintaxe de tipos e kinds, permitindo reutilizar coerções de tipo como coerções de kind. [...] Além disso, nossas regras incluem o axioma *:* o que significa que não há distinção real entre tipos e kinds."
Ver também Sistema U – um exemplo de PTS inconsistente Cálculo λμ usa uma abordagem diferente para controle do que CPTS
Referências
Bibliografia
Leitura adicional
Ligações externas
Categoria:Matemática Categoria:Ciência da computação