Miscellaneous-B

This afternoon Kerry and I spent some time looking at a particular aspect of Tefkat that was troubling us. We had a couple of rules of the following form:

RULE one(f, b)
FORALL Foo f
MAKE DYNAMIC Bar b // implicitly FROM one(f)
;

RULE two(f, b) EXTENDS one(f, b)
WHERE f.attr = 0
MAKE DYNAMIC Baz b // implicitly FROM two(f)
;

the idea being that for each of a subset of the instances of Foo, one should create an instance of Baz instead of an instance of Bar (this requires that Baz is a subtype of Bar).

To cut a long story short, the problem we were running in to is that there are different function symbols in the implicit FROM clauses of each of the rules, thus leading to the situation where separate Bar and Baz instances were being created and then asserted as being the same object.

My first instinct was to say, “oh, we’ve found an implementation bug, let’s fix it“. I was thinking that while the Tefkat FROM clauses must behave as injections, that there were actually effectively multiple functions involved and thus it was okay for one(f) = two(f). Unfortunately, it’s not that simple; in summary, my original Tefkat implementation was correctly implementing an injective function of the form I(<func>, <args>) and thus ensuring I(one, f) != I(two, f).

In summary, the fragment MAKE Foo f FROM p(1), Foo f FROM q(1) will always fail (consider the semantically equivalent fragment MAKE Foo f FROM p(1), Foo g FROM q(1) SET f = g).

So, what’s the F-Logic reference in the title about? Well, F-Logic allows the definition of one’s own equality theory, Tefkat is based on a (very) restricted subset of F-Logic, and the FROM “functions” in Tefkat behave as F-Logic OIDs. That is, they act as logical object identifiers, and an F-Logic equality theory allows you to say that two (or more) logical object identifiers refer to the same object.

What does all this mean? Well, it means that there is a formal basis we can use to allow for multiple injective functions, but there is a cost. The cost is that any test for object equality (or inequality) must take into account any specific equality theory defined by the transformation rules. Fortunately, such an equality theory can only apply to objects created by the transformation which limits the impact somewhat, but even so I’m not yet sure that the cost of the resulting inter-rule dependencies is not too high. It’s not even clear, from a language usability-design perspective, if there is much of a gain in allowing MAKE Foo f FROM p(1), Foo f FROM q(1).

I think the path to understanding and answering this last question may be had from an analysis of the underlying relationship between Tefkat’s transformation rules and the mathematics of mapping relations between models along the lines of Akehurst, Kent, and Patrascoiu’s “A relational approach to defining and implementing transformations between metamodels“ (actually, I’m yet to read this paper, but I think it should be relevant based on David Akehurt’s other publications on the topic).