Computational Models and Function Algebras
Computational Models and Function Algebras
复制标题
计算模型和函数代数
DOI：
10.1007/3-540-60178-3_81
复制
发表时间：
1994
期刊：
影响因子：
--
通讯作者：
P. Clote
中科院分区：
文献类型：
--
作者：
P. Clote
The modern digital computer, a force which has shaped the latter part of the. 20-th century, can trace its origins back to work in mathematical logic concerning the formalization of concepts such as proof and computable function. Numerous examples support this assertion. For instance, in his development of the universal Turing machine, AM Taring seems to have been the first, along with J. von Neumann, to understand the potential of memory-stored programs executed by a universal computational device. Moreover, certain function classes and proof systems can be viewed as prototypes of programming languages: the Kleene#-calculus and imperative programming (PASCAL, C); resolution (Gentzen sequent calculus) and logic programming (PROLOG); the Church-Kleene A-calculus and functional programming (LISP); the Girard system F (polymorphic A-calculus) and polymorphic functional programming (ML). One recurring theme in recursion theory is that of a function algebra--ie a smallest class of functions containing certain initial functions and closed under certain operations. In 1925, as a technical tool in his claimed sketch proof of the continuum hypothesis, D. Hilbert [48] defined classes of higher type functionals by recursion. In 1928, W. Ackermann [1] furnished a proof that the diagonal function~ a (a, a) of Hilbert [48], a variant of the Ackermann function, is not primitive recursive. In 1931, K. GSdel [35] defined the primitive recursive functions, calling them" rekursive Funktionen", and used them to arithmetize logical syntax via GSdel numbers for his incompleteness theorem. Generalizing Ackermann's work, in 1936 R. Pdter [72] defined and studied the k-fold recursive
The modern digital computer, a force which has shaped the latter part of the. 20-th century, can trace its origins back to work in mathematical logic concerning the formalization of concepts such as proof and computable function. Numerous examples support this assertion. For instance, in his development of the universal Turing machine, AM Taring seems to have been the first, along with J. von Neumann, to understand the potential of memory-stored programs executed by a universal computational device. Moreover, certain function classes and proof systems can be viewed as prototypes of programming languages: the Kleene#-calculus and imperative programming (PASCAL, C); resolution (Gentzen sequent calculus) and logic programming (PROLOG); the Church-Kleene A-calculus and functional programming (LISP); the Girard system F (polymorphic A-calculus) and polymorphic functional programming (ML). One recurring theme in recursion theory is that of a function algebra--ie a smallest class of functions containing certain initial functions and closed under certain operations. In 1925, as a technical tool in his claimed sketch proof of the continuum hypothesis, D. Hilbert [48] defined classes of higher type functionals by recursion. In 1928, W. Ackermann [1] furnished a proof that the diagonal function~ a (a, a) of Hilbert [48], a variant of the Ackermann function, is not primitive recursive. In 1931, K. GSdel [35] defined the primitive recursive functions, calling them" rekursive Funktionen", and used them to arithmetize logical syntax via GSdel numbers for his incompleteness theorem. Generalizing Ackermann's work, in 1936 R. Pdter [72] defined and studied the k-fold recursive