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. Dougherty | 1 | 413 | 32.13 |