Closed stefjoosten closed 2 years ago
I disagree that this might be a bug (for now), quoting from FormalAmpersand (two parts of Relations.adl):
RELATION sign[Relation*Signature] [UNI]
MEANING "The signature of a relation."
IDENT Relation: Relation( name, sign[Relation*Signature];src, sign[Relation*Signature];tgt[Signature*Concept] , relsDefdIn[Relation*Context])
RULE "eq relation": name[Relation*RelationName];name[Relation*RelationName]~
/\ sign[Relation*Signature];src[Signature*Concept];(sign[Relation*Signature];src[Signature*Concept])~
/\ sign[Relation*Signature];tgt[Signature*Concept];(sign[Relation*Signature];tgt[Signature*Concept])~
|- I[Relation]
MEANING "The unique signature of a relation consists of a relation name, a source concept, and a target concept."
I read this as saying that a relation can have at most one signature (by UNI) so the two different signatures for assignment make it that these must be different relations. They can therefore have different populations too. Second reason is going off the "eq relation" rule, which doesn't formally specify the same thing, but in its meaning that same train of thought seems to be implied.
Third reason: you might wish to express the following in your script:
RULE "eq assignment": assignment[BusinessActor*BusinessProcess] = assignment[BusinessRole*BusinessProcess]
If the two relations were the same, the rule would be trivially true and therefore not expressible (that is, in a formal sense: writing 'True' as a rule would have the same formal meaning).
Your suggestion to add RULE "eq assignment"
does not solve the error message, because that is a type error.
Besides, RULE "eq assignment"
is already satisfied by the following reasoning:
A
,B
be concepts and let $A$ be the set of atoms in A
and let $B$ be the set of atoms in B
.CLASSIFY A IS B
means that A
$=$B
, i.e. $\forall x: x\in A\ \Leftrightarrow\ x\in B$.RULE "eq relation"
means:
$name(r)=name(s)\ \wedge\ src(sign(r))=src(sign(s))\ \wedge\ tgt(sign(r))=tgt(sign(s))\ \Rightarrow\ r=s$RELATION assignment[BusinessActor*BusinessProcess]
RELATION assignment[BusinessRole*BusinessProcess]
CLASSIFY BusinessActor IS BusinessRole
means that assignment[BusinessActor*BusinessProcess]
$=$assignment[BusinessRole*BusinessProcess]
, i.e. $\forall (p,q): (p,q)\in$assignment[BusinessActor*BusinessProcess]
$\ \Leftrightarrow\ (p,q)\in$assignment[BusinessRole*BusinessProcess]
.
Both relations are the same, simply because BusinessActor
and BusinessRole
are the same. Note that the implementation in the database is already consistent with this.
So maybe you could reconsider your answer...?
(@sjcjoosten, Did you accidentally read the inclusion in RULE "eq relation"
the other way around?)
Note that the MEANING
of RULE "eq relation"
in FormalAmpersand is confusing due to the word "unique".
Aha, I see! (The quarter has fallen...). The culprit of our misunderstanding is in FormalAmpersand:
RELATION sign[Relation*Signature] [UNI]
This is wrong. It should not be univalent at all.
Aha, I see! (The quarter has fallen...). The culprit of our misunderstanding is in FormalAmpersand:
RELATION sign[Relation*Signature] [UNI]
This is wrong. It should not be univalent at all.
Interesting. This has consequences for EQ on relations. @stefjoosten, please explain what the EQ on relations should be?
Yeah, you are right. My comment "The quarter has fallen" is nonsense. I have slept a night over it and it dawned on me as I woke up. So Please ignore that comment.
Surely, RELATION sign[Relation*Signature]
is univalent for the same reason: A
$=$B
implies that [A*C]
$=$[B*C]
.
So let us leave FormalAmpersand as it is. Sorry for generating noise.
By the way, I believe that FormalAmpersand isn't strict enough: The relation sign[Relation*Signature]
should be total as well, but I do not want to interfere with the discussion between @sjcjoosten and @stefjoosten
I don't think it is a good idea to interpret CLASSIFY A IS B
as A = B
. I'd rather interpret it as saying that the population of A
and B
are equal whenever the database is stable/consistent. So I agree with $\forall x: x\in P(A)\ \Leftrightarrow\ x\in P(B)$ (I read the $P$ as 'Population at some point in time', and I intend universal quantification over all such populations).
Consider this script:
CONCEPT Actor MEANING "An organizational entity that is capable of performing behavior."
CONCEPT Role
CLASSIFY Actor IS Role
I believe that Role should not carry the meaning An organizational entity that is capable of performing behavior.
.
We need to discuss this...
It seems obvious to me what is going on. Let me try to phrase this:
First the facts: 1) In your script you have two relations ($r$ and $s$) where: 1) $name(r) == name(s)$ 1) $typology(source(r)) == typology(source(s))$ 1) $typology(target(r)) == typology(target(s))$ 1) As @sjcjoosten explained, these relations are not equal. 1) The &-generator refuses your script with a confusing error message.
The way ampersand works, we cannot administer the population of both relations, because they would be implemented as a single relation. Aslo, (as suggested by your intent) it makes sense to think about both relations as being semantically the same. The script would be perfectly OK if the most specific relation (I know, this cannot be said formally, but I guess/hope you understand what I mean) was left out.
So in formal ampersand we should have a rule, saying that two relations with the same name, where the sources share the same typology and the targets share the same typology must not exist. Then implement that rule, give it a nice error message.
Thanks for a good discussion, @sjcjoosten. Let me summarize my lessons learned and close this issue.
The desired effect in this issue is that two concepts, A
(population is $A$) and B
(population is $B$), are brought together to form one concept C
with the population $A\cup B$.
Concepts A
and B
both have a different MEANING
:
CONCEPT A "This is the meaning of A."
CONCEPT B "This is the meaning of B."
Now we want to state that their populations are equal:
CLASSIFY A, B ISA C
RULE I[A]=I[B]
This keeps the type checker happy. However, if we add some population we can see that something is wrong:
CONTEXT Issue1306
CONCEPT A "This is the meaning of A."
CONCEPT B "This is the meaning of B."
CLASSIFY A, B ISA C
RULE I[A]=I[B]
POPULATION A CONTAINS ["a5", "a2"]
POPULATION B CONTAINS ["b5"]
ENDCONTEXT
This produces 3 violations of RULE I[A]=I[B]
:
("a5", "a5")
("a2", "a2")
("b5", "b5")
So, the populations of concepts $A$ and $B$ are still different. We must add
CLASSIFY C ISA A
CLASSIFY C ISA B
to make the populations identical. Now the type checker is happy and RULE I[A]=I[B]
is satisfied.
the script that started this issue should have been written as:
CONTEXT "Issue1306"
RELATION triggering[BusinessProcess*BusinessProcess] -- from ArchiMetaModel.adl
RELATION assignment[BusinessActor*BusinessProcess] -- from ArchiMetaModel.adl
RELATION assignment[BusinessRole*BusinessProcess] -- from ArchiMetaModel.adl
CLASSIFY BusinessActor, BusinessRole ISA C
CLASSIFY C ISA BusinessActor
CLASSIFY C ISA BusinessRole
RULE SubsequentSteps : triggering[BusinessProcess] |- assignment~;assignment
ENDCONTEXT
This keeps the type checker happy and RULE SubsequentSteps
treats business actors and business roles as the same concept (which was the intention of the author in this situation).
What happened
I tried to compile the following script
I got the following error messages from the compiler:
What I expected
I expected that this script is correct, because the declaration
CLASSIFY BusinessActor IS BusinessRole
would makeBusinessActor
andBusinessRole
100% synonym. This implies that relationsassignment[BusinessActor*BusinessProcess]
andassignment[BusinessRole*BusinessProcess]
are provably the same relations. Hence, there is nothing to disambiguate.Version of ampersand that was used
Ampersand-v4.6.3 [feature/typecheck-ENFORCE:b7df07b3c*]