proving a hasse diagrams to be complete

Stream: Equational

[Mario Carneiro]

I think the process is something like:

• Maintain a set S of missing laws and a frontier F of the hasse diagram (working bottom up)
• Initialize S to the set of all laws and F to the empty set
• On each step you may do one of following:
  • Remove an element a of S, prove it is equivalent to an element b of F and drop a
  • Remove an element a of S and add it to F
  • Take an element a of F, prove a -> b for some other b in F and c !-> a for all other c in F and drop a
• The process stops when S is empty and F is the singleton {Law1}

I claim that if this process can run to completion, then we have completeness

[Mario Carneiro]

the invariant is that for every law, either it is in S, or it is below an element of F (call B the set of elements strictly below some element of F), and for any two laws, if both are in B, or if one is in B and the other is in F, then we have determined their implication or nonimplication

[Joachim Breitner]

I must read the rules wrongly: I move all elements from S to F by rule 2, and then remove all but Law2 from it.

[Mario Carneiro]

yeah no I'm missing a step, I think you also need to prove c !-> a for all c in F when dropping a in rule 3

[Mario Carneiro]

but this is too conservative

[Mario Carneiro]

(typo, the top of the lattice is Law1 not Law2)

[Joachim Breitner]

Thinking graphically, it seems sufficient to proof an anti implication from a node to all maximal nodes in the graph of unreachable nodes. And it seems that we only need to look at nodes that are not “below-dominated” by another node. (Sorry, this is still vague)

[Mario Carneiro]

what is a maximal node in the graph of unreachable nodes?

[Joachim Breitner]

Mario Carneiro said:

what is a maximal node in the graph of unreachable nodes?

Sorry, on the phone here, so hard to type a lot.

The maximal elements of A \ { b | a known to imply b }. Because if we know that a does not imply these, it cannot imply anything else that we claim it doesn't imply.

[Mario Carneiro]

Agreed. The trouble is that we don't want to actually compute that set for every node

[Mario Carneiro]

nor figure out what its maximal elements are, at least explicitly

[Mario Carneiro]

The idea with the "frontier" is that we can sweep an antichain across the graph and determine these properties "on-line" as they pass by

[Joachim Breitner]

Is there a min-cut/max-flow argument we can make here, for a divide and conquer algorithm? :-D (ransom guess)

[Mario Carneiro]

For a small example, consider the diagram

  1
 / \
b   |
|   c
a   |
\  /
  0

The minimal implications we need here are all the edges of the graph, plus the non-edges a !-> c and c !-> b

[Joachim Breitner]

And b! -> a. Or are these implied?

[Mario Carneiro]

for each edge of the graph we have to explicitly prove implication and reverse non-implication

[Joachim Breitner]

Sounds like if we find a horizontal cut in the graph, prove the nodes on this cut to be mutual non-implied, then we can continue with the two halfs separately?

[Mario Carneiro]

right, that's the role of the frontier F

[Mario Carneiro]

For the invariant there are a few options for whether we should know implication and non-implication between two elements of F, between an element of B and an element of F, or between an element of F and an element of B

[Mario Carneiro]

depending on which of those you pick you get different algorithms which have to assert things as they enter F or when they leave F

[Joachim Breitner]

Ok, but maybe instead of sweeping, it makes sense to think of it as dividing and conquering? Recursively finding the smallest cut, and looking at both halfs? Maybe that's more efficient, or yields an inductive description of the graph that's easy to check?

[Mario Carneiro]

I don't think it can be divided and conquered left-to-right, only top and bottom, so it ends up as a sweep in the end

[Mario Carneiro]

you can break that proof into a tree shape of course

[Mario Carneiro]

you just snapshot the state in the middle of the algorithm and use that for your divide and conquer

[Joachim Breitner]

Not sure. If I have two unconnected graphs, then I can horizontally compose then after checking that rhe top elements of one graph don't imply the bottom elements of rhe other graph, and vice versa

[Mario Carneiro]

hm, you might be on to something. But I think it gets a lot more complicated to figure out what elements to compare with what other elements if the two subgraphs are not unconnected

[Mario Carneiro]

e.g. try doing this for the cube lattice

[Joachim Breitner]

Then you maybe have to cut horizontally, ideally at a min-cut, until it's falls apart some more?

[Joachim Breitner]

Maybe that ends up doing the sweep :-)

[Mario Carneiro]

in particular there are no quadratic steps in the sweep algorithm, so it's clear how you can control things by keeping the frontier small

[Mario Carneiro]

when you cut vertically you might have a quadratic number of things to check and so it's not clear you have really conquered with your dividing

[Mario Carneiro]

(of course they are both worst case quadratic since in the totally disconnected graph there are no shortcuts)

[Mario Carneiro]

I think the trouble with the frontier algorithm is that it is optimized for the case where the frontier is an antichain and it's not clear how to make use of implications inside the frontier. I think what you need instead is something like a high H and low L set for the frontier, where L contains the elements of F not above another element of F, and H contains the elements of F not below an element of F. Then, when removing an element from F it suffices to check that it is not above every element of L and not below every element of H. I'll have to think about how to make the steps in this refined algorithm more precise

[Mario Carneiro]

(For example, in the 5 point lattice above, if F is {a, b, c} then L is {a, c} and H is {b, c})

[Joachim Breitner]

That sounds good

[Notification Bot]

36 messages were moved here from #Equational > A final end-to-end theorem in Lean by Joachim Breitner.

[Mario Carneiro]

it's not yet clear to me whether elements sandwiched between H and L, e.g. if I added a -> a' -> b in the 5 point diagram, are done and dusted or whether we need to keep track of them for a while longer

[Joachim Breitner]

How about this algorithm:
Let H be a Hasse diagram with more than one element. Let U and L be the maximal resp. minimal elements of H. Prove a /-> b for a ∈ U and b ∈ L, a ≠ b. (It seems that these anti-implications are unavoidable to check, because there is no other anti-implication that we can check to prove them.). Now split the graph into its connected components, and then remove U and L from the graph, and repeat. (It seems important to split into connected components before removing the max and min elements.)

In your example above it would prove 1 /→ 0 in the first step, and then b /-> c b /-> a c /→ a in the second step, seems legit, but maybe not optimal yet? Also I’m not sure if removing both U and L at the same time is ok? But it’s getting late and brain doesn’t work well anymore.

[Joachim Breitner]

Hmm, probably bogus. It may be true that there anti implications are necessary to check, but not that we can then remove these maximum/minimum nodes.

[Mario Carneiro]

Proving 1 !-> 0 means it's not optimal

[Mario Carneiro]

because that is definitely not in the transitive reduction

[Joachim Breitner]

Depends on whether we assume the implications to be strict to begin with. But if we don't then the algorithm misses anti-implications it has to check. So nevermind.

But the following is at least true, isn't it:
If H is not connected, then proving anti-implications from every minimal element to every maximal element in a different component suffices and is necessary to then consider each component separately.

[Joachim Breitner]

Because adding any implication between the components would contradict one of these anti-implications, and none of them entail any other?

[Joachim Breitner]

Ah, related to this: If a is minimal and b is maximal in H without a path from a to b, then the anti-implications a /-> b cannot be inferred by anything else, so it has to be proven.

And proving it for all such bs entails all anti-implications from a, so we can drop a from the graph. But that's somehow throwing away information, because we actually proved all anti-implications between nodes above a to nodes below b. Does that mean we can then separate the subgraph above a and recourse on the two parts? Not quite, for that we need to show anti-implications to all elements that are maximal in H without the cone above a. And with that I ran into a circle of ideas.

Although, if indeed

• the anti-implications from a minimal element to the maximal elements of H without the cone above are necessary (and it seems like they are), and
• if checking them allows me to cut away that cone and recurse (removing a in this step),

then this would give an optional greedy algorithm, wouldn't it?

Ah, but I can't quite cut yet. I know I don't need to look at any more edges from the cone to the outside of it, but I still need to check some edges from other remainder into the cone as well. Hmm. The first assumption may still hold and tell us a bunch of non-implications that we must check. Unclear only how to then proceed.

[Mario Carneiro]

Joachim Breitner said:

Depends on whether we assume the implications to be strict to begin with. But if we don't then the algorithm misses anti-implications it has to check. So nevermind.

Just to be a bit more formal here, the criteria I am looking for in this (nondeterministic) algorithm is that if I have a Hasse diagram and give it a transitively reduced set of base facts whose transitive closure is complete, then there exists some accepting path which only requires the given base facts.

[Mario Carneiro]

Joachim Breitner said:

If H is not connected, then proving anti-implications from every minimal element to every maximal element in a different component suffices and is necessary to then consider each component separately.

Yes, this is true, but it doesn't look like a general case to me. Maybe you have another trick?

[Mario Carneiro]

I think it is better to think one element at a time instead of trying to cut the graph into sub-pieces, I don't think that's going to work because you don't know which base edges you need to check except in specific situations. The whole proof should still end up O(e log n) large and O(log n) deep if this is done right

[Joachim Breitner]

No, it's not a general case, but it's always a useful move if H is not connected, in the sense that it's correct and not wasteful to look at each component separately.

Another valid move is to remove unique top and unique bottom elements.

Our graph with top and bottom removed, does that maybe fall into many small components?

So maybe it helps to think about diagrams that are connected and have at multiple minimal and multiple maximal elements. For these I think can identify anti-implications that I have to check, but I don't see yet how to then continue.

Anyways, bedtime

[Mario Carneiro]

again, consider the cube graph, after you take off the top and bottom you end up with something that has a bunch of edges and no disconnection

[Joachim Breitner]

Right, I'm not saying that this is a complete procedure. So far merely that taking off tops and bottoms and splitting into components, when possible, is never bad (as in wrong, or leading to checking more anti-implications than necessary).

[Joachim Breitner]

The minimals-to-maximals-in-cocone rule in the capped cube says we have to check from lower corners to their opposite upper corner, so that's at least looks correct.

[Hugo Angulo]

taxi cab numbers, how do you figure?

[Mario Carneiro]

Here's an example sweep through the cube graph, together with the minimal base facts and approximately when they need to be asserted:

      7
    / | \
  3   5   6
  | X   X |
  1   2   4
    \ | /
      0

U = {0},        L = {0}
U = {1},        L = {0},        1 > 0
U = {1, 2},     L = {0},        2 > 0
U = {1, 2, 4},  L = {0},        4 > 0
U = {1, 2, 4},  L = {1, 2, 4}
U = {3, 4},     L = {1, 2, 4},  3 > 1, 3 > 2
U = {3, 5},     L = {1, 2, 4},  5 > 1, 5 > 4
U = {3, 5, 6},  L = {1, 2, 4},  6 > 2, 6 > 4
U = {3, 5, 6},  L = {2, 4},     1 !> 6
U = {3, 5, 6},  L = {2, 5},     4 !> 3
U = {3, 5, 6},  L = {3, 5, 6},  2 !> 5
U = {7},        L = {3, 5, 6},  7 > 3, 7 > 5, 7 > 6
U = {7},        L = {7}

[Mario Carneiro]

This isn't exactly an algorithm because I haven't said what the legal moves are, but the invariants it wants to preserve are:

1. Every path from 0 to 7 intersects U ∪ L somewhere
2. the downward closure of U ∪ L is monotonically increasing
3. U and L are antichains (although as you can tell from when facts are asserted, the algorithm doesn't prove this)
4. Every element of U is above some element of L and every element of L is below some element of U
5. Every condition between elements strictly below U ∪ L has been checked

There is an additional invariant I don't quite understand: at one point I tried to have U = {3, 5} and L = {2, 4}, but this is an invalid state because we will miss the chance to assert 1 !> 6 non-implication if we pass through this state. I think we also need paths from 0 to 7 that include non-implication base facts to intersect U ∪ L

[Mario Carneiro]

Here's a variation where facts are asserted only when they leave the lower set, meaning that invariant 4 is also true but with deferred proof:

U = {0},        L = {0}
U = {1},        L = {0}
U = {1, 2},     L = {0}
U = {1, 2, 4},  L = {0}
U = {1, 2, 4},  L = {1, 2, 4},  1 > 0, 2 > 0, 4 > 0
U = {3, 4},     L = {1, 2, 4}
U = {3, 5},     L = {1, 2, 4}
U = {3, 5, 6},  L = {1, 2, 4}
U = {3, 5, 6},  L = {2, 4},     3 > 1, 5 > 1, 1 !> 6
U = {3, 5, 6},  L = {2, 5},     4 !> 3, 5 > 4, 6 > 4
U = {3, 5, 6},  L = {3, 5, 6},  3 > 2, 2 !> 5, 6 > 2
U = {7},        L = {3, 5, 6}
U = {7},        L = {7},        7 > 3, 7 > 5, 7 > 6

This looks a bit more implementable, since now you can see the checks like 3 > 1, 5 > 1, 1 !> 6 as being an iteration over U