T2 - Bidirectional Transformation of Non-hierarchical Models

This task aims at defining a generic bidirectional transformation framework for non-hierarchical models, that does not suffer from the shortcomings of existing systems. It will serve as foundation for the application domains of tasks 3, 4, and 5, and thus constitutes the key deliverable of the project. As argued in the work plan, we believe the PF relational calculus is the ideal formalism to support such framework. As such, we intend to use that formalism to redefine our own 2LT framework, currently built around the PF functional calculus for inductive data types. There are two alternatives we intend to explore in order to support non-hierarchical models in 2LT:

  • Many non-hierarchical data models can be represented by mere inductive data types enriched with invariants. For instance, sharing in an XML schema with references can be captured by an invariant forcing some elements of the document to be equal. To define a BT over a source data type with invariants, calculations must be performed in order to determine how that invariant migrates to the target, and how it is combined with backwards propagation to achieve consistent updating. The PF relational calculus is particularly well-suited for these calculations, since invariants are naturally captured by coreflexive relations (fragments of the identity relation that model predicates) [3].
  • Likewise to the functional calculus, it is possible to define a higher-order PF relational calculus. This opens interesting opportunities to use relations not only to specify transformations but as data themselves. The connection to graphs is obvious, since the adjacency matrix is just a representation of a binary relation between nodes. Although calculating with higher-order expressions is not trivial, we have shown in the past how it can be simplified using the PF style [28].

Concerning the implementation, we intend to stay with the previous type-safe approach based on the Haskell functional programming language. This reduces implementation errors, by enforcing the connection between BT rules specified at the type (meta-model) level and the respective forward and backwards implementations at the value (model) level. In order to support optimization and invariant manipulation, a simplifier for PF relational expressions must be developed. For this we intend to capitalize on the experience gathered in the design of Galculator [27], a prototype of a proof assistant based on the algebra of Galois connections, and a simplifier developed for PF program transformations based on strategic rewrite combinators [30]. Likewise to the former version, this new version of the 2LT framework will be distributed as open source software.

The expected deliverables of this task are:

  • A new version of the 2LT framework supporting non-hirarchical data models.
  • Two international conference papers and a journal paper describing the achieved results.
  • A master thesis describing the implementation of the new version of 2LT.

Given the criticality of this common framework to the success of the project, Alcino Cunha (the project PI) will be responsible for this task. He was also the responsible for the development of the first version of 2LT. The bulk of the research work will be developed by the PhD student Nuno Macedo, given his thesis on using the PF relational calculus for BT. A BI grant is planed to support a master student in the implementation of the new version of 2LT. All the remaining members of the team are involved in defining the requirements for the framework, since it will be used to implement the high-level tools for the three application domains to be tackled on tasks 3, 4, and 5.

Team

  • Manuel Alcino Cunha
  • José Nuno Oliveira
  • João Saraiva
  • Eric Van Wyk
  • Hugo Pacheco
  • Jácome Cunha
  • João Fernandes
  • Nuno Macedo [PhD]
  • BI1