Abstract

We introduce a concept of \textbf{computability relative to a structure}, which specifies which functions on the universe of a first-order structure are computable, using the lambda calculus with patterns. In doing so, we add a new congruence, $\equiv_\mathfrak{A}$, called \textbf{congruence in a structure} to identify two syntactically different terms which represent the same element of the universe. 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.

This work is licensed under a Creative Commons Attribution 4.0 License.