Sistema F

O sistema F é um formalismo lógico que torna possível expressar funções de uma forma muito rica e rigorosa e demonstrar formalmente propriedades difíceis. Especificamente, o sistema F (também conhecido como cálculo polimórfico lambda ou cálculo lambda de segunda ordem ) é uma extensão do cálculo lambda simplesmente digitada, introduzida de forma independente pelo lógico Jean-Yves Girard e pelo cientista da computação John C. Reynolds . Este sistema se distingue do lambda-cálculo simplesmente tipado pela existência de uma quantificação universal dos tipos que torna possível expressar o polimorfismo.

O Sistema F tem duas propriedades cruciais:

1. a redução de termos é fortemente normalizadora (de forma mais direta: todos os cálculos terminam);
2. ela corresponde por correspondência Curry-Howard à lógica mínimo proposicional a segunda ordem . Quer dizer: o cálculo proposicional, sem a negação mas com os quantificadores .

Nota introdutória  : A leitura deste artigo pressupõe a leitura preliminar do artigo "  lambda-cálculo  " e sua assimilação.

Introdução

Como atesta sua origem dupla, o sistema F pode ser estudado em dois contextos muito diferentes:

• No campo da programação funcional, onde surge como uma extensão muito expressiva do núcleo da linguagem ML. Sua expressividade é ilustrada pelo fato de que os tipos de dados comuns (booleanos, inteiros, listas, etc.) são definíveis no sistema F a partir das construções básicas;

• No campo da lógica e, mais particularmente, da teoria da prova. Por meio da correspondência Curry-Howard , o sistema F é de fato isomórfico à lógica mínima de segunda ordem. Além disso, esse sistema captura exatamente a classe de funções numéricas cuja existência pode ser comprovada na aritmética intuicionista de segunda ordem (às vezes chamada de análise intuicionista ). Além disso, é esta propriedade notável do sistema F que motivou historicamente a sua introdução por Jean-Yves Girard, na medida em que esta propriedade permite resolver o problema da eliminação de cortes na aritmética de segunda ordem, conjecturado por Takeuti  (in) .

Historicamente, o sistema F desempenhou um papel essencial nos fundamentos da ciência da computação ao propor, desde o início da década de 1970, um formalismo de tipo rico, simples e muito expressivo de funções calculáveis ​​muito gerais. Ele abriu o caminho para linguagens de programação digitadas modernas e assistentes de prova como COQ .

Como o cálculo lambda simplesmente digitado, o sistema F admite duas apresentações equivalentes:

• Uma apresentação à Igreja , em que cada termo contém todas as anotações de tipo necessárias para a reconstrução de seu tipo (inequivocamente);

• Uma apresentação à la Curry , do cientista da computação Daniel Leivant, em que os termos (que são os do lambda-cálculo puro) são desprovidos de qualquer tipo de anotação e, portanto, sujeitos aos problemas da ambigüidade típica.

Apresentação na Igreja

O sistema F admite dois tipos de objetos: tipos e termos . Os termos podem ser "recolhidos" e traduzir funções computáveis, enquanto os tipos anotam os termos e permitem que sejam categorizados.

A sintaxe

O tipo de sistema de F (denotado , , , etc.) são formados a partir de um conjunto de tipos de variáveis (classificado , , etc.) utilizando os seguintes três regras de construção: NO{\ displaystyle A}B{\ displaystyle B}VS{\ displaystyle C}α{\ displaystyle \ alpha}β{\ displaystyle \ beta}γ{\ displaystyle \ gamma}

• ( Variável de tipo ) Se for uma variável de tipo, então é um tipo;α{\ displaystyle \ alpha}α{\ displaystyle \ alpha}
• ( Tipo de seta ) Se e são tipos, então é um tipo;NO{\ displaystyle A}B{\ displaystyle B}NO→B{\ displaystyle A \ a B}
• ( Tipo universal ) Se for uma variável de tipo e um tipo, então é um tipo.α{\ displaystyle \ alpha}B{\ displaystyle B}∀α B{\ displaystyle \ forall \ alpha ~ B}

Em resumo, os tipos do sistema F são dados pela gramática BNF  :

NO,B  :: =  α  |  NO→B  |  ∀α B.{\ displaystyle A, B ~~ :: = ~~ \ alpha ~~ | ~~ A \ to B ~~ | ~~ \ forall \ alpha ~ B.}

Como em lambda-calculus ou em cálculo de predicado, a presença de um símbolo mutante requer distinguir as noções de variável livre e variável ligada , e introduzir os mecanismos usuais de renomeação que permitem trabalhar até a -conversão. Finalmente, a álgebra de tipo do sistema F é dotada de uma operação de substituição semelhante à do cálculo lambda, e denotamos o tipo obtido substituindo no tipo todas as ocorrências livres da variável de tipo pelo tipo . ∀{\ displaystyle \ forall}α{\ displaystyle \ alpha}B{α: =NO}{\ displaystyle B \ {\ alpha: = A \}}B{\ displaystyle B}α{\ displaystyle \ alpha}NO{\ displaystyle A}

Os termos (bruto) Sistema F (classificado , etc.) são formados a partir de um conjunto de termos de variáveis (denotado , , , etc.), utilizando as cinco seguintes regras de construção: M{\ displaystyle M}NÃO{\ displaystyle N}x{\ displaystyle x}y{\ displaystyle y}z{\ displaystyle z}

• ( Variável ) Se for uma variável de termo, então é um termo;x{\ displaystyle x}x{\ displaystyle x}
• ( Abstração ) Se for uma variável de termo, um tipo e um termo, então é um termo;x{\ displaystyle x}NO{\ displaystyle A}M{\ displaystyle M}λx:NO.M{\ displaystyle \ lambda x: AM}
• ( Aplicação ) Se e forem termos, então é um termo;M{\ displaystyle M}NÃO{\ displaystyle N}MNÃO{\ displaystyle MN}
• ( Abstração de tipo ) Se for uma variável de tipo e um termo, então é um termo;α{\ displaystyle \ alpha}M{\ displaystyle M}Λα.M{\ displaystyle \ Lambda \ alpha .M}
• ( Tipo de aplicação ) Se for um termo e um tipo, será um termo.M{\ displaystyle M}NO{\ displaystyle A}MNO{\ displaystyle MA}

Em resumo, os termos (brutos) do sistema F são dados pela gramática BNF:

M,NÃO  :: =  x  |  λx:NO.M  |  MNÃO  |  Λα.M  |  MNO.{\ displaystyle M, N ~~ :: = ~~ x ~~ | ~~ \ lambda x \, {:} \, A \ ,. \, M ~~ | ~~ MN ~~ | ~~ \ Lambda \ alpha \ ,. \, M ~~ | ~~ MA.}

Os termos do sistema F incorporam dois mecanismos de ligação variável: um mecanismo de ligação variável de termo (por construção ) e um mecanismo de ligação variável de tipo (por construção ), os quais são levados em consideração no nível da relação de conversão. Esse mecanismo duplo dá origem naturalmente a duas operações de substituição: uma substituição de termo anotada e uma substituição de tipo anotada . λx:NO.M{\ displaystyle \ lambda x \, {:} \, A \ ,. \, M}Λα.M{\ displaystyle \ Lambda \ alpha \ ,. \, M}α{\ displaystyle \ alpha}M{x: =NÃO}{\ displaystyle M \ {x: = N \}}M{α: =NO}{\ displaystyle M \ {\ alpha: = A \}}

A -reduçãoβ{\ displaystyle \ beta}

A presença de um duplo mecanismo de abstração e aplicação (abstração / aplicação de termo e abstração / aplicação de tipo) dá origem a duas regras de -redução, cuja união gera passando para o contexto a relação de -redução em uma etapa do sistema F: β{\ displaystyle \ beta}β{\ displaystyle \ beta}

• (λx:NO.M)NÃO⟶M{x: =NÃO}{\ displaystyle (\ lambda x \, {:} \, A \ ,. \, M) N \ longrightarrow M \ {x: = N \}} ;
• (Λα.M)NO⟶M{α: =NO}{\ displaystyle (\ Lambda \ alpha \ ,. \, M) A \ longrightarrow M \ {\ alpha: = A \}}.

Quanto ao cálculo lambda puro, a -redução do sistema F é confluente (nos termos brutos) e satisfaz a propriedade de Church-Rosser  : β{\ displaystyle \ beta}

• (Confluência de -redução) Se e , então existe um termo tal que e  ;β{\ displaystyle \ beta}M⟶∗M1{\ displaystyle M \ longrightarrow ^ {*} M_ {1}}M⟶∗M2{\ displaystyle M \ longrightarrow ^ {*} M_ {2}}M′{\ displaystyle M '}M1⟶∗M′{\ displaystyle M_ {1} \ longrightarrow ^ {*} M '}M2⟶∗M′{\ displaystyle M_ {2} \ longrightarrow ^ {*} M '}
• (Propriedade de Church-Rosser) Para dois termos e para ser convertível, é necessário e suficiente que exista um termo como e .M1{\ displaystyle M_ {1}}M2{\ displaystyle M_ {2}}β{\ displaystyle \ beta}M′{\ displaystyle M '}M1⟶∗M′{\ displaystyle M_ {1} \ longrightarrow ^ {*} M '}M2⟶∗M′{\ displaystyle M_ {2} \ longrightarrow ^ {*} M '}

O sistema de tipo

Chamado contexto tipagem (notação: , etc) qualquer lista finita de enunciados da forma (que é um termo variável e tipo) em que uma variável termo é declarado mais do que uma vez. Γ{\ displaystyle \ Gamma}Γ′{\ displaystyle \ Gamma '}x:NO{\ displaystyle x: A}x{\ displaystyle x}NO{\ displaystyle A}

O sistema de tipo do sistema F é construído em torno de um julgamento de digitação do formulário ("no contexto , o termo tem para tipo  "), que é definido a partir das seguintes regras de inferência: Γ⊢M:NO{\ displaystyle \ Gamma \ vdash M: A}Γ{\ displaystyle \ Gamma}M{\ displaystyle M}NO{\ displaystyle A}

• ( Axioma ) se  ;Γ⊢x:NO{\ displaystyle {\ frac {} {\ Gamma \ vdash x: A}}}(x:NO)∈Γ{\ displaystyle (x: A) \ in \ Gamma}

• ( -intro )  ;→{\ displaystyle \ to}Γ,x:NO⊢M:BΓ⊢λx:NO.M:NO→B{\ displaystyle {\ frac {\ Gamma, x: A \ vdash M: B} {\ Gamma \ vdash \ lambda x \, {:} \, A \ ,. \, M: A \ to B}}}

• ( -elim )  ;→{\ displaystyle \ to}Γ⊢M:NO→BΓ⊢NÃO:NOΓ⊢MNÃO:B{\ displaystyle {\ frac {\ Gamma \ vdash M: A \ to B \ quad \ Gamma \ vdash N: A} {\ Gamma \ vdash MN: B}}}

• ( -intro ) se não tiver ocorrência livre em  ;∀{\ displaystyle \ forall}Γ⊢M:BΓ⊢Λα.M:∀α B{\ displaystyle {\ frac {\ Gamma \ vdash M: B} {\ Gamma \ vdash \ Lambda \ alpha \ ,. \, M: \ forall \ alpha ~ B}}}α{\ displaystyle \ alpha}Γ{\ displaystyle \ Gamma}

• ( -elim ) .∀{\ displaystyle \ forall}Γ⊢M:∀α BΓ⊢MNO:B{α: =NO}{\ displaystyle {\ frac {\ Gamma \ vdash M: \ forall \ alpha ~ B} {\ Gamma \ vdash MA: B \ {\ alpha: = A \}}}}

As duas propriedades principais deste sistema de tipo são a propriedade de preservação do tipo de reduçãoβ{\ displaystyle \ beta} e a propriedade de normalização forte  :

• ( Preservação do tipo por redução ) Se e se , então  ;Γ⊢M:NO{\ displaystyle \ Gamma \ vdash M: A}M⟶∗M′{\ displaystyle M \ longrightarrow ^ {*} M '}Γ⊢M′:NO{\ displaystyle \ Gamma \ vdash M ': A}

• ( Normalização forte ) Se , então é fortemente normalizável.Γ⊢M:NO{\ displaystyle \ Gamma \ vdash M: A}M{\ displaystyle M}

A primeira dessas duas propriedades é uma propriedade puramente combinatória que é demonstrada por uma indução direta na derivação de tipagem. Por outro lado, a propriedade de normalização forte do sistema F é uma propriedade cuja prova se baseia fundamentalmente em métodos não combinatórios, baseados na noção de redutibilidade candidata.

Representação de tipos de dados

Para poder usar o lambda-cálculo simplesmente digitado como linguagem de programação, é necessário adicionar tipos básicos (booleanos, inteiros, etc.) e regras de redução adicionais que ampliam o poder expressivo do formalismo. Um exemplo de tal extensão é o sistema T de Gödel, que é obtido adicionando aos inteiros naturais primitivos lambda-calculus simplesmente digitados e um mecanismo de recursão semelhante à recursão primitiva (mas mais expressivo).

No sistema F, tal extensão não é necessária porque a expressividade do formalismo permite definir os tipos básicos e os construtores de tipo usuais sem que seja necessário modificar o sistema de tipos ou as regras de redução.

Booleanos e tipos finitos

O tipo de booleanos é definido no sistema F por

• Bool ≡ ∀γ(γ→γ→γ){\ displaystyle {\ textbf {Bool}} ~ \ equiv ~ \ forall \ gamma \, (\ gamma \ to \ gamma \ to \ gamma)}

e as constantes e por: verdadeiro{\ displaystyle {\ textbf {true}}}falso{\ displaystyle {\ textbf {false}}}

• verdadeiro ≡ Λγ.λx,y:γ.x : Bool{\ displaystyle {\ textbf {true}} ~ \ equiv ~ \ Lambda \ gamma \ ,. \, \ lambda x, y \, {:} \, \ gamma \ ,. \, x ~: ~ {\ textbf { Bool}}} ;
• falso ≡ Λγ.λx,y:γ.y : Bool{\ displaystyle {\ textbf {false}} ~ \ equiv ~ \ Lambda \ gamma \ ,. \, \ lambda x, y \, {:} \, \ gamma \ ,. \, y ~: ~ {\ textbf { Bool}}}.

Pode-se mostrar que os dois termos acima são os únicos dois termos fechados na forma normal do tipo . Assim, o tipo de dados captura efetivamente a noção de booleano. Bool{\ displaystyle {\ textbf {Bool}}}Bool{\ displaystyle {\ textbf {Bool}}}

A construção 'if ... then ... else ...' é definida por

• teixoVS M então NÃO1 senão NÃO2 ≡ MVSNÃO1NÃO2{\ displaystyle {\ texttt {if}} _ {C} ~ M ~ {\ texttt {then}} ~ N_ {1} ~ {\ texttt {else}} ~ N_ {2} ~ \ equiv ~ MCN_ {1} N_ {2}}

onde designa o tipo de eliminação da construção 'se ...', ou seja, o tipo comum aos dois ramos da condicional. Esta definição é correta do ponto de vista de digitação e do ponto de vista computacional na medida em que: VS{\ displaystyle C}

• Em qualquer contexto onde o termo tenha o tipo e onde os termos e tenham o tipo , a construção é bem tipificada e tem o tipo como seu tipo  ;M{\ displaystyle M}Bool{\ displaystyle {\ textbf {Bool}}}NÃO1{\ displaystyle N_ {1}}NÃO2{\ displaystyle N_ {2}}VS{\ displaystyle C}teixoVS M então NÃO1 senão NÃO2{\ displaystyle {\ texttt {if}} _ {C} ~ M ~ {\ texttt {then}} ~ N_ {1} ~ {\ texttt {else}} ~ N_ {2}}VS{\ displaystyle C}
• Se o prazo se reduz a , então a construção se reduz a  ;M{\ displaystyle M \, \!}verdadeiro{\ displaystyle {\ textbf {true}}}teixoVS M então NÃO1 senão NÃO2{\ displaystyle {\ texttt {if}} _ {C} ~ M ~ {\ texttt {then}} ~ N_ {1} ~ {\ texttt {else}} ~ N_ {2}}NÃO1{\ displaystyle N_ {1} \, \!}
• Se o prazo se reduz a , então a construção se reduz a .M{\ displaystyle M \, \!}falso{\ displaystyle {\ textbf {false}}}teixoVS M então NÃO1 senão NÃO2{\ displaystyle {\ texttt {if}} _ {C} ~ M ~ {\ texttt {then}} ~ N_ {1} ~ {\ texttt {else}} ~ N_ {2}}NÃO2{\ displaystyle N_ {2} \, \!}

De forma mais geral, pode-se definir um tipo finito com valores colocando: Enão{\ displaystyle E_ {n}}não{\ displaystyle n}e1,...,enão{\ displaystyle e_ {1}, \ ldots, e_ {n}}

• Enão ≡ ∀γ(γ→⋯→γ⏟não→γ){\ displaystyle E_ {n} ~ \ equiv ~ \ forall \ gamma \, (\ underbrace {\ gamma \ to \ cdots \ to \ gamma} _ {n} \ to \ gamma)} ;
• eeu ≡ Λγ.λx1,...,xnão:γ.xeu{\ displaystyle e_ {i} ~ \ equiv ~ \ Lambda \ gamma \ ,. \, \ lambda x_ {1}, \ ldots, x_ {n} \, {:} \, \ gamma \ ,. \, x_ { eu}}(para tudo ).1≤eu≤não{\ displaystyle 1 \ leq i \ leq n}

Novamente, pode ser mostrado que os termos são os únicos termos fechados na forma de tipo normal . A operação de filtragem correspondente é definida por: e1,...,enão{\ displaystyle e_ {1}, \ ldots, e_ {n}}Enão{\ displaystyle E_ {n}}

• partidaVS M com e1↦NÃO1|⋯|enão↦NÃOnão ≡ MVSNÃO1⋯NÃOnão{\ displaystyle {\ texttt {match}} _ {C} ~ M ~ {\ texttt {with}} ~ e_ {1} \ mapsto N_ {1} | \ cdots | e_ {n} \ mapsto N_ {n} ~ \ equiv ~ M \, C \, N_ {1} \ cdots N_ {n}}

(onde designa o tipo de ramificações do filtro). VS{\ displaystyle C}

Em particular :

• E2 ≡ ∀γ(γ→γ→γ) ≡ Bool{\ displaystyle E_ {2} ~ \ equiv ~ \ forall \ gamma \, (\ gamma \ to \ gamma \ to \ gamma) ~ \ equiv ~ {\ textbf {Bool}}} (tipo de booleanos);
• E1 ≡ ∀γ(γ→γ) ≡ Unidade{\ displaystyle E_ {1} ~ \ equiv ~ \ forall \ gamma \, (\ gamma \ to \ gamma) ~ \ equiv ~ {\ textbf {Unit}}} (tipo singleton);
• E0 ≡ ∀γγ ≡ Vazio{\ displaystyle E_ {0} ~ \ equiv ~ \ forall \ gamma \, \ gamma ~ \ equiv ~ {\ textbf {Vazio}}} (tipo vazio).

O tipo não é habitado por nenhum termo fechado na forma normal e, de acordo com o teorema de normalização forte, não é habitado por nenhum termo fechado. E0{\ displaystyle E_ {0}}

Produto cartesiano e soma direta

Um e dois tipos. O produto cartesiano é definido no sistema F por NO{\ displaystyle A}B{\ displaystyle B} NO×B{\ displaystyle A \ times B}

• NO×B ≡ ∀γ((NO→B→γ)→γ){\ displaystyle A \ times B ~ \ equiv ~ \ forall \ gamma \, ((A \ to B \ to \ gamma) \ to \ gamma)}

e a construção do casal por

• ⟨M;NÃO⟩ ≡ Λγ.λf:(NO→B→γ).fMNÃO : NO×B{\ displaystyle \ langle M; N \ rangle ~ \ equiv ~ \ Lambda \ gamma \ ,. \, \ lambda f \, {:} \, (A \ to B \ to \ gamma) \ ,. \, f \ , M \, N ~: ~ A \ vezes B}(se e )M:NO{\ displaystyle M: ​​A \, \!}NÃO:B{\ displaystyle N: B \, \!}

Quanto aos tipos enumerados, pode-se mostrar que os únicos termos fechados na forma normal do tipo são da forma , onde e são termos fechados na forma normal do tipo e , respectivamente. As funções de projeção correspondentes são fornecidas por NO×B{\ displaystyle A \ times B}⟨M;NÃO⟩{\ displaystyle \ langle M; N \ rangle}M{\ displaystyle M}NÃO{\ displaystyle N}NO{\ displaystyle A}B{\ displaystyle B}

• primeiro ≡ Λα,β.λp:(α×β).pα(λx:α.λy:β.x) : ∀α,β(α×β→α){\ displaystyle {\ textbf {fst}} ~ \ equiv ~ \ Lambda \ alpha, \ beta \ ,. \, \ lambda p \, {:} \, (\ alpha \ times \ beta) \ ,. \, p \, \ alpha \, (\ lambda x \, {:} \, \ alpha \ ,. \, \ lambda y \, {:} \, \ beta \ ,. \, x) ~: ~ \ forall \ alpha , \ beta \, (\ alpha \ times \ beta \ to \ alpha)}
• snd ≡ Λα,β.λp:(α×β).pβ(λx:α.λy:β.y) : ∀α,β(α×β→β){\ displaystyle {\ textbf {snd}} ~ \ equiv ~ \ Lambda \ alpha, \ beta \ ,. \, \ lambda p \, {:} \, (\ alpha \ times \ beta) \ ,. \, p \, \ beta \, (\ lambda x \, {:} \, \ alpha \ ,. \, \ lambda y \, {:} \, \ beta \ ,. \, y) ~: ~ \ forall \ alpha , \ beta \, (\ alpha \ times \ beta \ to \ beta)}

Essas funções verificam naturalmente as igualdades e . primeiroNOB⟨M;NÃO⟩=M{\ displaystyle {\ textbf {fst}} \, A \, B \, \ langle M; N \ rangle = M}sndNOB⟨M;NÃO⟩=NÃO{\ displaystyle {\ textbf {snd}} \, A \, B \, \ langle M; N \ rangle = N}

A soma direta é definida por NO+B{\ displaystyle A + B}

• NO+B ≡ ∀γ((NO→γ)→(B→γ)→γ){\ displaystyle A + B ~ \ equiv ~ \ forall \ gamma \, ((A \ to \ gamma) \ to (B \ to \ gamma) \ to \ gamma)}

Os habitantes dos tipos e são imersos no tipo com a ajuda das construções NO{\ displaystyle A}B{\ displaystyle B}NO+B{\ displaystyle A + B}

• inl(M) ≡ Λγ.λf:(NO→γ).λg:(B→γ).fM : NO+B{\ displaystyle {\ textbf {inl}} (M) ~ \ equiv ~ \ Lambda \ gamma \ ,. \, \ lambda f \, {:} \, (A \ to \ gamma) \ ,. \, \ lambda g \, {:} \, (B \ to \ gamma) \ ,. \, f \, M ~: ~ A + B}(se )M:NO{\ displaystyle M: ​​A \, \!}
• em R(M) ≡ Λγ.λf:(NO→γ).λg:(B→γ).gM : NO+B{\ displaystyle {\ textbf {inr}} (M) ~ \ equiv ~ \ Lambda \ gamma \ ,. \, \ lambda f \, {:} \, (A \ to \ gamma) \ ,. \, \ lambda g \, {:} \, (B \ to \ gamma) \ ,. \, g \, M ~: ~ A + B}(se )M:B{\ displaystyle M: ​​B \, \!}

enquanto a filtragem de elementos de tipo é fornecida pela construção NO+B{\ displaystyle A + B}

• partida NÃO com inl(x)↦M1 | em R(y)↦M2 ≡ NÃOVS(λx:NO.M1)(λy:B.M2){\ displaystyle {\ texttt {match}} ~ N ~ {\ texttt {with}} ~ {\ textbf {inl}} (x) \ mapsto M_ {1} ~ | ~ {\ textbf {inr}} (y) \ mapsto M_ {2} ~ \ equiv ~ N \, C \, (\ lambda x \, {:} \, A \ ,. \, M_ {1}) \, (\ lambda y \, {:} \ , B \ ,. \, M_ {2})}

que satisfaz a igualdade de definição esperada.

Ao contrário do produto cartesiano, a codificação da soma direta no sistema F nem sempre captura a noção de união disjunta, na medida em que é possível, em certos casos, construir termos fechados em forma normal de tipo que não são nem da forma (com ) nem da forma (com ) . NO+B{\ displaystyle A + B}inl(M){\ displaystyle {\ textbf {inl}} (M)}M:NO{\ displaystyle M: ​​A}em R(M){\ displaystyle {\ textbf {inr}} (M)}M:B{\ displaystyle M: ​​B}

Inteiros da igreja

O tipo de inteiros da Igreja é definido no sistema F por

• NÃOnot ≡ ∀γ(γ→(γ→γ)→γ){\ displaystyle \ mathbf {Nat} ~ \ equiv ~ \ forall \ gamma \, (\ gamma \ to (\ gamma \ to \ gamma) \ to \ gamma)}

Cada número natural é representado pelo termo não{\ displaystyle n}

• não¯ ≡ Λγλx:γ.λf:(γ→γ).f(⋯(f⏟nãox)⋯) : NÃOnot{\ displaystyle {\ bar {n}} ~ \ equiv ~ \ Lambda \ gamma \, \ lambda x \, {:} \, \ gamma \ ,. \, \ lambda f \, {:} \, (\ gamma \ to \ gamma) \ ,. \, \ underbrace {f (\ cdots (f} _ {n} \, x) \ cdots) ~: ~ \ mathbf {Nat}}

Quanto aos booleanos, o tipo captura a noção de inteiro natural, pois qualquer termo fechado de tipo na forma normal tem a forma de um certo inteiro natural . NÃOnot{\ displaystyle \ mathbf {Nat}}NÃOnot{\ displaystyle \ mathbf {Nat}}não¯{\ displaystyle {\ bar {n}}}não{\ displaystyle n}

Apresentação no Curry

A função de apagar

• |x|=x{\ displaystyle | x | = x}
• |λx:NO.M|=λx.|M|{\ displaystyle | \ lambda x: AM | = \ lambda x. | M |}
• |MNÃO|=|M||NÃO|{\ displaystyle | MN | = | M || N |}
• |Λα.M|=|M|{\ displaystyle | \ Lambda \ alpha .M | = | M |}
• |MNO|=|M|{\ displaystyle | MA | = | M |}

O sistema de tipo

• ( Axioma ) seΓ⊢x:NO{\ displaystyle {\ frac {} {\ Gamma \ vdash x: A}}}(x:NO)∈Γ{\ displaystyle (x: A) \ in \ Gamma}

• ( -intro )→{\ displaystyle \ to}Γ,x:NO⊢M:BΓ⊢λx.M:NO→B{\ displaystyle {\ frac {\ Gamma, x: A \ vdash M: B} {\ Gamma \ vdash \ lambda xM: A \ to B}}}

• ( -elim )→{\ displaystyle \ to}Γ⊢M:NO→BΓ⊢NÃO:NOΓ⊢MNÃO:B{\ displaystyle {\ frac {\ Gamma \ vdash M: A \ to B \ quad \ Gamma \ vdash N: A} {\ Gamma \ vdash MN: B}}}

• ( -intro ) se não tiver ocorrência livre em∀{\ displaystyle \ forall}Γ⊢M:BΓ⊢M:∀α B{\ displaystyle {\ frac {\ Gamma \ vdash M: B} {\ Gamma \ vdash M: \ forall \ alpha ~ B}}}α{\ displaystyle \ alpha}Γ{\ displaystyle \ Gamma}

• ( -elim ) .∀{\ displaystyle \ forall}Γ⊢M:∀α BΓ⊢M:B{α: =NO}{\ displaystyle {\ frac {\ Gamma \ vdash M: \ forall \ alpha ~ B} {\ Gamma \ vdash M: B \ {\ alpha: = A \}}}}

Equivalência entre os dois sistemas

O teorema de normalização forte

Os termos tipáveis ​​do sistema F são fortemente normalizáveis , ou seja, a redução dos termos é uma operação que sempre termina produzindo uma forma normal.

Correspondência com lógica de segunda ordem

Por meio da correspondência Curry-Howard , o sistema F corresponde exatamente à lógica mínima de segunda ordem , cujas fórmulas são construídas a partir de variáveis ​​proposicionais usando implicação e quantificação proposicional:

NO,B  : =  α  |  NO⇒B  |  ∀αB{\ displaystyle A, B ~~: = ~~ \ alpha ~~ | ~~ A \ Rightarrow B ~~ | ~~ \ forall \ alpha \, B}

Lembre-se de que, neste quadro, as unidades (verdade) e (absurdo), os conectores (negação), (conjunção) e (disjunção) e a quantificação existencial são definíveis por ⊤{\ displaystyle \ top}⊥{\ displaystyle \ bot}¬{\ displaystyle \ lnot}∧{\ displaystyle \ land}∨{\ displaystyle \ lor}∃αB(α){\ displaystyle \ exists \ alpha \, B (\ alpha)}

• ⊤ ≡ ∀γ(γ⇒γ){\ displaystyle \ top ~ \ equiv ~ \ forall \ gamma \, (\ gamma \ Rightarrow \ gamma)}
• ⊥ ≡ ∀γγ{\ displaystyle \ bot ~ \ equiv ~ \ forall \ gamma \, \ gamma}
• ¬NO ≡ NO⇒⊥{\ displaystyle \ lnot A ~ \ equiv ~ A \ Rightarrow \ bot}
• NO∧B ≡ ∀γ((NO⇒B⇒γ)⇒γ){\ displaystyle A \ land B ~ \ equiv ~ \ forall \ gamma \, ((A \ Rightarrow B \ Rightarrow \ gamma) \ Rightarrow \ gamma)}
• NO∨B ≡ ∀γ((NO⇒γ)⇒(B⇒γ)⇒γ){\ displaystyle A \ lor B ~ \ equiv ~ \ forall \ gamma \, ((A \ Rightarrow \ gamma) \ Rightarrow (B \ Rightarrow \ gamma) \ Rightarrow \ gamma)}
• ∃αB(α) ≡ ∀γ(∀α(B(α)⇒γ)⇒γ){\ displaystyle \ exists \ alpha \, B (\ alpha) ~ \ equiv ~ \ forall \ gamma \, (\ forall \ alpha \, (B (\ alpha) \ Rightarrow \ gamma) \ Rightarrow \ gamma)}

(Observe que, por meio da correspondência Curry-Howard, o absurdo corresponde ao tipo vazio, a verdade ao tipo singleton, a conjunção ao produto cartesiano e a disjunção à soma direta.)

Provamos que, neste formalismo, uma fórmula é demonstrável sem hipóteses se e somente se o tipo correspondente no sistema F é habitado por um termo fechado.

Correspondência com aritmética de segunda ordem

Bibliografia

• Lambda-calculus, types and models , Jean-Louis Krivine , capítulo VIII, Masson , 1990, ( ISBN  2-225-82091-0 )
• Provas e tipos ,Jean-Yves Girard, Paul Taylor, Yves Lafont, capítulo 11,Cambridge University Press, 1989, ( ISBN  0-521-37181-3 )

<img src="https://fr.wikipedia.org/wiki/Special:CentralAutoLogin/start?type=1x1" alt="" title="" width="1" height="1" style="border: none; position: absolute;">