[Top] [All Lists]

Re: [ontolog-forum] HOL decidability [Was: using SKOS for controlled val

To: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Tue, 12 Oct 2010 11:42:48 -0500
Message-id: <21CB16F0-274D-4DFE-9C25-8EC2CB6D5A35@xxxxxxxx>
On Oct 11, 2010, at 10:21 PM, doug foxvog wrote:
> On Mon, October 11, 2010 23:04, Christopher Menzel said:
>> On Mon, 2010-10-11 at 12:41 -0700, Rich Cooper wrote:
>> ...
>> Higher-order languages are indeed more expressive [than FOL].  As a
>> consequence, they are not even partially decidable.
> Maybe Higher-order languages as a whole are not even partially decidable,
> but large numbers of statements in them are.      (01)

Sure, but I'm not sure I see the point.  We're talking about the logics 
themselves.    (02)

> It was noted that normal computer languages embodied HOL.    (03)

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

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 higher-order is because it quantifies over 
functions.  It is true that higher-order logics can quantify over functions 
(and properties and relations) and, for this reason, 
functions/properties/relations  are often referred to as "higher-order 
objects".  But simply quantifying over such objects is not in itself what makes 
a logic higher-order; rather, the function/property/relation space must consist 
of all possible functions/properties/relations over (in the second-order case) 
the domain of individuals.  Absent that requirement, in the context of basic 
classical logic, one's logic is still first-order.  (I'd recommend Herbert 
Enderton's article "Second-order and Higher-order Logic" in the Stanford 
Encyclopedia of Philosophy for more on this -- http://goo.gl/Ubko.)    (05)

Now, with its ability to represent recursion as well as basic arithmetic, the 
lambda calculus certain far exceeds first-order logic in expressive power.  But 
it is not straightforwardly classified as a species of classical higher-order 
logic either, as standard higher-order 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 
higher-order logic; nor does the semantics allow for such constructs as 
functional self-application, which is possible in the untyped lambda calculus.  
Because of these features, the untyped lambda calculus does not have a 
classical higher-order 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 higher-order logic.    (06)

Bottom line: The sense in which normal computer languages "embody" higher-order 
logic is not a simple and straightforward matter.    (07)

-chris    (08)

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
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (09)

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