search

gruninger / Common-Logic

Documents for the developments of ISO 24707 Editiion 2 (Common Logic)
8 stars 3 forks source link

Circular Imports #35

Open greenTara opened 11 years ago

greenTara commented 11 years ago

The semantics of cl-imports needs to be clarified: are circular imports allowed? If yes, what is their semantics?

tillmo commented 11 years ago

Fabian has proposed a semantics of circular imports, which however is so complicated that we should not adopt it.

greenTara commented 11 years ago

Given

(cl-text <name> <body>)

John Sowa has proposed replacing

   (cl-imports <name>)

with

   (<name>)

which would require an additional semantic constraint equivalent to

(iff
    (<name>)
    (and <body>)
)

As far as I can see, this would take care of the issue with circular imports.

In particular, consider the case of two otherwise vacuous texts that import each other.

(cl-text "a" (b))
(cl-text "b" (a))

One interpretation assigns a value of true to both (a) and (b). Another interpretation assigns a value of false to both (a) and (b).

The advantages I see to this approach are

  1. There is no longer a conflict with Tarskian principles.
  2. There is no copying involved, virtual or otherwise.
  3. It is left to implementations whether they verify the extra semantics condition once and store this information somewhere, or recheck it (or "touch" it) again whenever the importation is encountered. CL is thus agnostic as to practical consequences of circular imports.
  4. It allows the truth value of an imported text to be a condition
(cl-text "a" (b))
(if ("a") <...>)
  1. It allows an importation to be conditional on other things
(cl-text "a" (b))
(if (c)  ("a"))
tillmo commented 11 years ago

What about keeping (cl-imports name), but equipping it with the above sketched semantics? The advantanges are

greenTara commented 11 years ago

That seems like an acceptable approach to me. As mentioned by Till on the mailing list, the ability to state an equivalence between a nullary proposition and some conjunction of sentences is already included in CL. So in that case, what is needed to turn this sketch into a proposal for revision of the standard is

  1. modification of the abstract semantics to include the notion of the interpretation of a (user-defined) collection where the interpretation of the collection is true exactly when a) all texts in the collection interpret to true b) there is exactly one named text in the collection for each name appearing in an importation phrase in any text of the collection c) there is consistency between the truth-value of an importation phrase (which is provided directly by the interpretation, similar to the approach for irregular sentences) and the truth value of the body of the named text of that name
  2. removal of the effects of publication of a named text on a network on the denotation of the name of the text

The interpretation of a text in a collection remains the same except that the truth-value of an importation phrase is provided directly by the interpretation.

How 1.c) is accomplished in practice depends on the mechanism for "retrieving" the text associated with a name. Here are a couple of options:

A. In the current CL standard, this is accomplished with the name-text pair denotation and the text() function. So 1.c) would look like I( text ( I(N) ) ) = I ( E ) where E is the importation phrase containing the name N.

B.We could make text() be a total function on the universe of reference and drop the notion of name-text pair, and modify the semantics of the named text expression. In this case, if E is a named text expression with name N and body text T, I(E) is true exactly when Tr_D ( T ) = text ( I (N) ), where Tr_D is a 1-1 translation mapping from the dialect D of the text T into a common dialect. This approach does away with the idea of a fixed denotation for an identifier, so that identifiers are just like any other name.

tillmo commented 11 years ago

New proposal for ci-imports developed in the teleconference on November 28, 2012:

keep cl-imports syntax, but with a new semantics: the model class of the importing text is defined as the class of all models (a) satisfying the axioms local to the importing text, and (b) are in the model class of the imported text (possibly after being restricted to the appropriate vocabulary). Put differently: a model satisfies the importing text if (a) it satisfies all the axioms local to the importing text, and (b) it is a model of the imported text. Note that this does not involve copying.

The difference to the current semantics in ISO 24707 is that currently, names of cl-texts denote in the universe of discourse. The rationale for let them not denote is the "small models" argument of Ian Horrocks. More precisely, if names of cl-texts (belonging to the meta level in my opinion) denote, they will mess up the model theory. Cf. Fabian's observation that in CLIF, you can prove that at least 100 different individuals exists, just because there are 100 different ct-texts. So the permutation group of degree 6 (which I use in my research) is not a CLIF model.

With this approach, it is also possible but more difficult to give a semantics to circular imports. (I would suggest to forbid ciruclar imports.)

Is there some example that would differentiate the current ISO 24707 from this new proposal? I guess it must be something like (forall (x) (if (= (author x) Fabian) (cl-imports x)), meaning "all texts authored by Fabian are true". Note that this example is not possible in the current ISO 24707, because cl-imports cannot occur within a sentence.

greenTara commented 11 years ago

This new proposal fails to mention the means by which an imported text is associated with a name/identifier. Is the intention for that to be dropped from the CL standard? to keep the existing mechanism of named texts but to require these names to be excluded from the universe of discourse? to introduce some other mechanism? It is difficult to evaluate this proposal without the full details.

Regarding the idea of some meta-level above CL semantics to handle importations, metadata etc, - in my view unnamed CL texts are the meta-level, with modules being the underlying level.

Take for example the mentioned example of the permutation group of degree 6, I would think there are other problems with this being a CLIF model besides its importation along with 100 other texts. One point is that the standard doesn't actually define the concept of a model, and this is less trivial than one might suppose. Aside from that, if these 100 texts together use more than 6 different predicates or 6 different functions, then there must be more than 6 individuals in the universe of discourse, because of the wild-west syntax.

To me, treating such a text as an ordinary named text seems like a very fragile approach to the problem, which would be solved by using a module construct (with more functionality than is currently present) because it seems to be inherently oriented towards a segregated representation. The module's universe of discourse should have a name (and does not belong to itself) and then certain axioms can be stated about it as a predicate, such as there exist exactly 6 members (1-tuples in its extension). This could be easily stated with the syntactic sugar version of the proposed numerical quantifier syntax. If the universe of discourse of the module were not required to contain all individuals of the universe of discourse of the text it is imported into except those explicitly listed in the exclusion list, then this axiom (of 6 individuals in the module's universe of discourse) could be easily satisfied. I believe that is the real problem, not the importation semantics.

The problem with requiring the name of texts (and modules and their universe of discourse) to always to be out of the universe of discourse is that it eliminates flexibility for those users who do want to have the name of some texts in the universe of discourse, for the purpose of expressing "metadata" about CL texts. The use case is as follows: a document contains a named text or module and also simple statements of metadata using the name of the text as an argument.

We can do this in (almost) the current CLIF, (assuming we adopt the IKL syntax for numerical quantification and resolve the ambiguous text production in a way that allows modules as phrases):

("http://purl.org/dc/terms/creator" "http://example.org/mytext.clif#pg6" "mailto:till@gmail.com")
(cl-module "http://example.org/mytext.clif#pg6"
   (cl-excludes 
      "http://purl.org/dc/terms/creator" 
      "http://example.org/mytext.clif#pg6" 
      "mailto:till@gmail.com")
   (exists 6 (x) ("http://example.org/mytext.clif#pg6" x))
   (not  (exists 7 (x) ("http://example.org/mytext.clif#pg6" x)))
   <module body here>)
)

The only problem is that it is annoying to have to list all these excluded names that may not even occur inside the module, and it is not feasible to keep the exclusion list up-to-date with all names from every text we might want to import this module into. So let's fix the module syntax and semantics (Issue #25) so that it is usable instead of expecting the importation/named-text semantics to solve this problem (the permutation group example).

tillmo commented 11 years ago

My proposal is to keep the association between names an CL texts outside CL models, and treat it at the meta level. I find it dubious to force inclusion of this association, which is highly dependent of context and on the state of the web, into models. This does not mean that the names have to be exlucded from models. They can occur in models, as in your example, or they can be left out. It is the choice of the user. My point is just that the user shouldn't be forced to have them in.

If you disagree, I would like to see a single example where the fact that the association between names an CL texts is part of CL models is actually used. Your example above is not such an example. An example would need to use cl-text, since cl-text is the only construct whose semantic refers to the association between names and CL texts (this association is called "text(...)" in the standard).

greenTara commented 11 years ago

I agree that a user shouldn't be forced to accept a name-text association just because it is published somewhere on the Web. That is why I have proposed, above, that we introduce the concept of an interpretation of a collection of texts, without specifying how such a collection of texts is constructed. In this way we can talk about a distributed representation of axioms in a very abstract manner. Application of this abstraction to concrete situations, such as the Web, would be outside of the scope of the CL standard.

Regarding the example above, the semantics of modules and texts is in flux now, but I think there is agreement that there is a strong relationship between modules and named texts. Otherwise, how is the importation of a module defined?

tillmo commented 11 years ago

Agreed, cl-text and cl-module should be combined now, as suggested by #24. Still, your example does not make direct use of the name-textassociation. It perfectly works as well if the association is kept at the meta level. I repeat: I guess an example must be something like (forall (x) (if (= (author x) Fabian) (cl-imports x)), meaning "all texts authored by Fabian are true". Note that this example is not possible in the current ISO 24707, because cl-imports cannot occur within a sentence.

fabianneuhaus commented 11 years ago

On 1/8/13 9:28 AM, Till Mossakowski wrote:

Agreed, cl-text and cl-module should be combined now, as suggested by

24 https://github.com/gruninger/Common-Logic/issues/24.

I tried to work out the details, and I haven't been able to make this proposal work yet. It is certainly not just a matter of reusing the proposed semantics for modules for (named) text. Let me ignore the "named" part of the text, because it is an additional complication.

Here is the requirement for segregation:

(cl:text (cl:segregate P) (P a) ) should not entail (exists (= x P))

However, (cl:module (cl:exclude P) (P a)) entails (exists (= x P))

It does not entail (cl:module (cl:exclude P) (exists (= x P))) but that is not what is required.

The reason for that is the following: The semantics of modules (or maybe a better term is "domain restrictions") is roughly the following (cl:domain_restriction my_domain my_text) is true under some interpretation X iff

Note that entailment is defined with respect to the "most-outside" interpretations, the restricted interpretation Y in the example above plays only a role in determining the truth value of the text. (In a similar way as quantifying over variants of interpretations is used to determine the truth-value of a quantified text.)

To make segregation work we can't reuse the proposed semantics for modules/domain_restrictions. Something along the lines of (cl:text (cl:segregate my_term) my_text ) is true with respect to I iff

(This does not really work, I am just trying to illustrate the difference between modules/domain_restrictions and segregation.)

It might be possible to merge texts and modules/domain_restrictions, but it is not obvious to me how.

Best Fabian

CL-mailing-list commented 11 years ago

More on the issue:

One question that we haven't addressed are the impacts on the definition of interpretation. In the current version of the standard an interpretation is defined with respect to a vocabulary. A vocabulary is partitioned into discourse names and non-discourse names. This is important for the following requirement: (R1) For any interpretation I of a vocabulary V, int_I(v) in domain_of_discourse iff v is a discourse name.

Now consider ontologies like the following

/* ontology1 */ (cl:text (cl:import foo) )

(cl:text foo (segregate Q) (P b) (Q a) )

It seems that we need to give up the idea that the vocabulary is partitioned into discourse names and non-discourse names. Because that would clash with the ability to declare non-discourse names as part of texts. However, this leaves us with the problem: What to do about (R1)?

If we just abandon (R1), then the semantics of CL is changed. Consider ontology2.

/* ontology2 */ (P a)

Currently, there are two possibilities: either P is a discourse name or P is a non-discourse name. If P is a discourse name, then in all interpretations that are satisfy ontology2 the interpretation of P is in the universe of discourse and, thus, ontology2 entails (exists (x) (= P x)). If P is not a discourse name, then in all interpretations that satisfy ontology2 the interpretation of P is not in the universe of discourse and, ontology2 would entail (not (exists (x) (= P x))) if it was syntactically valid CL. However, without (R1) ontology2 would be satisfied by interpretations of both kind.

The only way that I see to keep something like (R1) is to change the definition of interpretation in a way that that it is relative to a set of CL texts (and not just a vocabulary) because the segregations are declared within texts. Thus, all interpretations that satisfy ontology1 would have to treat Q as a non-discourse term and P, a, b as discourse terms.

However, this is pretty ugly, because logical truth would be only defined with respect to a set of texts. And what do we do with cases like ontology3?

/* ontology3 */ (cl:text (P Q) (cl:import foo) )

Best Fabian

tillmo commented 11 years ago

I welcome your last proposal, and would let it base on the fact that a vocabulary needs to specify which names are discourse and which are non-discourse. This is in accordance with the current standard, p.13: "A dialect may require some names to be non-discourse names, which are understood not to denote entities in the universe of discourse."