Theory of constructible domains for robotics: Why?

The goal of Recursion Manipulation (RM) is to design a calculator that provides formal proofs for a particular type of formulae corresponding to the task of program construction and program verification of recursive procedures. Recalling first that Gödel's result cannot be used as a mathematically justifiable argument against RM, the paper illustrates the strategic importance of RM in the design of autonomous, self-reprogrammable robots. In particular, on the basis of more technical papers making a necessary theoretical support for this paper, we illustrate that for roboticians it is sufficient to be concerned with an external characterization of RM. Relying on the Theory of Constructible Domains, the framework of RM is powerful enough to take care of logical justifications inherent to various forms of induction schemes (i.e., the termination justifications for recursive programs and plans). The paper illustrates also that two, not necessarily compatible, types of efficiency are related to recursive plans.