I’ve thought a fair bit about PLs for AI, mostly when I get pissed off by how bad current languages are for certain AI-related things.
My biggest complaint is: most languages make it a huge pain to write code which reasons about code written in the same language. For example: try writing a python function which takes in another python function, and tries to estimate its asymptotic runtime by analyzing the code. It doesn’t need to always work, since the problem is undecidable in general, but it would be nice if it could handle one specific thing, like maybe estimating runtime of a dynamic programming algorithm. Problem is, even if you have a nice algorithm for calculating asymptotic runtime of DP, it will be a huge pain to implement it—at best you’ll be working with an abstract syntax tree of the python function.
LISP makes this a bit more pleasant, since the code itself is already a data structure—the abstract syntax tree is the code. But abstract syntax trees still just aren’t that great a representation for reasoning about code. We use trees, and write tree-shaped code, because trees can be represented neatly in linear text files (by nesting lots of parens () or similar delimiters {}). But the semantics of code, or the execution of code, is usually not tree-shaped. What we’d really like is a better data structure for representing programs, something which is inherently closer to the semantics rather than the syntax. Then, with that data structure in hand, we could work backwards to find a good language to represent it.
I also have some opinions about what that data structure should be, but at this point I think posing the question is more useful than arguing about a solution. If you’re thinking about proofs and tactics, then I’d recommend thinking about a representation of tactics which makes it elegant and easy for them to operate on other tactics.
I’ve thought a fair bit about PLs for AI, mostly when I get pissed off by how bad current languages are for certain AI-related things.
My biggest complaint is: most languages make it a huge pain to write code which reasons about code written in the same language. For example: try writing a python function which takes in another python function, and tries to estimate its asymptotic runtime by analyzing the code. It doesn’t need to always work, since the problem is undecidable in general, but it would be nice if it could handle one specific thing, like maybe estimating runtime of a dynamic programming algorithm. Problem is, even if you have a nice algorithm for calculating asymptotic runtime of DP, it will be a huge pain to implement it—at best you’ll be working with an abstract syntax tree of the python function.
LISP makes this a bit more pleasant, since the code itself is already a data structure—the abstract syntax tree is the code. But abstract syntax trees still just aren’t that great a representation for reasoning about code. We use trees, and write tree-shaped code, because trees can be represented neatly in linear text files (by nesting lots of parens () or similar delimiters {}). But the semantics of code, or the execution of code, is usually not tree-shaped. What we’d really like is a better data structure for representing programs, something which is inherently closer to the semantics rather than the syntax. Then, with that data structure in hand, we could work backwards to find a good language to represent it.
I also have some opinions about what that data structure should be, but at this point I think posing the question is more useful than arguing about a solution. If you’re thinking about proofs and tactics, then I’d recommend thinking about a representation of tactics which makes it elegant and easy for them to operate on other tactics.