Cálculo Kappa

Em lógica matemática, teoria das categorias, e ciência da computação, kappa cálculo é um sistema formal para a definição de funções de primeira ordem.

Ao contrário do cálculo lambda, o cálculo kappa não tem funções de ordem superior; as suas funções não são objetos de primeira classe. Kappa-cálculo pode ser considerado como "uma reformulação do fragmento de primeira-ordem do cálculo lambda tipado".

Em razão do fato de que suas funções não são objetos de primeira classe, a avaliação de expressões de cálculo kappa não exige fechos.

Definição

A definição abaixo foi adaptada a partir de diagramas nas páginas 205 e 207 de Hasegawa.

Gramática

Cálculo kappa consiste em tipos e expressões, dado pela gramática abaixo:

$\tau =1\mid \tau \times \tau \mid \dots$

$e=x\mid i{d}_{\tau }\mid {!}_{\tau }\mid {\mathrm{lift}}_{\tau }(e)\mid e\circ e\mid \kappa x:1\to \tau .e$

Em outras palavras,

• 1 é um tipo
• If ${\tau }_1$ and ${\tau }_2$ forem tipos então ${\tau }_1\times {\tau }_2$é um tipo
• Toda variável é uma expressão
• Se $\tau$ for um tipo então $i{d}_{\tau }$ é uma expressão
• Se $\tau$ for um tipo então ${!}_{\tau }$ é uma expressão
• Se $\tau$ for um tipo e $e$ for uma expressão então ${\mathrm{lift}}_{\tau }(e)$ é uma expressão
• Se $e_1$ e $e_2$ forem expressões então $e_1\circ e_2$ é uma expressão
• Se $x$ for uma variável, $\tau$ for um tipo, e $e$ for uma expressão, então $\kappa x:1\to \tau .e$é uma expressão

O tipo $:1\to \tau$ e os índices de $id$, $!$, e $\mathrm{lift}$ são às vezes omitidos quando eles podem ser inequivocamente determinados a partir do contexto.

Justaposição é frequentemente usada como uma abreviação para uma combinação de "$\mathrm{lift}$" e composição:

$e_1{e}_2\stackrel{def}{=}{e}_1\circ \mathrm{lift}(e_2)$

Regras de tipagem

A apresentação aqui usa sequentes ($\mathrm{\Gamma }⊢e:\tau$) em vez de julgamentos hipotéticos, a fim de facilitar a comparação com o cálculo lambda simplesmente tipado. Isso requer que a adição da regra Var, que não aparecem no Hasegawa

No cálculo kappa existem dois tipos de expressões: o tipo de origem e o tipo de destino. A notação $e:{\tau }_1\to {\tau }_2$ é usada para indicar que a expressão $e$ tem o tipo da fonte ${\tau }_1$ e o tipo de destino ${\tau }_2$.

Expressões no cálculo kappa são tipos de atribuídos de acordo com as seguintes regras:

$\frac{x:1\to \tau \in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢x:1\to \tau }$ (Var)

$\frac{{\displaystyle }}{⊢i{d}_{\tau }:\tau \to \tau }$ (Id)

$\frac{{\displaystyle }}{⊢{!}_{\tau }:\tau \to 1}$ (Bang)

$\frac{\mathrm{\Gamma }⊢e_1:{\tau }_1\to {\tau }_2\mathrm{\Gamma }⊢e_2:{\tau }_2\to {\tau }_3}{\mathrm{\Gamma }⊢e_2\circ e_1:{\tau }_1\to {\tau }_3}$ (Comp)

$\frac{\mathrm{\Gamma }⊢e:1\to {\tau }_1}{\mathrm{\Gamma }⊢{\mathrm{lift}}_{{\tau }_2}(e):{\tau }_2\to ({\tau }_1\times {\tau }_2)}$ (Lift)

$\frac{\mathrm{\Gamma },x:1\to {\tau }_1⊢e:{\tau }_2\to {\tau }_3}{\mathrm{\Gamma }⊢\kappa x:1\to {\tau }_1.e:{\tau }_1\times {\tau }_2\to {\tau }_3}$ (Kappa)

Em outras palavras,

• Var: assumindo$x:1\to \tau$ permite você concluir que$x:1\to \tau$
• Id: para qualquer tipo , $i{d}_{\tau }:\tau \to \tau$
• Bang: para qualquer tipo $\tau$, ${!}_{\tau }:\tau \to 1$
• Comp: se o tipo de destino corresponde ao tipo de origem , eles podem ser compostos para formar uma expressão com o tipo de origem de e o tipo de destido de$e_2$
• Lift: se $e:1\to {\tau }_1$, então${\mathrm{lift}}_{{\tau }_2}(e):{\tau }_2\to ({\tau }_1\times {\tau }_2)$
• Kappa: se nós podemos concluir que sob a suposição que , então nós podemos concluir sem essa suposição que$\kappa x:1\to {\tau }_1.e:{\tau }_1\times {\tau }_2\to {\tau }_3$

Igualdades

Cálculo kappa obedece as seguintes igualdades:

• Neutralidade: Se $f:{\tau }_1\to {\tau }_2$ então $f\circ i{d}_{{\tau }_1}=f$ e $f=i{d}_{{\tau }_2}\circ f$
• Associatividade: Se $f:{\tau }_1\to {\tau }_2$, $g:{\tau }_2\to {\tau }_3$, e $h:{\tau }_3\to {\tau }_4$, então $(h\circ g)\circ f=h\circ (g\circ f)$.
• Terminalidade: Se e então$f=g$
• Redução de ascensor: $(\kappa x.f)\circ {\mathrm{lift}}_{\tau }(c)=f[c/x]$
• Redução Kappa: $\kappa x.(h\circ {\mathrm{lift}}_{\tau }(x))=h$ se x não é livre em h

As últimas duas igualdades são regras de redução para os cálculos, reescrevendo da esquerda para direita

Proriedades

O tipo 1 pode ser considerado como o tipo unitário. Devido a isso, quaisquer duas funções cujo tipo de argumento é o mesmo e cujo tipo de resultado é 1 deve ser igual - uma vez que existe apenas um único valor do tipo 1 as duas funções devem retornar esse valor para cada argumento (Terminalidade).

Expressões com tipo podem ser considerado como "constantes" ou valores de "tipo de base"; isto é porque o 1 é o tipo unitário e, portanto, uma função deste tipo é necessariamente uma função constante. Observe que o regra kappa permite abstrações apenas quando a variável que está sendo abstraída tem o tipo para alguns. Este é o mecanismo básico que garante que todas as funções são de primeira ordem.

Semântica categórica

Cálculo kappa destina-se a ser a linguagem interna de categorias completas contextualmente.

Exemplos

Expressões com múltiplos argumentos têm tipos fonte que são árvores binárias "desbalanceadas à direita". Por exemplo, uma função $f$ com três argumentos de tipos $A,B,$ e $C$ e tipo do resultado for $D$ terá tipo

$f:A\times (B\times (C\times 1))\to D$

Se definirmos justaposição associativa-à-esquerda (f c) como uma abreviação para $(f\circ \mathrm{lift}(c))$, então – assumindo que $a:1\to A$, $b:1\to B$, e que $c:1\to C$ – podemos aplicar essa função:

$fabc:1\to D$

Como a expressão $fabc$ tem tipo fonte 1, ela é um "valor básico" e pode ser passado como um argumento para uma outra função. Se $g:(D\times E)\to F$, então

$g(fabc):E\to F$

Bem semelhante a uma função "curryficada" de tipo $A\to (B\to (C\to D))$ no lambda cálculo, aplicação parcial é possível:

$fa:B\times (C\times 1)\to D$

Entretanto nenhum tipo de alta ordem (i.e. $(\tau \to \tau )\to \tau$) está envolvido. Note que em razão do fato de que o tipo fonte de $fa$ não é 1, a seguinte expressão não pode ser tipada sob as suposições mencionadas até aqui :

$h(fa)$

Em razão do fato de que a aplicação sucessiva é usada para argumentos múltiplos não é necessário saber a aridade de uma função para determinar sua tipagem; por exemplo, se sabemos que $c:1\to C$ então a expressão

$jc$

é bem tipada desde que j tenha tipo $(C\times \alpha )\to \beta$ para algum $\alpha$ e algum $\beta$. Essa propriedade é importante quando calculando o tipo principal de uma expressão, algo que pode ser difícil quando se tentar excluir funções de alta-ordem dos lambda-cálculos tipados restringindo a gramática de tipos.

História

Barendregt originalmente introduziu o termo "completude funcional" no contexto da álgebra combinatória. O Kappa cálculo surgiu a partir de esforços de Lambek para formular um análogo apropriado de completude funcional para categorias arbitrárias (ver Hermida & Jacobs, section 1). Hasegawa mais tarde desenvolveu o kappa cálculo para uma linguagem de programação utilizável (embora simples) incluindo aritmética sobre números naturais e recursão primitiva. Conexões a setas foram investigadas mais tarde por Power, Thielecke, e outros.

Variantes

É possível explorar versões do kappa cálculo com tipos subestruturais tais como linear, afim, e tipos ordenados. Essas extensões requerem eliminar ou restringir a expressão ${!}_{\tau }$. Em tais circunstâncias o operador de tipo $\times$ não é um verdadeiro produto cartesiano, e é geralmente escrito $\otimes$ para deixar isso claro.