[KIF] Fwd: CL & Types

[Francis McCabe]

>
>
> On Sunday, May 12, 2002, at 11:17 PM, Bill Andersen wrote:
>
>> On 5/13/02 0:44, "Francis McCabe" <francis.mccabe at sbcglobal.net> wrote:
>>
>>> Well some are going to schemas, but that isnt the point. (BTW A 
>>> pointer
>>> to XML-S would be appreciated. Google doesnt know about it)
>>
>> http://www.w3.org/XML/Schema
>
> Oops, I thought XML-S was a new logic language!
>
>>
>>> My issue for CL is this: I know that there are corner cases in any 
>>> type
>>> scheme that must be addressed if you want a usable system. It may be
>>> that CL is not at the appropriate level of abstraction; however I
>>> believe it is. For example, a model of types based on unary predicates
>>> would not work for me, unless predicate symbols themselves were
>>> manipulable constants -- in a different way than the automatic
>>> functionalization discussed in the document.
>>
>> Can you explain what you mean by "automatic functionalization"?  
>> Because of
>> CL's free syntax, any term (constant, function term, object variable, 
>> but
>> not row variables, for obvious reasons) may appear in predicate 
>> position.
>> Since you only mentioned constants, then what stops you from saying 
>> whatever
>> you want about those constants?
>
>
> To paraphrase: Toward that end for <e1,..,en> in D*, e0 in D st 
> <e0,e1,...,en> in D* then <f(e1,..,en),e1,..en) in ext(e)
> ....
> This mechanism enables one to use a term denoting a functional relation 
> as both a predicate and a function symbol.
>
> Or have I misunderstood?
>
>>
>> Could you give an example of some things you might want to say about 
>> them?
>> That would help.
>
> Me and my colleagues would argue that type inference is a form of 
> abstract interpretation; a program is type correct if the program's 
> denotation in the `type universe' is consistent. This is a much 
> stronger position than that implied by many-sorted logics, however it 
> fits quite well with most programmers' perspective. (To get an almost 
> equivalent position one would have to make a series of additional 
> assertions about sorts -- such as that the number and character unary 
> predicates etc. etc. are disjoint)
>
> So, one could certainly lay such a scheme over the CL; however my 
> assertion is that more is needed than is implied by the CL document.
>
> I guess this comes down to marketing: if it is desired to make CL 
> maximally relevant to the business community then the CL group must 
> take a stand on types; just as a stand on FOL is taken.
>
> Otherwise, consider my position for example, I need to develop a 
> logical content language. I could boil my own semantics or I could 
> attempt to use the CL semantics. To the extent that CL solves my 
> problems I would be willing to absorb some of the features I don't 
> specifically want (such as sequence variables).
>
> It may be in the form of a separate document, that isn't important for 
> me. What would be important would be a commitment to issue a 
> specification on types (I would be willing to participate in that).
>
> Frank McCabe
>