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.

The problem is that some types are uncountable so enumerating them in this manner isn't possible; for some types a finite member may not be at a finite index.

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.

  • $\begingroup$ What is r.e.? $\endgroup$
    – dokkat
    May 16 '14 at 5:16
  • $\begingroup$ Recursively enumerable. $\endgroup$ May 16 '14 at 5:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.