Chris, (01)
Denotational semantics (DS) has had a very poor effect on anything related
to program correctness or even optimization in computer science, and only a
minor effect on even FOL expressions of programs. It's a dead end that is
based on the assumption that translating meaningful expressions to
simplistic FOL doesn't require an interpreter who understands the notation.
I know that mathematical logicians love it, but it hasn't yielded results
worth the costs that have been spent on it. (02)
DS is useless for practical sized problems because it ignores scope; it will
be an academic curiosity for a long, long time. Fun and games for
logicians, but not useful. (03)
Rich (04)
Sincerely,
Rich Cooper
EnglishLogicKernel.com
Rich AT EnglishLogicKernel DOT com
9 4 9 \ 5 2 5  5 7 1 2 (05)
Original Message
From: ontologforumbounces@xxxxxxxxxxxxxxxx
[mailto:ontologforumbounces@xxxxxxxxxxxxxxxx] On Behalf Of Christopher
Menzel
Sent: Tuesday, October 12, 2010 9:43 AM
To: [ontologforum]
Subject: Re: [ontologforum] HOL decidability [Was: using SKOS forcontrolled
values for controlledvocabulary] (06)
On Oct 11, 2010, at 10:21 PM, doug foxvog wrote:
> On Mon, October 11, 2010 23:04, Christopher Menzel said:
>> On Mon, 20101011 at 12:41 0700, Rich Cooper wrote:
>> ...
>> Higherorder languages are indeed more expressive [than FOL]. As a
>> consequence, they are not even partially decidable.
>
> Maybe Higherorder languages as a whole are not even partially decidable,
> but large numbers of statements in them are. (07)
Sure, but I'm not sure I see the point. We're talking about the logics
themselves. (08)
> It was noted that normal computer languages embodied HOL. (09)
That's a statement that needs a great deal of qualification. I am far from
an expert on these matters, so someone with a more authoritative grasp of
the subjects might well usefully correct/qualify some of my remarks. But I
believe the gist of the following is correct. (010)
The logic that corresponds to most programming languages is the untyped
lambda calculus, which is designed to represent recursion. The reason the
lambda calculus is often referred to as higherorder is because it
quantifies over functions. It is true that higherorder logics can quantify
over functions (and properties and relations) and, for this reason,
functions/properties/relations are often referred to as "higherorder
objects". But simply quantifying over such objects is not in itself what
makes a logic higherorder; rather, the function/property/relation space
must consist of all possible functions/properties/relations over (in the
secondorder case) the domain of individuals. Absent that requirement, in
the context of basic classical logic, one's logic is still firstorder.
(I'd recommend Herbert Enderton's article "Secondorder and Higherorder
Logic" in the Stanford Encyclopedia of Philosophy for more on this 
http://goo.gl/Ubko.) (011)
Now, with its ability to represent recursion as well as basic arithmetic,
the lambda calculus certain far exceeds firstorder logic in expressive
power. But it is not straightforwardly classified as a species of classical
higherorder logic either, as standard higherorder logic does not of itself
support recursion, in the sense that mechanisms for defining recursive
functions and a proof of their existence do not simply fall out of the
semantics of higherorder logic; nor does the semantics allow for such
constructs as functional selfapplication, which is possible in the untyped
lambda calculus. Because of these features, the untyped lambda calculus
does not have a classical higherorder semantics and, indeed, finding a
semantics for it proved to be a very difficult problem that was not solved
until Scott's discovery of domain theory in the 1960s. Together with
Strachey, Scott applied domain theory to the development of denotational
semantics for programming languages.
Theoretically, this is a very beautiful semantics, but it is much more
complex than the simple and straightforward semantics of ordinary
higherorder logic. (012)
Bottom line: The sense in which normal computer languages "embody"
higherorder logic is not a simple and straightforward matter. (013)
chris (014)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontologforum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontologforum/
Unsubscribe: mailto:ontologforumleave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgibin/wiki.pl?WikiHomePage#nid1J
To Post: mailto:ontologforum@xxxxxxxxxxxxxxxx (015)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontologforum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontologforum/
Unsubscribe: mailto:ontologforumleave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgibin/wiki.pl?WikiHomePage#nid1J
To Post: mailto:ontologforum@xxxxxxxxxxxxxxxx (016)
