Re: Review of FLD

Michael Kifer wrote:
> 
> On Tue, 19 May 2009 09:11:24 -0400
> Chris Welty <cawelty@gmail.com> wrote:
> 
>>> Is ?X("abc"^^xs:string ?W)(?Y ?Z(?V "33"^^xs:integer)) an instance of Henkin's
>>> or CL syntax? Hint: check what plays the role of a function here.  
>> Ah, I see.  Henkin did not have functions.  Yes, this is valid CL syntax, and is 
>> still compact so still first order.  My understanding of compactness is that 
>> functions and constants are interchangeable in terms of their impact on it.
> 
> Are you saying that CL allows f(a)(b)(?X, foo) and things like that?
> I remember SKIF didn't have it and when I pointed this out to Pat he vigorously
> objected to this kind of terms.
> 
> As far as I am aware, these terms were first introduced in HiLog - more than 10
> years before CL.

Yes CL allows that, and references HiLog appropriately.  Chris Menzel even 
pointed at you while acknowledging that fact at the opening RIF meeting 
presentation on CL (you must have been reading your email).

CL is *not* KIF.  KIF and HiLog are ancestors of CL in a lot of ways, but CL is 
neither HiLog nor KIF.  It definitely is a far cry from SKIF.  SKIF was invented 
by Adam Pease and was thrown out, along with Adam, of the CL effort on day 1. 
CL allows everything that, as of 2005, was provably first-order, plus it adds 
sequences (which are not).

Anyway, my point is that saying the FLD syntax "generalizes first order syntax" 
is not accurate, in my understanding.  It *is* first order syntax.

-Chris

-- 
Dr. Christopher A. Welty                    IBM Watson Research Center
+1.914.784.7055                             19 Skyline Dr.
cawelty@gmail.com                           Hawthorne, NY 10532
http://www.research.ibm.com/people/w/welty

Received on Tuesday, 26 May 2009 14:02:44 UTC