A RECURSIVE 2ND-ORDER INITIAL ALGEBRA SPECIFICATION OF PRIMITIVE-RECURSION

被引:8
作者
MEINKE, K
机构
[1] Department of Computer Science, University College of Swansea, Swansea, SA2 8PP, Singleton Park
关键词
D O I
10.1007/BF01178510
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Theoretical results on the scope and limits of first order algebraic specifications can be used to show that certain natural algebras have no recursively enumerable equational specification under first order initial algebra semantics. A well known example is the algebra PR of primitive recursive functions over the natural numbers. In this paper we show that PR has a recursive equational specification under second order initial algebra semantics. It follows that higher order initial algebra specifications are strictly more powerful than first order initial algebra specifications.
引用
收藏
页码:329 / 340
页数:12
相关论文
共 12 条
[1]   INITIAL AND FINAL ALGEBRA-SEMANTICS FOR DATA TYPE SPECIFICATIONS - 2 CHARACTERIZATION THEOREMS [J].
BERGSTRA, JA ;
TUCKER, JV .
SIAM JOURNAL ON COMPUTING, 1983, 12 (02) :366-387
[2]   ALGEBRAIC SPECIFICATIONS OF COMPUTABLE AND SEMICOMPUTABLE DATA-TYPES [J].
BERGSTRA, JA ;
TUCKER, JV .
THEORETICAL COMPUTER SCIENCE, 1987, 50 (02) :137-181
[3]  
BERGSTRA JA, 1980, B EATCS, V11, P23
[4]  
GOGUEN JA, 1985, ALGEBRAIC METHODS SE, P459
[5]  
MALCEV AI, 1961, RUSS MATH SURV, V16, P77
[6]   UNIVERSAL ALGEBRA IN HIGHER TYPES [J].
MEINKE, K .
THEORETICAL COMPUTER SCIENCE, 1992, 100 (02) :385-417
[7]  
Meinke K., 1993, Many-sorted logic and its applications, P135
[8]  
Meinke K., 1992, HDB LOGIC COMPUTER S, VI, P189
[9]  
MOLLER B, 1988, LECT NOTES COMPUT SC, V332, P154
[10]  
MOLLER B, 1987, THESIS TU MUNCHEN