Program reasoning about own source code

Question

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.

Here were some of my first thoughts on the question (warning: rather vague). See also my comments on Martin Berger's answer.

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-?).

Answer 1

I think you are asking about two different things.

• 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.

What you probably have in mind is something much nicer. E.g. if $P$ is a program, then $\newcommand{\QUOTE}[1]{\langle #1\rangle}\QUOTE{P}$ is $P$, but as data, at hand for manipulation and analysis. This is often called quotation. In practise, quotation is inflexible, so we use quasi-quotation instead, which is a generalisation of quotation where the quote can have 'holes' in which programs can be run that provide data to 'fill' the holes. For example $$\newcommand{\SYNTAX}[1]{\mathsf{#1}} \newcommand{\IF}[3]{\SYNTAX{if}\; #1 \; \SYNTAX{then}\; #2\; \SYNTAX{else}\; #3}\QUOTE{\IF{[\cdot]}{7}{8+9}}$$ is a quasi-quote representing a conditional where instead of a condition we have a hole $[\cdot]$. If the program $M$ evaluates to the data $\QUOTE{x > 0}$, then the quasi-quote $$\QUOTE{\IF{[M]}{7}{8+9}}$$ evaluates to the data $$\QUOTE{\IF{x > 0}{7}{8+9}}.$$

(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. Multi-Stage Programming: Its Theory and Applications.

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

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

4. L. Tratt. Compile-time meta-programming in a dynamically typed OO language.

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

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

7. R. Davies, A Temporal-Logic Approach to Binding-Time Analysis.

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

Answer 2

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.

Answer 3

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.

Answer 4

This paper by Jurgen Schmidthuber might be of interest:

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