Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Circular Imports #35

Open
greenTara opened this issue Oct 23, 2012 · 12 comments
Open

Circular Imports #35

greenTara opened this issue Oct 23, 2012 · 12 comments
Assignees
@gruninger
Labels
bug

Comments

@greenTara
Copy link
Collaborator

The semantics of cl-imports needs to be clarified: are circular imports allowed? If yes, what is their semantics?
@ghost ghost assigned gruninger Oct 23, 2012
@tillmo
Copy link
Collaborator

tillmo commented Nov 19, 2012

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

@greenTara
Copy link
Collaborator Author

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
Copy link
Collaborator

tillmo commented Nov 27, 2012

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

  • more backwards compatibility
  • things like (if (cl-imports name) ...) are disallowed, and the resulting scaling problems are avoided.

@greenTara
Copy link
Collaborator Author

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
Copy link
Collaborator

tillmo commented Nov 29, 2012

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
Copy link
Collaborator Author

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).

@greenTara greenTara mentioned this issue Dec 4, 2012
Open
@tillmo
Copy link
Collaborator

tillmo commented Jan 8, 2013

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
Copy link
Collaborator Author

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
Copy link
Collaborator

tillmo commented Jan 8, 2013

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
Copy link

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

Agreed, cl-text and cl-module should be combined now, as suggested by
#24 #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

  • there is some interpretation Y which differs from X by restricting the
    domain in some way such that Y makes my_text true.
  • some additional conditions about non-denoting terms not occurring in
    argument position.

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

  • int_I(my_term) not in universe of discourse of I
  • I(my_text) = true

(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
Copy link

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
Copy link
Collaborator

tillmo commented Jan 8, 2013

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."

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@gruninger gruninger

Labels
bug
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
5 participants
@tillmo @greenTara @gruninger @fabianneuhaus @CL-mailing-list