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^[1]".

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.^[2]

Gramática

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

${\displaystyle \tau =1\mid \tau \times \tau \mid \ldots }$

${\displaystyle 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 ${\displaystyle \tau _{1}}$ and ${\displaystyle \tau _{2}}$ forem tipos então ${\displaystyle \tau _{1}\times \tau _{2}}$é um tipo
• Toda variável é uma expressão
• Se ${\displaystyle \tau }$ for um tipo então ${\displaystyle id_{\tau }}$ é uma expressão
• Se ${\displaystyle \tau }$ for um tipo então ${\displaystyle !_{\tau }}$ é uma expressão
• Se ${\displaystyle \tau }$ for um tipo e ${\displaystyle e}$ for uma expressão então ${\displaystyle \operatorname {lift} _{\tau }(e)}$ é uma expressão
• Se ${\displaystyle e_{1}}$ e ${\displaystyle e_{2}}$ forem expressões então ${\displaystyle e_{1}\circ e_{2}}$ é uma expressão
• Se ${\displaystyle x}$ for uma variável, ${\displaystyle \tau }$ for um tipo, e ${\displaystyle e}$ for uma expressão, então ${\displaystyle \kappa x{:}1{\to }\tau \;.\;e}$é uma expressão

O tipo ${\displaystyle :1{\to }\tau }$ e os índices de ${\displaystyle id}$, ${\displaystyle !}$, e ${\displaystyle \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 "${\displaystyle \operatorname {lift} }$" e composição:

Regras de tipagem

A apresentação aqui usa sequentes (${\displaystyle \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^[3]

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

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

Em outras palavras,

• Var: assumindo${\displaystyle x:1{\to }\tau }$ permite você concluir que${\displaystyle x:1{\to }\tau }$
• Id: para qualquer tipo , ${\displaystyle id_{\tau }:\tau {\to }\tau }$
• Bang: para qualquer tipo ${\displaystyle \tau }$, ${\displaystyle !_{\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${\displaystyle e_{2}}$
• Lift: se ${\displaystyle e:1{\to }\tau _{1}}$, então${\displaystyle \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${\displaystyle \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 ${\displaystyle f:\tau _{1}{\to }\tau _{2}}$ então ${\displaystyle f{\circ }id_{\tau _{1}}=f}$ e ${\displaystyle f=id_{\tau _{2}}{\circ }f}$
• Associatividade: Se ${\displaystyle f:\tau _{1}{\to }\tau _{2}}$, ${\displaystyle g:\tau _{2}{\to }\tau _{3}}$, e ${\displaystyle h:\tau _{3}{\to }\tau _{4}}$, então ${\displaystyle (h{\circ }g){\circ }f=h{\circ }(g{\circ }f)}$.
• Terminalidade: Se e então${\displaystyle f=g}$
• Redução de ascensor: ${\displaystyle (\kappa x.f)\circ \operatorname {lift} _{\tau }(c)=f[c/x]}$
• Redução Kappa: ${\displaystyle \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 ${\displaystyle f}$ com três argumentos de tipos ${\displaystyle A,B,}$ e ${\displaystyle C}$ e tipo do resultado for ${\displaystyle D}$ terá tipo

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

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

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

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

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 ${\displaystyle c:1{\to }C}$ então a expressão

é bem tipada desde que j tenha tipo ${\displaystyle (C\times \alpha ){\to }\beta }$ para algum ${\displaystyle \alpha }$ e algum ${\displaystyle \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^[4] o termo "completude funcional" no contexto da álgebra combinatória. O Kappa cálculo surgiu a partir de esforços de Lambek^[5] para formular um análogo apropriado de completude funcional para categorias arbitrárias (ver Hermida & Jacobs,^[6] 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.^[1] Conexões a setas foram investigadas mais tarde^[7] 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 ${\displaystyle !_{\tau }}$. Em tais circunstâncias o operador de tipo ${\displaystyle \times }$ não é um verdadeiro produto cartesiano, e é geralmente escrito ${\displaystyle \otimes }$ para deixar isso claro.

Referências

Erro de citação: Elemento <ref> definido em <references> não tem um atributo de nome.