Usuário(a):Milton Vasconcelos da Gama Neto/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 funções de primeira ordem.

Ao contrário do cálculo lambda, o cálculo kappa não tem nenhum 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".

Porque suas funções não são objetos de primeira classe, a avaliação de expressões de cálculo kappa não exigem fechamentos.

Definição

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

Gramática

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

Em outras palavras,

• 1 é um tipo
• If $\tau _{1}$ and $\tau _{2}$ are types then $\tau _{1}\times \tau _{2}$ is a type
• Toda variável é uma expressão
• Se é um tipo, então é uma expressão
• Se é um tipo, então é uma expressão
• Se é um tipo e 'e' é uma expressão, então é uma expressão
• Se é uma expressão, então é uma expressão
• Se x é uma variável, é um tipo, e é uma expressão, então é uma expressão. 

Os subscritos de id, !, ${\displaystyle }$são às vezes omitido quando eles podem ser inequivocamente determinados a partir do contexto.

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

Regras de tipagem

A apresentação aqui usa sequentes (${\displaystyle }$) 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 ${\displaystyle }$ é usado para indicar que a expressão 'e' tem o tipo da fonte ${\displaystyle }$ e o tipo de destino ${\displaystyle }$.

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 ${\displaystyle }$ 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 ${\displaystyle }$para alguns ${\displaystyle }$. 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.

História

Barendregt introduzido originalmente o termo "completude funcional" no contexto de álgebra combinatória. Cálculo kappa surgiu dos esforços de Lambek para formulação de um adequado de completude funcional  para categorias arbitrárias (ver Hermida e Jacobs, seção 1). Hasegawa, posteriormente, desenvolveu cálculo kappa em uma linguagem de programação utilizável (embora simples), incluindo aritmética sobre números naturais e recursões primitivas. Ligações com setas foram posteriormente investigadas por Power, Thielecke, e outros.

Variantes

É possível explorar as versões do cálculo kappa com tipos de substrutura, tais como linear, afim, e tipos ordenados. Essas extensões requerem a eliminação ou restrição da ${\displaystyle }$expressão. Em tais circunstâncias, o ${\displaystyle }$ operador de tipo não é um verdadeiro produto cartesiano, e, geralmente, é escrito ${\displaystyle }$ para tornar isso mais claro.