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 \ldots$

$e=x\mid id_{\tau }\mid !_{\tau }\mid \operatorname {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 $id_{\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 $\operatorname {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 $\operatorname {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 "$\operatorname {lift}$" e composição:

$e_{1}e_{2}{\overset {def}{=}}e_{1}\circ \operatorname {lift} (e_{2})$

Regras de tipagem

A apresentação aqui usa sequentes ($\Gamma \vdash 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:

${x{:}1{\to }\tau \;\in \;\Gamma } \over {\Gamma \vdash x:1{\to }\tau }$ (Var)

${} \over {\vdash id_{\tau }\;:\;\tau \to \tau }$ (Id)

${} \over {\vdash !_{\tau }\;:\;\tau \to 1}$ (Bang)

${\Gamma \vdash e_{1}{:}\tau _{1}{\to }\tau _{2}\;\;\;\;\;\;\Gamma \vdash e_{2}{:}\tau _{2}{\to }\tau _{3}} \over {\Gamma \vdash e_{2}\circ e_{1}:\tau _{1}{\to }\tau _{3}}$ (Comp)

${\Gamma \vdash e{:}1{\to }\tau _{1}} \over {\Gamma \vdash \operatorname {lift} _{\tau _{2}}(e)\;:\;\tau _{2}\to (\tau _{1}\times \tau _{2})}$ (Lift)

${\Gamma ,\;x{:}1{\to }\tau _{1}\;\vdash \;e:\tau _{2}{\to }\tau _{3}} \over {\Gamma \vdash \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 , $id_{\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$\operatorname {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 }id_{\tau _{1}}=f$ e $f=id_{\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 \operatorname {lift} _{\tau }(c)=f[c/x]$
• Redução Kappa: $\kappa x.(h\circ \operatorname {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 \operatorname {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:

$f\;a\;b\;c\;:\;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\;(f\;a\;b\;c)\;:\;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:

$f\;a\;:\;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\;(f\;a)$

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

$j\;c$

é 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.