The universal resolving algorithm and its correctness: inverse computation in a functional language