Cubo lambda - Lambda cube

O cubo lambda. A direção de cada seta é a direção de inclusão.

Na lógica matemática e na teoria dos tipos , o λ-cubo é uma estrutura introduzida por Henk Barendregt para investigar as diferentes dimensões nas quais o cálculo das construções é uma generalização do λ-cálculo simplesmente tipado . Cada dimensão do cubo corresponde a um novo tipo de dependência entre termos e tipos. Aqui, "dependência" refere-se à capacidade de um termo ou tipo de ligar um termo ou tipo. As respectivas dimensões do cubo λ correspondem a:

• eixo x ( ): tipos que podem vincular termos, correspondendo a tipos dependentes .${\ displaystyle \ rightarrow}$
• eixo y ( ): termos que podem ligar tipos, correspondendo ao polimorfismo .${\ displaystyle \ uparrow}$
• eixo z ( ): tipos que podem vincular tipos, correspondendo a operadores de tipo (vinculação) .${\ displaystyle \ nearrow}$

As diferentes maneiras de combinar essas três dimensões produzem os 8 vértices do cubo, cada um correspondendo a um tipo diferente de sistema tipado. O cubo λ pode ser generalizado no conceito de um sistema de tipo puro .

Exemplos de sistemas

(λ →) Cálculo lambda simplesmente digitado

O sistema mais simples encontrado no cubo λ é o cálculo lambda simplesmente digitado , também chamado de λ →. Nesse sistema, a única maneira de construir uma abstração é fazer um termo depender de um termo , com a regra de digitação

${\ displaystyle {\ frac {\ Gamma, x: \ sigma \; \ vdash \; t: \ tau} {\ Gamma \; \ vdash \; \ lambda xt: \ sigma \ to \ tau}}}$

(λ2) Sistema F

No Sistema F (também denominado λ2 para o "cálculo lambda tipado de segunda ordem") há outro tipo de abstração, escrito com a , que permite que os termos dependam de tipos , com a seguinte regra: ${\ displaystyle \ Lambda}$

${\ displaystyle {\ frac {\ Gamma \; \ vdash \; t: \ sigma} {\ Gamma \; \ vdash \; \ Lambda \ alpha .t: \ Pi \ alpha. \ sigma}} \; {\ text {if}} \ alpha {\ text {não ocorre gratuitamente em}} \ Gamma}$

Os termos que começam com a são chamados de polimórficos , pois podem ser aplicados a diferentes tipos para obter funções diferentes, de forma semelhante a funções polimórficas em linguagens do tipo ML . Por exemplo, a identidade polimórfica${\ displaystyle \ Lambda}$

fun x -> x

de OCaml tem tipo

'a -> 'a

o que significa que pode receber um argumento de qualquer tipo 'ae retornar um elemento desse tipo. Este tipo corresponde em λ2 ao tipo . ${\ displaystyle \ Pi \ alpha. \ alpha \ to \ alpha}$

(λ ω ) Sistema F ω

No Sistema F, uma construção é introduzida para fornecer tipos que dependem de outros tipos . Isso é chamado de construtor de tipo e fornece uma maneira de construir "uma função com um tipo como valor ". Um exemplo de um construtor de tipo é , onde " " informalmente significa " é um tipo". Esta é uma função que recebe um parâmetro de tipo como argumento e retorna o tipo de valores de tipo . Na programação concreta, esse recurso corresponde à capacidade de definir construtores de tipo dentro da linguagem, ao invés de considerá-los como primitivos. O construtor de tipo anterior corresponde aproximadamente à seguinte definição de uma árvore com folhas rotuladas em OCaml:${\ displaystyle {\ underline {\ omega}}}$${\ displaystyle {\ mathsf {TREE}}: = \ lambda A: *. \ Pi B. (A \ to B) \ to (B \ to B \ to B) \ to B}$${\ displaystyle A: *}$${\ displaystyle A}$${\ displaystyle A}$${\ displaystyle {\ mathsf {ÁRVORE}}}$${\ displaystyle A}$

type 'a tree = | Leaf of 'a | Node of 'a tree * 'a tree

Este construtor de tipo pode ser aplicado a outros tipos para obter novos tipos. Por exemplo, para obter tipos de árvores de inteiros:

type int_tree = int tree

O sistema F geralmente não é usado sozinho, mas é útil para isolar o recurso independente dos construtores de tipo. ${\ displaystyle {\ underline {\ omega}}}$

(λP) Lambda-P

No λP sistema, também chamado ΛΠ, e intimamente relacionado com o LF Quadro Lógico , se tem chamado tipos dependentes . Esses são tipos que podem depender de termos . A regra de introdução crucial do sistema é

${\ displaystyle {\ frac {\ Gamma, x: A \; \ vdash \; B: *} {\ Gamma \; \ vdash \; (\ Pi x: AB): *}}}$

onde representa tipos válidos. O novo construtor de tipo corresponde através do isomorfismo de Curry-Howard a um quantificador universal, e o sistema λP como um todo corresponde à lógica de primeira ordem com a implicação apenas como conectiva. Um exemplo desses tipos dependentes na programação concreta é o tipo de vetores em um determinado comprimento: o comprimento é um termo, do qual o tipo depende. ${\ displaystyle *}$${\ displaystyle \ Pi}$

(Fω) Sistema Fω

Sistema Fω combina tanto o construtor do sistema de F eo tipo construtores de sistema F . Assim, System Fω fornece termos que dependem de tipos e tipos que dependem de tipos . ${\ displaystyle \ Lambda}$${\ displaystyle {\ underline {\ omega}}}$

(λC) Cálculo de construções

No cálculo de construções , denotadas como λC no cubo ou como λPω, essas quatro características coabitam, de modo que ambos os tipos e termos podem depender de tipos e termos. A fronteira clara que existe em λ → entre termos e tipos é um tanto abolida, já que todos os tipos, exceto o universal, são eles próprios termos com um tipo. ${\ displaystyle \ square}$

Definição formal

Como para todos os sistemas baseados no cálculo lambda simplesmente digitado, todos os sistemas no cubo são dados em duas etapas: primeiro, termos brutos, junto com uma noção de redução β e , em seguida, regras de digitação que permitem digitar esses termos.

O conjunto de classificações é definido como , as classificações são representadas com a letra . Existe também um conjunto de variáveis, representadas pelas letras . Os termos brutos dos oito sistemas do cubo são dados pela seguinte sintaxe: ${\ displaystyle S: = \ {*, \ square \}}$${\ displaystyle s}$${\ displaystyle V}$${\ displaystyle x, y, \ dots}$

${\ displaystyle A: = x \ mid s \ mid A ~ A \ mid \ lambda x: AA \ mid \ Pi x: AA}$

e denotando quando não ocorre gratuitamente em . ${\ displaystyle A \ a B}$${\ displaystyle \ Pi x: AB}$${\ displaystyle x}$${\ displaystyle B}$

O ambiente, como é usual em sistemas tipados, são dados por ${\ displaystyle \ Gamma: = \ emptyset \ mid \ Gamma, x: T}$

A noção de redução β é comum a todos os sistemas no cubo. É escrito e dado pelas regras${\ displaystyle \ to _ {\ beta}}$

$${\ displaystyle {\ frac {} {(\ lambda x: AB) ~ C \ to _ {\ beta} B [C / x]}}}$$

$${\ displaystyle {\ frac {B \ to _ {\ beta} B '} {\ lambda x: AB \ to _ {\ beta} \ lambda x: A.B'}}}$$

$${\ displaystyle {\ frac {A \ to _ {\ beta} A '} {\ lambda x: AB \ to _ {\ beta} \ lambda x: A'.B}}}$$

$${\ displaystyle {\ frac {B \ to _ {\ beta} B '} {\ Pi x: AB \ to _ {\ beta} \ Pi x: A.B'}}}$$

$${\ displaystyle {\ frac {A \ to _ {\ beta} A '} {\ Pi x: AB \ to _ {\ beta} \ Pi x: A'.B}}}$$

${\ displaystyle = _ {\ beta}}$

As seguintes regras de digitação também são comuns a todos os sistemas no cubo:

$${\ displaystyle {\ frac {} {\ vdash *: \ square}} \ quad {\ text {(Axioma)}}}$$

$${\ displaystyle {\ frac {\ Gamma \ vdash A: s \ quad x {\ text {não ocorre em}} \ Gamma} {\ Gamma, x: A \ vdash x: A}} \ quad {\ text { (Começar)}}}$$

$${\ displaystyle {\ frac {\ Gamma \ vdash A: B \ quad \ Gamma \ vdash C: s} {\ Gamma, x: C \ vdash A: B}} \ quad {\ text {(enfraquecimento)}}}$$

$${\ displaystyle {\ frac {\ Gamma \ vdash C: \ Pi x: AB \ quad \ Gamma \ vdash a: A} {\ Gamma \ vdash Ca: B [a / x]}} \ quad {\ text {( Aplicativo)}}}$$

$${\ displaystyle {\ frac {\ Gamma \ vdash A: B \ quad B = _ {\ beta} B '\ quad \ Gamma \ vdash B': s} {\ Gamma \ vdash A: B '}} \ quad { \ text {(conversão)}}}$$

${\ textstyle (s_ {1}, s_ {2})}$

$${\ displaystyle {\ frac {\ Gamma \ vdash A: s_ {1} \ quad \ Gamma, x: A \ vdash B: s_ {2}} {\ Gamma \ vdash \ Pi x: AB: s_ {2}} } \ quad {\ text {(Produto)}}}$$

${\ displaystyle {\ frac {\ Gamma \ vdash A: s_ {1} \ quad \ Gamma, x: A \ vdash b: B \ quad \ Gamma, x: A \ vdash B: s_ {2}} {\ Gamma \ vdash \ lambda x: Ab: \ Pi x: AB}} \ quad {\ text {(Abstração)}}}$

A correspondência entre os sistemas e os pares permitidos nas regras é a seguinte: ${\ textstyle (s_ {1}, s_ {2})}$

${\ displaystyle (s_ {1}, s_ {2})}$	${\ displaystyle (*, *)}$	${\ displaystyle (*, \ square)}$	${\ displaystyle (\ square, *)}$	${\ displaystyle (\ square, \ square)}$
λ →
λP
λ2
λ ω
λP2
λP ω
λω
λC

Cada direção do cubo corresponde a um par (excluindo o par compartilhado por todos os sistemas), e por sua vez cada par corresponde a uma possibilidade de dependência entre termos e tipos: ${\ textstyle (*, *)}$

• ${\ textstyle (*, *)}$ permite que os termos dependam dos termos.
• ${\ textstyle (*, \ square)}$ permite que os tipos dependam dos termos.
• ${\ textstyle (\ square, *)}$ permite que os termos dependam dos tipos.
• ${\ textstyle (\ square, \ square)}$ permite que os tipos dependam de tipos.

Comparação entre os sistemas

λ →

Uma derivação típica que pode ser obtida é

$${\ displaystyle \ alpha: * \ vdash \ lambda x: \ alpha .x: \ Pi x: \ alpha. \ alpha}$$

$${\ displaystyle \ alpha: * \ vdash \ lambda x: \ alpha .x: \ alpha \ to \ alpha}$$

${\ textstyle \ alpha}$

${\ textstyle \ vdash *: \ square}$

O poder de computação é bastante fraco, corresponde aos polinômios estendidos (polinômios junto com um operador condicional).

λ2

Em λ2, tais termos podem ser obtidos como

$${\ displaystyle \ vdash (\ lambda \ beta: *. \ lambda x: \ bot .x \ beta): \ Pi \ beta: *. \ bot \ to \ beta}$$

segunda ordem . Em particular, todas as funções recursivas primitivas são definíveis. ${\ textstyle \ bot = \ Pi \ alpha: *. \ alpha}$${\ textstyle \ Pi}$${\ textstyle \ bot}$

λP

Em λP, a capacidade de ter tipos dependendo dos termos significa que se pode expressar predicados lógicos. Por exemplo, o seguinte é derivável:

$${\ displaystyle \ alpha: *, a_ {0}: \ alpha, p: \ alpha \ to *, q: * \ vdash \ lambda z: (\ Pi x: \ alpha .px \ to q). \ lambda y : (\ Pi x: \ alpha .px). (Za_ {0}) (ya_ {0}): (\ Pi x: \ alpha .px \ to q) \ to (\ Pi x: \ alpha .px) \ para q}$$

que corresponde, através do isomorfismo de Curry-Howard, a uma prova de . Do ponto de vista computacional, entretanto, ter tipos dependentes não aumenta o poder computacional, apenas a possibilidade de expressar propriedades de tipo mais precisas. ${\ displaystyle (\ forall x: A, Px \ to Q) \ to (\ forall x: A, Px) \ to Q}$

A regra de conversão é fortemente necessária ao lidar com tipos dependentes, porque permite realizar cálculos nos termos do tipo. Por exemplo, se você tem e , você precisa aplicar a regra de conversão para conseguir digitar . ${\ displaystyle \ Gamma \ vdash A: P ((\ lambda xx) y)}$${\ displaystyle \ Gamma \ vdash B: \ Pi x: P (y) .C}$${\ displaystyle \ Gamma \ vdash A: P (y)}$${\ displaystyle \ Gamma \ vdash BA: C}$

λω

Em λω, o seguinte operador

$${\ displaystyle AND: = \ lambda \ alpha: *. \ lambda \ beta: *. \ Pi \ gamma: *. (\ alpha \ to \ beta \ to \ gamma) \ to \ gamma}$$

é definível, isto é . A derivação${\ displaystyle \ vdash AND: * \ to * \ to *}$

$${\ displaystyle \ alpha: *, \ beta: * \ vdash \ Pi \ gamma: *. (\ alpha \ to \ beta \ to \ gamma) \ to \ gamma: *}$$

pode ser obtido já em λ2, porém o polimórfico só pode ser definido se a regra também estiver presente. ${\ textstyle AND}$${\ textstyle (\ square, *)}$

Do ponto de vista computacional, λω é extremamente forte e tem sido considerado a base para linguagens de programação.

λC

O cálculo das construções tem a expressividade do predicado de λP e o poder computacional de λω, daí porque λC também é chamado de λPω, por isso é muito poderoso, tanto do lado lógico quanto do lado computacional.

Relação com outros sistemas

O sistema Automath é semelhante a λ2 do ponto de vista lógico. As linguagens do tipo ML , do ponto de vista da tipificação, situam-se em algum lugar entre λ → e λ2, pois admitem um tipo restrito de tipos polimórficos, ou seja, os tipos na forma normal prenex. No entanto, como eles apresentam alguns operadores de recursão, seu poder de computação é maior do que o de λ2. O sistema Coq é baseado em uma extensão de λC com uma hierarquia linear de universos, ao invés de apenas um não tipável , e a capacidade de construir tipos indutivos. ${\ textstyle \ square}$

Os Pure Type Systems podem ser vistos como uma generalização do cubo, com um conjunto arbitrário de tipos, axiomas, produtos e regras de abstração. Por outro lado, os sistemas do cubo lambda podem ser expressos como Sistemas de Tipo Puro com dois tipos , o único axioma e um conjunto de regras como esse . ${\ displaystyle \ {*, \ square \}}$${\ textstyle \ {*, \ square \}}$${\ textstyle R}$${\ displaystyle \ {(*, *, *) \} \ subseteq R \ subseteq \ {(*, *, *), (*, \ square, \ square), (\ square, *, *), (\ quadrado, \ quadrado, \ quadrado) \}}$

Por meio do isomorfismo de Curry-Howard, há uma correspondência um a um entre os sistemas no cubo lambda e os sistemas lógicos, a saber:

Sistema do cubo	Sistema Lógico
λ →	(Primeira ordem) Cálculo proposicional
λ2	Cálculo proposicional de segunda ordem
λ ω	Cálculo proposicional de ordem fracamente superior
λω	Cálculo proposicional de ordem superior
λP	(Primeira ordem) Lógica de Predicado
λP2	Cálculo de predicado de segunda ordem
λP ω	Cálculo de predicado de ordem superior fraca
λC	Cálculo de Construções

Todas as lógicas são implicativas (isto é, os únicos conectivos são e ), no entanto, pode-se definir outros conectivos como ou de uma forma

em lógicas de segunda ordem e superiores. Nas lógicas fracas de ordem superior, existem variáveis ​​para predicados de ordem superior, mas nenhuma quantificação pode ser feita. ${\ textstyle \ to}$${\ textstyle \ forall}$${\ displaystyle \ wedge}$${\ displaystyle \ neg}$

Propriedades comuns

Todos os sistemas do cubo desfrutam

• a propriedade Church-Rosser : se e então existe tal que e ;${\ displaystyle M \ to _ {\ beta} N}$${\ displaystyle M \ to _ {\ beta} N '}$${\ displaystyle N ''}$${\ displaystyle N \ to _ {\ beta} ^ {*} N ''}$${\ displaystyle N '\ to _ {\ beta} ^ {*} N' '}$
• a propriedade de redução de assunto : se e então ;${\ displaystyle \ Gamma \ vdash M: T}$${\ displaystyle M \ to _ {\ beta} M '}$${\ displaystyle \ Gamma \ vdash M ': T}$
• a singularidade dos tipos: se e então .${\ displaystyle \ Gamma \ vdash A: B}$${\ displaystyle \ Gamma \ vdash A: B '}$${\ displaystyle B = _ {\ beta} B '}$

Tudo isso pode ser comprovado em sistemas de tipo puro genérico.

Qualquer termo bem digitado em um sistema do cubo é fortemente normalizado, embora essa propriedade não seja comum a todos os sistemas de tipo puro. Nenhum sistema no cubo é Turing completo.

Subtipagem

A subtipagem, no entanto, não é representada no cubo, embora sistemas como , conhecido como

; esses sistemas foram geralmente desenvolvidos depois que o papel do cubo lambda foi publicado. ${\ displaystyle F _ {<:} ^ {\ omega}}$${\ displaystyle F _ {<:} ^ {\ omega}}$

A ideia do cubo deve-se ao matemático Henk Barendregt (1991). A estrutura dos sistemas de tipo puro generaliza o cubo lambda no sentido de que todos os cantos do cubo, bem como muitos outros sistemas, podem ser representados como instâncias dessa estrutura geral. Essa estrutura é anterior ao cubo lambda em alguns anos. Em seu artigo de 1991, Barendregt também define os cantos do cubo nesta estrutura.

Veja também

• Em sua Habilitation à diriger les recherches, Olivier Ridoux fornece um molde recortado do cubo lambda e também uma representação dual do cubo como um octaedro, onde os 8 vértices são substituídos por faces, bem como uma representação dual como um dodecaedro , onde as 12 arestas são substituídas por faces.
• Teoria do tipo de homotopia

Notas

Leitura adicional

• Peyton Jones, Simon; Meijer, Erik (1997). "Henk: A Typed Intermediate Language" (PDF) . Henk é baseado diretamente no cubo lambda , uma família expressiva de cálculos lambda digitados.

links externos

• Lambda Cube de Barendregt no contexto de sistemas de tipo puro por Roger Bishop Jones