# Is there a name for defining recursive functions as an infinite list of input/output pairs?

Recursive functions are usually defined by directly calling a function inside its own body.

Nat = Z | S Nat
double Z = Z
double (S x) = S (S (double x)))


What if, instead of defining them this way, we just enumerated two recursive datatypes and zipped them?

To be more descriptive, mind the following functions/types:

enum Nat = [Z, S Z, S S Z, S S S Z ...]
elem (S S S Z) (enum Nat) = 3
[4,5,6] !! 1 = 5
zip [1,2,3] [4,5,6] = [(1,4), (2,5), (3,6)]
# a b = \x -> (zip (enum a) (enum b)) !! (elem x (enum a))


That is, enum enumerates elements of a recursive datatype, elem, !! and zip are just as defined by Haskel. Now, using #, there is an interesting way to define some recursive functions.

Even = Z | S (S Even)
double = Nat # Even


This makes double equivalent to:

double x = [(0,0),(1,2),(2,4),(3,6)...] !! x


In other words, instead of defining the function recursively, we just created an infinite list with the input/output pairs of that function, by zipping two recursive datatypes together. I never heard of this approach being used, so my question is: this there a name for this? Any relevant papers? What kinds of functions can be defined this way?

Well it's the "set-theoritic" perspective of a function where a function from A onto B is really just the a subset of A x B where each a in A appears only once.
Consider for example, how you would do this for Double.
For a function $f\colon D \to R$, the set $\{(x,f(x)) : x \in D\} \subseteq D \times R$ is known as the graph of the function. We can think of the graph as a sequence (ordered arbitrarily), and then we can say that the graph is r.e. if it can be recursively enumerated in some order. Assuming the function is total (and domain and range are both the natural numbers), the graph of a function is r.e. iff the function is computable.
• What is r.e.? – dokkat May 16 '14 at 5:16