How Incomputable is the Separable Hahn-Banach Theorem?

We investigate some basic connections between reverse mathematics and computable analysis. In particular, we show how to use Weak K¨onig’s Lemma within the framework of computable analysis to classify incomputable functions of low complexity. By defining the multi-valued function Sep and through the definition of a natural notion of reducibility for multi-valued functions, we obtain a computational counterpart of the subsystem of second order arithmetic WKL0. We study analogies and differences between WKL0 and the class of Sep-computable multi-valued functions. We use these notions to provide a method to determine the computational complexity of the Hahn-Banach Extension Theorem.