General recursive functions in a very simply interpretable typed \(\lambda\)-calculus (Q1314352)

This paper is in the setting of simply typed lambda-calculus. It is well known that not all partial recursive functions can be represented in this system. The authors propose to add to the \(\lambda\)-calculus four constants and two reduction rules: the first two constants represent the zero and successor for type 0. The other two allow, using the new rules, the changes of types for integers which are necessary for dealing with primitive recursion and the \(\mu\)-operator. This results in a typed \(\lambda\)-calculus, where all partial recursive functions are represented. A model is provided, using simply a hierarchy of function spaces based upon an infinite base set. Finally a curious new extension with one more constant allows the description of some parallel operators.