From: crawford@boole.mitre.org (Randy Crawford)
Subject: Re: Programming by Description of Output...
Organization: The MITRE Corporation, McLean, VA
Date: Mon, 4 Jan 1993 05:09:05 GMT

In article <C01yxr.BGF@phage.cshl.org> boutell@isis.cshl.org (Tom Boutell) writes:
>In learning about methods of proving algorithms correct (and the
>various difficulties of doing same), I have come to wonder
>to what degree it is possible to create a language in which
>the programmer specifies not the steps to be accomplished
>but rather the goal to be achieved-in other words, whether it
>is possible, working from a specification of the initial state
>and a specification of the final state, to derive an algorithm
>automatically which permutes the one into the other. I suppose
>this is similar to other generalized AI problem-solving tasks,
>but a notable advantage is that the goal state is well-defined
>(none of the AI problems of needing to operate in non-abstract
>universes come into play, at least not for a decently interesting
>set of cases). 
>
>Are there languages/programming systems that attempt this sort
>of thing? I'm sure it's impossible to guarantee a solution
>to every request that has a possible solution, since this would
>imply the ability to prove that fact, and the statement of the
>problem is likely to be equivalent to second-order predicate
>calculus, in which a proof (by resolution) cannot be guaranteed 
>in finite time. But if the system can recognize solved problems
>as subsets of the problem at hand, it can move more quickly toward
>assembling a solution, or deciding it's overwhelmed. 
>
>An example of what I have in mind:
>
>Initial state:
>Array A[] contains n whole numbers. 
>Final state:
>Array B[] contains n whole numbers such that each element of
>A[] appears in B[] and for all i such that 1<=i<n, B[i]<B[i+1].
>
>How might the problem of calculating B[] (a sorted version of
>A[]) be solved in a general fashion, absent a known
>method of sorting?

I see a couple of responses to your query.

1)  John Koza of Stanford has written a recent text on the use of genetic 
    algorithms in developing programs which have clearly defined start and 
    end states.

    At AAAI-92 in San Jose, I saw him describe a system he had devised which
    generated Lisp code for use in a Pac-Man game to maneuver yourself 
    properly through the antagonists without being eaten, while also 
    eating all the edibles as well as activating the occasional role-reversal 
    triggers and then pursuing your pursuers.  It seemed to work rather well
    in devising the program on its own with no human intervention, as I 
    recall.  Of course, the Lisp was completely illegible.

    In this case, the goal state was an evaluation function which determined
    where changes to the program might be made to improve the next generation
    of the program.  It was an interesting idea.


2)  As someone else has pointed out, there's been a lot of work at all levels
    of automatic programming from formal requirement specification languages
    to verifiable implementation PLs to very-high-level PLs which bind the two 
    together into a complete application development system.  

    As I see it, the problem with these is the fact that in any novel software
    system, the fraction of the requirements which are known falls somewhere 
    between 70% and 10%.  If the software developer (a domain expert, not a 
    programmer) is to iterate through each version of the system, alternately 
    specifying and then generating a new implementation, an awful lot of CPU 
    horsepower will be necessary to regenerate each new system as the end user
    looks at each incarnation and says, "No.  That's not quite what I had in 
    mind.  Please change everything."

    Of course, something like this is in the cards eventually.  But considering
    the mind-boggling complexity necessary to verify even a small bit of code
    now, and the great difficulty in implementing a constraint-style PL to
    perform all the algebraic translations and transformations necessary in
    sych a system, a complete verifiable VHLPL is going to be a long time in 
    coming, and a really useable system much longer yet.

    And then there's the ever-present looming spectre of the halting problem
    to contend with.  Every program must necessarily be composed with only 
    first-order predicate logical constructions and be complete in its
    specification.  The VHLPL will have to be able to detect violations of 
    these too.  So much for Lisp closures.

    Of course, this doesn't even begin to address the automatic programming 
    of high level algorithmic constructs like "Give me an efficient solution 
    to this problem."  And the system decides to use a dynamic programming
    approach to a travelling salesman model of the problem.  Yeah.  Right.

    
    Both are interesting, but not the place for your retirement investments.



-- 

| Randy Crawford        crawford@mitre.org        The MITRE Corporation
|                                                 7525 Colshire Dr., MS Z421
| N=1 -> P=NP           703 883-7940              McLean, VA  22102