Sistema F - System F

O sistema F , também conhecido como cálculo lambda polimórfico ( Girard-Reynolds ) ou cálculo lambda de segunda ordem , é um cálculo lambda tipado que difere do cálculo lambda simplesmente tipado pela introdução de um mecanismo de quantificação universal sobre os tipos. O sistema F, portanto, formaliza a noção de polimorfismo paramétrico em linguagens de programação e forma uma base teórica para linguagens como Haskell e ML . O Sistema F foi descoberto de forma independente pelo lógico Jean-Yves Girard (1972) e pelo cientista da computação John C. Reynolds (1974).

Enquanto o cálculo lambda simplesmente digitado tem variáveis ​​que variam sobre os termos e fichários para eles, o Sistema F adicionalmente tem variáveis ​​que variam sobre os tipos e fichários para eles. A título de exemplo, o fato de a função de identidade poder ter qualquer tipo da forma A → A seria formalizado no Sistema F como o julgamento

${\ displaystyle \ vdash \ Lambda \ alpha. \ lambda x ^ {\ alpha} .x: \ forall \ alpha. \ alpha \ to \ alpha}$

onde é uma variável de tipo . O maiúsculo é tradicionalmente usado para denotar funções de nível de tipo, ao contrário do minúsculo que é usado para funções de nível de valor. (O sobrescrito significa que o limite x é do tipo ; a expressão após os dois pontos é o tipo da expressão lambda que o precede.) ${\ displaystyle \ alpha}$${\ displaystyle \ Lambda}$${\ displaystyle \ lambda}$${\ displaystyle \ alpha}$${\ displaystyle \ alpha}$

Como um sistema de reescrita de termos , o Sistema F está se normalizando fortemente . No entanto, a inferência de tipo no Sistema 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 quantificação universal. O sistema F pode ser visto como parte do cubo lambda , junto com cálculos lambda digitados ainda mais expressivos, incluindo aqueles com tipos dependentes .

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

Regras de digitação

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

${\ displaystyle {\ frac {\ Gamma \ vdash M {\ mathbin {:}} \ forall \ alpha. \ sigma} {\ Gamma \ vdash M \ tau {\ mathbin {:}} \ sigma [\ tau / \ alpha ]}}}$ (1)

${\ displaystyle {\ frac {\ Gamma, \ alpha ~ {\ text {type}} \ vdash M {\ mathbin {:}} \ sigma} {\ Gamma \ vdash \ Lambda \ alpha .M {\ mathbin {:} } \ forall \ alpha. \ sigma}}}$ (2)

onde são tipos, é uma variável de tipo e no contexto indica que está ligado. A primeira regra é a da aplicação e a segunda é a da abstração. ${\ displaystyle \ sigma, \ tau}$${\ displaystyle \ alpha}$${\ displaystyle \ alpha ~ {\ text {type}}}$${\ displaystyle \ alpha}$

Lógica e predicados

O tipo é definido como:, onde é uma variável de tipo . Isso significa: é o tipo de todas as funções que tomam 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 ). ${\ displaystyle {\ mathsf {Boolean}}}$${\ displaystyle \ forall \ alpha. \ alpha \ to \ alpha \ to \ alpha}$${\ displaystyle \ alpha}$${\ displaystyle {\ mathsf {Boolean}}}$${\ displaystyle \ to}$

As duas definições a seguir para os valores booleanos e são usadas, estendendo a definição de booleanos da Igreja : ${\ displaystyle \ mathbf {T}}$${\ displaystyle \ mathbf {F}}$

${\ displaystyle \ mathbf {T} = \ Lambda \ alpha {.} \ lambda x ^ {\ alpha} \ lambda y ^ {\ alpha} {.} x}$

${\ displaystyle \ mathbf {F} = \ Lambda \ alpha {.} \ lambda x ^ {\ alpha} \ lambda y ^ {\ alpha} {.} y}$

(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 se reflete no fato de que o tipo dessas expressões é ; o quantificador universal ligar o α corresponde a Λ ligando o alfa na própria expressão lambda. Além disso, observe que é uma abreviatura 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 de Bourbaki ); caso contrário, se tais funções pudessem ser nomeadas (dentro do Sistema F), então não haveria necessidade do aparelho lambda-expressivo capaz de definir funções anonimamente e para o combinador de ponto fixo , que contorna essa restrição.) ${\ displaystyle \ forall \ alpha. \ alpha \ to \ alpha \ to \ alpha}$${\ displaystyle {\ mathsf {Boolean}}}$${\ displaystyle \ forall \ alpha. \ alpha \ to \ alpha \ to \ alpha}$${\ displaystyle \ mathbf {T}}$${\ displaystyle \ mathbf {F}}$

Então, com esses dois termos , podemos definir alguns operadores lógicos (que são do tipo ): ${\ displaystyle \ lambda}$${\ displaystyle {\ mathsf {Boolean}} \ rightarrow {\ mathsf {Boolean}} \ rightarrow {\ mathsf {Boolean}}}$

${\ displaystyle {\ begin {align} \ mathrm {AND} & = \ lambda x ^ {\ mathsf {Boolean}} \ lambda y ^ {\ mathsf {Boolean}} {.} x \, {\ mathsf {Boolean} } \, y \, \ mathbf {F} \\\ mathrm {OR} & = \ lambda x ^ {\ mathsf {Booleano}} \ lambda y ^ {\ mathsf {Booleano}} {.} x \, {\ mathsf {Boolean}} \, \ mathbf {T} \, y \\\ mathrm {NOT} & = \ lambda x ^ {\ mathsf {Boolean}} {.} x \, {\ mathsf {Boolean}} \, \ mathbf {F} \, \ mathbf {T} \ end {alinhado}}}$

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 do tipo bruto como funções de decisão. No entanto, se for solicitado: ${\ displaystyle {\ mathsf {Boolean}}}$${\ displaystyle x}$${\ displaystyle x}$${\ displaystyle {\ mathsf {Boolean}}}$${\ displaystyle {\ mathsf {Boolean}}}$

${\ displaystyle \ mathrm {IFTHENELSE} = \ Lambda \ alpha. \ lambda x ^ {\ mathsf {Booleano}} \ lambda y ^ {\ alpha} \ lambda z ^ {\ alpha} .x \ alpha yz}$

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 de Igreja 0 : ${\ displaystyle {\ mathsf {Boolean}}}$${\ displaystyle \ mathbf {T}}$

${\ displaystyle \ mathrm {ISZERO} = \ lambda n ^ {\ forall \ alpha. (\ alpha \ rightarrow \ alpha) \ rightarrow \ alpha \ rightarrow \ alpha} {.} n \, {\ mathsf {Booleano}} \ , (\ lambda x ^ {\ mathsf {Booleano}} {.} \ mathbf {F}) \, \ mathbf {T}}$

Estruturas do sistema F

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

${\ displaystyle K_ {1} \ rightarrow K_ {2} \ rightarrow \ dots \ rightarrow S}$.

A recursividade é manifestada quando ela mesma aparece em um dos tipos . Se você tiver um desses construtores, poderá definir o tipo de como: ${\ displaystyle S}$${\ displaystyle K_ {i}}$${\ displaystyle m}$${\ displaystyle S}$

${\ displaystyle \ forall \ alpha. (K_ {1} ^ {1} [\ alpha / S] \ rightarrow \ dots \ rightarrow \ alpha) \ dots \ rightarrow (K_ {1} ^ {m} [\ alpha / S ] \ rightarrow \ dots \ rightarrow \ alpha) \ rightarrow \ alpha}$

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

${\ displaystyle {\ mathit {zero}}: \ mathrm {N}}$

${\ displaystyle {\ mathit {succ}}: \ mathrm {N} \ rightarrow \ mathrm {N}}$

O tipo de sistema F correspondente a esta estrutura é . Os termos deste tipo compreendem uma versão digitada dos numerais da Igreja , os primeiros dos quais são: ${\ displaystyle \ forall \ alpha. \ alpha \ to (\ alpha \ to \ alpha) \ to \ alpha}$

{{{1}}}${\ displaystyle \ Lambda \ alpha. \ lambda x ^ {\ alpha}. \ lambda f ^ {\ alpha \ to \ alpha} .x}$

{{{1}}}${\ displaystyle \ Lambda \ alpha. \ lambda x ^ {\ alpha}. \ lambda f ^ {\ alpha \ to \ alpha} .fx}$

{{{1}}}${\ displaystyle \ Lambda \ alpha. \ lambda x ^ {\ alpha}. \ lambda f ^ {\ alpha \ to \ alpha} .f (fx)}$

{{{1}}}${\ displaystyle \ Lambda \ alpha. \ lambda x ^ {\ alpha}. \ lambda f ^ {\ alpha \ to \ alpha} .f (f (fx))}$

Se invertermos a ordem dos argumentos curry ( isto é, ), então o numeral da Igreja para é uma função que recebe uma função f como argumento e retorna a ^ésima potência de f . Ou seja, um numeral de Igreja é uma função de ordem superior - ela recebe uma função f de argumento único e retorna outra função de argumento único. ${\ displaystyle \ forall \ alpha. (\ alpha \ rightarrow \ alpha) \ rightarrow \ alpha \ rightarrow \ alpha}$${\ displaystyle n}$${\ displaystyle n}$

Use em linguagens de programação

A versão do Sistema F usada neste artigo é um cálculo explicitamente digitado ou no estilo de Church. As informações de digitação contidas em termos λ tornam a verificação de tipo direta. Joe Wells (1994) resolveu um "embaraçoso problema aberto" provando 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.

O resultado de Wells implica que a inferência de tipo para o Sistema F é impossível. Uma restrição do Sistema F conhecida como " Hindley-Milner ", ou simplesmente "HM", tem um algoritmo de inferência de tipo fácil e é usada para muitas linguagens de programação funcional de tipo estático , como Haskell 98 e a família ML . Com o tempo, à medida que as restrições dos sistemas de tipos de estilo HM se tornaram aparentes, as linguagens 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 Sistema F estendido com igualdade de tipo não sintática; recursos não-HM no sistema de tipos do OCaml incluem GADT .

O 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). Girard provou o Teorema da Representação : que na lógica dos predicados intuicionistas de segunda ordem (P2), as funções dos números naturais para os números naturais que podem ser provados totais formam uma projeção de P2 para F2. 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. Reynolds provou que uma projeção de Girard seguida por uma incorporação de Reynolds forma a identidade, ou seja, o isomorfismo de Girard-Reynolds .

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 e 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:

• ${\ displaystyle F_ {n}}$ permite tipos:
  • ${\ displaystyle \ star}$ (o tipo de tipos) e
  • ${\ displaystyle J \ Rightarrow K}$onde e (o tipo de funções de tipos para tipos, onde o tipo de argumento é de uma ordem inferior)${\ displaystyle J \ in F_ {n-1}}$${\ displaystyle K \ in F_ {n}}$

No limite, podemos definir o sistema para ser ${\ displaystyle F _ {\ omega}}$

• ${\ displaystyle F _ {\ omega} = {\ underset {1 \ leq i} {\ bigcup}} F_ {i}}$

Ou seja, F _ω é o sistema que permite funções de tipos a tipos onde o argumento (e o resultado) podem 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 ) ${\ displaystyle \ lambda}$${\ displaystyle \ Lambda}$${\ displaystyle \ lambda}$

Veja também

• Tipos existenciais - as contrapartes quantificadas existencialmente de tipos universais
• Sistema F _<: - estende o sistema F com subtipagem
• System U

Notas

Referências

Leitura adicional

• Pierce, Benjamin (2002). "V Polymorphism Ch. 23. Universal Types, Ch. 25. An ML Implementation of System F" . Tipos e linguagens de programação . MIT Press. pp. 339-362, 381-388. ISBN 0-262-16209-1.

links externos

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