On the proof techniques of Udi Manber

Question

I was familiar with the approach of first coming up with an algorithm, and then proving the loop invariant to come up with an algorithm as elucidated in CLRS (Introduction to algorithms, Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein). Lately, on reading Udi Manber's introduction 'A creative approach' I have come across the idea of positing and algorithm and then proving it using induction and also getting the algorithm itself. It's like having your cake and eating it too.

There is one question which remains inexplicable to me. When I am proving an algorithm using Udi Manber's approach, am I arguing in the object language or in the meta language? In either of these cases, how am I just generating a proof? From the meta language it seems sensible to generate a proof in the object language, but arguing the soundness/completeness of these class of arguments appears difficult. But how do I guarantee that the proof is correct in the object language if it is generated by the object language itself? It is unclear to me if it is the metalanguage or the object language that is involved in here.

This question might seem poorly phrased, but I cannot find a better way to express it. Udi Manber's approach seems to generate an algorithm despite not knowing a priori what the algorithm itself is. This is something counter intuitive to me. Please kindly explain.

Answer 1

It is not a rigorous answer, but if we are to posit in the way of Udi Manber using induction, we are tacitly positing a recursively enumerable algorithm that can terminate. Udi Manber's algorithmic approach though does not necessarily posit a primitive recursive algorithm. If the problem in our class is not recursively enumerable, then we cannot use Udi Manber's approach, and it may as well be uncomputable. A primitive recursive algorithm is likely to be more efficient than a recursively enumerable one.