On Mon, November 19, 2012 20:43, Rich Cooper wrote:
> Dear John, Doug, Ed, Pat, Ian, (01)
Rich, (02)
I think we all agree with you. The fact that programming languages have
the power (and undecidability) of higher order logic does not mean that
they should be executed through a general logical engine, nor that their
operations should be validated through theorem provers. The mentions
that programming languages are not decidable, yet are well accepted by
industry, was a counter to claims that industry requires that SW languages
be decidable. (03)
-- doug (04)
> Every time a programmer writes a function that she
> will use one or more times in a large program, she
> has sought expressiveness that was not provided in
> the language proper. That modularization choice
> is usually required because writing monolithic
> telephone books of code provides no insight into
> the workings of the program at levels appropriate
> to large applications. Organizing regions of code
> into objects with associated functions is
> essential for constructing and maintaining sizable
> programs, i.e., above 1,000 lines or so.
>
> Programmers think in chunks, as is well known from
> an article in the CACM decades ago when software
> engineering was first being developed for large
> system applications. They also design in chunks,
> and relate some chunks to others in higher
> conceptual levels. That is not doable using FOL
> Before and After assertions.
>
> Constraint propagation is another example of
> something you can't usually do in a program with a
> tree structured design; it requires that the
> program investigate constraint sets that are cross
> coupled. Constraints that are not cross coupled
> are not very useful.
>
> The idea of asserting the Before and After logic
> statements and then expecting automatic generation
> of a sizable program is simply impractical. The
> complexity of the assertions is every bit as great
> as the complexity of the programs that might be
> generated by an automatic programmer. Theorem
> proving as a means to generate said programs is
> only good for very, very small programs - less
> than 1,000 lines. This has been a long and tiring
> holy grail for people who are tightly focused on
> the FOL inclined, but it just doesn't work for
> people who work with large applications. The
> complexity is simply too great to make that
> approach work in large applications.
>
> But if enough people insist on trying it, someday
> maybe a breakthrough will happen. It just won't
> be in my lifetime. If modularization of programs
> could be organized with insight to automatically
> generate numerous small programs that work
> together properly, that could make a change. That
> hasn't happened yet.
>
> -Rich
>
> Sincerely,
> Rich Cooper
> EnglishLogicKernel.com
> Rich AT EnglishLogicKernel DOT com
> 9 4 9 \ 5 2 5 - 5 7 1 2
> -----Original Message-----
> From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx
> [mailto:ontolog-forum-bounces@xxxxxxxxxxxxxxxx] On
> Behalf Of doug foxvog
> Sent: Monday, November 19, 2012 2:58 PM
> To: [ontolog-forum]
> Subject: Re: [ontolog-forum] Webby objects
>
> On Mon, November 19, 2012 16:44, Edward Barkmeyer
> wrote:
>> I think Amanda is right about getting lost in
> the academic descriptions
>> of the properties of reasoners and languages. I
> phrased my concerns
>> inappropriately, it seems.
>>
>> John Sowa originally wrote that no user asks for
> decidability, users
>> always ask for more expressiveness. I have yet
> to hear a user ask for
>> either. Industry users are interested in
> capability and performance.
>> They ask for more capability, but they want a
> guarantee of performance.
>> "Capability" is the combination of an expressive
> language for axioms and
>> questions and the availability of a reasoning
> tool that uses them to
>> return answers.
>
> By asking for more capability, the industry uses
> are -- without knowing it --
> asking for more expressiveness.
>
>> Performance is the returning of answers in a
> reasonable length of time.
>
> I note that performance is a scale, not a binary
> relation. It revolves
> around the quality of the answer as well as the
> amount of time it
> takes to provide it. Within reason, a user
> (industry or other) would
> be willing to trade off some time for a higher
> quality answer.
>
>> Amanda Vizedom wrote:
>> ...
>>> There are lots of ways to design systems to
> either disallow certain
>>> statements (IMHO, better done semantically than
>>> via unusably counter-intuitive or restricted
> syntax), or decline to
>>> process certain reasoning patters that have a
> high rabbit-hole risk,
>>> or cut out after a certain time, or use other
> techniques to tune
>>> performance. The line between decidable and
> undecidable systems
>>> is not a sweet spot for this.
>
>> Of course. But the line between DLs and FOLs
> *is* a sweet spot for
>> this.
>
> Ed, i almost always agree with you 95+% of the
> time, but i beg to
> differ here. No business programmer programs in a
> DL language,
> from COBOL onward.
>
>> There are many industry applications that can be
> met by DLs with
>> their measurable performance, in spite of the
> fact that their
>> expressiveness is limited and some of the axiom
> formulations are hard
>> for human experts to read. The land of FOLs is
> significantly more
>> expressive, but it has many more cliffs and
> sinkholes that make it much
>> more difficult to predict performance.
>
> I note that a FOL can compute whatever a DL can
> compute in the same
> amount of time. So, how could a FOL be worse?
>
> If programmed well, an FOL can compute far more
> calculations efficiently
> than a DL can compute at all. Note that the
> limitations on FOL are for
> the most extreme situations. It does not mean
> that any reasoning in
> the FOL will be undecidable.
>
> I remember a case in an algorithm's class where an
> inefficient order N
> algorithm was deemed "better" than an efficient NP
> algorithm. However,
> the complexity of the input necessary before the
> number of calculations
> curves crossed made this crossing point at over
> 10^105 calculations.
> I argued that the higher-order algorithm was
> "better" as no inputs
> given to both algorithms would come out with an
> answer first from
> the polynomial algorithm within the lifetime of
> the poser (or the poser's
> machine, or the poser's nation).
>
> -- doug f
>
>>> For all of these reasons, IMHO, decidability is
> a red herring. Worse,
>>> and to mix my metaphors, it is a red herring
> that has led far too many
>>> talented people on a wild goose chase when they
> could be doing much
>>> more useful work to advance the state of the
> science and technology in
>>> really valuable ways.
>
>> I'm not so sure that academic pursuits like
> decidability actually lead
>> talented people away from useful work. We have
> a rule that a Ph.D. has
>> to advance the state of the art. It means that
> to get a Ph.D from a
>> prestigious institution will require you to do a
> few years work in some
>> esoteric field like decidability. In the course
> of that work, you will
>> learn what all the academic terminology means,
> how the concept space is
>> related, and what the state of the art actually
> is. When you have the
>> degree, you can start doing "useful" things,
> that use some parts of the
>> knowledge you gained, and the skills you gained
> in comprehending
>> ill-written technical literature. It is
> unlikely that you will have a
>> direct application for what you know about
> decidability, but it is
>> equally unlikely that a talented mathematician
> will find an industry
>> application for counting graphs or proving the
> convergence of Sobolev
>> methods, or that a botanist will find industry
> application for isolating
>> cabbage genomes. The loss only occurs when the
> talented student isn't
>> prepared for the fact that industry is more
> interested in what else s/he
>> knows, and continues looking for interest in
> his/her academic
>> specialty. The purely academic pursuit is part
> of the rite of passage,
>> and the maintenance of expertise in it may later
> be important in guiding
>> others. The truly talented people will find
> useful things to do; the
>> others are just intellectually gifted. It takes
> most of us a long time
>> to understand what knowledge we really have and
> what its value is. Some
>> of the gifted never do.
>>
>> -Ed
>>
>>>
>>> Best,
>>>
>>> Amanda
>>>
>>> On Mon, Nov 19, 2012 at 1:52 PM, Ed Barkmeyer
> <edbark@xxxxxxxx
>>> <mailto:edbark@xxxxxxxx>> wrote:
>>>
>>>
>>> [snip]
>>> Everyone agrees that FOL is more expressive
> and potentially more
>>> useful,
>>> but all of the reasoning procedures that
> are widely used in academia
>>> either restrict the allowable FOL inputs in
> some way that greatly
>>> reduces its expressiveness or are
> programmed to throw up their
>>> hands at
>>> some point -- they "halt" by saying "not
> determinable" (in some
>>> language). The problem of not knowing the
> relationship between
>>> input
>>> data -- the sets of valid sentences -- and
> the "not determinable"
>>> result
>>> is what causes industry to shy away from
> FOL reasoners.
>>> [sniip]
>>>
>>
>>
>> --
>> Edward J. Barkmeyer
> Email: edbark@xxxxxxxx
>> National Institute of Standards & Technology
>> Systems Integration Division, Engineering
> Laboratory
>> 100 Bureau Drive, Stop 8263 Tel:
> +1 301-975-3528
>> Gaithersburg, MD 20899-8263 Cel:
> +1 240-672-5800
>>
>> "The opinions expressed above do not reflect
> consensus of NIST,
>> and have not been reviewed by any Government
> authority."
>>
>>
>>
>>
> __________________________________________________
> _______________
>> Message Archives:
> http://ontolog.cim3.net/forum/ontolog-forum/
>> Config Subscr:
> http://ontolog.cim3.net/mailman/listinfo/ontolog-f
> orum/
>> Unsubscribe:
> mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
>> Shared Files: http://ontolog.cim3.net/file/
>> Community Wiki: http://ontolog.cim3.net/wiki/
>> To join:
> http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePa
> ge#nid1J
>>
>>
>
>
>
> __________________________________________________
> _______________
> Message Archives:
> http://ontolog.cim3.net/forum/ontolog-forum/
> Config Subscr:
> http://ontolog.cim3.net/mailman/listinfo/ontolog-f
> orum/
> Unsubscribe:
> mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
> Shared Files: http://ontolog.cim3.net/file/
> Community Wiki: http://ontolog.cim3.net/wiki/
> To join:
> http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePa
> ge#nid1J
>
>
> (05)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (06)
|