Pat Hayes wrote:
>> Pat Hayes wrote:
>>>> PH:
>>>>
>>>>> Our IKRIS project made a small start on this. In
>>>>> IKL, all character strings are in the domain and
>>>>> they are all 'potential' names. A string gets to
>>>>> be a name when it is used as one in the language,
>>>>> ie when it is used in a formula. For those, we
>>>>> have a special rule that relates the name's
>>>>> meaning to the name OF the name. Its very simple:
>>>>> if you give a character sting as an argument to
>>>>> the special function tnb (thing named by), its
>>>>> value is required to be whatever that character
>>>>> string would denote if you were to use it as a
>>>>> name. Formally,
>>>>>
>>>>> (= (tnb 'name') name)
>>>>
>>>> Clearly, but you either have to assume a single global context (for
>>>> 'name' to always denote the same entity),
>>>
>>> I do assume a global context, yes. In fact, in IKL we assume no
>>> context at all. The logic simply isn't contextual, which IMO is the
>>> way the base logic should be for information interchange. So names
>>> are global, just as URIs are.
>>>
>>>> or, having admitted local
>>>> contexts -- some sort of lexical or other scoping -- you leave way
>>>> for a
>>>> name to denote different entities.
>>>
>>> If one wants to admit local name scoping - and we did need to do this
>>> for IKL - then the appropriate way to do it is to combine the context
>>> with the *quoted* name (not the name itself), and in IKL this is done
>>> by simply adding a context argument:
>>> (tnb 'name' context1)
>>> denotes the thing that 'name' denotes in context1. This handles
>>> referential opacity and so on very neatly.
>>>
>>>> For example, you may have two contexts c1 and c2 such that (= (tnb
>>>> 'name') name) evaluates to true in both of them
>>>
>>> That is meaningless in IKL. Contexts are objects in the domain, not
>>> entities in which sentences are evaluated. You are talking 'context
>>> logic' style. IMO context logic is a dead end. One of John McCarthy's
>>> rare blunders.
>>
>> I was thinking about syntactic contexts, syntactic closures, as
>> first-class objects.
>
> Well, Im not sure what you mean by this terminology. The word "context"
> is, unfortunately, very dependent on the context for its meaning. It
> sounds as though you mean the scope of a syntactic binder such as a
> quantifier, is that correct? (01)
Not necessarily a quantifier. Perhaps mislead by the syntactic
similarity of IKL (and KIF, for that matter), I was thinking in terms of
LISP (Scheme, for that matter). Then, a syntactic binder is not
necessarily a quantifier, as in a do-loop, it can be a lambda
expression, or the syntactic sugar let: (02)
(let ((x 1))
(= (tnb 'x') x))
(let ((x 2))
(= (tnb 'x') x)) (03)
=> true
=> true (04)
though 'x' does not denote the same object in the whole scope. (05)
I am not quite familiar with IKL, and it seems that you do not have such
syntactic scoping there. (06)
>> Within each closure, clearly, 'x' (a name) means x (the denotation of
>> 'x' in that context).
>
> In IKL, every *use* of a name, anywhere in the language, means the same
> thing. There is no idea of a use of a name 'within' anything. Hence the
> entire language is referentially transparent. (07)
You can have referential transparence with lexical scoping. The point
is not to have dynamic scoping. A purely functional language is
referentially transparent, though names have meanings dependent on the
context (the environment). (08)
'Referential transparence' may be an ambiguous term. (09)
>
>> Across closures, though, the meaning of 'x' may be different.
>>
>> In this sense, your (tnb name context) is equivalent to looking up the
>> specified closure for the name's entry, and (tnb name) is implicitly
>> using the closest closure
>
> Hmm, I have no idea what 'closest' could mean. (010)
Another import from lisp. Inessential here. (011)
>
>> (do you allow hierarchically nested contexts?)
>
> Contexts have whatever structure ones axioms describe them to have. They
> are simply entities in the domain of discourse, and have no particular
> logical role. (012)
Since we were talking about an artificial language which has to have
some means for binding identifiers with semantic objects, I was thinking
of a context as of an environment, which provides bindings for
identifiers. In lisp (scheme, at least), environments are hierarchical,
and the referent of an identifier is looked up in the current
environment of the computation, if not found there, there in the next
enclosing environment, and so on, until the global one, if needed. (013)
Apparently in IKL contexts are whatever one wishes them to be. I guess
my dog might be a context in IKL, it seems. Do you have any definition
of context there? (014)
>
>>
>> Whatever the relation to McCarthy's dead idea, let it be.
>
> McCarthy is widely credited with the idea of introducing contexts to logic.
>
>>
>>>
>>>> , 'name' as in c1 =
>>>> 'name' as in c2 (trivially), yet name as in c1 != name as in c2.
>>>
>>> In IKL:
>>> (not (= (tnb s context1) (tnb s context2)))
>>>
>>> where s is 'name'. Indeed, this situation can arise. But there are
>>> types of 'context', such as times and locations - parts of the 'real
>>> world' - which do not affect the meanings of names. In IKL these can
>>> be defined axiomatically:
>>>
>>> (forall (x) (iff (transparentContext x)
>>> (forall ((s charseq))(= (tnb s)(tnb s x)))
>>> ))
>>
>> Yes, if (tnb s) is equivalent to (tnb s the-global-context), with
>> the-global-context being the global context
>
> Well, there is no global context as such in IKL, any more than there is
> in, say, first-order logic. (015)
OK. Then what does (tnb s) actually mean? And what does (tnb s x)
actually mean? (I guess I'd better consult the documentation.) (016)
>
>> , rather than (tnb s) being eqivalent to (tnb s
>> (the-current-context)), with the-current-context a function returning
>> the current context.
>
> I really have no idea what you mean by global/current/etc. contexts. It
> sounds as though you have a complete framework or theory of contexts in
> mind. Can you briefly explicate it? (017)
I have no particular theory, as explained above, it was an (possibly
unfortunate) import from lisp. I just thought a context in the context
of IKL is more or less the same as an environment in the environment of
lisp. Sorry about the hassle. (018)
vQ (019)
>
>> (The latter case qould still be ok if the statement above is made
>> within the global context.)
>>
>> vQ
>>
>>>
>>> Pat
>>>
>>>>
>>>> Simply put: the rule that 'e' should always mean e may be satisfied
>>>> even if 'e' denotes different entities (on different occasions of use).
>>>>
>>>> vQ
>>>>
>>>> _________________________________________________________________
>>>> Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
>>>> Subscribe/Config:
>>>> 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 Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx
>>>>
>>>
>>>
>>
>> --
>> Wacek Kusnierczyk
>>
>> ------------------------------------------------------
>> Department of Information and Computer Science (IDI)
>> Norwegian University of Science and Technology (NTNU)
>> Sem Saelandsv. 7-9
>> 7027 Trondheim
>> Norway
>>
>> tel. 0047 73591875
>> fax 0047 73594466
>> ------------------------------------------------------
>
> (020)
--
Wacek Kusnierczyk (021)
------------------------------------------------------
Department of Information and Computer Science (IDI)
Norwegian University of Science and Technology (NTNU)
Sem Saelandsv. 7-9
7027 Trondheim
Norway (022)
tel. 0047 73591875
fax 0047 73594466
------------------------------------------------------ (023)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Subscribe/Config: 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 Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (024)
|