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.

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

Modules Refactoring #50

Open
2 of 7 tasks
jsbezerra opened this issue May 22, 2017 · 3 comments
Open
2 of 7 tasks

Modules Refactoring #50

jsbezerra opened this issue May 22, 2017 · 3 comments

Comments

@jsbezerra
Copy link
Member

jsbezerra commented May 22, 2017

There are some operations spread among the modules of DPO and AdhesiveHLR that do not appear to be in the right place. Specially regarding NACs and rewritting. Such as:

DPO:
nacDownwardShift

AdhesiveHLR:
MatchRestriction
matchRestrictionToMorphismType
NacSatisfaction

Since we are in a process of refactoring the projects architecture, should we create new specific modules for?

  • NAC-Adhesive Categories
    • Renaming the current module?
  • Abstract Rewritting Approaches
  • DPO Rewritting approach outside the Category module
  • Change MatchRestriction to MorphismType.

Related Issues:

@ggazzi
Copy link
Member

ggazzi commented May 22, 2017

Regarding nacDownwardShift, couldn't we frame it as shifting a constraint rather than an application condition? After all, an application condition is essentially a constraint whose "antecedent-object" is the left-hand side of the rule.

In this case, we could rename it to shiftConstraintDown, place it on the constraint module, and document it as: "Given a constraint c : P -> C and a morphism f : P -> P', obtains an equivalent set of constraints c'i : P' -> C. That is, for any graph, the original constraint c is satisfied if and only if all constraints c'i are satisfied."

@ggazzi
Copy link
Member

ggazzi commented May 22, 2017

Regarding the match restriction and NAC satisfaction, this will interact with a complexity of symbolic graphs: we don't want to restrict matches to be completely monic, just monic on the graph part (the attribute part may be non-monic). So we'll need to express different classes of morphisms, which may be specific to particular categories. This is all to say that we don't have enough information to make a good choice at this point.

In this case, I think match restriction and NAC satisfaction belong in the DPO module, along with its configuration (MorphismsConfig). We could even remove MatchRestriction, use just a MorphismType.

Even the NAC satisfaction could be removed. We could have a function findSpanCommuter : MorphismType -> MorphismType -> morph -> morph -> morph, where the first restriction is for the mappings induced by the span and the second restriction is for the mappings outside the image of the span. Then, NacSatisfaction could also be replaced by a simple MorphismType.

@jsbezerra
Copy link
Member Author

jsbezerra commented May 23, 2017

@ggazzi about your first comment:

"an application condition is essentially a constraint whose "antecedent-object" is the left-hand side of the rule"

I don't think that applies, as only atomic constraints have premise objects and only the negative ones could be used to emulate NACs like that. Furthermore, the module Constraints deals not only with atomic, but with the more generic (logical) form of constraints.

Moreover, there is no notion (as far as I know) of shifting constraints over morphisms, as they apply over the objects of a category, not the morphisms themselves1.

Instead, this shifiting of nacs over morphisms does belong to the class of NAC-adhesive HLR Categories, as shown in Lambers2010, section 3.3. This also seems to be the case for all the other NAC operations implemented so far.

I agree with the change of MatchRestriction ot MorphismType. And I also think that there is no problem in not knowing right now which are (all) kinds of morphisms we may have to deal with. Worst case: we make the adhesive type class requiring concrete categories to provide which are the M-, E- or any other necessary class of morphisms.


1 Maybe this could be case with nested application conditions?

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