Hi Till, (01)
time really for your input on this issue: this is the typed/nontyped
question for CASL / Common Logic again. It would be good to have the
results of your considerations of the consequences / nonconsequences
of having strong typing in the language of choice wrt the
positions described below. (02)
Best,
John. (03)
-------- Original Message --------
Subject: Re: "Typed" CL
Date: Tue, 28 Feb 2006 17:22:52 -0600
From: Pat Hayes <phayes@xxxxxxx>
To: Bill Andersen <andersen@xxxxxxxxxxxxxxxxx>
CC: Chris Menzel <cmenzel@xxxxxxxx>, Gruninger Michael
<gruninger@xxxxxxxxxxxxxxx>, "John A.Bateman" <bateman@xxxxxxxxxxxxx>
References: <D2A59CA5-3780-494B-AB11-6D9EFD10A795@xxxxxxxxxxxxxxxxx>
<p06230900c02a70534e06@[10.100.0.25]>
<0E2651A5-25FB-471D-9060-DA63B27D40FE@xxxxxxxxxxxxxxxxx> (04)
>Hey Pat...
>
>You interpreted types semantically. This was my first inclination
>on hearing what John was after.
>
>We, at OW, have an axiom in our upper level (that includes types)
>something like:
>
> (forall (x) (exists (t) (and (Type t) (t x))))
>
>of course we interpret it specially in code and such but the idea is
>similar to what you have below.
>
>Chris interpreted what John was asking for syntactically - a typed
>non-logical lexicon (05)
Well, CL doesn't have syntactic lexical typing: it is almost
aggressively un-typed in this sense, and deliberately so. But perhaps
unlike Chris M., I do not regard this as a big issue. As far as I can
see, the only operational difference between syntactic and semantic
typing is whether you get a type error message from a parser or a
reasoner. If you are willing to use special-purpose reasoners to
check types, this hardly seems like an important operational
distinction, even though it looms large in traditional logical
discussions. So if John wants strong lexical typing, I'd like to ask
him: what for? If he wants it merely as a discipline for
axiom-writers, then he can have it for that in CL: its a set of
conventions for writing axioms in a certain style. If he wants it
also to be machine-checkable, then he can have that in CL if he
agrees on a style of encoding his typing into CL, e.g. along the
lines suggested, and is willing to write a John-type-legality-checker
as a special-purpose CL reasoner, perhaps one to be applied before
others are used. I am willing to bet an expensive dinner that the
work required to write such a special-purpose reasoner for the
CL-embedded type theories, and that required to write a type-checking
parser for the lexically typed language, will not differ by a
significant amount (since they will use the same algorithm). (06)
As a passing remark, on a slightly different topic, are Michael and
John aware that CL provides for naming and importing of ontologies,
with a fully defined semantics, and a way (using the module
construction) to specify a local universe of discourse and to relate
it to other ontologies' universes? This would allow content from one
source to be labelled with the name of the source, e.g. one could say
that a predicate was a type in the ontology JohnsOntology, but merely
a predicate in the ontology MichaelsOntology, or to have classes of
ontologies defined by the kind of typing conventions in use in them. (07)
BTW, is this part of some larger conversation? (08)
Pat (09)
>- also a reasonable interpretation. I guess John would have to tell
>us what he means by "typed".
>
> .bill
>
>On Feb 28, 2006, at 16:37 , Pat Hayes wrote:
>
>>>John,
>>>
>>>I took this from the UOS conveners group and am resending it to
>>>the CL principals. Chris & Pat... Do you have any comment on
>>>this?
>>>
>>>>I think we'd almost support Michael Gruninger's
>>>>proposal. Apart from a possible clarification wrt
>>>>1 and 2:
>>>>
>>>>>- A theory is a set of sentences in a language conformant with
>>>>>Common Logic.
>>>>>- An ontology is a set of theories.
>>>>>
>>>>
>>>>The language we use for ontologies is CASL (see
>>>>previous email), which is strongly typed. As long
>>>>as this is 'conformant' in the intended sense
>>>>fine. Or has CL moved on the typing issue?
>>
>>CL itself is not a typed logic. However, one can express typed
>>content in CL, most obviously by treating the types as predicates
>>(classes). Since everything is an individual, the types themselves
>>can be classified as being in a special category of 'type
>>predicates' by writing things like (isType Human) and treating type
>>predications in a special way by axioms like
>>
>>(forall ((type isType) y) (iff (type y)(IsOfType y type)) )
>>
>>This style of embedding would make type errors be CL unsatisfiable.
>>A more nuanced embedding would distinguish the simple predication
>>from the assignment of a type, and make type errors entail special
>>signalling propositions, eg
>>
>>(forall ((type isType) y) (if (and (IsOfType y type)(not (type y)))
>>(typeError) ))
>>
>>Hope this helps.
>>
>>BTW, this is how I will be recommending that typed languages be
>>treated in IKL, but there we will have the extra luxury of being
>>able to refer explicitly to the ill-typed sentence as an IKL
>>proposition, and predicate typeError of it directly as a property
>>of the proposition. This would be a CL extension, of course, but it
>>could be treated as CL conformant.
>>
>>Pat
>>
>>>Bill Andersen (andersen@xxxxxxxxxxxxxxxxx)
>>>Chief Scientist
>>>Ontology Works, Inc. (www.ontologyworks.com)
>>>3600 O'Donnell Street, Suite 600
>>>Baltimore, MD 21224
>>>Office: 410-675-1201
>>>Cell: 443-858-6444
>>
>>
>>--
>>---------------------------------------------------------------------
>>IHMC (850)434 8903 or (650)494 3973 home
>>40 South Alcaniz St. (850)202 4416 office
>>Pensacola (850)202 4440 fax
>>FL 32502 (850)291 0667 cell
>>phayesAT-SIGNihmc.us http://www.ihmc.us/users/phayes
>>
>
>Bill Andersen (andersen@xxxxxxxxxxxxxxxxx)
>Chief Scientist
>Ontology Works, Inc. (www.ontologyworks.com)
>3600 O'Donnell Street, Suite 600
>Baltimore, MD 21224
>Office: 410-675-1201
>Cell: 443-858-6444 (010)
--
---------------------------------------------------------------------
IHMC (850)434 8903 or (650)494 3973 home
40 South Alcaniz St. (850)202 4416 office
Pensacola (850)202 4440 fax
FL 32502 (850)291 0667 cell
phayesAT-SIGNihmc.us http://www.ihmc.us/users/phayes (011)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/uos-convene/
To Post: mailto:uos-convene@xxxxxxxxxxxxxxxx
Community Portal: http://ontolog.cim3.net/
Shared Files: http://ontolog.cim3.net/file/work/UpperOntologySummit/uos-convene/
Community Wiki: http://ontolog.cim3.net/cgi-bin/wiki.pl?UpperOntologySummit (012)
|