Traced monoidal closed categories are a model for higher- order functional computation. We develop a formal language of string diagrams for these categories, and a faithful interpretation in terms of certain hypergraphs. We then use the interpretation to show that string diagram rewriting can be implemented as double-pushout rewriting in a sound and complete way. Finally, we showcase our approach on the λ-calculus with explicit recursion.