One of the targeted application combines the semantic web with transformation system engineering. In the framework of the semantic web, knowledge will be independently described by different organisations in different ways. These organisations will need to combine knowledge originating from hererogeneous sources. It is thus necessary to transform knowledge before using it. The safety of the transformations must then be ensured.
This drives us directly to a framework in which transformations from one representation language to another are available from the network and proofs of various properties of these languages are attached to them. It is noteworthy that transformations and proofs do not have to come from the same origin. They can even be produced by the application client.
The transformation system engineer can gather these transformations and their proofs, check the proofs before importing them in its transformation development environment. She will then be able to create a new transformation flow and generate the proofs of the properties that she requires. Finally, she will be able to publish the transformation and its proof on the network.
This same framework applies with knowledge transformation. Indeed, if knowledge is expressed in the same language it is not necessarily expressed in the same modelling style: the ontologies can be dramatically different. To that extent, it is necessary to find the correspondences between these ontologies and take advantage of these correspondences (for transforming for instance).
In the same extent as before, alignments can be published on the web, together with some assertions of properties and exploited for transforming or merging knowledge.
The components of such an infrastructure are presented here.
In order to prove or check the properties of transformations, it is necessary to have a representation of these transformations. The XSLT language enables the expression of a transformation in XML but is relatively difficult to analyse. In order to overcome that problem, we have designed and developed, in collaboration with the FluxMedia company, the Transmorpher environment. Transmorpher allows the expression of complex transformation flows.
Transmorpher enables the definition and processing of transformations of XML documents by composing other transformations. It describes the transformation flows in XML. Input/output channels carry the information, mainly XML, from one transformation to another. Transmorpher provides a set of abstract elementary transformations (including their execution model) and one default instantiation. Such elementary transformations include external call, e.g., XSLT, dispatcher, serializer, query engine, iterator, merger, generator and rule sets.
An extension of Transmorpher towards safer transformations consists of attaching assertions to the transformations in a transformation flow in order to tell if a property is assumed, proved or to be checked. This will allow real experimentation of proving properties of compound transformations.
Alignment are more intelligible than transformations: they only express correspondences between ontology entities. This can be the basis for studying their properties (moreover, these properties can also be inferred from the methods used for generating alignments). In addition, from an alignment, it is possible to generate a transformation. So ontology alignments are natural candidates for expressing ontologydependent transformations [Euzenat 2008a].
We have developed an alignment exchange format and Alignment API [David 2011a] which enable the communication of ontology alignments on the network. It also provides a number of features such as the ability to compose alignments and to generate transformations from alignments.
We aim at using the Alignment API and implementation as a facility for communicating alignments on the web. Several potential uses of this facility are currently under study including:
Services that are necessary in such an infrastructure are:
EXMO has no ambition to generally contribute to transformation proofs, but to establish that of particular proofs of compound tranformations made of elementary transformations.
One of EXMO's goals is the consideration of transformation flows resulting from the composition of more elementary transformations. If each of these more elementary transformations is annotated by the assertion of the properties it satisfies, it remains to generate the property concerning the compound transformation. A very simple example is the termination property on finite input that is preserved through composition (but not by fixpoint computation). Model preservation for its part is preserved through both composition and iteration. So, given transformations and proofs of some of their properties, it is sometime possible to establish properties of the compound tranformation.
We want to list both the transformation constructors, e.g., composition, iteration, data separation, and the properties that can be satisfied by transformations, e.g., classifications, privileges, relevance, granularity, traceability. We can then develop a taxonomy of (machine processable) transformations for which (mainly syntactical) properties can easily be established. We could then generate, through composition, the proof of a transformation flow satisfying a property. Another line of study is the interference between properties of different types, e.g., how to preserve traceability in face of information classification?.
In a web context, transformations, their properties and their proofs can be made available on the network. Knowing the semantics of languages and the proofs of the transformation enables the application of the "proofcarrying code" idea [Necula 1998]. Consequently, the user can be sure that the result of the transformation is the transcription of the initial knowledge with the desired properties.
In order to check the proof of semantic properties, like (1) and (2), it is necessary to have (a) a representation of the transformation, (b) a specification of the semantics of languages (or of pattern specifications) and (c) a representation of the proof. These three elements will have to be developed in order to communicate and check proofs:
We have experimented with the semantics description language in the definition of DLML (so that a DSD is automatically provided with each language from the semantics of individual constructors). We have built a few proof examples, mainly equivalence proofs, in description logics. They should be a good first example for testing concepts. We are preparing the proof of model preservation of the OWL to RDF transformation that we have written.
< Dynamics  Index  References  Computational semiotics > 
http://exmo.inria.fr/research/infstruct.html
