[CL] inconsistency in Annex B? (actually types in general)
phayes at ihmc.us
Wed Nov 14 10:33:49 CST 2007
>> The whole point of creating an interoperability standard is
>> to avoid the need for people to have to negotiate and come
>> to an agreement to use the same conventions.
>But every standard is *preceded* by a period of negotiation.
The CL standard was already preceded by over a decade of such
negotiation. Its time we stopped being an endless committee and
actually wrote a standard. In fact, I thought this was what we had
>What I was proposing is a report (which would be expected to
>grow and evolve over a period of several years) that would
>document the negotiations and suggested conventions that
>might eventually become part of a future standard.
Sounds like deja vu all over again to me.
>> there should be ONE way to translate or embed a dialect into CL.
>I agree, but different dialects may have incompatible conventions
>for representing features that are outside the core. That is a
>natural and appropriate development, not one to be deplored.
If those features are intended to be meaningful and also
interoperable, then it is to be deplored. In fact, I would go so far
as to say that it should be made explicitly non-conformant.
>> First, CL core does not include restricted quantifiers (they
>> are syntactic sugar in CLIF).
>I originally wanted them in the core, but I have now come to
>the conclusion that they don't belong in the core. Since they
>don't affect the truth value, they have no affect on the model
>theory. They might affect the way people *use* the core, but
>if we place restrictions on that, we'll block other legitimate
>> But even if they were, they can be used with any predicate, not
>> just type predicates: so the 'convention' of using them to encode
>> that meaning is inappropriate, since it is guaranteed to be
>> violated by some legitimate uses of CL.
>As I replied to your previous copy of that statement, that is
>irrelevant. If language A uses that feature to mark types and
>language B uses it for some other purpose, users of the two
>languages could happily interchange statements through CL core,
>and neither group would be aware that the other had some
>intended "meaning" that is inexpressible in the CL core.
Well, this gets to the heart of the matter. Are those quotes round
"meaning" real or not? If being or not being a 'type' is considered
to be a meaningful distinction, then presumably the users of language
A will require that content in A will retain this structure if
translated into CL and then translated back. Since CL allows for
interoperability between many dialects, this can result in some
content which does not imply A-typehood being mistranslated into A is
a type. This IS a problem, and one that we should make efforts to
overcome. The idea of marking XCL content by the form of its origin
was a small tentative step in this direction, but we need to be able
to do better.
I don't accept that this is irrelevant or a non-problem. It is right
at the heart of the idea of a common logic for interoperability.
>> There is too much foundational work [for IKL] yet to be done.
>> We still do not have a completely guaranteed sound basic semantics,
>> and nothing lie a proof theory.
>There is a very fine subset of IKL that has had a sound semantics
>and a sound proof theory for over 70 years:
Rubbish. The IKL syntax and model theory was only invented two years
ago. Maybe one can define an IKL-1.1 which has the Tarski hierarchy
as its model theory, but I havn't seen it done, and I personally
don't feel competent to actually do it. And it wouldn't be IKL
itself, any way, since IKL as presently defined has Taski's
T-condition as a valid inference rule.
> Tarski's hierarchy
>of metalanguages. The IKL syntactic extensions to CL that are
>necessary to support that subset do not exclude many other models,
>some of which, I admit, may be weird.
>That state of affairs is not unlike Peano's axioms for arithmetic
>and many other widely used axiomatizations. You only need one
>model to show that the framework is sound.
Quite, but we havn't even managed to that for IKL yet.
>> IKL is way beyond FOL. I would be very unhappy putting IKL forward
>> as a candidate for standardization at any predictable date at this
>It took over half a century to untangle the issues involved with
>Peano's axioms. I wouldn't be surprised if people are still
>arguing about nonstandard models of IKL for another century.
>Another example is every major programming language in existence
>today: they all permit programs that cannot be proved to terminate,
>but people have been using them successfully for over 70 years.
>But the point is that there is at least one very good and usable
>model (Tarski's hierarchy). Trying to exclude other models would
>require more complex syntactic machinery, and nobody knows what
>uses, if any, those many other models might have. Various groups
>in the IKRIS workshop have found IKL-like features very useful,
>and they've been using them for years.
I agree: but before attempting to write a standard we need some
foundational work done, or at the least a good story to tell about
why it isn't needed. I don't feel I have either of them. If you have,
please supply more details.
>If anybody wants to play around with other models, we can warn
>them that they're treading on unexplored territory, but there
>is no reason why we should try to stop them.
>JFS>> Following are some possibilities:
>>> 1. Many people use IKL and get good results.
>PH> What does that mean?
>The obvious. IKL attracts users who are happy with the results
My point was, what counts as a "result" here?
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
More information about the CL