ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] Hybrid Reasoning Literature / Systems / Model Theory

To: "[ontolog-forum] " <ontolog-forum@xxxxxxxxxxxxxxxx>
From: "Obrst, Leo J." <lobrst@xxxxxxxxx>
Date: Sun, 9 Dec 2012 18:57:09 +0000
Message-id: <FDFBC56B2482EE48850DB651ADF7FEB01E86ADCB@xxxxxxxxxxxxxxxxxx>
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:    (01)

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.     (02)

Thanks,
Leo    (03)

>-----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
>    (04)

_________________________________________________________________
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    (05)

<Prev in Thread] Current Thread [Next in Thread>