Lambda the Ultimate

generic solution for an arbitrary search from start state to end state = AI, the programmer is supposed to write the function. think of initial to goal state as like if the parameters of the function are valid integers within range (initial), this function will output the product of the integers(goal)

If you restrict yourself to int types, and anything that can be mapped to it, you might want to look at BDDs. It is pretty easy to encode the relation between your pre- and poststates as BDDs and extract a function out of it.

I'm still looking into the subject, but just right off the top of my head, this approach is still very similar to standard imperative programming, except that the functions you call might be swapped out for another one that does the same thing. and it doesn't make heads pop =P (I learned lisp instead of prolog)

Do you know Icon? It is goal-directed like Prolog, but imperative. Do you have something similar in mind?

Right, that's the part that I'm working out now. Goal/initial are all states, and defining states in a way that is intuitive to humans, and can be understood by a solver is hard... but it's also what we normally use languages to do. A simple state info would be a list of object value pairs. So to make it intuitive we need to make the objects reflect how we categorize objects. A helpful "library" to include in programs would be a common sense definition of different objects. The hope is that w/ a sorting algorithm, you can just write init: x is-a list, goal: x.list.sorted = true.

Or, nearly impossible with current techniques. [This is the same as asking in COQ to develop a witness (=function) of an ordering relation without user-guidance. Now, mathematically this can be done (just try all algorithms up to a certain complexity), but I don't think COQ can do this without user guidance, yet.]

sorry, i don't understand the issue. Is it with resolving whether or not we're in a specific state?

Unless I misunderstood you. You want to derive a function which takes an unordered list to an ordered list. That means your specification of that function is at least second-order (one order up from prolog). There is no general [effective] means to derive such a function.

[Removed a lot of crap]

...it would be a hard problem, but any automated planning system, just like a human, can sort a list without using a hard-coded algorithm, and could probably do it in polynomial time, too (abstractly, of course).

Caveat: the subject is quite a deep rabbit hole; it's called Automated planning and scheduling. NASA has been using it for awhile in their spacecraft! Read about that here. Generally you can search for "automated planning" and find alot about it.

Other people have used the same idea. Google for goal-based programming. Another similar idea is called declarative metaprogramming, which is somewhat like having IO monads in a logic language.

Hopefully this helps.

Planning through constraint propagation means they're doing some kind of propositional logic. Their problems reduce to problems which are solvable by a sat-solver. Maybe often this means problems will be solvable in polynomial time (if the structure of the problem allows it). However, it is also easy to encode NP-hard problems in SAT, so, no dice: it may be fast for most problems, but you can always encode a problem for which the planner will not find a solution fast (probably).

[I assume they don't restrict their problems to problems which may equivalently stated as boolean logic terms which are in Horn form, because for those particular problems fast linear solvers exist.]

[Actually, I am one of the very few people who believe that P=NP might actually be true. But until someone comes around who actually proves that, and exploitable algorithms come up, that discussion is moot.]

[Hehe, I think I actually found a (small beginning of) an attack on the problem. But I will not share ;-)]

Hmmm, maybe I need to reword some stuff, I didn't intend to build a function generator (that takes in specifications for initial / goal state, and produces a function), but a function library (where the computer can decide which of its functions are best suited to the task at hand). It would be cool if the compiler can fill in the gaps in case it isn't supplied with the function, but just the specs. btw, thanks to everyone for their input, got lots of reading material to go through now =D.

out of a library without explicitly given heuristics, or run-time heuristics, is hard (assuming you know which functions satisfy the specification). If you don't know which functions satisfy a given specification, it is in general impossible for a computer to decide because it would need to give an automatic proof for that.

There is an applied difference between design-by-contract and automated planning:

• In DbC, pre/post conditions act as a controller for program validity (and consequently, our source code).
• In automated planning, pre/post conditions (in conjunction with a goal) act as a controller for execution flow.

Ah. Thank you. I'd overlooked the comment to the effect that "...a STRIPS-like calculation will be done to plan which specific functions to call..." I agree, that sounds like automated planning (the reference to STRIPS should have caught my eye). There's certainly been plenty of work in that area, including practical applications in areas like spacecraft autonomy (e.g. compiling high-level science goals down to low-level spacecraft commands).

I fear I don't see why it is innovative. Are you referring to template meta-programming or to generic programming in general?

This is idea is far from new, nor did it originate with C++. I suggest you pursue the LtU archive, where generic programming in its many forms, as well as Stepanov's earlier work (in Ada) were discussed many times.

Like I said, all this was discussed here many times.
Please try to post your replies by clicking "reply" so as to maintain threading.

Check out:

Ireland and Stark (2006). Combining Proof Plans with Partial Order Planning for Imperative Program Synthesis. In Journal of Automated Software Engineering 13(1).

The article descibes an implemented system that does synthesis of code based on Hoare logic. It does not handle prewritten subroutines, though handling that is mentioned in the further work section. The central technique is searching the space of proofs in Hoare logic of the desired specification, and the heart of the discussion is focussed on the problem area #2 I described above, where they use partial-order planning. They describe its application to some small examples that involve synthesis of loops. The authors cite no similar work (except their own prior efforts), but some prior works on automatic program synthesis by Manna and Waldinger (1977 & later), Dershowitz and Reddy (1994), and also some later articles on logic program synthesis.

I think it is clear that, while there is extensive relevant literature, your idea is quite different from anything described in this thread.

As a point of etiquette, the LtU social norms are to use real names; cf. Marc Hamman Most of us here post with our real, full names as a sign that we are prepared to stand behind our opinions, from The Spirit of LtU. So maybe...

The secret it out!! my pseudonym is my real-nym in disguise =P

I gave some unintelligent remarks which I'll try to clarify, for your benefit (I hope).

You're going to do something with pre-/postconditions, goals and program derivation. so you'll end up doing something with logic (and you are restricted to fundamental results in logic).

To go up the tree, here are some fundamental results (I can think of):

1. your pre- postconditions are stated in (or equivalent to) propositional logic. You can use BDDs to describe the relation and derive functions from them. (Or use BDD checking to see that your relation holds).

2. your pre- postconditions are stated in/equivalent to first-order predicate calculus (in Horn from) (i.e. Prolog). You can use unification for specific instances to derive solutions. You can get rid of the Horn form restriction, I think at the expense of a possible exponential blow-up of the term (I am not sure here).

3. your pre- postconditions are stated in (second or) higher order logic and you try to find matching functions. You can use tactics and heuristics to prove correctness to spec. But don't expect proofs for programs complexer than, say fac, and maybe, sorting.

4. your pre- postconditions are stated in (second or) higher order logic. You can use tactics and heuristics to derive programs, and proofs from the specifications. But don't expect to derive any programs complexer than, say fac.

5. your pre- postconditions are stated in higher order logic but over a finite domain. Try to use quantified BDDs. I have no idea where you'll end up.

I think I understand what you're trying to say... that if you have a well-defined pre-post condition, you can use a variety of methods to create functions. That's good and well, and I would probably include something like it in the language, but the problem I see with making that an integral part of the language is that there isn't a one-size fits-all planner.
Mainly, the issue is, as you mentioned, the expressiveness of the knowledge representation. Too expressive, and the search space explodes, and it'll take forever. Not expressive enough and there will be many things you can't solve.
I hoped to have a very expressive kr, ideally one that can express anything you need with as little repetition as possible, that will store the function's information. As a programming language, the programmer will input the plan (in a classical planning sense) and we won't have to worry about search space. The compiler would have enough information, however, to swap out functions that do the same thing, but better for a given situation.
I think your suggestion would work well with this idea, because you can convert a subset of the functions in a library from the high order logic into a lower order one, and create other functions on the fly. But I wanted to leave that part up to the programmer to fiddle with, not the language.
I know I wasn't clear on the STRIPS part, which prolly confused a lotta people, but it's mostly because there are still a lotta hairy issues w/ it and I didn't think it was central to the main idea of the language. The reason why I need a planner here is to find out about state information. It's impossible and illogical to store ALL the information in the world, you should store just the ones you need -- you don't care about the weather when you're cooking indoors, but you do care about the weather when you need to go out to buy eggs. So the planner is supposed to spit out the information that each algorithm needs by using a library of information retrieval functions (ie the goal is to obtain information). The other option (which I think is less elegant) would be to make no distinction between information retrieval functions and normal functions, and require the user to call them manually (through goal-based function calls, of course), but then garbage collection would be needed.
So hopefully that was clear, if not, please wait till I read up on some of these papers, make some decisions on this aspect of the language, and write a follow-up to the original post.

It's the logical expressiveness of your language, or the equivalence of it to a certain logic, which decides up to what point you can automate parts of your language. [I don't write professionaly about it so it takes some time to state it correctly.]

I don't understand STRIPS, didn't read enough about it. (I think I saw linear backchaining [uh, I meant linear search], which would hint at a weak form of boolean logic, or some resolution based proving. Dunno)

What I get from most planners is that they start out as general solvers on (something as expressive as) boolean logic, and features are added which improve the expressiveness.

I would say that is the wrong way around. If you want to implement a [planner] language with a certain expressiveness, choose a logic which will satisfy your requirements, choose a technology you can easily implement, and build a planner language around that.

[Actually, if it is a planning language you want. I guess I would look at QBDDs, unless you're looking at infinite domains.]

[And also, sorry to say, but I don't like your approach which would work with adding features. Say you start out with something equivalent to boolean logic and add some specific search algorithms on first-order predicates you also want to express. You'll end up with some (weird) hybrid between a classical boolean solver and Prolog. Plz, just implement something akin to Prolog and you're done, and you'll know exactly what is expressible and what not. Or go QBDDs, or something.]