Cubo lambda 📖 Wikipedia

Em lógica matemática e teoria dos tipos, o λ-cubo (também escrito cubo lambda) é uma estrutura introduzida por Henk Barendregt^[1] para investigar as diferentes dimensões nas quais o cálculo das construções é uma generalização do cálculo lambda 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 (${\displaystyle \rightarrow }$): tipos que podem depender de termos, correspondendo a tipos dependentes.
• eixo y (${\displaystyle \uparrow }$): termos que podem depender de tipos, correspondendo ao polimorfismo.
• eixo z (${\displaystyle \nearrow }$): tipos que podem depender de outros tipos, correspondendo a operadores de tipo (de ligação).

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 sistema de tipos puro.

O sistema mais simples encontrado no λ-cubo é o cálculo lambda simplesmente tipado, também chamado de λ→. Neste sistema, a única maneira de construir uma abstração é fazendo um termo depender de um termo, com a regra de tipagem:

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

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

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

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

fun x -> x

do OCaml tem tipo

'a -> 'a

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

No Sistema F${\displaystyle {\underline {\omega }}}$ 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".^[3] Um exemplo de tal construtor de tipo é o tipo de árvores binárias com folhas rotuladas por dados de um determinado tipo ${\displaystyle A}$: ${\displaystyle {\mathsf {TREE}}:=\lambda A:*.\Pi B.(A\to B)\to (B\to B\to B)\to B}$, onde "${\displaystyle A:*}$" significa informalmente "${\displaystyle A}$ é um tipo". Esta é uma função que recebe um parâmetro de tipo ${\displaystyle A}$ como argumento e retorna o tipo de ${\displaystyle {\mathsf {TREE}}}$s de valores do tipo ${\displaystyle A}$. Na programação concreta, esta característica corresponde à capacidade de definir construtores de tipo dentro da linguagem, em vez de considerá-los como primitivos. O construtor de tipo anterior corresponde aproximadamente à seguinte definição de uma árvore com folhas rotuladas em OCaml:

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 o tipo de árvores de inteiros:

type int_tree = int tree

O Sistema F${\displaystyle {\underline {\omega }}}$ geralmente não é usado por si só, mas é útil para isolar a característica independente dos construtores de tipo.^[4]

No sistema λP, também chamado de λΠ, que está intimamente relacionado ao LF Logical Framework, tem-se os chamados tipos dependentes. Estes 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:A.B):*}}}$

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

O Sistema Fω combina tanto o construtor ${\displaystyle \Lambda }$ do Sistema F quanto os construtores de tipo do Sistema F${\displaystyle {\underline {\omega }}}$. Assim, o Sistema Fω fornece tanto termos que dependem de tipos quanto tipos que dependem de tipos.

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

Como para todos os sistemas baseados no cálculo lambda simplesmente tipado, todos os sistemas no cubo são dados em duas etapas: primeiro, termos brutos, juntamente com uma noção de β-redução, e depois regras de tipagem que permitem tipar esses termos.

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

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

e ${\displaystyle A\to B}$ denotando ${\displaystyle \Pi x:A.B}$ quando ${\displaystyle x}$ não ocorre livre em ${\displaystyle B}$.

Os ambientes, como é usual em sistemas tipados, são dados por ${\displaystyle \Gamma :=\emptyset \mid \Gamma ,x:A}$

A noção de β-redução é comum a todos os sistemas do cubo. É escrita ${\displaystyle \to _{\beta }}$ e dada pelas regras$${\displaystyle {\frac {}{(\lambda x:A.B)~C\to _{\beta }B[C/x]}}}$$$${\displaystyle {\frac {B\to _{\beta }B'}{\lambda x:A.B\to _{\beta }\lambda x:A.B'}}}$$$${\displaystyle {\frac {A\to _{\beta }A'}{\lambda x:A.B\to _{\beta }\lambda x:A'.B}}}$$$${\displaystyle {\frac {B\to _{\beta }B'}{\Pi x:A.B\to _{\beta }\Pi x:A.B'}}}$$$${\displaystyle {\frac {A\to _{\beta }A'}{\Pi x:A.B\to _{\beta }\Pi x:A'.B}}}$$Seu fecho reflexivo e transitivo é escrito ${\displaystyle =_{\beta }}$.

As seguintes regras de tipagem também são comuns a todos os sistemas do cubo:$${\displaystyle {\frac {}{\vdash *:\square }}\quad {\text{(Axioma)}}}$$$${\displaystyle {\frac {\Gamma \vdash A:s}{\Gamma ,x:A\vdash x:A}}x\not \in \Gamma \quad {\text{(Início)}}}$$$${\displaystyle {\frac {\Gamma \vdash A:B\quad \Gamma \vdash C:s}{\Gamma ,x:C\vdash A:B}}x\not \in \Gamma \quad {\text{(Enfraquecimento)}}}$$$${\displaystyle {\frac {\Gamma \vdash C:\Pi x:A.B\quad \Gamma \vdash D:A}{\Gamma \vdash CD:B[D/x]}}\quad {\text{(Aplicação)}}}$$$${\displaystyle {\frac {\Gamma \vdash A:B\quad B=_{\beta }B'\quad \Gamma \vdash B':s}{\Gamma \vdash A:B'}}\quad {\text{(Conversão)}}}$$

A diferença entre os sistemas está nos pares de sortes ${\textstyle (s_{1},s_{2})}$ que são permitidos nas duas seguintes regras de tipagem:$${\displaystyle {\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash B:s_{2}}{\Gamma \vdash \Pi x:A.B:s_{2}}}\quad {\text{(Produto)}}}$$${\displaystyle {\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash B:s_{2}\quad \Gamma ,x:A\vdash C:B}{\Gamma \vdash \lambda x:A.C:\Pi x:A.B}}\quad {\text{(Abstração)}}}$

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

${\displaystyle (s_{1},s_{2})}$	${\displaystyle (*,*)}$	${\displaystyle (*,\square )}$	${\displaystyle (\square ,*)}$	${\displaystyle (\square ,\square )}$
λ→		—comentário não assinado de Usuário não informado (data/hora não informada)	—comentário não assinado de Usuário não informado (data/hora não informada)	—comentário não assinado de Usuário não informado (data/hora não informada)
λP			—comentário não assinado de Usuário não informado (data/hora não informada)	—comentário não assinado de Usuário não informado (data/hora não informada)
λ2		—comentário não assinado de Usuário não informado (data/hora não informada)		—comentário não assinado de Usuário não informado (data/hora não informada)
λω		—comentário não assinado de Usuário não informado (data/hora não informada)	—comentário não assinado de Usuário não informado (data/hora não informada)
λP2				—comentário não assinado de Usuário não informado (data/hora não informada)
λPω			—comentário não assinado de Usuário não informado (data/hora não informada)
λω		—comentário não assinado de Usuário não informado (data/hora não informada)
λC

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

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

Uma derivação típica que pode ser obtida é$${\displaystyle \alpha :*\vdash \lambda x:\alpha .x:\Pi x:\alpha .\alpha }$$ou com o atalho da seta$${\displaystyle \alpha :*\vdash \lambda x:\alpha .x:\alpha \to \alpha }$$assemelhando-se fortemente à identidade (do tipo ${\textstyle \alpha }$) do λ→ usual. Note que todos os tipos usados devem aparecer no contexto, porque a única derivação que pode ser feita em um contexto vazio é ${\textstyle \vdash *:\square }$.

O poder computacional é bastante fraco, corresponde aos polinômios estendidos (polinômios juntamente com um operador condicional).^[5]

Em λ2, tais termos podem ser obtidos como$${\displaystyle \vdash (\lambda \beta :*.\lambda x:\bot .x\beta ):\Pi \beta :*.\bot \to \beta }$$com ${\textstyle \bot =\Pi \alpha :*.\alpha }$. Se lê-se ${\textstyle \Pi }$ como uma quantificação universal, via isomorfismo de Curry-Howard, isso pode ser visto como uma prova do princípio da explosão. Em geral, λ2 adiciona a possibilidade de ter tipos impredicativos como ${\textstyle \bot }$, isto é, termos que quantificam sobre todos os tipos, incluindo eles mesmos.
O polimorfismo também permite a construção de funções que não eram construíveis em λ→. Mais precisamente, as funções definíveis em λ2 são aquelas provavelmente totais na aritmética de Peano de segunda ordem.^[6] Em particular, todas as funções recursivas primitivas são definíveis.

Em λP, a capacidade de ter tipos dependendo de termos significa que se pode expressar predicados lógicos. Por exemplo, o seguinte é derivável:$${\displaystyle {\begin{array}{l}\alpha :*,a_{0}:\alpha ,p:\alpha \to *,q:*\vdash \\\quad \lambda z:(\Pi x:\alpha .px\to q).\\\quad \lambda y:(\Pi x:\alpha .px).\\\quad (za_{0})(ya_{0}):(\Pi x:\alpha .px\to q)\to (\Pi x:\alpha .px)\to q\end{array}}}$$que corresponde, via isomorfismo de Curry-Howard, a uma prova de ${\displaystyle (\forall x:A,Px\to Q)\to (\forall x:A,Px)\to Q}$.
Do ponto de vista computacional, no entanto, ter tipos dependentes não aumenta o poder computacional, apenas a possibilidade de expressar propriedades de tipo mais precisas.^[7]

A regra de conversão é fortemente necessária ao lidar com tipos dependentes, porque permite realizar computação nos termos do tipo. Por exemplo, se tem-se ${\displaystyle \Gamma \vdash A:P((\lambda x.x)y)}$ e ${\displaystyle \Gamma \vdash B:\Pi x:P(y).C}$, precisa-se aplicar a regra de conversão^[a] para obter ${\displaystyle \Gamma \vdash A:P(y)}$ para poder tipar ${\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 é, ${\displaystyle \vdash AND:*\to *\to *}$. A derivação$${\displaystyle \alpha :*,\beta :*\vdash \Pi \gamma :*.(\alpha \to \beta \to \gamma )\to \gamma :*}$$já pode ser obtida em λ2, no entanto o ${\textstyle AND}$ polimórfico só pode ser definido se a regra ${\textstyle (\square ,*)}$ também estiver presente.

Do ponto de vista computacional, λω é extremamente forte, e tem sido considerado como uma base para linguagens de programação.^[10]

O cálculo das construções tem tanto a expressividade predicativa de λP quanto o poder computacional de λω, por isso λC também é chamado de λPω,^[1]:130 sendo, portanto, muito poderoso, tanto no lado lógico quanto no lado computacional.

O sistema Automath é similar ao λ2 do ponto de vista lógico. As linguagens do tipo ML, do ponto de vista da tipagem, situam-se em algum lugar entre λ→ e λ2, pois admitem um tipo restrito de tipos polimórficos, isto é, os tipos na forma normal prenex. No entanto, como apresentam alguns operadores de recursão, seu poder computacional é maior que o do λ2.^[7] O sistema Coq é baseado em uma extensão do λC com uma hierarquia linear de universos, em vez de apenas um único ${\textstyle \square }$ não tipável, e a capacidade de construir tipos indutivos.

Sistemas de tipos puros podem ser vistos como uma generalização do cubo, com um conjunto arbitrário de sortes, axiomas, regras de produto e abstração. Inversamente, os sistemas do cubo lambda podem ser expressos como sistemas de tipos puros com duas sortes ${\displaystyle \{*,\square \}}$, o único axioma ${\textstyle \{*,\square \}}$, e um conjunto de regras ${\textstyle R}$ tal que ${\displaystyle \{(*,*,*)\}\subseteq R\subseteq \{(*,*,*),(*,\square ,\square ),(\square ,*,*),(\square ,\square ,\square )\}}$.^[1]

Via isomorfismo de Curry-Howard, há uma correspondência biunívoca entre os sistemas no cubo lambda e sistemas lógicos,^[1] a saber:

Todas as lógicas são implicativas (ou seja, os únicos conectivos são ${\textstyle \to }$ e ${\textstyle \forall }$); no entanto, pode-se definir outros conectivos como ${\displaystyle \wedge }$ ou ${\displaystyle \neg }$ de maneira impredicativa em lógicas de segunda ordem e ordem superior. Nas lógicas fracas de ordem superior, existem variáveis para predicados de ordem superior, mas não se pode fazer quantificação sobre elas.

Todos os sistemas no cubo possuem:

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

Todas essas podem ser provadas em sistemas de tipos puros genéricos.^[11]

Qualquer termo bem tipado em um sistema do cubo é fortemente normalizante,^[1] embora esta propriedade não seja comum a todos os sistemas de tipos puros. Nenhum sistema no cubo é Turing completo.^[7]

A subtipagem no entanto não é representada no cubo, embora sistemas como ${\displaystyle F_{<:}^{\omega }}$, conhecido como quantificação limitada de ordem superior, que combinam subtipagem e polimorfismo sejam de interesse prático, e podem ser generalizados ainda mais para operadores de tipo limitados. Extensões adicionais ao ${\displaystyle F_{<:}^{\omega }}$ permitem a definição de objetos puramente funcionais; esses sistemas foram geralmente desenvolvidos após a publicação do artigo do cubo lambda.^[12]

A ideia do cubo é devida ao matemático Henk Barendregt (1991). O arcabouço dos sistemas de tipos puros generaliza o cubo lambda no sentido de que todos os cantos do cubo, bem como muitos outros sistemas, podem ser representados como instâncias deste arcabouço geral.^[13] Este arcabouço antecede o cubo lambda em alguns anos. Em seu artigo de 1991, Barendregt também define os cantos do cubo neste arcabouço.

• Em sua Habilitation à diriger les recherches,^[14] Olivier Ridoux fornece um modelo recortável 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.
• Cubo lógico
• Hexágono lógico
• Quadrado de oposição
• Triângulo de oposição

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

• O Cubo Lambda de Barendregt no contexto de sistema de tipo puro por Roger Bishop Jones