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

editar

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

Gramática

editar

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

 

 

Em outras palavras,

  • 1 é um tipo
  • If   and   forem tipos então  é um tipo
  • Toda variável é uma expressão
  • Se   for um tipo então   é uma expressão
  • Se   for um tipo então   é uma expressão
  • Se   for um tipo e   for uma expressão então   é uma expressão
  • Se   e   forem expressões então   é uma expressão
  • Se   for uma variável,   for um tipo, e   for uma expressão, então  é uma expressão

O tipo   e os índices de  ,  , e   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 " " e composição:

 

Regras de tipagem

editar

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

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

  (Var)

  (Id)

  (Bang)

  (Comp)

  (Lift)

  (Kappa)

Em outras palavras,

  • Var: assumindo  permite você concluir que 
  • Id: para qualquer tipo ,  
  • Bang: para qualquer tipo  ,  
  • 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 
  • Lift: se  , então 
  • Kappa: se nós podemos concluir que sob a suposição que , então nós podemos concluir sem essa suposição que 

Igualdades

editar

Cálculo kappa obedece as seguintes igualdades:

  • Neutralidade: Se   então   e  
  • Associatividade: Se  ,  , e  , então  .
  • Terminalidade: Se e então 
  • Redução de ascensor:  
  • Redução Kappa:   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

editar

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

editar

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

Exemplos

editar

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

 

Se definirmos justaposição associativa-à-esquerda (f c) como uma abreviação para  , então – assumindo que  ,  , e que   – podemos aplicar essa função:

 

Como a expressão   tem tipo fonte 1, ela é um "valor básico" e pode ser passado como um argumento para uma outra função. Se  , então

 

Bem semelhante a uma função "curryficada" de tipo   no lambda cálculo, aplicação parcial é possível:

 

Entretanto nenhum tipo de alta ordem (i.e.  ) está envolvido. Note que em razão do fato de que o tipo fonte de   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   então a expressão

 

é bem tipada desde que j tenha tipo   para algum   e algum  . 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

editar

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

editar

É 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  . Em tais circunstâncias o operador de tipo   não é um verdadeiro produto cartesiano, e é geralmente escrito   para deixar isso claro.

Referências

editar
  1. a b Hasegawa, Masahito (1995). Pitt, David; Rydeheard, David E.; Johnstone, Peter, eds. «Decomposing typed lambda calculus into a couple of categorical programming languages». Springer-Verlag Berlin Heidelberg. Category Theory and Computer Science: 6th International Conference, CTCS '95 Cambridge, United Kingdom, August 7–11, 1995 Proceedings. Lecture Notes in Computer Science. 953: 200–219. ISBN 978-3-540-60164-7. ISSN 0302-9743. doi:10.1007/3-540-60164-3_28. Resumo divulgativo"Adam" answering "What are  -categories?" on MathOverflow (31 de agosto de 2010) 
  2. Hasegawa, Masahito (1995). Pitt, David; Rydeheard, David E.; Johnstone, Peter, eds. «Decomposing typed lambda calculus into a couple of categorical programming languages». Springer-Verlag Berlin Heidelberg. Category Theory and Computer Science: 6th International Conference, CTCS '95 Cambridge, United Kingdom, August 7–11, 1995 Proceedings. Lecture Notes in Computer Science. 953: 200–219. ISBN 978-3-540-60164-7. ISSN 0302-9743. doi:10.1007/3-540-60164-3_28. Resumo divulgativo"Adam" answering "What are  -categories?" on MathOverflow (31 de agosto de 2010) 
  3. Hasegawa, Masahito (1995). Pitt, David; Rydeheard, David E.; Johnstone, Peter, eds. «Decomposing typed lambda calculus into a couple of categorical programming languages». Springer-Verlag Berlin Heidelberg. Category Theory and Computer Science: 6th International Conference, CTCS '95 Cambridge, United Kingdom, August 7–11, 1995 Proceedings. Lecture Notes in Computer Science. 953: 200–219. ISBN 978-3-540-60164-7. ISSN 0302-9743. doi:10.1007/3-540-60164-3_28. Resumo divulgativo"Adam" answering "What are  -categories?" on MathOverflow (31 de agosto de 2010) 
  4. Barendregt, Hendrik Pieter, ed. (1 de outubro de 1984). «The Lambda Calculus: Its Syntax and Semantics» Revised ed. Amsterdam, North Holland: Elsevier Science. Studies in Logic and the Foundations of Mathematics. 103. ISBN 0-444-87508-5 
  5. Lambek, Joachim (1 de agosto de 1973). «Functional completeness of cartesian categories». Amsterdam, North Holland: North-Holland Publishing Company (publicado em março de 1974). Annals of Mathematical Logic. 6 (3-4): 259-292. ISSN 0003-4843. doi:10.1016/0003-4843(74)90003-5. Resumo divulgativo"Adam" answering "What are  -categories?" on MathOverflow (31 de agosto de 2010) 
  6. Hermida, Claudio; Jacobs, Bart (dezembro de 1995). «Fibrations with indeterminates: contextual and functional completeness for polymorphic lambda calculi». Cambridge, England: Cambridge University Press. Mathematical Structures in Computer Science. 5 (4): 501–531. ISSN 1469-8072. doi:10.1017/S0960129500001213 
  7. Power, John; Thielecke, Hayo (1999). Wiedermann, Jiří; van Emde Boas, Peter; Nielsen, Mogens, eds. «Closed Freyd- and  -Categories». Springer-Verlag Berlin Heidelberg. Automata, Languages and Programming: 26th International Colloquium, ICALP’99 Prague, Czech Republic, July 11–15, 1999 Proceedings. Lecture Notes in Computer Science. 1644: 625–634. ISBN 978-3-540-66224-2. ISSN 0302-9743. doi:10.1007/3-540-48523-6_59 

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