Client-side Transitive Closure Computation
Original High-level Overviews
A fixed collection of logical implications will be provided to the algorithm in a specified, standardized format. The implications will be roughly of the following form, where P, Q, and R are predicates.
For all x1, x2, x3. P(x1,x2) and Q(x2,x3) => R(x1,x3)
A hypergraph is an abstract concept that can be used to represent how a collection of predicates applies to a collection of expressions. For example, suppose the predicate * is less than * applies to the expressions 1 and 2 (because 1 is less than 2 is a true expression). This can be represented using a graph in which 1 and 2 are nodes and * is less than * is a labelled edge. If we allow edges to have zero or more nodes (since the predicates they represent can have zero or more arguments), this becomes a hypergraph.
The algorithm should represent a collection of predicates and how they apply to a collection of expressions by maintaining a data structure similar to a hypergraph. It should be able to compute the transitive closure of any instance of a hypergraph with respect to the fixed collection of logical implications.
The focus of this project is a correct (logically consistent) but also efficient implementation of the hypergraph data structure and closure algorithm. Existing techniques from related literature on computing congruence closures can be consulted. It should be possible to integrate this algorithm with reasonably little effort with any tools produced by the first project ("Client-side Parsing and Verification") described above.
- insert a new labelled node (preferably in O(1) time)
- insert a new labelled hyperedge between zero or more nodes (preferably in O(log n) time or better)
- given an edge label and collection of node labels, determine whether a hyperedge with the specified label exists between the nodes with the specified labels.
It is possible to use a working closure operation algorithm as a validation algorithm for propositional logic. This is done by specifying a fixed list of formulas that correspond to propositional logic, converting an input formula into a hypergraph instance, running the closure operation to obtain a new hypergraph, and then checking whether in this hypergraph that formula is indicated to be true. You may assume the formula will have an implication operator at its root (i.e. be of the form "F implies F'").