Sistema F

O Sistema F (também chamado de cálculo lambda polimórfico ou cálculo lambda de segunda ordem ) é um cálculo lambda tipado que introduz, ao cálculo lambda simplesmente digitado , um mecanismo de quantificação universal sobre tipos. O Sistema F formaliza o polimorfismo paramétrico em linguagens de programação , formando assim uma base teórica para linguagens como Haskell e ML . Foi descoberto independentemente pelo lógico Jean-Yves Girard (1972) e pelo cientista da computação John C. Reynolds .

Enquanto o cálculo lambda simplesmente digitado tem variáveis ​​que variam entre termos e ligantes para eles, o Sistema F também possui variáveis ​​que variam entre tipos e ligantes para eles. Como exemplo, o fato da função identidade poder ter qualquer tipo da forma AA seria formalizado no Sistema F como o julgamento

onde é uma variável de tipo . A caixa alta é tradicionalmente usada para denotar funções de nível de tipo, em oposição à caixa baixa que é usada para funções de nível de valor. (O sobrescrito significa que o x vinculado é do tipo ; a expressão após os dois pontos é o tipo da expressão lambda que a precede.)

Como um sistema de reescrita de termos , o Sistema F é fortemente normalizador . No entanto, a inferência de tipo no System F (sem anotações de tipo explícitas) é indecidível. Sob o isomorfismo de Curry-Howard , o Sistema F corresponde ao fragmento da lógica intuicionista de segunda ordem que usa apenas a quantificação universal. O sistema F pode ser visto como parte do cubo lambda , juntamente com cálculos lambda tipados ainda mais expressivos, incluindo aqueles com tipos dependentes .

De acordo com Girard, o "F" no Sistema F foi escolhido por acaso. [1]

regras de digitação

As regras de tipagem do Sistema F são aquelas do cálculo lambda simplesmente digitado com a adição do seguinte:

(1) (2)

onde são tipos, é uma variável de tipo e no contexto indica que está vinculado. A primeira regra é a da aplicação e a segunda é a da abstração. [2] [3]

Lógica e predicados

O tipo é definido como: , onde é uma variável de tipo . Isso significa: é o tipo de todas as funções que recebem como entrada um tipo α e duas expressões do tipo α, e produzem como saída uma expressão do tipo α (observe que consideramos ser associativa à direita .)

As duas definições a seguir para os valores booleanos e são usadas, estendendo a definição de booleanos da Igreja :

(Observe que as duas funções acima requerem três — não dois — argumentos. Os dois últimos devem ser expressões lambda, mas o primeiro deve ser um tipo. Esse fato é refletido no fato de que o tipo dessas expressões é ; o quantificador universal vincular o α corresponde ao Λ vincular o alfa na própria expressão lambda. Além disso, observe que é uma abreviação conveniente para , mas não é um símbolo do próprio Sistema F, mas sim um "meta-símbolo". Da mesma forma, e são também "meta-símbolos", abreviações convenientes, de "conjuntos" do Sistema F (no sentido Bourbaki); caso contrário, se tais funções pudessem ser nomeadas (dentro do Sistema F),então não haveria necessidade do aparato expressivo lambda capaz de definir funções anonimamente e para ocombinador de ponto fixo , que contorna essa restrição.)

Então, com esses dois termos, podemos definir alguns operadores lógicos (que são do tipo ):

Observe que nas definições acima, é um argumento de tipo para , especificando que os outros dois parâmetros fornecidos a são do tipo . Como nas codificações da Igreja, não há necessidade de uma função IFTHENELSE , pois pode-se usar apenas termos de tipo bruto como funções de decisão. No entanto, se for solicitado:

vai fazer. Um predicado é uma função que retorna um valor digitado. O predicado mais fundamental é ISZERO que retorna se e somente se seu argumento for o numeral 0 da Igreja :

Estruturas do Sistema F

O Sistema F permite que construções recursivas sejam incorporadas de maneira natural, semelhante à teoria dos tipos de Martin-Löf . Estruturas abstratas ( S ) são criadas usando construtores . Estas são funções digitadas como:

.

A recursividade se manifesta quando o próprio S aparece dentro de um dos tipos . Se você tiver m desses construtores, poderá definir o tipo de S como:

Por exemplo, os números naturais podem ser definidos como um tipo de dados indutivo N com construtores

O tipo System F correspondente a esta estrutura é . Os termos desse tipo compreendem uma versão datilografada dos numerais da Igreja , sendo os primeiros:

Se invertermos a ordem dos argumentos usados ​​( ou seja, ), então o numeral da Igreja para n é uma função que usa uma função f como argumento e retorna a enésima potência de f . Ou seja, um numeral Church é uma função de ordem superior – ele recebe uma função de argumento único f e retorna outra função de argumento único.

Uso em linguagens de programação

A versão do Sistema F usada neste artigo é como um cálculo tipificado explicitamente ou no estilo da Igreja. As informações de tipagem contidas nos termos λ simplificam a verificação de tipo . Joe Wells (1994) resolveu um "problema embaraçoso em aberto" ao provar que a verificação de tipo é indecidível para uma variante do Sistema F no estilo Curry, ou seja, uma que carece de anotações de digitação explícitas. [4] [5]

O resultado de Wells implica que a inferência de tipos para o Sistema F é impossível. Uma restrição do Sistema F conhecida como " Hindley–Milner ", ou simplesmente "HM", possui um algoritmo de inferência de tipo fácil e é usado para muitas linguagens de programação funcional estaticamente tipadas , como Haskell 98 e a família ML . Com o tempo, à medida que as restrições dos sistemas de tipos do estilo HM se tornaram aparentes, as línguas mudaram constantemente para lógicas mais expressivas para seus sistemas de tipos. GHC um compilador Haskell, vai além do HM (a partir de 2008) e usa o System F estendido com igualdade de tipo não sintática; [6] recursos não-HM no sistema de tipos do OCaml incluemGADT . [7] [8]

Isomorfismo de Girard-Reynolds

Na lógica intuicionista de segunda ordem , o cálculo lambda polimórfico de segunda ordem (F2) foi descoberto por Girard (1972) e independentemente por Reynolds (1974). [9] Girard provou o Teorema da Representação : que na lógica de predicados intuicionistas de segunda ordem (P2), as funções dos números naturais aos números naturais que podem ser provados totais, formam uma projeção de P2 em F2. [9] Reynolds provou o Teorema da Abstração : que todo termo em F2 satisfaz uma relação lógica, que pode ser embutida nas relações lógicas P2. [9] Reynolds provou que uma projeção de Girard seguida por uma incorporação de Reynolds formam a identidade, ou seja, o isomorfismo de Girard-Reynolds. [9]

Sistema F ω

Enquanto o Sistema F corresponde ao primeiro eixo do cubo lambda de Barendregt , o Sistema F ω ou o cálculo lambda polimórfico de ordem superior combina o primeiro eixo (polimorfismo) com o segundo eixo ( operadores de tipo ); é um sistema diferente, mais complexo.

O sistema F ω pode ser definido indutivamente em uma família de sistemas, onde a indução é baseada nos tipos permitidos em cada sistema:

  • permite tipos:
    • (o tipo de tipos) e
    • onde e (o tipo de funções de tipos para tipos, onde o tipo de argumento é de ordem inferior)

No limite, podemos definir o sistema como sendo

Ou seja, F ω é o sistema que permite funções de tipos em tipos onde o argumento (e resultado) pode ser de qualquer ordem.

Observe que, embora F ω não coloque restrições na ordem dos argumentos nesses mapeamentos, ele restringe o universo dos argumentos para esses mapeamentos: eles devem ser tipos em vez de valores. O Sistema F ω não permite mapeamentos de valores para tipos ( Tipos dependentes ), embora permita mapeamentos de valores para valores ( abstração), mapeamentos de tipos para valores ( abstração) e mapeamentos de tipos para tipos ( abstração no nível de tipos).

Sistema F <:

System F <: , pronunciado "F-sub", é uma extensão do sistema F com subtipagem . System F <: tem sido de importância central para a teoria da linguagem de programação desde a década de 1980 [ carece de fontes ] porque o núcleo das linguagens de programação funcional , como as da família ML , suporta tanto o polimorfismo paramétrico quanto a subtipagem de registros , que podem ser expressos no System F <: . [10] [11]

Veja também

Notas

  1. ^ Girard, Jean-Yves (1986). "O sistema F de tipos variáveis, quinze anos depois". Ciência da Computação Teórica . 45 : 160. doi : 10.1016/0304-3975(86)90044-7 . Entretanto, em [3] foi mostrado que as regras óbvias de conversão para este sistema, chamado por acaso de F, eram convergentes.
  2. ^ Harper R. "Fundamentos práticos para linguagens de programação, segunda edição" (PDF) . págs. 142–3.
  3. ^ Geuvers H, Nordström B, Dowek G. "Provas de Programas e Formalização da Matemática" (PDF) . pág. 51.
  4. ^ Wells, JB (2005-01-20). "Interesses de pesquisa de Joe Wells". Universidade Heriot-Watt.
  5. ^ Poços, JB (1999). "Tipabilidade e verificação de tipo no Sistema F são equivalentes e indecidíveis". Ana. Puro Aplic. Lógica . 98 (1–3): 111–156. doi : 10.1016/S0168-0072(98)00047-5 ."O Projeto da Igreja: tipabilidade e verificação de tipo no {S}sistema {F} são equivalentes e indecidíveis". 29 de setembro de 2007. Arquivado do original em 29 de setembro de 2007.
  6. ^ "Sistema FC: restrições de igualdade e coerções" . gitlab.haskell.org . Recuperado 2019-07-08 .
  7. ^ "Notas de versão do OCaml 4.00.1" . ocaml.org . 05/10/2012 . Recuperado 2019-09-23 .
  8. ^ "Manual de referência do OCaml 4.09" . 11/09/2012 . Recuperado 2019-09-23 .
  9. ^ abcd Philip Wadler (2005) The Girard-Reynolds Isomorphism (segunda edição) University of Edinburgh , Programming Languages ​​and Foundations at Edinburgh
  10. ^ Cardelli, Luca; Martini, Simone; Mitchell, John C.; Scedrov, André (1994). "Uma extensão do sistema F com subtipagem". Informação e Computação, vol. 9 . Holanda do Norte, Amsterdã. pp. 4–56. doi : 10.1006/inco.1994.1013 .
  11. ^ Pierce, Benjamin (2002). Tipos e linguagens de programação . Imprensa MIT. ISBN 978-0-262-16209-8., Capítulo 26: Quantificação limitada

Referências

  • Girard, Jean-Yves (1971). "Une Extension de l'Interpretation de Gödel à l'Analyse, et son Application à l'Elimination des Coupures dans l'Analyse et la Théorie des Types". Anais do Segundo Simpósio de Lógica Escandinavo . Amsterdã. pp. 63–92. doi :10.1016/S0049-237X(08)70843-7.
  • Girard, Jean-Yves (1972), Interpretation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur (tese de doutorado) (em francês), Université Paris 7.
  • Reynolds, John (1974). Rumo a uma teoria da estrutura de tipos (PDF) .
  • Girard, Jean-Yves; Lafont, Yves; TAYLOR, Paul (1989). Provas e tipos. Cambridge University Press. ISBN 978-0-521-37181-0.
  • Wells, JB (1994). "Tipabilidade e verificação de tipo no cálculo lambda de segunda ordem são equivalentes e indecidíveis". Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS) . pp. 176–185. doi : 10.1109/LICS.1994.316068. ISBN 0-8186-6310-3.versão pós-script

Leitura adicional

  • Pierce, Benjamim (2002). "V Polimorfismo Ch. 23. Tipos Universais, Ch. 25. Uma Implementação ML do Sistema F". Tipos e linguagens de programação . Imprensa MIT. pp. 339–362, 381–388. ISBN 0-262-16209-1.

links externos

  • Resumo do Sistema F por Franck Binard.
  • System Fω: o burro de carga dos compiladores modernos por Greg Morrisett