To be more concrete. Consider the C programming language. Is this function “equivalent to a mapping from input values to output values”

I don’t seem to be able to explain this clearly enough in this forum/format, or without a degree of formal setup that would be way too tedious both to write and read. But the question you are posing is not exactly well formed regarding what I am suggesting. I am not suggesting that a function *in the language* be a “set theoretic function” *in the language*. I am suggesting that its *semantic interpretation* (which presupposes a fixed choice of a semantics) be equivalent *by the rules of equivalence of the target semantics in the given semantic interpretation* to a function *in the domain of interpretation* which is in some sense “a set theoretic function”, which, typically would arise because e.g. the categorical semantics would take place in a setting in which something like FinSet embeds in a natural way.

So to answer the intended meaning of your question fully, one would need to specify an intepretation function for the C language into some semantic domain where there’s a given notion of equivalence and an obvious embedding of FinSet. One would then translate the given function over that mapping and ask if it lands in the image of the embedding of FinSet. There might be something in Strachey’s papers or the like that does some of this setup, but I don’t care to try to dig through them at the moment.

Edit: I suppose one could try to “internalize” this in some way, which might have been how my original suggestion read. In such a case one would simply define a notion of “set theoretic function” internal to C, which would be somewhat ad-hoc, but attempt to capture universally the class of things that the more extended version I suggested does. So for the C language that could be “functions that can be written solely with the case and return constructs”. Since your example function cannot be written solely with case and return, it would not fall in the given class.