Usuário(a):Milton Vasconcelos da Gama Neto/Cálculo Kappa: diferenças entre revisões
Conteúdo apagado Conteúdo adicionado
Criado ao traduzir a página "Kappa calculus" |
m WP:BOT: Substituindo sintaxe matemática obsoleta de acordo com mw:Extension:Math/Roadmap |
||
Linha 33:
=== Regras de tipagem ===
''A apresentação aqui usa sequentes (<math />) 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''<ref name="Hasegawa">{{Citar periódico|author-last=Hasegawa|author-first=Masahito|year=1995|editor1-last=Pitt|editor1-first=David|editor2-last=Rydeheard|editor2-first=David E.|editor3-last=Johnstone|editor3-first=Peter|editor3-link=Peter Johnstone (mathematician)|title=Decomposing typed lambda calculus into a couple of categorical programming languages|url=http://link.springer.com/chapter/10.1007\%2F3-540-60164-3_28|journal=Category Theory and Computer Science: 6th International Conference, CTCS '95 Cambridge, United Kingdom, August 7–11, 1995 Proceedings|series=Lecture Notes in Computer Science|publisher=Springer-Verlag Berlin Heidelberg|volume=953|pages=200–219|doi=10.1007/3-540-60164-3_28|id=|isbn=978-3-540-60164-7|issn=0302-9743|layurl=http://mathoverflow.net/questions/37180|laysource="Adam" answering "What are <math>\kappa</math>-categories?" on MathOverflow|laydate=August 31, 2010}}</ref>
No cálculo kappa existem dois tipos de expressões: o tipo de ''origem'' e o tipo de ''destino''. A notação <math /> é usado para indicar que a expressão 'e' tem o tipo da fonte <math /> e o tipo de destino <math />.
| |||