Title
Some Lambda Calculi with Categorial Sums and Products
Abstract
. We consider the simply typed -calculus with primitive recursionoperators and types corresponding to categorical products andcoproducts.. The standard equations corresponding to extensionality andto surjectivity of pairing and its dual are oriented as expansion rules.Strong normalization and ground (base-type) confluence is proved forthe full calculus; full confluence is proved for the calculus omitting therule for strong sums. In the latter case, fixed-point constructors may be...
Year
DOI
Venue
1993
10.1007/3-540-56868-9_12
RTA
Keywords
Field
DocType
categorial sums,lambda calculi,fixed point
Discrete mathematics,Extensionality,Lambda calculus,Primitive recursive function,Normalization (statistics),Categorical variable,Pairing,Operator (computer programming),Confluence,Mathematics
Conference
ISBN
Citations 
PageRank 
3-540-56868-9
23
1.98
References 
Authors
5
1
Name
Order
Citations
PageRank
Daniel J. Dougherty141332.13