Improve ProofNodeCollection

[ceilican]

1) right now all ProofNodeCollections have a children relation. But it would make sense to have a more basic type of ProofNodeCollection without a children relation too.

2) ProofNodeCollection should do a few more things (e.g. implement canBuildFrom) in order to be usable as any other usual Scala collection.

3) There should be specialized subtypes of ProofNodeCollection that do parallel foldDown, for example.

4) ProofNodeCollection could provide methods to get its roots or leaves, to add and remove nodes, to compose itself with other ProofNodeCollections,...

[ceilican]

Joseph's comments:

Technically this makes sense too, I think. Many times writing code I feel uncomfortable because I used sometimes "proof", sometimes "node" for the same object. I really think the code will be much more clear with this distinction.

You are right. We should make an effort to establish a consistent terminology.

There is another property of a proof. It's closed with respect to the premise relation : every premise of a node in a proof belongs to the proof too.

The real issue is that ProofNodeCollection is still far from perfect. There are many things that could be improved:

1) right now all ProofNodeCollections have a children relation. But, as you observed, it would make sense to have a more basic type of ProofNodeCollection without a children relation too.

This question is quite difficult, I think. There is two different conceptual views for a ProofNodeCollection. Firstly it could be a set of proof nodes with a partial order corresponding to the premise relation (and have the children property). Secondly it could be a set of proof nodes with a total order extending the previous partial order. In this second case, I don't know if the children relation should be added.

[Jogo27]

One more argument on the fact that ProofNodeCollection actually IS the class for proofs (not for arbitrary collection of nodes). The foldDown method has no meaning for arbitrary nodes collection : the returned value is arbitrary if there is more than one root. Moreover, the usual use of this function is :

def visit(node: P, calculatedPremises: List[Something]) =
  match node {
    case Axiom(_) => f1(node)
    case CutIC(_,_,_,_) => f2(node, calculatedPremises)
  }

It is assumed that if a node is in the collection, all its premises are.

[ceilican]

Backward Subsumption needs a fast way to find ancestor nodes of a node satisfying a given predicate:

One reason why BWS is still slower than desirable is that "bottomUp" will traverse the whole subproof trying to find the ancestor, and will continue traversing even after it has found the ancestor. Fixing this in an elegant way will require some refactoring of the Proof class.

We need a more lightweight Proof class that does not do topological sorting on construction.

[Jogo27]

I think we already have such a lightweight Proof class : ProofNode. An existsAmongAncestor method could be easily added to this (abstract) class.

[ceilican]

That is indeed an easy solution w.r.t. coding effort. (Andreas or Joseph: feel free to implement this solution, if you need an efficient way to find ancestors right now).

But, conceptually, I think this solution is not ideal. I like to think of "ProofNode" as a single node in the proof, and "Proof" as collection of nodes. All methods related to traversing a collection should be implemented in "Proof" in order to keep this conceptual separation clear.

[Jogo27]

The conceptual difference between a Proof and a ProofNode has always been difficult. One reason is that there is nothing like a node in the code. A node would be a conclusion and a pivot alone, without premises (which are the edges of the proof). Therefore ProofNode are in fact subproofs. And conceptually a subproof is a proof...

I think the difference between those classes is both in their purpose and weight. Proof is an heavy class meant to represent a complete proof to work on. ProofNode is a lightweight class meant to represent the subproofs of a main proof.

Adding a third class for proofs won't simplify anything. I think it will make the architecture even more confusing (and slow).

[ceilican]

The Proof class could be more flexible with respect to the order in which nodes are traversed. For example, right now, "foldDown" traverses the proof in a top-down left-to-right way. Being able to traverse the proof in a top-down right-to-left seems to be useful for subsumption algorithms. There might be other algorithms that could benefit from different traversal orders.