NetNews Usenet Archive 1993 #1/NN_1993_1.iso/spool/comp/programm/3404

Text File | 1993-01-04 | 5.4 KB | 111 lines

Newsgroups: comp.programming
Path: sparky!uunet!gatech!usenet.ins.cwru.edu!agate!linus!linus.mitre.org!boole.mitre.org!crawford
From: [e-mail] (Randy Crawford)
Subject: Re: Programming by Description of Output...
Message-ID: <[e-mail]>
Sender: [e-mail] (NONUSER)
Nntp-Posting-Host: boole.mitre.org
Organization: The MITRE Corporation, McLean, VA
References: <[e-mail]>
Date: Mon, 4 Jan 1993 05:09:05 GMT
Lines: 98

In article <[e-mail]> [e-mail] (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        [e-mail]        The MITRE Corporation
|                                                 7525 Colshire Dr., MS Z421
| N=1 -> P=NP           703 883-7940              McLean, VA  22102