Program reasoning about own source code

manpreet Best Answer 2 years ago

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

manpreet 2 years ago

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 PP is a program, then ⟨P⟩⟨P⟩ is PP, 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

is a quasi-quote representing a conditional where instead of a condition we have a hole [⋅][⋅]. If the program MM evaluates to the data ⟨x>0⟩⟨x>0⟩, then the quasi-quote

evaluates to the data