Language Lattice

From RuleML Wiki
Jump to: navigation, search

1 Formal Definitions and Proofs

1.1 Definitions

To formally define the various partial orderings, we will make use of the concept of "semantics-preserving mappings" (see for example http://www.w3.org/2005/rules/wiki/BLD#Conformance_Clauses.) A complete definition of "semantics-preserving mapping" in a particular situation depends on the formal semantics of the languages involved. On this page, we primarily consider syntax, so it is not necesary to know the details of the formal semantics of RuleML. Instead, we will utilize an abstract definition of semantics for a language L . In particular:

  • We suppose there is a semantic entailment relation for L, symbolized by |=L.
  • Let L1 and L2 be languages with entailment relations |=1 and |=2. Then F is a semantics-preserving mapping from L1 (or some subset of L1) into L2 exactly when F(D1) =|=2 F(D2) iff D1 =|=1 D2.
  • We assume we are working within a family of overlapping languages (there are expressions that belong to both languages) where the semantics is invariant between languages. That is, the identity mapping is a semantics-preserving mapping on the intersection of any two languages within a language family, i.e., if A and B belong to both L1 and L2, then A =|=1 B iff A =|=2 B .
  • We also assume semantics are invariant to schema validation. That is, the mapping V from an instance document in, say, XML-format to its post-schema validation infoset (PSVI) is a semantics-preserving mapping of L into LV (the set of PSVIs of expressions in L), so that D1 |=L D2, then V(D1) |=LV V(D2).
  • Normalization is an idempotent mapping (N) defined for every grammatically-valid instance document of a language L into a subset, LN, of such documents. We assume that normalization is semantics-preserving. That is, N(D) =|= D.
  • Semantic Containment: A language L1 is a semantic sublanguage of another language L2 if there is a semantics-preserving mapping defined on L1 into L2.
  • PSVI Containment: A language L1 is a PSVI sublanguage of another language L2 if there is a semantics-preserving mapping F defined on L1 into L2 where for every valid instance document D in L1, D and F(D) have the same post-schema-validation infoset. That is, V1(D) = V2(F(D)).
  • Normalized Containment: A language L1 is a normalization sublanguage of another language L2 if there is a semantics-preserving mapping F from L1 into L2 where for every valid instance document D in L1, D and F(D) have the same "normalization". That is, N1(D) = N2(F(D)).
  • Syntactic Containment: A language L1 is a syntactic sublanguage of another language L2 if every grammatically-valid instance document of L1 is also a grammatically-valid instance document of L2. That is, D "in" L1 implies D "in" L2.
  • Grammatical Containment: A formal grammar is defined by its sets of terminal, non-terminal and start symbols, and its production rules. A language L1 is a grammatical sublanguage of another language L2 if the set of terminal symbols of L1 are a subset of the terminal symbols of L2, and there is a one-to-one mapping M from the nonterminal and start symbols of L1 into the respective sets of symbols of L2 such that every production rule in the grammar of L1 may be transformed into a production rule in the grammar of L2 by applying the mapping M.

Note: There are generally many equivalent ways to state a set of grammar rules, in the sense that they generate languages which are equivalent (each contains the other), and this is not taken into account in the definition of grammatical containment. Equivalence classes may be defined for grammars in terms of the languages they define, using any of the first four definitions of containment may be used to define equivalence classes for grammars, and these equivalence classes can be partially ordered by utilizing the order relation of the languages they generate. That is, for each containment relation, an isomorphism may be defined from the poset of languages to a poset of equivalence classes of grammars. grammars.

1.2 Theorems

Theorem 1. Let G be a lattice with order relation ≤, with meet * and join +, G' be a subset of G, and f be an idempotent, order-preserving mapping defined on G onto G'. Then G' is also a lattice w.r.t. ≤, with meet *' and join +', where

g1 +' g2 = f( g1 + g2)

and

g1 *' g2 = f( g1 * g2).

Proof. Let g1, g2 and g3 belong to G', with g1 ≤ g3 and g2 ≤ g3. Then g1, g2 and g3 also belong to G, so

g1+g2 ≤ g3

Because f is order preserving, we have

f(g1+g2) ≤ f(g3)

Because f is idempotent and g3 belongs to G', then f(g3) = g3 and consequently

f(g1+g2) ≤ g3

Also for i = 1,2

gi ≤ g1+g2

so

gi = f(gi) ≤ f(g1+g2) ≤ g3

That is, f(g1+g2) is the l.u.b. of {g1, g2} in G', so g1+'g2 = f(g1+g2)

The derivation of the meet *' is similar.

1.3 Applications

1.3.1 Language Poset Generated from RuleML RNC Modules is a Lattice

Application of Theorem 1. It is sufficient to construct the mapping f. The lattice G is the powerset of optional modules. G' is a poset that we will show is isomorphic to the language poset, by constructing an invertible, order-preserving mapping from G' to the PHP query string.

@@@ paste PHP code for mapping f here @@@