Cubo lambda

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 ( $\rightarrow$ ): tipos que podem depender de termos, correspondendo a tipos dependentes.
eixo y ( $\uparrow$ ): termos que podem depender de tipos, correspondendo ao polimorfismo.
eixo z ( $\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.

Exemplos de sistemas

(λ→) Cálculo lambda simplesmente tipado

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:

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

(λ2) Sistema F

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 $\Lambda$ , que permite que termos dependam de tipos, com a seguinte regra:

${\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 $\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 $\Pi \alpha .\alpha \to \alpha$ .

(λω) Sistema Fω

No Sistema F ${\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 $A$ : ${\mathsf {TREE}}:=\lambda A:*.\Pi B.(A\to B)\to (B\to B\to B)\to B$ , onde " $A:*$ " significa informalmente " $A$ é um tipo". Esta é uma função que recebe um parâmetro de tipo $A$ como argumento e retorna o tipo de ${\mathsf {TREE}}$ s de valores do tipo $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 ${\underline {\omega }}$ geralmente não é usado por si só, mas é útil para isolar a característica independente dos construtores de tipo.^[4]

(λP) Lambda-P

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 é

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

onde $*$ representa tipos válidos. O novo construtor de tipo $\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.

(λω) Sistema Fω

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

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

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 $\square$ , são eles próprios termos com um tipo.

Definição formal

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

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

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

Os ambientes, como é usual em sistemas tipados, são dados por ${\displaystyle \Gamma$

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

As seguintes regras de tipagem também são comuns a todos os sistemas do cubo: ${\frac {}{\vdash *:\square }}\quad {\text{(Axioma)}}$ ${\frac {\Gamma \vdash A:s}{\Gamma ,x:A\vdash x:A}}x\not \in \Gamma \quad {\text{(Início)}}$ ${\frac {\Gamma \vdash A:B\quad \Gamma \vdash C:s}{\Gamma ,x:C\vdash A:B}}x\not \in \Gamma \quad {\text{(Enfraquecimento)}}$ ${\frac {\Gamma \vdash C:\Pi x:A.B\quad \Gamma \vdash D:A}{\Gamma \vdash CD:B[D/x]}}\quad {\text{(Aplicação)}}$ ${\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: ${\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)}}$ ${\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:

$(s_{1},s_{2})$	$(*,\square )$	$(\square ,*)$	$(\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.

Comparação entre os sistemas

λ→

Uma derivação típica que pode ser obtida é ${\displaystyle \alpha$ ou com o atalho da seta ${\displaystyle \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]

λ2

Em λ2, tais termos podem ser obtidos como ${\displaystyle \vdash (\lambda \beta$ com ${\textstyle \bot =\Pi \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.

λP

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$ que corresponde, via isomorfismo de Curry-Howard, a uma prova de $(\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 $\Gamma \vdash A:P((\lambda x.x)y)$ e $\Gamma \vdash B:\Pi x:P(y).C$ , precisa-se aplicar a regra de conversão^[a] para obter $\Gamma \vdash A:P(y)$ para poder tipar $\Gamma \vdash BA:C$ .

λω

Em λω, o seguinte operador ${\displaystyle AND:=\lambda \alpha$ é definível, isto é, $\vdash AND:*\to *\to *$ . A derivação ${\displaystyle \alpha$ 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]

λC

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.

Relação com outros sistemas

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 $\{*,\square \}$ , o único axioma ${\textstyle \{*,\square \}}$ , e um conjunto de regras ${\textstyle R}$ tal que $\{(*,*,*)\}\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:

Sistema do cubo	Sistema Lógico
λ→	Cálculo Proposicional (de ordem zero)
λ2	Cálculo Proposicional de Segunda Ordem
λω	Cálculo Proposicional de Ordem Superior Fraco
λω	Cálculo Proposicional de Ordem Superior
λP	Lógica de Predicados (de primeira ordem)
λP2	Cálculo de Predicados de Segunda Ordem
λPω	Cálculo de Predicados de Ordem Superior Fraco
λC	Cálculo das construções

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 $\wedge$ ou $\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.

Propriedades comuns

Todos os sistemas no cubo possuem:

a propriedade de Church-Rosser: se $M\to _{\beta }N$ e $M\to _{\beta }N'$ então existe $N''$ tal que $N\to _{\beta }^{*}N''$ e $N'\to _{\beta }^{*}N''$ ;
a propriedade de redução de sujeito: se $\Gamma \vdash M:T$ e $M\to _{\beta }M'$ então $\Gamma \vdash M':T$ ;
a unicidade de tipos: se $\Gamma \vdash A:B$ e $\Gamma \vdash A:B'$ então $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]

Subtipagem

A subtipagem no entanto não é representada no cubo, embora sistemas como $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 $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.

Ver também

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

Notas e Referências

1 2 3 4 5 6 Barendregt, Henk (1991). «Introduction to generalized type systems». Journal of Functional Programming. 1 (2): 125–154. ISSN 0956-7968. doi:10.1017/s0956796800020025. hdl:2066/17240
↑ Nederpelt, Rob; Geuvers, Herman (2014). Type Theory and Formal Proof. [S.l.]: Cambridge University Press. p. 69. ISBN 9781107036505
↑ Nederpelt & Geuvers 2014, p. 85
↑ Nederpelt & Geuvers 2014, p. 100
↑ Schwichtenberg, Helmut (1975). «Definierbare Funktionen imλ-Kalkül mit Typen». Archiv für Mathematische Logik und Grundlagenforschung (em alemão). 17 (3–4): 113–114. ISSN 0933-5846. doi:10.1007/bf02276799
↑ Girard, Jean-Yves; Lafont, Yves; Taylor, Paul (1989). Proofs and Types. Col: Cambridge Tracts in Theoretical Computer Science. 7. [S.l.]: Cambridge University Press. ISBN 9780521371810
1 2 3 Ridoux, Olivier (1998). Lambda-Prolog de A à Z ... ou presque (PDF). [S.l.]: [s.n.] OCLC 494473554
↑ Angiuli, Carlo; Gratzer, Daniel (2024). «2.1.3 Who type-checks the typing rules? and 2.2 Towards the syntax of dependent type theory». Principles of Dependent Type Theory (PDF). [S.l.]: Indiana University and Aarhus University. Consultado em 7 de setembro de 2024
↑ Favier, Naïm (17 de agosto de 2023). «In the Conversion inference rule of the lambda cube, why is Γ ⊢ B′:s necessary?». Computer Science Stack Exchange. Consultado em 7 de setembro de 2024
↑ Pierce, Benjamin; Dietzen, Scott; Michaylov, Spiro (1989). Programming in higher-order typed lambda-calculi. [S.l.]: Computer Science Department, Carnegie Mellon University. OCLC 20442222. CMU-CS-89-111 ERGO-89-075
↑ Sørensen, Morten Heine; Urzyczyin, Pawel (2006). «Pure type systems and the λ-cube». Lectures on the Curry-Howard Isomorphism. [S.l.]: Elsevier. pp. 343–359. ISBN 9780444520777. doi:10.1016/s0049-237x(06)80015-7
↑ Pierce, Benjamin (2002). Types and programming languages. [S.l.]: MIT Press. pp. 467–490. ISBN 978-0262162098. OCLC 300712077
↑ Pierce 2002, p. 466
↑ Ridoux 1998, p. 70

↑ A suposição $\Gamma \vdash B':s$ na regra de Conversão é uma conveniência; pode-se provar um meta-teorema de que $\Gamma \vdash A:B\land B=_{\beta }B'\Rightarrow \Gamma \vdash B':s$ em vez disso.^[8]^[9]

Leitura adicional

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.

Ligações externas

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

[:0-1] 1 2 3 4 5 6 Barendregt, Henk (1991). «Introduction to generalized type systems». Journal of Functional Programming. 1 (2): 125–154. ISSN 0956-7968. doi:10.1017/s0956796800020025. hdl:2066/17240

[2] Nederpelt, Rob; Geuvers, Herman (2014). Type Theory and Formal Proof. [S.l.]: Cambridge University Press. p. 69. ISBN 9781107036505

[3] Nederpelt & Geuvers 2014, p. 85

[4] Nederpelt & Geuvers 2014, p. 100

[5] Schwichtenberg, Helmut (1975). «Definierbare Funktionen imλ-Kalkül mit Typen». Archiv für Mathematische Logik und Grundlagenforschung (em alemão). 17 (3–4): 113–114. ISSN 0933-5846. doi:10.1007/bf02276799

[6] Girard, Jean-Yves; Lafont, Yves; Taylor, Paul (1989). Proofs and Types. Col: Cambridge Tracts in Theoretical Computer Science. 7. [S.l.]: Cambridge University Press. ISBN 9780521371810

[:1-7] 1 2 3 Ridoux, Olivier (1998). Lambda-Prolog de A à Z ... ou presque (PDF). [S.l.]: [s.n.] OCLC 494473554

[8] Angiuli, Carlo; Gratzer, Daniel (2024). «2.1.3 Who type-checks the typing rules? and 2.2 Towards the syntax of dependent type theory». Principles of Dependent Type Theory (PDF). [S.l.]: Indiana University and Aarhus University. Consultado em 7 de setembro de 2024

[9] Favier, Naïm (17 de agosto de 2023). «In the Conversion inference rule of the lambda cube, why is Γ ⊢ B′:s necessary?». Computer Science Stack Exchange. Consultado em 7 de setembro de 2024

[11] Pierce, Benjamin; Dietzen, Scott; Michaylov, Spiro (1989). Programming in higher-order typed lambda-calculi. [S.l.]: Computer Science Department, Carnegie Mellon University. OCLC 20442222. CMU-CS-89-111 ERGO-89-075

[12] Sørensen, Morten Heine; Urzyczyin, Pawel (2006). «Pure type systems and the λ-cube». Lectures on the Curry-Howard Isomorphism. [S.l.]: Elsevier. pp. 343–359. ISBN 9780444520777. doi:10.1016/s0049-237x(06)80015-7

[13] Pierce, Benjamin (2002). Types and programming languages. [S.l.]: MIT Press. pp. 467–490. ISBN 978-0262162098. OCLC 300712077

[14] Pierce 2002, p. 466

[15] Ridoux 1998, p. 70

[dependentTypeConvent-10] A suposição $\Gamma \vdash B':s$ na regra de Conversão é uma conveniência; pode-se provar um meta-teorema de que $\Gamma \vdash A:B\land B=_{\beta }B'\Rightarrow \Gamma \vdash B':s$ em vez disso.^[8]^[9]

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[a]

[10]

[11]

[12]

[13]

[14]

[8]

[9]