Zhentao Li

École normale supérieure

Fixed Points and Self-referential Programs

A quine is a computer program that outputs its own source code when run, i.e., it is a fixed point of the "run" (or "evaluate") function. We discuss how a generalization of quines could be used to speed up computer program creation (by human programmers). By moving in the space of all possible programs that can generate themselves as well as "nearby" programs, we can arrive at a final destination program more quickly. We illustrate this method using examples from different contexts and discuss some theoretical subproblems. If time permits, I will discuss possible generalization of this approach applied to theorem proving.