Cálculo Kappa: diferenças entre revisões
Criado ao traduzir a página "Kappa calculus" |
(Sem diferenças)
|
Revisão das 17h54min de 8 de julho de 2016
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[1]".
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.[1]
Gramática
Cálculo kappa consiste em tipos e expressões, dado pelo a gramática abaixo:
Em outras palavras,
- 1 é um tipo
- If and are types then 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, !, 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 "" e composição:
Regras de tipagem
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[1]
No cálculo kappa existem dois tipos de expressões: o tipo de origem e o tipo de destino. A notação é usado para indicar que a expressão 'e' 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
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
References
- ↑ a b c 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 (August 31, 2010) Verifique data em:
|resumo-data=
(ajuda)
Erro de citação: Elemento <ref>
com nome "Lambek" definido em <references>
não é utilizado no texto da página.
Erro de citação: Elemento <ref>
com nome "HermidaJacobs" definido em <references>
não é utilizado no texto da página.
Erro de citação: Elemento <ref>
com nome "Barendregt" definido em <references>
não é utilizado no texto da página.
Erro de citação: Elemento <ref>
com nome "closed" definido em <references>
não é utilizado no texto da página.