Re: [ontolog-forum] mKR proof of correctness

["Barkmeyer, Edward J" <edward.barkmeyer@xxxxxxxx>]

Dick,

 

Some topics from below.

 

Pragmatics:  If Mrs. X says “We are going to the store” to her child, the pragmatic interpretation might be “I have decided that we will go to the store, and you don’t get a choice.”  If Mrs. X says “we are going to the store” to Mrs. Y as she passes her on the walkway, it is probably just a statement of a situation in progress.  The words are the same.  The difference is all about the speech act:  the circumstance, the audience, the tone of voice, etc.  Pragmatics is about what the audience is expected to understand, as distinct from the nominal meaning (semantics) of the utterance.  People do try to codify some of those things in logic; or they may just replace what was said with what was meant.  When you try to codify the “illocutionary force” (a kind of pragmatics) of an utterance, you usually get “modes” or “modalities” --  Declarative, Interrogative, Imperative, Hortatory – which you somehow attach to the “locutionary” interpretation of the utterance – the interpretation of the construct and the words.  In formal languages, we usually only have declarative sentences, and they mean exactly what they say.  There is no tone, no subtlety, and the audience is machines or people that can read that language.

 

Meaning:  a very soft concept.  The function of the formal terminology is to sort out the possible intentions of the term.  Noun terms have two related kinds of meanings:  the denotation – the specific things it refers to (the extensional meaning); or the ‘connotation’ – the set of properties that would make a thing a member of the denotation (the intensional meaning).  Technically verb terms are similar, but in practice a verb term is associated with an intension that is a pattern for situations that are ‘instances’ of the verb.  The meaning of a sentence consisting of a subject noun a verb and a direct object noun is an instance of the verb pattern in which the subject noun and the object noun play roles.  The meaning of IF S1 THEN S2 is more complex, but it is still a grammatical construct in the language.  These layers of meaning – the meaning of a noun, the meaning of a qualified noun, the meaning of a simple sentence, the meaning of a complex grammatical structure are all “semantics”.  They can, however, be subdivided into the meaning of the terms and meaning of the constructs.  Even in “we are going to the store”, you have to connect the senses of “we”, “are going”, “to”, and “the store” to obtain the meaning of the construct.  How do you know which of ‘we’ and ‘the store’ are ‘going’?  It requires a grammatical (structural) interpretation, which itself is independent of whether the subject is ‘we’ or ‘the store’.  The grammar gives us the concept ‘subject’, and that is a particular kind of “meaning”.

 

Symbols:  in a formal language (and in analysis of natural language), the nature of the grammatical constructs is a set of fixed (terminal) symbols and a set of variable (non-terminal) symbols for which terms or expressions can be substituted in creating instances of the grammatical construct.  BNF is a way of writing down the possible constructs; there are many others.  For example:

  simple-sentence = subject, verb, object ;

says that a simple sentence has three components, and they are all non-terminal.  In creating an instance, you insert some noun or _expression_ in the subject slot, another in the object slot, and some verb in the middle.  That is the mechanical interpretation of the productions (grammar rules).  The meaning of the construct is that the referent(s) of the _expression_ in the subject slot is the acting agent of the verb, and the referent(s) of the object _expression_ is the passive agent/thing.  That may not sound like much, but it is not necessarily true in other languages, which may use word forms to distinguish roles, just as we use ‘we’ and ‘us’.  So, when we try to explain the semantics of a simple sentence structure, we talk about the symbols:  subject, verb, object.  In that explanation we also specifically talk about the referent(s) of terms and expressions that are substituted for the symbols, which is how we relate the grammatical utterance to the “world of interest”.

 

In the example:

  implication = “if”, antecedent, “then”,  consequent ;

  antecedent = sentence ;

  consequent = sentence ;

we use two terminal symbols – “if” and “then” -- to distinguish this kind of sentence from others, and we use the non-terminal symbols ‘antecedent’ and ‘consequent’ to refer to two different sentences (which can have pretty much any form, or we might constrain it to some kinds of ‘sentence’) that have different meanings with respect to the implication, regardless of what the sentences themselves mean.  We may define the meaning as:  If the set of states denoted by the antecedent has a member in the world of interest, then the set of state denoted by the consequent also has a member.  These latter circumlocutions are chosen for the specific notions you want to use to describe “meaning” of grammatical structures.

 

Primitive terms:  The ‘meaning’ of individual terms is “quite another thing entirely”.    You may be able to define a classifier term in terms of a set of properties that characterize it, or not.  The rule may be:  it is one if (and only if) I say it is one.  That is why we separate the meanings of words from the meanings of constructs.  You may be able to define “bird” in terms of other terms you have defined.  If you can’t, the term has no formal or axiomatic meaning.  You are depending on humans to know intuitively what you mean by “bird”.  When that doesn’t work, we resort to drawing pictures, or constructing elaborate circumlocutions in natural language.

 

Enumerating instances is not a ‘pragmatics’ concept, in the formal sense.  It may be a pragmatic solution to the problem of getting the audience to know what the term means.  A term always has a set of referents.  We can define a term “extensionally” by specifying the members of the set.

 

Yes, programming languages are formal languages, and the same division of ideas applies.  The Java language specifies the meaning of the grammatical constructs with respect to machine execution, but it has no idea what your variable-names mean.  They are just primitive terms whose computational representation is specified, which may have nothing whatever to do with what it means.  The planet Mars can be represented by the integer 4.

 

Jargon:  Yes.  Every other word you/I use in this business is jargon, because we are trying to make a lot of subtle distinctions that the average football fan is not going to understand or try to.  So, we create new terms (or reuse old ones) with very specific meanings, and we define them as formally as we can.  You talk about genus and species;  but your usage is only analogous to biological classification.  I use ‘semantics’ and ‘pragmatics’ with a very special meaning that is only somewhat analogous to the natural language usage (if any).

 

I did mark one section below in which I don’t understand what you are saying.

 

 

From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum-bounces@xxxxxxxxxxxxxxxx] On Behalf Of Richard H. McCullough
Sent: Thursday, April 03, 2014 3:29 PM
To: [ontolog-forum]; Richard S. Latimer
Subject: Re: [ontolog-forum] mKR proof of correctness

 

Ed
>> see below
 
Dick McCullough
Context Knowledge Systems
mKE and the mKR language
mKR/mKE tutorial

---

From: edward.barkmeyer@xxxxxxxx
To: rhm@xxxxxxxxxxxxx; ontolog-forum@xxxxxxxxxxxxxxxx
Date: Thu, 3 Apr 2014 16:49:39 +0000
Subject: Re: [ontolog-forum] mKR proof of correctness

Well, Dick, what can I say?  I’m probably older than you, and the term ‘pragmatics’ was around in the early 1960s.

 >>      I had already graduated from college then -- before transistors & computers & computer science were the mainstream

‘Semantics’ is not about the meaning of ‘words’; it is about the meaning of ‘utterances’ – typically statements in the language.  It is the meaning conveyed by the syntax given the terms that appear in the syntactic construct.

 >>     don't sentences and words both have meanings?

‘Pragmatics’ is about overloading the utterance per se with meaning conveyed by the speech act itself, and perhaps its context, and it touches on the notion ‘modality’ in logic and natural language.

 >> now you've lost me.  can you say that in simpler terms?

The semantics of a formal language is primarily about the meaning of its syntactic constructs, stated in terms of parametric entities that are the non-terminal symbols in the construct specification. 

 >> i.e., it's all about symbols, and not connected to the real world?  I prefer natural language.

>> do you call a computer language a formal language? it has a real world connection to an executable program.

>> the mKR language has an executable program

Formal language semantics can only deal with the meaning of terms (“words”) that have formal definitions in the language.  Ultimately, any given ‘terminological dictionary’ must be founded on a set of ‘primitive’ terms that do not have formal definitions.  In the best of cases, e.g., mathematics, in lieu of a formal definition of a ‘primitive’ term, there is a set of axioms about the term, and any “thing” in the universe of discourse that satisfies those axioms is necessarily a referent of the term.  That is, if it walks like a duck and talks like a duck, it IS a duck.  If you don’t have a formal definition or an axiomatic characterization, the term is formally UNDEFINED.  The meaning is something that only some speech community knows.

 >> I agree, up to the last sentence which I don't understand.  Are you saying only people know what axiomatic concepts are,

>> and they know the meaning by direct perception (ostensive definition)

In formal languages, we tend to shy away from pragmatics.  The speech act is almost always just presentation of a text corpus that stands for itself.  That said, the intended USE of the text corpus may have some pragmatic impact on its interpretation, but that is often confined to the intent of the primitive terms.

 >> there's so much jargon in these last two sentences, I don't know what you mean

In logic languages, the semantics of the language is usually stated in terms of a set – the universe of discourse, the things that the language can refer to – and two “distinguished values”:  True and False.  And the semantics of each syntactic construct is explained in terms of those elements.  The “meaning” of a term is either a syntactic construct that is so described, or “unknown” -- the term is ‘primitive’.  For example, an OWL Class term refers to some subset of the universe of discourse set.  If the term is said to be equivalent to an OWL Class _expression_, then you have a formal way of relating that set to other sets.  If the term is primitive, you don’t have a language rule that tells you anything much about what set that is, and in all probability the user will end up enumerating all the individual things that are interesting and are in it.

 >> that sounds more like pragmatics, or is that forbidden in a logic language?

If you want to talk about the meanings of terms, and you are producing what you bel ieve are formal definitions of the terms, you have to explain the syntax of your formal definitions clearly, and you have to give the rule that explains how each syntactic construct relates to the universe of discourse, TRUE and FALSE (or something very much the like).

 >> the syntax of mKR formal definition is:   concept is genus with differentia;

So, if:

  existent: entity, characteristic, proposition

>> you stumped me with this one, Ed.

 

 

>> I did not define a syntax for definition by enumeration.

>> I have enumerations, exclusive ors, etc.

>> but they are all designed to allow you to incrementally add species.

>> existent isc entity, characteristic, proposition;  means a concept with 3 or more species

>> my actual complete meaning for this [no syntax defined]:

>>       it is a definition by enumeration

>>       species are mutually exclusive

>>       species are exhaustive

>> this comment applies to all hierarchy descriptions

>> the species may be exclusive or not

>> the species may be exhaustive or not

>> if you choose to use only "isa", "isc", the species may actually be a unit or not

>> genus may be unique or not (if not, I call it ambiguous)

 

[EJB] As the explanation for a formal construct, there is a lot of information here that I cannot assemble into a meaningful structure.

 

I would think that  

 existent isc entity, characteristic, proposition;

is an instance of a declaration/axiom that follows some grammar rule, and in that rule, I would expect that ‘isc’ is some reserved word which the grammar or the language vocabulary defines.  So I am not sure what the parenthetical “[no syntax defined]” applies to.

 

Your “actual complete meaning” is:  the term on the left of the ‘isc’ is defined to be a ‘genus’ that is defined “by enumeration” (which means ‘defined to be the union of the species named by the terms listed on the right’) ...

You left most of the careful elaboration of the “complete” meaning out.

 

I assume “this comment applies to all hierarchy descriptions” actually refers to the two bullets that follow it, not to the bullets that precede it.  It must be that the syntax for declaring a list of species that is not exhaustive, or that is not mutually exclusive must be different from the above. 

I am guessing that “a species may actually be a unit” means that the term for the species may refer to exactly one individual thing in the UoD (ever).  How that relates to the use of “isa” or “isc” is not at all clear.  Do you mean “isa” refers to units and “isc” refers to more general species?

 

I have no idea what “genus may be unique or not” means.  I also don’t know whether a genus can also be a species of some higher level ‘genus’ in the ‘hierarchy’.  I have the impression that ‘genus’ and ‘species’ are just roles of ‘concept’ in a specific subtype relation.

 

To borrow from The Music Man, “I call that ‘slop’ – the first big step on the road to the depths of degradation ... We got trouble, folks, ...”

As I said before, this is a discipline.  If you are defining a formal ontology language, you need to do it carefully.  You don’t have to use the jargon, you can roll your own, but you do have to accept the discipline.  That is what Pat and others are on about.

 

The rest of what I wrote in this area is clearly a misunderstanding of what you are doing. 

[/EJB]

 

 

 

has a meaning in mKR, then there must be a syntax rule, e.g.,

  definition = defined-term, “:”,  defining-construct ;

  defining-construct = union-construct | ... ;

  union-construct  = term1 { “,” termK } ;

and some ‘semantics’ rule that says:

The defined-term denotes a mapping from each element of the universe of discourse to exactly one of {TRUE, FALSE}.

  For every element of the universe of discourse, the defined-term maps the element to TRUE if the defining-construct maps the element to TRUE, and otherwise the defined-term maps the element to false.

Then you can define the union-construct as a mapping from the UoD to True/False in terms of term1 and each termK:  For any element of the UoD, if ANY termK in the list maps it to True, then the union-construct maps it to True; if no termK maps it to True, then the union-construct maps it to False.

 

There are other ways to do this.  You can talk about sets instead of mappings, for example, as in the OWL semantics.  But you need some kind of formal basis for describing “semantics”.  In fact, I think you did this, in your own way, to explain the meaning of that particular construct.  But your readers are still pretty much in the dark about what the syntax rules are, and what the formal interpretation of an arbitrary rule is.

 

>> I use Backus-Naur form to define syntax

>> I also plan to use standard iyacc/ulex tools (Unicon's variant of original yacc/lex tools)

>> but for my original implementation, I hand coded all my parsers using Unicon pattern matching

This approach has been in use since the 1950s, even though I did not learn its application to formal logic until 1970.  It is a version of “Tarski’s method”.  Peter Naur and friends used a very similar approach in defining the Algol programming language in 1960.  You can see versions of it in the specifications for COBOL, Euclid, Pascal, Ada and C.  That said, it took OMG a mere 12 years to figure out that they needed to do something like this for UML. 

 

There are lots of people trying to capture knowledge in various ways, coming from different backgrounds that don’t involve the formal concepts associated with “semantics”.  They use the term to mean “what the author meant by the word”, or “what my program does with that”, and that is NOT what ‘semantics’ means in ontological circles, including linguistics.  And that is part of why your audience on this Forum is confused by your writing.

 

I understand “proof of correctness” to be a characterization of an algorithm in terms of a parametrized start state and a corresponding end state that is seen as the “correct result” of the start state.  Then, using some formal characterization of the behavior of the algorithm, e.g. Z, you create a formal logical proof that the “correct” end state is exactly what is produced from the start state.  That is you prove that, for all admissible S1(v1, ..., vN), A maps S1 to S2 (v1, ..., vN).  This is the Holy Grail of software assurance.

 

I have no idea what “proof of correctness” could possibly mean for an ontology.  By definition, every assertion in an ontology is True.  What you may be able to prove is “consistency” --  that the intended reasoning rules applied to the ontology as a whole cannot produce (and P (not P)) for any proposition P.

 >> I agree

-Ed

 

From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum-bounces@xxxxxxxxxxxxxxxx] On Behalf Of Richard H. McCullough
Sent: Thursday, April 03, 2014 7:05 AM
To: [ontolo g- forum]
Subject: Re: [ontolog-forum] mKR proof of correctness

 

Well -- I knew my age would betray me eventually.
I grew up in the era when the terms were
          syntax
          semantics
and semantics was concerned with the meaning of words.
Today, I think the popular terms  are
         syntax
         semantics
         pragmatics
and semantics is concerned with transformations of propositions
and pragmatics is concerned with the meaning of words.

So I am more focused on pragmatics, and haven't thought that much
about semantics.

But old habits are hard to break, and I keep saying semantics
when I shouldn't.  I apologize for the confusion.
 
My errors in terminology do not alter the validity of the
Objectivist Axioms, or their usefulness.  I will say more about
that later -- in response to another question which was rais ed
here in the Ontolog Forum.

Dick McCullough
Context Knowledge Systems
mKE and the mKR language
mKR/mKE tutorial

---

Date: Wed, 2 Apr 2014 23:26:21 -0700
From: steven@xxxxxxx
To: ontolog-forum@xxxxxxxxxxxxxxxx
Subject: Re: [ontolog-forum] mKR proof of correctness

Dear Pat,

 

Semantics generally say nothing about the world. They are the valid rules of syntax transformation (per Carnap).

 

McCullough's axioms make little sense to me. Indeed, they do not appear, in fact, to be axioms.  

 

Regards,

Steven

 

 

 

 

On Wed, Apr 2, 2014 at 8:21 PM, Pat Hayes <phayes@xxxxxxx> wrote:

On Apr 2, 2014, at 5:10 PM, Richard H. McCullough <rhmccullough@xxxxxxxxx> wrote:

> John
>
> I don't want there to be any doubt about what I'm saying,
> so I'm devoting one extra email to this topic.
>
> The mKR language is proved semantically correct
> because the mKR run-time system guarantees
> that the Objectivist Axioms are satisfied.

I actually laughed out loud when I read this. First, I have no idea what you mean by proving a language to be semantically correct, but claiming anything semantic **because some axioms are present** misses the entire point of having semantics in the first place, which is to connect formal sentences with claims about the actual world. Then again there is your conflation of semantics with a 'run-time system', which I take it means a system that performs inferences. But without an independent semantics, how does one know that these inferences are valid or complete? The general problem of proving that a program is correct is still open, of course, but any approach to even defining what this means requires that the language of the program has some kind of separate semantics. If the run-time system *Is* the semantics then 'correctness' is trivial to prove - the program does what the program does - but also trivially meaningless. But the final howler here is the idea that Ayn Rand's
  thoughts might have anything, even the shred of a remotest connection, to do with correctness, in any sense of that word.

IF your notation had a semantic theory that would enable an objective check to be made on its validity, and IF you could then show that those axioms were satisfied AND that your run-time system preserved truth (or whatever your semantics calls it), then you might reasonably claim that mKE had a property that one might call Randianicity: conformity to the thoughts of Ayn Rand. But to call this property "semantic correctness" is simply farcical.

Pat Hayes

>
>  Dick McCullough
> Context Knowledge Systems
> mKE and the mKR language
> mKR/mKE tutorial

------------------------------------------------------------
IHMC               ;                       (850)434 8903(850)434 8903 home
40 South Alcaniz St.            (850)202 4416(850)202 4416   office
Pensacola                            (850)202 4440(850)202 4440   fax
FL 32502                              (850)291 0667(850)291 0667   mobile (preferred)
phayes@xxxxxxx       http://www.ihmc.us/users/phayes







_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: 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 join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J

 

_________________________________________________________________ Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/ Config Subscr: 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 join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J

--_0 00_82a39a95ab534c0bbd3708fdcf902e81BN1PR09MB073namprd09pro_--
_________________________________________________________________ Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/ Config Subscr: 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 join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J

Call

Send SMS

Add to Skype

You'll need Skype CreditFree via Skype

_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Config Subscr: 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 join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J    (01)