Computability via the lambda-calculus with patterns

Abstract

We introduce a concept of computability relative to a structure, which specifies which functions on the domain of a first-order structure are computable, using the lambda calculus with patterns. In doing so, we add a new congruence, called a congruence in a structure to identify two syntactically different terms which represent the same element of the domain. We then show that, with the introduction of the new congruence, all the basic properties of the original lambda calculus with patterns still hold, including the Church-Rosser theorem. To justify the word "computable", we first prove that if a total function on N is recursive then it is computable relative to N, the standard structure for N. For the converse, we construct a Goedel coding for terms in the lambda calculus with patterns and investigate how to perform various steps in the reduction of an encoded term using recursive functions