On 12/9/2012 10:57 AM, Obrst, Leo J. wrote:
> My point, John, is that most of these approaches require translation to a
>functional or declarative language, i.e., your "depends on a special language
>for writing the procedures". I am familiar with the literature, and largely
>agree with Hassan: however, I was not aware of his reference:
>
> Denotational semantics of ANSI C:
> - C (a sketch, but apparently the author has worked out full ANSI C):
> http://www.softlab.ntua.gr/~nickie/Papers/papaspyrou-2001-dsac.pdf.
>
> Thanks,
> Leo (01)
Incidentally Leo (and all others interested in this thread), Hoare Logic
interpreted as constraint logic can be made to work for effective
stateful rule-based programming (i.e, Production Rules à la Forgy's). (02)
To wit, the superb PhD thesis and related papers recently done by Bruno
Berstel (http://swt.informatik.uni-freiburg.de/staff/berstel) and
available there: http://www.freidok.uni-freiburg.de/volltexte/8799/. (03)
Referring to John Sowa's (perfectly valid) point that "academics should
address problems faced in industry", Bruno does precisely that with more
than 15 years of experience as one of the main developers of ILOG's (now
IBM's) BRMS (Business Rule Management System) product. Bruno is still
active in the core development staff of this product. (04)
Thought you might enjoy this contribution as it is based on Hoare Logic
for a "real-life" industrial product and also since, IMHO, it is
excellent work both in form and contents. (05)
Cheers, (06)
=hak (07)
>> -----Original Message-----
>> From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum-
>> bounces@xxxxxxxxxxxxxxxx] On Behalf Of John F Sowa
>> Sent: Sunday, December 09, 2012 1:02 PM
>> To: ontolog-forum@xxxxxxxxxxxxxxxx
>> Subject: Re: [ontolog-forum] Hybrid Reasoning Literature / Systems / Model
>> Theory
>>
>> On 12/8/2012 7:03 PM, Obrst, Leo J. wrote:
>>> There is limited research in general for denotational
>>> semantics of procedural programming.
>>
>> There has been an enormous amount of research in that area, but
>> it usually depends on a special language for writing the procedures:
>>
>> 1. Formal specifications: The Vienna Definition Language (VDL) was
>> a logic-based language and methodology (VDM) that was started by
>> Heinz Zemanek in the 1960s. Their most notable achievement was
>> the formal definition of PL/I, which led to important changes in
>> the language. They used an axiomatic method for specifying an
>> abstract machine that executed the language. This method is
>> logic-based, but it's not really denotational semantics.
>>
>> 2. Scott-Strachey denotational semantics: In the early 1970s,
>> Dana Scott worked at Oxford U. with Christopher Strachey
>> on denotational semantics. Scott earned his PhD at Princeton
>> with Alonzo Church as his thesis adviser. It's no coincidence
>> that he based the semantics on lambda calculus. Joseph Stoy
>> wrote a book on that semantics (1977).
>>
>> 3. Hoare Logic: Tony Hoare developed a system for representing,
>> analyzing, and reasoning about programs. It's based on
>> "Hoare Triples":
>>
>> {Preconditions} Command {Postconditions}
>>
>> Then he developed methods for relating the preconditions and
>> postconditions of any procedure to those of each command or
>> subprocedure in it. When such procedures are combined with logic,
>> the preconditions and postconditions can be added to the axioms
>> of the ontology. For example, Peano's axioms could specify the
>> arithmetic operators that are implemented procedurally.
>>
>> 4. Functional programming: A function is a formal object in logic,
>> and it can also be implemented efficiently on a digital computer.
>> Functional programming is a method of creating programs as pure
>> functions defined as the composition of more primitive functions.
>> The resulting program *is* a logical expression that has a well-
>> defined denotation. McCarthy designed LISP as a functional
>> language, but the "scruffies" added a lot of procedural stuff.
>>
>> 5. Logic programming: This is a relation-based alternative to
>> functional programming. Cordell Green proposed it in 1969.
>> Prolog is the most widely known version, but it has a lot
>> of procedural features. But there are more pure versions.
>>
>> 6. Pi calculus. This is Robin Milner's method for specifying
>> concurrent systems that pass messages among themselves.
>> Milner describes it as the concurrent extension to lambda
>> calculus: any function can be implemented by message passing,
>> but pi calculus is much more flexible and extensible.
>>
>> At VivoMind, we use a method of message passing that implements
>> a version of pi calculus for message passing among independent
>> modules or agents. For a purely formal system, the agents would
>> have to be specified by some pure version of functional or
>> logic programming.
>>
>> In practice, it's necessary to accommodate legacy systems and
>> anything anyone might invent in the future. That would limit
>> the ability to prove everything formally. But it's still possible
>> to do some useful reasoning:
>>
>> 1. Every module would have some specified constraints (preconditions
>> and postconditions) on what it does with messages.
>>
>> 2. But these constraints would be *underspecified*. Any module
>> might have side effects that other modules might not know.
>>
>> 3. This is a realistic approach that is better than what we have
>> today, but requiring total specifications of what each module
>> does is impossible to achieve.
>>
>> 4. Furthermore, privacy and security reasons would make total
>> knowledge undesirable or even dangerous.
>>
>> John
>>
>> ___________________________________________________________
>> ______
>> 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
>>
>
> _________________________________________________________________
> 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
>
>
> (08)
--
http://www.hassan-ait-kaci.net/contactme.html (09)
hak.vcf
Description: Vcard
_________________________________________________________________
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 (01)
|