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