Closed zhangyuanlin closed 6 years ago
I will comment out the section that is generating this semantic error. Another nail in the coffin of the idea of "source sorts" being in the DAG sense (leaf in the hierarchy).
There is no more sematic error, however the produced program has no answerset. I am closing this issue since the semantic error is resolved.
Ed,
Thanks! I think I understand to some extent your concern.
If you remember, there is a big assumption in the paper (roughly) that every function name is unique. So, we do the same for constants.
In fact, in future, all your concerns can be properly addressed by removing those assumptions (by introducing "local names" and "name spaces.").
A quick conclusion.
For the SPARC program we discussed, I tested and when asking query source(elevations), the answer is no. So, CALM is not correct according to definition of sort-hierarchy. Remember, programer can use source() in their ALM program.
YL
PS I moved these discuss to issue tracker.
From: Edward Wertz edward.o.wertz@gmail.com Sent: Thursday, August 23, 2018 6:44 AM To: Zhang, Y; Chandrasekaran, Anuradha Subject: Re: Fw: [Topology/ALM-Compiler] CALM bug? - "singleton" anonymous subsort of elevations in basicmotion_yn (#8)
Since we have no way of marking a sort as closed, every user defined sort can be extended in the future. Any constants declared would become instances of non-source sorts ( dag sense of source).
I do not think my translation is solid because I try to erase the inferred singletons in the final program, but do not do a complete job of it. Since we invent the name of the created singleton, it looks ugly and may be unexpected by the programmer. But I think the correct solution is to leave them in and have the constants have is_a( const, singleton-sort) be true.
For type checking, the singletons are used as valid types.
Ultimately the final solver has no concept of sort or type, and treats all entities with the same syntax as the same entity. These types of issues can only be caught by type checking if we want to enforce them.
Part of the problem is that ALM has no facility for namespace. And this is where the java sense of package is not just a set of classes. The name of the package is also the namespace of the classes it contains. If two different packages have the same name of a class, they are not the same class. If another class uses both classes of the same name, they must always use the fully qualified name to differentiate usage and avoid ambiguity.
The reason I am always going to a theoretic discussion on this bug report is because I feel like our formal understanding here is weak.
In Java, if a third class imports two other classes, all instances keep their state separate from each other because in reality the package name of the class and the class name itself act as a namespace on the internal state, keeping it separate.
An ALM module import/dependency says "take your insides and make them my insides". Which is fine for completely orthogonal modules that do not share named entities. But since we have no concept of namespaces, flattening modules which overlap in named entities may have significant and subtle unintended consequences, such as treating what were different semantic entities as the same semantic entity from the ambiguity of using the same syntactic representation in separate modules.
This is why I brought up the example of not wanting to treat these two constant declarations as the same.
John : horse, person
And
John :horse John :person
The first gets an inferred singleton or "anonymous" subsort that acts as the source of the instance.
The second may be a result of two different module imports contributing the statements separately.
So the original question in your bug report is do these anonymous singletons we introduced matter? Are they evidence of non-source (dag sense) of the parent sort? My answer is yes. We added them to the hierarchy for a reason, which is to carry the work of semantic unification of two constants of two different sorts. John being a horse and a person in the same statement makes john different from every other person and every other horse. He is a different fundamental kind of entity and we can create state constraints which target John specifically apart from other persons. In that sense, John is not in the same equivalence class as other persons or horses.
Regardless.of what my compiler does now, what it should do is a big open question. If we automatically unify all entities with the same syntax as the same semantic entity during module flattening, then a programmer must fully understand all modules and the interaction between all modules when flattened. This severely limits the modularity and reusability of the modules. In Java, I don't have to worry about colliding with another objects private state since they are kept separate by namespace. I can write java programs which have 50 chains deep of nested imports and dependencies, all hidden from my view and of no concern to me.
But with module flattening... now I have to know the full stack of dependencies and interactions on flattening. Fine for small problems. But if ALM programming takes off, name collision is going to become a serious issue.
Edward
On Aug 23, 2018 12:25 AM, "Zhang, Y" Y.Zhang@ttu.edu wrote: thanks. I think that is not what I want to know about my question. Maybe my question is not clear.
1) Is it true that some source sort has hidden subsort? (we have [[no text]] is a subsort of elevations, roughly).
2) If a source sort A has a hidden subsort, is A a source sort? (My understanding is yes. But from the bug report, it seems that CALM treats elevations as a non-source sort. If you think that is correct, that is fine. I just want to make sure you are aware of it.)
YL
CALM aug 20 version still has this complaint
for the program
basicmotion_yn.tp
below