Programming Languages For AI

Firstly a chess analogy

Sup­pose that you were part of a team try­ing to build a chess play­ing pro­gram. Your team has not yet had the fun­da­men­tal in­sight of min-max search with ap­prox­i­mate eval­u­a­tions. While you definitely want some peo­ple on the team think­ing hard about the ab­stract na­ture of chess, this is a some­what se­rial pro­cess, is there any­thing else that could use­fully be done in par­allel?

While we wouldn’t have the in­sights to no ex­actly what a chess en­g­ine would look like, we can say some things about the code. The code will al­most cer­tainly want some sort of rep­re­sen­ta­tion of chess pieces or chess boards. So im­ple­ment­ing a vir­tual chess­board would not be a waste of time.

More spec­u­la­tively, you might over­hear the Think­ing Hard About Chess de­part­ment talk about how a good chess po­si­tion was defined in terms of mak­ing the op­po­nents move not good, and in­vent re­cur­sion.

Ideally, when the cru­cial in­sights have been had, all the build­ing blocks needed to make it are ready to go. The first chess en­g­ine is half a page of chess­lang code.

On to AI

So, can we think of any pro­gram­matic build­ing blocks that are likely to be use­ful in build­ing an AI. Yes, ar­ith­matic, if state­ments, lists and so on.

Th­ese fea­tures have already been im­ple­mented in many pro­gram­ming lan­guages, can we think of any fea­tures that might be use­ful in mak­ing AI that aren’t eas­ily available in any pro­gram­ming lan­guages?

Much cur­rent AI is ar­ith­meti­cal with neu­ral net­works and prop­a­ga­tion. How­ever, there are already sev­eral fairly easy to use libraries for this, and I can’t see how to make it sub­stan­tially eas­ier to pro­gram this sort of AI, other than stuff like hy­per­pa­ram­e­ter op­ti­miza­tion that lots of peo­ple are already work­ing on.

Much the­o­ret­i­cal re­search on AI is sym­bolic, even Godelian. AIXItl for ex­am­ple, ex­e­cutes ev­ery piece of code up to a cer­tain length and run­time. That would sug­gest that the pro­gram­ming lan­guage should make it easy to gen­er­ate syn­tac­ti­cally cor­rect code, and to run it for a bounded time with­out side effects. This is also what you would want if you were gen­er­at­ing code with an evolu­tion­ary al­gorithm.

On the al­ign­ment fo­rum, sev­eral de­signs of AI men­tioned in­volve “search for a proof that this piece of code halts”. So our pro­gram­ming lan­guage for AI should have pow­er­ful proof han­dling fa­cil­ities.

Suggested Mechanics

Some in­spira­tion for the po­ten­tial pro­gram­ming lan­guage designer

For any­one think­ing that lisp isn’t ab­stract and self refer­en­tial enough

First draft level.

Start with an “ev­ery­thing is a list” ap­proach from lisp/​scheme.

First or­der propo­si­tional logic can be defined in terms of the sym­bols and the propo­si­tions . When you are try­ing to prove some­thing about propo­si­tional logic, the fewer sym­bols to deal with the bet­ter. How­ever, when you are try­ing to prove some­thing in propo­si­tional logic, you want ex­tra sym­bols like . This can be man­aged by con­sid­er­ing as syn­tac­tic short­hand for . Lisp style macros are good for this.

We can con­sider pro­grams as for­mu­las in some first or­der the­ory.

Con­sider the pro­gram The in­ter­preter can syn­tac­ti­cally mod­ify it into the sim­pler pro­gram and then into .

A more com­plex ex­am­ple. goes to then to and fi­nally to .

Con­sid­ered like this, the in­ter­preter is au­to­mat­i­cally gen­er­at­ing a proof that the pro­gram is equal to some value. Its au­to­mat­i­cally sim­plify­ing the pro­gram un­til it gets its an­swer. Note that it doesn’t har­ness the full power of first or­der ar­ith­metic, its miss­ing pred­i­cates like . It can also get stuck in in­finite loops.

In the gen­eral view, there are a finite num­ber of trans­for­ma­tions that can be ap­plied, and you want a se­quence of trans­for­ma­tions that leads from one tree to an­other. Th­ese trans­for­ma­tions are the atomic tac­tics. (They are equiv­a­lent to ax­ioms in some sense).

Ex­am­ple can be trans­formed by the gen­eral rule that for any and func­tion , ex­pres­sions of the form are equiv­a­lent to . This gives (y=9) . This turns into and then .

Note that the only differ­ence is that here the choice of lo­cal trans­for­ma­tions is not uniquely de­ter­mined. makes the ab­stract sym­bol available in its in­te­rior in much the same way that lisps “let” does. Here the nat­u­ral num­ber type. This lan­guage would be typed at parse time, the type of an ex­pres­sion should de­pend only on the type of its sub-com­po­nents. (A strict in­ter­pre­ta­tion might have less_re­als and less_ints dis­tinct func­tions, one of type, but us­ing the < sym­bol for both should work.) A type is just a vari­able of type type, so us­ing a type that you haven’t defined, and isn’t builtin is just a spe­cial case of us­ing an un­defined vari­able. When pars­ing the code, use of any un­defined vari­able fails syn­tac­ti­cally. Types can be com­bined with union and struct as com­mon in strongly typed pro­gram­ming lan­guages. Stan­dard cat­e­gory the­ory based type sys­tem.

This is where the idea of tac­tics comes in. (word defi­ni­tion) A tac­tic is a func­tion that takes in an ar­bi­trary for­mu­lae (and pos­si­bly some other stuff), and pro­cesses it and out­puts a se­man­ti­cally iden­ti­cal for­mu­lae. (with run­time bounds on it do­ing so if need be, and the pos­si­bil­ity of ar­bi­trary pro­gram­mer sup­plied hints)(it ap­plies a se­ries of syn­tac­tic trans­for­ma­tions)

Here a func­tion is any ex­pres­sion with free vari­ables to sub­sti­tute. is a perfectly good func­tion, which re­turns when called on .

One builtin tac­tic would be eval­u­ate, which eval­u­ates ex­pres­sions and finite loops, and ig­nores any pred­i­cate. If you just wrapped the rest of the code in an eval­u­ate, an never used any other tac­tics, you would have a side effect free ver­sion of lisp. (or some­thing like it)

Another tac­tic might be called ex­am­ple, which re­moves by hav­ing the pro­gram­mer give a suit­able .

A toy ex­am­ple would be this func­tion, which trans­forms into . Ie into (us­ing x=2)

Another could be min­i­mize_met­ric_neigh­bor­hood this would take in some met­ric, eg num­ber of sub-ex­pres­sions, and try a bunch of other tac­tics to min­i­mize it.

other tac­tics would be in­duc­tion. de­duc­tion_thm ect.

The im­por­tant point is that the pro­gram­mer is free to de­sign new tac­tics. The job of the com­piler/​in­ter­preter is to en­sure the tac­tics trans­form code in a syn­tac­ti­cally valid manor, and to im­ple­ment the built in tac­tics.

Note that you need to use a tac­tic to define new tac­tics.

Sup­pose you didn’t have the de­duc­tion the­o­rem and you wanted to define it

Sup­pose you provide a func­tion that takes in a proof us­ing the de­duc­tion the­o­rem, and out­puts a proof not us­ing the de­duc­tion the­o­rem, with­out prov­ing that this func­tion always out­puts a valid proof. All you have is a macro, a con­ve­nient pro­gram­mer short­cut. When­ever you use the de­duc­tion the­o­rem macro, the proof is ex­panded out be­hind the scenes. Con­ve­nient, but not a new tac­tic.

Sup­pose you prove that “any the­o­rem that can be proved us­ing the de­duc­tion the­o­rem can also be proved with­out it”, not nec­es­sar­ily in a con­struc­tive manor. Then any time you want to use the de­duc­tion the­o­rem, the pro­gram can use that tac­tic with­out ex­pand­ing it out in this spe­cific case.

To avoid Lo­bian ob­sta­cles to do with self trust­ing proof sys­tems, all tac­tics must have a rank, which is an or­di­nal.

Sup­pose a tac­tic is defined as an ar­bi­trary func­tion from an ex­pres­sion and a hint to an out­put .

You val­i­date by prov­ing (us­ing tac­tics ) that

(You needn’t calcu­late or ex­plic­itly, just show that they must ex­ist.)

Where is a set such that where is some or­di­nal. Then the rank of must be cho­sen such that and . Most of the time, these will be small finite or­di­nals that could be filled in au­to­mat­i­cally.

Note that any proof that uses tac­tics of rank at most is a valid proof in the lan­guage of . The ba­sic lan­guage would have a ZFC set type, (you need it for the or­di­nals), but if it wasn’t there, you should be able to define it by declar­ing a bunch of atomic tac­tics ).

Ques­tions to dis­cuss in comments

1) Is it a good real world strat­egy to de­sign new pro­gram­ming lan­guages more suit­able for AI?

2) Are there any fea­tures a good AI lan­guage might want other than an ex­ces­sive amount of self refer­ence and ab­stract math­e­mat­i­cal­lity.

3) Any more sug­ges­tions or am­bi­gui­ties re­lated to the pro­gram­ming lan­guage out­lined above?

4) If a pro­gram­ing lan­guage like this already ex­ists, let me know.