# Passing arrays vs functions as arguments in SMT?

In SAT Modulo Theories (SMT), with the theory of uninterpreted functions, all functions are first order, that is, they don't take functions as arguments or return functions.

In the theory of arrays, however, functions can take arrays as arguments, and return arrays as values.

However, my understanding is that arrays in SMT are just syntactic sugar for functions. That is, an array $a$ indexed by $I$ with elements of type $T$ is just modeled as a function $f: I \to T$. Lookup is just a function call, and extending an array $a[i] := e$ produces the array described by the function $f'(x) = ite(i=x, e, f(x))$, where $ite$ is an if-then-else operator.

Is there something fundamentally different between arrays and functions that allows them to be passed as arguments? Or is the limitation that functions are first-order an artificial one?

• Can you provide a link to a paper that reduces the theory of arrays to the theory of uninterpreted functions? It may just be that functions can be used for global arrays as a kind of poor man's theory of arrays. Similarly, there's a kind of poor man's theory of higher order functions by turning $f(x)$ into $\mathtt{apply}(\ulcorner f\urcorner,x)$ with the equation $\mathtt{apply}(\ulcorner f\urcorner,x)=f(x)$. Using defunctionalization and given inductive types, you could be a bit more systematic but non-modular. – Derek Elkins left SE Nov 30 '17 at 0:23
• @DerekElkins: the reference: In this paper we present combinatory array logic, CAL, using a small, but powerful core of combinators, and reduce it to the theory of uninterpreted functions.. I haven't read the paper in full (I just found the link on the CVC4 website). – jmite Nov 30 '17 at 4:13
• Okay, for the basic theory of arrays described in that paper at the beginning, the compilation scheme described by the related work sounds similar to defunctionalization, so I'm inclined to think that there is no real difference, and the techniques to handle the basic theory of arrays could be (and probably are) used to handle a theory with higher-order functions. – Derek Elkins left SE Nov 30 '17 at 4:32