# Program reasoning about own source code

The inspiration for this question is the following (vague) question: What are the programming language/logical foundations for having an AI which could reason about its own source code and modify it?

This isn't at all rigorous, so here is my attempt to extract a concrete question out of it. There are two things I'm interested in:

(A) A programming language P that can represent and manipulate its own programs as a datatype Program (e.g., as an AST). (If desired, a object of type Program can be converted into a String, which is the text of a valid program in that language. This would be the opposite of what a compiler does.)

(B) A method to reason about what a program in language P does. Here are two levels I'm thinking about it:

1. Another language Q (with theorem proving capabilities) which models what a P-program does. It should be able to express and prove statements like "the outcome of running Program p is foo."
2. A way to reason about what a program p:Program does in the language P itself. (So we are taking P=Q above.)

To what degree has something like this been implemented, or what is progress in this direction? What are the practical obstacles? In light of the original intention of the question, what is the best way to formalize the problem?

*

As the answers show (thanks!), both (A) and (B1) can be done separately, though it seems doing them together is more of a research question.

I'm interested in the programming language modeling the same programming language, rather than a simpler one (so P=Q above). This would be a "proof of concept" of a program being able to "reason about its own source code." Dependently typed programming languages can give guarantees about the outputs of its functions, but this doesn't count as "reasoning about its own source code" any more than a "Hello world!" counts as a quine in a language that will automatically prints out a naked string---there needs to be some kind of quoting/self-reference. The analogue here is having a datatype representing Program.

It seems like a rather large project - the simpler the language, the harder it is to express everything within it; the more complicated the language, the more work has to be done to model the language.

In the spirit of the Recursion Theorem, a program can then "get" its own source code and modify it (i.e., output a modified version of itself). (B2) then tells us that the program should be able to express a guarantee about the modified program (this should be able to recurse, i.e., it should be able to express something about all future modifications-?).

• Why do you need the language to act as a theorem prover to establish that "the outcome of running Program p is foo"? The language could simply run p! Indeed, that's what's happening. – Martin Berger Sep 4 '15 at 19:11
• en.wikipedia.org/wiki/Reflection_(computer_programming) – Kaveh Sep 4 '15 at 20:24
• Note that in principle all language which can implement an interpreter for themselves can do things you are requiring. In a more mathematical way, the recursion theorem holds for any strong enough model of computation. Some programming languages just make it easier by having it built in. Same for reasoning: you can implement any reasoning system inside these languages. Of course one cannot expect to reason everything, e.g. the halting problem for the programs. – Kaveh Sep 4 '15 at 20:35
• I think the question is not very clear. You should have a look at the programming languages like Python, Java, and those mentioned by Martin in his answer and clarify the question so either it is clear that they meet what you are looking for or if not why not. – Kaveh Sep 4 '15 at 20:36
• @HoldenLee As to "P=Q", the established terminology is "homogeneous meta-programming", which is opposed to "heterogeneous meta-programming" where P $\neq$ Q. – Martin Berger Sep 5 '15 at 6:04

• The ability of a programming language to represent all its programs as data.
• Reasoning about programs as data.

For analytical purposes it's useful to keep them apart. I will focus on the former.

The ability of a programming languages to represent, manipulate (and run) its programs as data goes under terms such as meta-programming or homoiconicity.

In an (awkward) way, all well-known programming languages can do meta-programming, namely by using the string data type together with the ability of invoking external programs (compiler, linker etc) on strings (e.g. by writing them to the file system first). However, that's probably not what you mean. You probably have nice syntax in mind. Strings are not nice syntax for program representation because almost all strings don't represent programs, i.e. the string data type contains a lot of 'junk' when seen as a program representation mechanism. To make matters worse, the algebra of string operations has essentially no connection with the algebra of program construction.


(Note that $M$ is a normal program (not a program as data) that returns a quoted program, i.e. program as data.) In order for this to work, you need a data-type to represent programs. Typically that data-type is called AST (abstract syntax tree), and you can see (quasi-)quotes as abbreviation mechanisms for ASTs.

Several programming languages offer quasi-quotes and other feature for meta-programming. It was Lisp with its macroing functionality that pioneered this ability to treat programs as data. Perhaps unfortunately, the power of Lisp-based macros was long seen to rest largely on Lisp’s minimalistic syntax; it was not until MetaML (1) that a modern, syntactically rich language was shown to be capable of meta-programming. Since then, MetaOCaml (2) (a descendant of MetaML, important for its breakthrough in the still ongoing quest to solve the problem of how to type programs as data), Template Haskell (3) and Converge (4) (the first language to get all key meta-programming features right in my opinion) have shown that a variety of modern programming languages can house meta-programming. It is important to realise that we can take any programming language $L$ and turn it into a meta-programming language $L_{mp}$ that is $L$ together with the ability of representing (and evaluating) its own programs as data.

Representing the outcome of running program, given as data, is achieved by adding an $\newcommand{\EVAL}{\mathsf{eval}}\EVAL(\cdot)$ function that takes a program (given as data) as input and runs it, returning its result. E.g. if $P$ is a program evaluating to 17 and $\QUOTE{P}$, the (quasi-)quoted version of $P$, i.e. $P$ as data, then $\EVAL(\QUOTE{P})$ also returns 17. There are all manner of subtleties here that I'm ignoring here such as the question when meta-programmed programs are being evaluated (giving rise to the distinction between compile-time and run-time meta-programmed), what to do with types or failing evaluations, what happens to bound and free variables in the process of going from $P$ to $\QUOTE{P}$ or vice versa.

As to the second dimension, reasoning about programs given as data. As soon as you can convert programs into data, they are 'normal' data and can be reasoned about as data. You can use all manner of prover technology, e.g. dependent types or contracts or interactive theorem provers or automated tools, as Joshua has pointed out. However you will have to represent the semantics of your language in the reasoning process. If that language, as you require, have meta-programming abilities, things can become a bit tricky and not much work has been done in this direction, with (5) being the only program logic for this purpose. There is also Curry-Howard based work on reasoning about meta-programming (6, 7, 8). Note that these logic-based approaches, and the type-based approach (2) can indeed express properties that hold for all future meta-programming stages. Apart from (2) none of those papers have been implemented.

In summary: what you asked for has been implemented, but it's quite subtle, and there are still open questions, in particular to do with types and streamlined reasoning.

1. W. Taha and M. F. Nielsen. Environment classifiers.

2. T. Sheard and S. Peyton Jones. Template meta-programming for Haskell.

3. M. Berger, L. Tratt, Program Logics for Homogeneous Meta-Programming.

4. R. Davies, F. Pfenning, A modal analysis of staged computation.

5. T. Tsukada, A. Igarashi. A logical foundation for environment classifiers.

• You're right - the programming language P can be different from the language Q that expresses theorems/proofs about programs in that language (which can be in Coq for instance). The kind of theorem that I'm thinking about goes like this: Suppose we have a carefully designed program A_1. Thm: For every n the following holds: Program A_n will output (m_n, A_{n+1}), where m_n is an integer, A_{n+1} is another program (e.g., obtained by modifying A_n in some way), and for all n, we have that m_n>0. – Holden Lee Sep 4 '15 at 20:43
• (The science fiction version of this is that we have a "proof" that a program that keeps modifying itself, will never press the button that launches a nuclear missile, say, or that the program will always optimize a certain quantity.) – Holden Lee Sep 4 '15 at 20:43
• This is why I wanted to make a distinction between running the program, and reasoning on what the program will output - we want to know properties of what it will do before it's run, without running it. Note that if we want A_n to be able to "modify its source code" to produce A_{n+1}, then P will necessarily have metaprogramming abilities (which puts us in the position of (5)). – Holden Lee Sep 4 '15 at 20:43
• It still seems to me that it would be interesting for P=Q. Hypothetically, A is an AI program and the way that would modify itself is by reasoning about its own code - for example, write down theorems about bits of code, proving them, and only then modifying its code. Then it seems P would need to have the capabilities of Q. – Holden Lee Sep 4 '15 at 20:43
• @HoldenLee It's possible to write programs like A_n. If you use strings as representative of programs, this can be done trivially in any language, if you want quasi-quotes or similar, this is possible in e.g. Converge. I don't understand the role of m_n in the construction. – Martin Berger Sep 4 '15 at 20:48

No there is no current system that does all four steps in your system. If you want to design a system one of the first requirements is homoiconic language. At minimum you would want your core programming language that you have as small as possible so that when you enter the system and start to make it interpret itself it will work. So therefore you want a metacircular interpreter which was pioneered in lisp. Other languages have done it also but there is a enormous amount of existing research on lisp.

The first step if you want to do this is to have a homoiconic language like Lisp or some framework where you can reason about a running program. Lisp is used for this for the sole reason that you could define a metacircular interpreter in the language or you can just treat your code as data. Treating the code as data is the most important thing. There is along discussion about what homoiconic means on c2 wiki.

For example in Lisp your "Program" datatype is valid lisp programs. You pass the lisp programs to an interpreter and it computes something. It gets rejected by the interpreter if you don't program a valid "Program".

Therefore a homoiconic language does three of your requirements. You can even in lisp define the idea of a formal program.

Can you model lisp inside lisp? Yes this is frequently done mainly as an exercise at the end of a lisp programming book to test your abilities. SICP

At the current time issue four is a research question and below is what I have found that attempts to answer this question.

I would say there are many types of programs that attempt to do this. Below is all of the programs that I know about.

• JSLint is an example of a static analyzers that take machine code or some other language and look for bugs explicitly. Then it asks for a programmer to correct that.

• Coq is a environment that allows you to specify proofs using a programming language. It also has tactics where it suggests ways for you to solve the problem. Still this expects a human to do the work. Coq uses dependant types to work and is therefore very type theoretic. It is very popular among computer scientists and people working on Homotopy Type Theory.

• ACL2 on the other hand is an automated theorem prover. This system will prove statements based on something that you program.

• ACL2 and Coq have a software plugin that interface their system with a machine learning system. What is used to train these systems are previously written programs. From my understanding these systems add another feature where you have not only your tactics but suggested theorems that aid in proof development.

Below is more of a foundational of what your question means.

• gcc is an example of an optimizng compiler which can take itself as input and then output an optimized version of itself. The idea of a compiler that translates programs from one representation to another and improves the speed due to some optimization flag is very well understood. Once you bootstrap the compiler and it generates valid machine code then you can add an optimization and recompile the compiler and it makes a more efficient version of itself.
• There is no need to make the language as minimal as possible. You can add the relevant meta-programming features to any language. Taha's MetaML work has shown this. Indeed the addition of meta-programming capabilities is mechanical. – Martin Berger Sep 4 '15 at 19:17
• I also disagree that "no current system that does all four steps". Question 4 only talks about running programs given as code. That's perfectly possible, indeed even Javascript's eval does it. – Martin Berger Sep 4 '15 at 19:18
• @MartinBerger what I mean is you make the core kernel as minimal as possible . Also if you even begin to want to hope that your system will do #4 you will want a system that you can train not just humans but computers to use so it would benefit you to have a minimal system and they have libraries that are coded in that system like a meta programming template – Joshua Herman Sep 4 '15 at 19:19
• It depends on what (4) we are talking about. The original question contains two elaborations of those. The first is trivial, you just run the program. The second one can be handled by the logic I cited as (5) in my answer of the typing system (2). The later is implemented in MetaOCaml. But there is scope for more research: neither (2) nor (5) can deal with arbitrary forms of meta-programming, and the properties guarantedd by (2) are a bit weak (after all, it's a typing system with type inference). – Martin Berger Sep 4 '15 at 19:34
• As to "you make the core kernel as minimal as possible": that's not required. You can add full meta-programming to any language. – Martin Berger Sep 4 '15 at 19:36

As @user217281728's answer mentions there are a type of machines related more to inference and AI, called Gödel Machines

A Gödel machine is a self-improving computer program invented by Jürgen Schmidhuber that solves problems in an optimal way. It uses a recursive self-improvement protocol in which it rewrites its own code when it can prove the new code provides a more optimal strategy. The machine was invented by Jürgen Schmidhuber, but is named after Kurt Gödel who inspired the mathematical theories.

The referenced publication of Jürgen Schmidhuber on "Goedel Machines: Self-Referential Universal Problem Solvers Making Provably Optimal Self-Improvements", (2006) arXiv:cs/0309048v5

The way the machine works to implement meta-learning has two phases:

1. Learning from data (level 1, learn)
2. Using learned data to modify/optimise its source code/algorithm (level 2, learn to learn)

Since the machine modifies its own source it is self-referential, i.e has the self-modification property (see also here).

In this sense it can modify the learning algorithm itself in a rigorous sense (proving optimal self-modifications). There are the problems with self-reference and undecidability which in this case take the form:

..a Gödel machine with unlimited computational resources must ignore those self-improvements whose effectiveness it cannot prove

Other languages (and their associated interpreter machines) which have the self-modification property are for example LISP.

In LISP code and data are inter-changeable, or the source code AST is available as data, in the LISP program and can be modified as data. On the other hand, data can be seen as AST, for some source code.

update

There are other machines as well, like self-programming machines (among others) which combine self-reference, self-reproduction and self-programming.

One interesting aspect of the above is that self-reference is not problematic at all, rather it is a necessary element in self-reproduction / self-programming automata.

For further details (and more publications) refer to J.P Moulin, C.R Biologies 329 (2006)

abstract

Living systems are capable to have appropriate responses to unpredictable environment. This kind of self-organisation seems to operate as a self-programming machine, i.e an oprganisation able to modify itself. Until now the models of self-organisation of living beings proposed are functions solutions of differential systems or transition functions of automata. These functions are fixed and these models are therefore unable to modify their organisation. On the other hand, computer science propose a lot of models having the properties of adaptive systems of living beings, but all these models depend on the comparison between a goal and the results and ingenious choices of parameters by programmers, whereas there are no programmer's intention nor choice in the living systems. From two best known examples of adaptive systems of living beings, nervous system and immune system that have in common that the external signals modify the rewriting of their organisation and therefore works as a self-organising machines, we devised machines with a finite set of inputs, based upon a recurrence, are able to rewrite their organisation (Self-programming machines or $\mathbb{m}_\mathbb{sp}$) whenever external conditions vary and have striking properties of adaptation. $\mathbb{M}_\mathbb{sp}$ have similar properties whatever the operation defining the recurrence maybe. These results bring us to make the following statement: adaptive properties of living systems can be explained by their ability to rewrite their organisation whenever external conditions vary under the only assumption that the rewriting mechanism be a deterministic constant recurrence in a finite state set.

This paper by Jurgen Schmidthuber might be of interest:

http://arxiv.org/pdf/cs/0309048.pdf

• plz give a summary at least – vzn Jan 22 '16 at 5:09