Firstly a chess analogy

Suppose that you were part of a team trying to build a chess playing program. Your team has not yet had the fundamental insight of min-max search with approximate evaluations. While you definitely want some people on the team thinking hard about the abstract nature of chess, this is a somewhat serial process, is there anything else that could usefully be done in parallel?

While we wouldn't have the insights to no exactly what a chess engine would look like, we can say some things about the code. The code will almost certainly want some sort of representation of chess pieces or chess boards. So implementing a virtual chessboard would not be a waste of time.

More speculatively, you might overhear the Thinking Hard About Chess department talk about how a good chess position was defined in terms of making the opponents move not good, and invent recursion.

Ideally, when the crucial insights have been had, all the building blocks needed to make it are ready to go. The first chess engine is half a page of chesslang code.

On to AI

So, can we think of any programmatic building blocks that are likely to be useful in building an AI. Yes, arithmatic, if statements, lists and so on.

These features have already been implemented in many programming languages, can we think of any features that might be useful in making AI that aren't easily available in any programming languages?

Much current AI is arithmetical with neural networks and propagation. However, there are already several fairly easy to use libraries for this, and I can't see how to make it substantially easier to program this sort of AI, other than stuff like hyperparameter optimization that lots of people are already working on.

Much theoretical research on AI is symbolic, even Godelian. AIXItl for example, executes every piece of code up to a certain length and runtime. That would suggest that the programming language should make it easy to generate syntactically correct code, and to run it for a bounded time without side effects. This is also what you would want if you were generating code with an evolutionary algorithm.

On the alignment forum, several designs of AI mentioned involve "search for a proof that this piece of code halts". So our programming language for AI should have powerful proof handling facilities.

Suggested Mechanics

Some inspiration for the potential programming language designer

For anyone thinking that lisp isn't abstract and self referential enough

First draft level.

Start with an "everything is a list" approach from lisp/scheme.

First order propositional logic can be defined in terms of the symbols $(,),⟹,\perp$ and the propositions $p_1,p_2,\cdots$. When you are trying to prove something about propositional logic, the fewer symbols to deal with the better. However, when you are trying to prove something in propositional logic, you want extra symbols like $\wedge$. This can be managed by considering $(a\wedge b)$ as syntactic shorthand for $(a⟹(b⟹\perp \left)\right)⟹\perp$. Lisp style macros are good for this.

We can consider programs as formulas in some first order theory.

Consider the program $\text{(+ 5 (* 2 3))}$ The interpreter can syntactically modify it into the simpler program $\text{(+ 5 6)}$ and then into $11$.

A more complex example. $\text{(sum (map '(1 2 3) (lambda (x) (* x x))))}$ goes to $\text{(sum '((* 1 1) (* 2 2) (* 3 3)))}$ then to $\text{(sum '(1 4 9))}$ and finally to $14$.

Considered like this, the interpreter is automatically generating a proof that the program is equal to some value. Its automatically simplifying the program until it gets its answer. Note that it doesn't harness the full power of first order arithmetic, its missing predicates like $(\forall n\in N)$ . It can also get stuck in infinite loops.

In the general view, there are a finite number of transformations that can be applied, and you want a sequence of transformations that leads from one tree to another. These transformations are the atomic tactics. (They are equivalent to axioms in some sense).

Example $\text{(forall (x N) (< x 7))}$ can be transformed by the general rule that for any $\text{y}\in \text{N}$ and function $\text{p}:\text{N}\to \text{Bool}$, expressions of the form $\text{(forall (x N) (p x))}$ are equivalent to $\text{(and (p y) (forall (x N) (p x)))}$. This gives (y=9) $\text{(and (< 9 7) (forall (x N) (< x 7)))}$. This turns into $\text{(and False (forall (x N) (< x 7)))}$ and then $\text{False}$.

Note that the only difference is that here the choice of local transformations is not uniquely determined. $\text{forall}$ makes the abstract symbol $\text{x}$ available in its interior in much the same way that lisps "let" does. Here $\text{N}$ the natural number type. This language would be typed at parse time, the type of an expression should depend only on the type of its sub-components. (A strict interpretation might have less_reals and less_ints distinct functions, one of type, but using the < symbol for both should work.) A type is just a variable of type type, so using a type that you haven't defined, and isn't builtin is just a special case of using an undefined variable. When parsing the code, use of any undefined variable fails syntactically. Types can be combined with union and struct as common in strongly typed programming languages. Standard category theory based type system.

This is where the idea of tactics comes in. (word definition) A tactic is a function that takes in an arbitrary formulae (and possibly some other stuff), and processes it and outputs a semantically identical formulae. (with runtime bounds on it doing so if need be, and the possibility of arbitrary programmer supplied hints)(it applies a series of syntactic transformations)

Here a function is any expression with free variables to substitute. $\text{(lambda (x) (exists (y N) (= (* y 2) x)))}$ is a perfectly good function, which returns $\text{(exists (y N) (= (* y 2) 4))}$ when called on $4$.

One builtin tactic would be evaluate, which evaluates expressions and finite loops, and ignores any predicate. If you just wrapped the rest of the code in an evaluate, an never used any other tactics, you would have a side effect free version of lisp. (or something like it)

Another tactic might be called example, which removes $\left(\exists x\right)$ by having the programmer give a suitable $x$.

A toy example would be this function, which transforms $\exists y:p\left(y\right)$ into $\left(p\right(x\left)\right)\vee (\exists y:p(y\left)\right)$ . Ie $\text{(exists (y N) (= (* y 2) 4))}$ into (using x=2)$\text{(or (= (* 2 2) 4) (exists (y N) (= (* y 2) 4)))}$

$\text{(lambda (f x) (if (= (car f) 'exists) (list 'or (cddr f) (replace f (caadr f) x)) f))}$

Another could be minimize_metric_neighborhood this would take in some metric, eg number of sub-expressions, and try a bunch of other tactics to minimize it.

other tactics would be induction. deduction_thm ect.

The important point is that the programmer is free to design new tactics. The job of the compiler/interpreter is to ensure the tactics transform code in a syntactically valid manor, and to implement the built in tactics.

Note that you need to use a tactic to define new tactics.

Suppose you didn't have the deduction theorem and you wanted to define it

Suppose you provide a function that takes in a proof using the deduction theorem, and outputs a proof not using the deduction theorem, without proving that this function always outputs a valid proof. All you have is a macro, a convenient programmer shortcut. Whenever you use the deduction theorem macro, the proof is expanded out behind the scenes. Convenient, but not a new tactic.

Suppose you prove that "any theorem that can be proved using the deduction theorem can also be proved without it", not necessarily in a constructive manor. Then any time you want to use the deduction theorem, the program can use that tactic without expanding it out in this specific case.

To avoid Lobian obstacles to do with self trusting proof systems, all tactics must have a rank, which is an ordinal.

Suppose a tactic $A$ is defined as an arbitrary function from an expression $e$ and a hint $h$ to an output $s$.

You validate $A$ by proving (using tactics $t_1,t_2\cdots t_n$) that $\forall e:\exists i\in N:\exists r_1,r_2,\cdots r_i\in Q:\exists h_1,h_2,\cdots h_i\in \text{hints}:A(e,h)=r_1\left(r_2\right(\cdots r_i(e,h_i),\cdots ,h_2),h_1)$

(You needn't calculate $r_i$ or $h_i$ explicitly, just show that they must exist.)

Where $Q\subset \text{tactics}$ is a set such that ${sup}_{q\in Q}\left(\text{rank}\right(q)+1)=\alpha$ where $\alpha$ is some ordinal. Then the rank of $A$ must be chosen such that $\text{rank}\left(A\right)\ge \alpha$ and $\forall j\le n:\text{rank}\left(A\right)\ge \text{rank}\left(t_j\right)$. Most of the time, these will be small finite ordinals that could be filled in automatically.

Note that any proof that uses tactics of rank at most $\alpha$ is a valid proof in the language of $ZFC+\alpha$. The basic language would have a ZFC set type, (you need it for the ordinals), but if it wasn't there, you should be able to define it by declaring a bunch of atomic tactics ).

Questions to discuss in comments

1) Is it a good real world strategy to design new programming languages more suitable for AI?

2) Are there any features a good AI language might want other than an excessive amount of self reference and abstract mathematicallity.

3) Any more suggestions or ambiguities related to the programming language outlined above?

4) If a programing language like this already exists, let me know.