GENERAL RECURSIVE FUNCTIONS IN A VERY SIMPLY INTERPRETABLE TYPED LAMBDA-CALCULUS

Citation
G. Jacopini et G. Sontacchi, GENERAL RECURSIVE FUNCTIONS IN A VERY SIMPLY INTERPRETABLE TYPED LAMBDA-CALCULUS, Theoretical computer science, 121(1-2), 1993, pp. 169-178
Citations number
5
Categorie Soggetti
Computer Sciences","Computer Applications & Cybernetics",Mathematics
ISSN journal
03043975
Volume
121
Issue
1-2
Year of publication
1993
Pages
169 - 178
Database
ISI
SICI code
0304-3975(1993)121:1-2<169:GRFIAV>2.0.ZU;2-V
Abstract
In this paper we add to the usual typed lambda-calculus four constants (DELTA, OMEGA, rho, theta) and two reduction rules (delta, omega). Th is language combines the simplicity of interpretation of the usual typ ed lambda-calculus and the universatity of the untyped lambda-calculus . We prove, in fact, that each partial recursive function is represent able in this language.