Global decomposition does not work across library borders

[till]

Attached two files that illustrate the problem. The view in GlobDecomp2.casl is provable, although it should not. The problem is that the node sp (and therefore also its axioms) are never reached by global decomposition. How to fix: Global decomposition should not only follow any DGRef nodes (this is done now already), but also examine the ingoing links into such node that are present in the other library. These links (and the corresponding source nodes) should be duplicated in the present library.

[ken]

In one library there could be more than one referenced node, whose original nodes are the same. This could firstly lead to redundancy and came to problems, e.g. in the case of this ticket, which tries to apply global decomposition along library border.

It's fixed by:

in module

Static.AnalysisLibrary

the function refNodesig is modified to advoid inserting duplicating referenced nodes by calling a check function checkHasExistedNode

[ken]

To fix the actual problem, the current library will be checked everytime before a GlobalDecomposition? is actually applied, to see if the current library contains some referenced nodes, which are related to the global edges being involved. If so, the referenced node will be extended by taking all its predecessors out of the referenced library and inserting them into the current one.

The corresponding changes are:

in module

Proofs.Global

several functions are added to try to extend the current library if necessary. The extending action will be carried out by calling the function updateCurrentDGraphWithReferencedLib.

However, there is still a efficiency's problem here. The checking of an existed Node costs too much, because it has to take all the nodes out of current library firstly and go through them for checking. Solution to better it would be, to save all the referenced nodes(by saving their referenced Library and referened node) in the current library, which again needs a reconstruction of the DGraph by packing it into a nicely capsulated ADT.

[ken]

the current version should be working now, although it's not so efficient. the next step(improvement) is related to ticket 269.

[ken]

the task remains undone, because a bug was found due to the changing above.

[ken]

As described above,the module

Static.DevGraph

is modified. A new map is inserted into the new datatype DGraph to store all the referenced nodes(lib name and node name), so that searching of a specific referenced node is much faster than before. This map(refNodes) can only be modified in two cases:
1. during process of static analysis, which builds the whole library, new referenced nodes are inserted into the map once they are inserted into current library.
2. during applying rule Global decomposition, which will expand some refereced nodes if they are involved by the rule, then the involved nodes will be deleted out of the map so that they can't be expanded again.

[ken]

A change is made in the module

Static.AnalysisLibrary

there could be a chain among nodes before which is like this:

a -> b -> c

it means c is a referenced node pointing to b, and b itself is also a referenced node pointing to a. This kind of chain makes analysis between libraries much harder and more inefficient than it should be. So the changing which refers to the function refNodeSig and its recursiv invokers advoids the construction of this kind of chains and therefor makes the previous example in the form of:

a -> b
a -> c

which means there would only be two levels for referenced nodes and no chain structure can appear at all.

[ken]

added a function createGThWith into module

Static.GTheory

to create a new G_theory with a given G_theory

[ken]

added a new map allRefNodes into DGraph in module

Static.DevGraph

which stores all the refnodes of current library, but this map uses (refnode's library, refnode's id) as key, which can speed up checking of existence of a refnode.
the function addToRefNodesDG is also modified to insert corresponding pairs into the new map while inserting into refNodes map.

[ken]

in module

Proofs.Global

changes are made to try to extend the current DGraph if the global decomposition is applied as described in the ticket.
the idea is like this:
1. take all the global unproven theorem links(gutl)
2. check all the src nodes of the gutl to see if they are refnodes.
3. if so, check if they are extended or not according to refNodes field in DGraph
4. if they are not extended then try to extend them by
4.1: getting all their incoming edges and the connected nodes in the referenced library.
4.2: see if the connected partner exists by checking allRefNodes in DGraph. if so, then we only need to insert the edges. otherwise we'll insert the partner into current library firstly then the edges.

[ken]

deleted the function checkHasExistedNode in Module

Static.AnalysisLibrary

because there is another direct and more efficient way to check the existency of a referenced node in the module

Static.DevGraph

after adding the referenced node map into DGraph

[maeder]

In Proofs.Global I've created new links as copies (without proofs) of the edges from other libraries in addParentLinks.

[maeder]

copying reference nodes is rather inefficient, since more reference nodes will be copied in every iteration. The given example works fast by a local inference if the global theory (instead of the empty local one) is taken from reference nodes. It remains the question if global decomposition should create a local theorem link from such reference nodes or if a global theorem link should be created plus a global inference rule.

[maeder]

I'm closing this since the time for #672 went down considerably. Yet copying so many reference nodes some how defeats the purpose of keeping development graphs for imported libraries.

Modularity is a problem since properties (i.e. transitivity of some comparison predicates over Nat) might flow from a top-level library into the basic Nat node and are then available in all other theories relying on Nat that are supposedly unrelated to the top-level library. Some proofs may no longer go through with such additional axioms. And, on the other hand, some proofs will only go through with such auxiliary axioms and fail if "unrelated" theories are removed.

[till]

Replying to maeder:

Some proofs may no longer go through with such additional axioms. And, on the other hand, some proofs will only go through with such auxiliary axioms and fail if "unrelated" theories are removed.

I do not understand what you mean by "additional axioms". The development graph calculus can only lead to additional theorems, not axioms.