blob: 9ac35b21750dac5274783d92e1ff4a5ae6b1f434 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
+++
title = "PTrue predicate under dominance"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g5e2"]
forwardlinks = ["3a8g5e4", "3a8g5e3a"]
zettelid = "3a8g5e3"
+++
The global predicate correct property is only true under dominance of
the header (even though in reality this seems to be an optimisation
actually). This means that not every predicate needs to be checked, but
only the predicates that are actually dominated by the header node.
Because of this optimisation, however, we actually need to preserve the
fact that if the successor is dominated by the original header, that the
current node is dominated too.
This is correct, because if the successor is strictly dominated by the
node, then all the previous nodes have to be dominated too, or one of
the previous nodes must be the dominator, and there must be a path from
that node to the other predecessors of the current node. Otherwise, not
all paths from the input to the current node would pass through the
dominator.
|
