paniq · July 28, 2024 12:59 · Jul 28, 2024 · Jul 25, 2024 · Jul 25, 2024 · Jul 24, 2024
diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -86,6 +86,10 @@ Negated Events
 
 (Subject to ongoing research)
 
+We might also interpret the graph as functional flow, i.e. we start from the goals and work backwards to the facts. This isn't compatible with the event interpretation, since each function can then produce multiple results (as a generator), but it gives us a better understanding of what a negated event is. In the functional interpretation, a function either produces one or more results (indicating the function succeeded), or none, in which case it failed, implying the event failed. This requires stratification since the event conditions must be evaluated before we know if it succeeded.
+
+In effect, an event can succeed (when any of its rules apply) or fail (when none of its rules apply), and we can define default flow.
+
 Merge Events
 ------------
 

diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -60,6 +60,27 @@ It appears i need to go this route:
 
 Ideally it would be nice if we had a form that could do it all.
 
+
+
+
+DRIL hypergraph is like a CFF with multiple conditional calls per node, in sequence, since conditions can be conjunctions.
+we prefer acyclical (returning) calls to be executed before the cyclical (interminable) ones.
+and among cyclical calls, we prefer cycles that reenter further back before cycles that reenter closely.
+arguably, each call could also be a thread invocation, which would at least be fair as to how they are scheduled (because they aren't).
+
+DRIL data dependencies are mapped by closures sourcing values that aren't on their control path - which can be fixed by creating a control path.
+but we also have order-dependency constraints, where we just depend on a control path having been executed.
+
+```
+node(args...) -> cont:
+    after <node>
+    <op> <arg> | <other_node.arg> ...
+    set
+        [<boolean_condition>] node args... -> cont
+        ...
+
+```
+
 Negated Events
 --------------
 

diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -43,6 +43,23 @@ The resulting callgraph must still be converted to a CFG. The primary transforma
 2. Likewise, rules are merged non-exclusive, meaning all incoming edges of an event `E` exist in an `OR` relationship and must be serialized in arbitrary order, with `E` as the final event. Where we can prove incoming edges to be exclusive, a phi-node optimization can be performed.
 3. Because sources are not required to dominate the reduced rules, we can not guarantee at compile time that all source events of a rule will always have happened; we can only verify that a goal is connected to all sources. An additional transformation of the callgraph is required, in which non-dominating sources are structured to optional arguments on the dominant path, and then tested and destructured where the rule conditions are checked. Once destructured, subsequent events with the same dependence can reuse the work. This mechanism saves the user from having to implement sum type encodings to circumvent dominance issues.
 
+Lowering Path
+-------------
+
+(Subject to ongoing research)
+
+It appears i need to go this route:
+
+* Reduce data dependency hypergraph to get control graph:
+    * Collapse all determinable B-arcs by connecting directly to a suitable linear control graph path, which leads through all sources and doesn't have any cycles. This path always ends on the closest source, which is where we connect.
+    * TODO: Ambiguous cases exist where multiple B-arc edges lie on suitable paths. We need to find a heuristic to make a good choice.
+    * TODO: Undecidable cases exist where no B-arc edge lies on a suitable path. However, once the branching events have been sequencing their calls, such a path _does_ exist. Therefore, we need to sequence branches ASAP.
+* Using the data dependency hypergraph and the control graph, apply lambda lifting to all sources on non-dominant paths, because they would violate lexical scope. Each dependency on a non-dominant path is optional. Hence such events are translated to optional arguments for subsequent events.
+* Lower both graphs to Control Flow Form, where each event constitutes a continuation closure. Branching events produce sequences of conditional returning calls (of which acyclical paths should be favored before cyclical ones). Merging events represent closure entry points. 
+* Lower Control Flow Form to SSA?
+
+Ideally it would be nice if we had a form that could do it all.
+
 Negated Events
 --------------
 

diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -43,6 +43,11 @@ The resulting callgraph must still be converted to a CFG. The primary transforma
 2. Likewise, rules are merged non-exclusive, meaning all incoming edges of an event `E` exist in an `OR` relationship and must be serialized in arbitrary order, with `E` as the final event. Where we can prove incoming edges to be exclusive, a phi-node optimization can be performed.
 3. Because sources are not required to dominate the reduced rules, we can not guarantee at compile time that all source events of a rule will always have happened; we can only verify that a goal is connected to all sources. An additional transformation of the callgraph is required, in which non-dominating sources are structured to optional arguments on the dominant path, and then tested and destructured where the rule conditions are checked. Once destructured, subsequent events with the same dependence can reuse the work. This mechanism saves the user from having to implement sum type encodings to circumvent dominance issues.
 
+Negated Events
+--------------
+
+(Subject to ongoing research)
+
 Merge Events
 ------------
 

diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -50,9 +50,9 @@ Merge Events
 
 The semantics of merging events (continuations with multiple in-edges, which have a non-exclusive OR relationship) need to be defined. Merging events must be sync points, analog to how branching events are (non-exclusive) forks of execution flow.
 
-Let's model rules for an interpreter to gain more clarity on this question.
+Let's model rules for an interpreter to gain more clarity on this question. The interpreter works in iterations. Each iteration, the state of an event changes when at least one of its input states has changed. We model changed events as bits that are zero at the beginning of an iteration, and are turned on as events are updated, based on the set bits of the previous iteration.
 
-To begin with, it seems necessary to require that merge events only evaluate their rules once all linear events reach a fixed state. But merge event data is still ambiguous.
+To begin with, it seems necessary to require that merge events are only activated once all linear events reach a fixed state. But merge event data is still ambiguous.
 
 One prerequisite of our events is that each event is linear, i.e. has a single optional state: `Some` definitive value or `None`.
 
@@ -64,7 +64,7 @@ Our 4 options are:
 
 2) The event doesn't happen when there is more than one possible value (XOR behavior). 
 
-3) A fold operator `f` decides how the values are to be combined. The controller logic is described by the following Scopes pseudocode:
+3) An aggregate function `f` decides how the values are to be combined. The controller logic is described by the following Scopes pseudocode:
     ```
     fold (x = empty) for y in source-events
         if (empty? x) y
@@ -78,8 +78,12 @@ To evaluate:
 
 (1) is surprising to the user. Even when deterministic, its behavior is difficult to predict and subject to subtle behavioral change when the program is altered.
 
-(2) might be surprising to the user since it alters datalog semantics. The `:-` operator is expected to describe a non-exclusive implication. We would need to use a different operator such as `-:-`, standing for `iff` (if and only if). It requires the user to define a separate rule for every possible conjunctive case. Where an event should merge a set of 16 different events, 65535 rules would have to be defined to cover every case. The complexity can be reduced by chaining 15 events of which each defines three rules (`a ^ b ^ ab`), but that would still require the definition of 45 rules!
+(2) might be surprising to the user since it alters datalog semantics. The `:-` operator is expected to describe a non-exclusive implication. We would need to use a different operator such as `-:-`, standing for `iff` (if and only if). It requires the user to define a separate rule for every possible conjunctive case. Where an event should merge a set of 16 different events, 65535 rules would have to be defined to cover every case. The complexity can be reduced by chaining 15 events of which each defines three rules `a ^ b ^ ab`, but that would still require the definition of 45 rules!
+
+(3) could be quite powerful, and forms an implicit implementation of (2), but adds complexity to the system. This is only permissible when there is no other way. 
+
+(4) is predictable and stable under program changes, but limits expressiveness. Due to relaxed dominance, subsequent rules may still depend on both the merge event and one of the events that it merged, but this way, branching values remain irreconcilable. There simply is no way to merge data from two different events into a single one. We can not even build flow that combines booleans from two events.
+
+Let's explore what an implementation of (3) could look like. We could type the merge event as a prefabricated aggregate class (`min`, `max`, `count`, `sum`).
 
-(3) could be quite powerful, but adds complexity to the system. This is only permissible when there is no other way. 
 
-(4) is predictable and stable under program changes, but limits expressiveness. Due to relaxed dominance, subsequent rules may still depend on both the merge event and one of the events that it merged, but this way, branching values remain irreconcilable. There simply is no way to merge data from two different events into a single one. We can not even build flow that combines two booleans.
diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -67,7 +67,6 @@ Our 4 options are:
 3) A fold operator `f` decides how the values are to be combined. The controller logic is described by the following Scopes pseudocode:
     ```
     fold (x = empty) for y in source-events
-        # x ^ y ^ (f x y) == 1
         if (empty? x) y
         elseif (empty? y) x
         else (f x y)

diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -68,8 +68,8 @@ Our 4 options are:
     ```
     fold (x = empty) for y in source-events
         # x ^ y ^ (f x y) == 1
-        if (empty? y) x
-        elseif (empty? x) y
+        if (empty? x) y
+        elseif (empty? y) x
         else (f x y)
     ```
 

diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -67,6 +67,7 @@ Our 4 options are:
 3) A fold operator `f` decides how the values are to be combined. The controller logic is described by the following Scopes pseudocode:
     ```
     fold (x = empty) for y in source-events
+        # x ^ y ^ (f x y) == 1
         if (empty? y) x
         elseif (empty? x) y
         else (f x y)

diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -67,10 +67,9 @@ Our 4 options are:
 3) A fold operator `f` decides how the values are to be combined. The controller logic is described by the following Scopes pseudocode:
     ```
     fold (x = empty) for y in source-events
-        if (not empty? x)
-            if (empty? x) y
-            else (f x y)
-        else x
+        if (empty? y) x
+        elseif (empty? x) y
+        else (f x y)
     ```
 
 4) The event must not take any arguments (void fold operator).

diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -64,7 +64,14 @@ Our 4 options are:
 
 2) The event doesn't happen when there is more than one possible value (XOR behavior). 
 
-3) A fold operator decides how the values are to be combined.
+3) A fold operator `f` decides how the values are to be combined. The controller logic is described by the following Scopes pseudocode:
+    ```
+    fold (x = empty) for y in source-events
+        if (not empty? x)
+            if (empty? x) y
+            else (f x y)
+        else x
+    ```
 
 4) The event must not take any arguments (void fold operator).
 
@@ -74,6 +81,6 @@ To evaluate:
 
 (2) might be surprising to the user since it alters datalog semantics. The `:-` operator is expected to describe a non-exclusive implication. We would need to use a different operator such as `-:-`, standing for `iff` (if and only if). It requires the user to define a separate rule for every possible conjunctive case. Where an event should merge a set of 16 different events, 65535 rules would have to be defined to cover every case. The complexity can be reduced by chaining 15 events of which each defines three rules (`a ^ b ^ ab`), but that would still require the definition of 45 rules!
 
-(3) could be quite powerful, but adds complexity to the system. This is only permissible when there is no other way.
+(3) could be quite powerful, but adds complexity to the system. This is only permissible when there is no other way. 
 
 (4) is predictable and stable under program changes, but limits expressiveness. Due to relaxed dominance, subsequent rules may still depend on both the merge event and one of the events that it merged, but this way, branching values remain irreconcilable. There simply is no way to merge data from two different events into a single one. We can not even build flow that combines two booleans.
diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -72,7 +72,7 @@ To evaluate:
 
 (1) is surprising to the user. Even when deterministic, its behavior is difficult to predict and subject to subtle behavioral change when the program is altered.
 
-(2) might be surprising to the user since it alters datalog semantics. The `:-` operator is expected to describe a non-exclusive implication. We would need to use a different operator such as `-:-`, standing for `iff` (if and only if). It requires the user to define a separate rule for every possible conjunctive case. Where an event should merge a set of 16 different events, 65535 rules would have to be defined to cover every case!
+(2) might be surprising to the user since it alters datalog semantics. The `:-` operator is expected to describe a non-exclusive implication. We would need to use a different operator such as `-:-`, standing for `iff` (if and only if). It requires the user to define a separate rule for every possible conjunctive case. Where an event should merge a set of 16 different events, 65535 rules would have to be defined to cover every case. The complexity can be reduced by chaining 15 events of which each defines three rules (`a ^ b ^ ab`), but that would still require the definition of 45 rules!
 
 (3) could be quite powerful, but adds complexity to the system. This is only permissible when there is no other way.
 

diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -70,7 +70,9 @@ Our 4 options are:
 
 To evaluate:
 
-(1) and (2) are surprising to the user. Even when deterministic, they are both difficult to predict and subject to subtle behavioral change when the program is altered.
+(1) is surprising to the user. Even when deterministic, its behavior is difficult to predict and subject to subtle behavioral change when the program is altered.
+
+(2) might be surprising to the user since it alters datalog semantics. The `:-` operator is expected to describe a non-exclusive implication. We would need to use a different operator such as `-:-`, standing for `iff` (if and only if). It requires the user to define a separate rule for every possible conjunctive case. Where an event should merge a set of 16 different events, 65535 rules would have to be defined to cover every case!
 
 (3) could be quite powerful, but adds complexity to the system. This is only permissible when there is no other way.
 

diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -46,32 +46,32 @@ The resulting callgraph must still be converted to a CFG. The primary transforma
 Merge Events
 ------------
 
-(subject to ongoing research)
+(Subject to ongoing research)
 
-i really need to figure out what the semantics of merge-events (continuations with multiple in-edges, which have a non-exclusive OR relationship) are, first. these must be sync points, analog to how branch-events are (non-exclusive) forks.
+The semantics of merging events (continuations with multiple in-edges, which have a non-exclusive OR relationship) need to be defined. Merging events must be sync points, analog to how branching events are (non-exclusive) forks of execution flow.
 
-i am trying to model an interpreter to gain more clarity on this question. 
+Let's model rules for an interpreter to gain more clarity on this question.
 
-for starters, it seems necessary to require that merge events only evaluate their rules once all linear events reach a fixed state.
+To begin with, it seems necessary to require that merge events only evaluate their rules once all linear events reach a fixed state. But merge event data is still ambiguous.
 
-but merge event data is still ambiguous.
+One prerequisite of our events is that each event is linear, i.e. has a single optional state: `Some` definitive value or `None`.
 
-one prerequisite of our events is that each event is linear, i.e. has a single optional state: Some definitive value or None.
+But multiple rules may apply different values to the same merge event, meaning we need to merge those values somehow.
 
-but multiple rules may apply different values to the same merge event, meaning we need to merge those values somehow.
+Our 4 options are:
 
-our 4 options:
+1) We arbitrarily choose a value.
 
-1) we choose a value. 
+2) The event doesn't happen when there is more than one possible value (XOR behavior). 
 
-2) the event doesn't happen when there is more than one possible value (XOR behavior). 
+3) A fold operator decides how the values are to be combined.
 
-3) a fold operator decides how the values are to be combined.
+4) The event must not take any arguments (void fold operator).
 
-4) the event must not take any arguments (void fold operator).
+To evaluate:
 
-(1) and (2) are surprising to the user. they are both difficult to predict and subject to subtle behavioral change when the program is altered.
+(1) and (2) are surprising to the user. Even when deterministic, they are both difficult to predict and subject to subtle behavioral change when the program is altered.
 
-(3) could be quite powerful, but adds complexity to the system. this is only permissible when there is no other way.
+(3) could be quite powerful, but adds complexity to the system. This is only permissible when there is no other way.
 
-(4) is predictable and stable under program changes, but limits expressiveness.
+(4) is predictable and stable under program changes, but limits expressiveness. Due to relaxed dominance, subsequent rules may still depend on both the merge event and one of the events that it merged, but this way, branching values remain irreconcilable. There simply is no way to merge data from two different events into a single one. We can not even build flow that combines two booleans.
diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -42,3 +42,36 @@ The resulting callgraph must still be converted to a CFG. The primary transforma
 1. Branching rules may have non-exclusive conditions, implying that all outgoing edges of an event must be called in arbitrary order. Where we can prove outgoing edges to be exclusive, an if/switch optimization can be performed.
 2. Likewise, rules are merged non-exclusive, meaning all incoming edges of an event `E` exist in an `OR` relationship and must be serialized in arbitrary order, with `E` as the final event. Where we can prove incoming edges to be exclusive, a phi-node optimization can be performed.
 3. Because sources are not required to dominate the reduced rules, we can not guarantee at compile time that all source events of a rule will always have happened; we can only verify that a goal is connected to all sources. An additional transformation of the callgraph is required, in which non-dominating sources are structured to optional arguments on the dominant path, and then tested and destructured where the rule conditions are checked. Once destructured, subsequent events with the same dependence can reuse the work. This mechanism saves the user from having to implement sum type encodings to circumvent dominance issues.
+
+Merge Events
+------------
+
+(subject to ongoing research)
+
+i really need to figure out what the semantics of merge-events (continuations with multiple in-edges, which have a non-exclusive OR relationship) are, first. these must be sync points, analog to how branch-events are (non-exclusive) forks.
+
+i am trying to model an interpreter to gain more clarity on this question. 
+
+for starters, it seems necessary to require that merge events only evaluate their rules once all linear events reach a fixed state.
+
+but merge event data is still ambiguous.
+
+one prerequisite of our events is that each event is linear, i.e. has a single optional state: Some definitive value or None.
+
+but multiple rules may apply different values to the same merge event, meaning we need to merge those values somehow.
+
+our 4 options:
+
+1) we choose a value. 
+
+2) the event doesn't happen when there is more than one possible value (XOR behavior). 
+
+3) a fold operator decides how the values are to be combined.
+
+4) the event must not take any arguments (void fold operator).
+
+(1) and (2) are surprising to the user. they are both difficult to predict and subject to subtle behavioral change when the program is altered.
+
+(3) could be quite powerful, but adds complexity to the system. this is only permissible when there is no other way.
+
+(4) is predictable and stable under program changes, but limits expressiveness.
diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -41,4 +41,4 @@ The resulting callgraph must still be converted to a CFG. The primary transforma
 
 1. Branching rules may have non-exclusive conditions, implying that all outgoing edges of an event must be called in arbitrary order. Where we can prove outgoing edges to be exclusive, an if/switch optimization can be performed.
 2. Likewise, rules are merged non-exclusive, meaning all incoming edges of an event `E` exist in an `OR` relationship and must be serialized in arbitrary order, with `E` as the final event. Where we can prove incoming edges to be exclusive, a phi-node optimization can be performed.
-3. Because sources are not required to dominate the reduced rules, we can not guarantee at compile time that all source events of a rule will always have happened; we can only verify that a goal is connected to all sources. An additional transformation of the callgraph is required, in which non-dominating sources are serialized to optional arguments on the dominant path, and then tested and dispatched where the rule conditions are checked. This mechanism saves the user from having to implement sum type encodings to circumvent dominance issues.
+3. Because sources are not required to dominate the reduced rules, we can not guarantee at compile time that all source events of a rule will always have happened; we can only verify that a goal is connected to all sources. An additional transformation of the callgraph is required, in which non-dominating sources are structured to optional arguments on the dominant path, and then tested and destructured where the rule conditions are checked. Once destructured, subsequent events with the same dependence can reuse the work. This mechanism saves the user from having to implement sum type encodings to circumvent dominance issues.
diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -37,4 +37,8 @@ If a rule reduction leads to more than one possible callgraph edge, there exists
 
 If one or more rules remain undecidable after the fixpoint, the user should be warned as the rules would never be applied.
 
-Because sources are not required to dominate the reduced rules, we can not guarantee at compile time that all source events of a rule will always have happened; we can only verify that a goal is connected to all sources. An additional transformation of the callgraph is required, in which non-dominating sources are serialized to optional arguments on the dominant path, and then tested and dispatched where the rule conditions are checked. This mechanism saves the user from having to implement sum type encodings to circumvent dominance issues.
+The resulting callgraph must still be converted to a CFG. The primary transformation required here is to bring all calls in topological order. Noteworthy are these caveats:
+
+1. Branching rules may have non-exclusive conditions, implying that all outgoing edges of an event must be called in arbitrary order. Where we can prove outgoing edges to be exclusive, an if/switch optimization can be performed.
+2. Likewise, rules are merged non-exclusive, meaning all incoming edges of an event `E` exist in an `OR` relationship and must be serialized in arbitrary order, with `E` as the final event. Where we can prove incoming edges to be exclusive, a phi-node optimization can be performed.
+3. Because sources are not required to dominate the reduced rules, we can not guarantee at compile time that all source events of a rule will always have happened; we can only verify that a goal is connected to all sources. An additional transformation of the callgraph is required, in which non-dominating sources are serialized to optional arguments on the dominant path, and then tested and dispatched where the rule conditions are checked. This mechanism saves the user from having to implement sum type encodings to circumvent dominance issues.
diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -1,5 +1,7 @@
 Relation-Rule Based Callgraph Inference
 =======================================
+2024/07/23
+Leonard Ritter, Duangle GbR
 
 A relational event graph is described with unpredicated rules relating events, connecting a product of `n` sources and `m` conditions to a single sink (also called the goal). The format is as follows:
 ```

diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -11,7 +11,7 @@ The resulting graph is a directed hypergraph of the [B-graph](https://en.wikiped
 
 The task is now to manifest the relational event graph as a callgraph (as precursor of a [control flow graph](https://en.wikipedia.org/wiki/Control-flow_graph)) that satisfies all rules. 
 
-We recognize the callgraph as a transitive reduction of the hypergraph, which means all source edges of a rule are reducible to one (and only one) edge that, in the strict interpretation, is dominated by all sources reachable through existing callgraph edges.
+We recognize the callgraph as a transitive reduction of the hypergraph, which means all source edges of a rule are reducible to one (and only one) edge that connects to a callgraph path through all sources of the rule.
 
 Because the callgraph is initially incomplete, we must start from trivially reducible rules with single sources. This adds more edges to the callgraph, which allows us to reduce more complex rules, until a fixpoint is reached because no more rules can be reduced. See this example (conditions omitted for clarity):
 
@@ -20,20 +20,19 @@ Because the callgraph is initially incomplete, we must start from trivially redu
 (2) B :- A.
 (3) B :- A, B, C.
 (4) C :- A, B.
-(5) D :- A, B.
+(5) D :- A, B, C.
 // iteration 1: trivially reducible rules
 (1) A.
 (2) B :- A.
 // iteration 2
 (4) C :- B. // :- A
-(5) D :- B. // :- A
 // iteration 3
 (3) B :- C. // :- B :- A
+(5) D :- C. // :- B :- A
 ```
 
 If a rule reduction leads to more than one possible callgraph edge, there exists an ambiguity in the program that the user must resolve by adding more edges.
 
 If one or more rules remain undecidable after the fixpoint, the user should be warned as the rules would never be applied.
 
-
-
+Because sources are not required to dominate the reduced rules, we can not guarantee at compile time that all source events of a rule will always have happened; we can only verify that a goal is connected to all sources. An additional transformation of the callgraph is required, in which non-dominating sources are serialized to optional arguments on the dominant path, and then tested and dispatched where the rule conditions are checked. This mechanism saves the user from having to implement sum type encodings to circumvent dominance issues.
diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -13,7 +13,23 @@ The task is now to manifest the relational event graph as a callgraph (as precur
 
 We recognize the callgraph as a transitive reduction of the hypergraph, which means all source edges of a rule are reducible to one (and only one) edge that, in the strict interpretation, is dominated by all sources reachable through existing callgraph edges.
 
-Because the callgraph is initially incomplete, we must start from trivially reducible rules with single sources. This adds more edges to the callgraph, which allows us to reduce more complex rules, until a fixpoint is reached because no more rules can be reduced.
+Because the callgraph is initially incomplete, we must start from trivially reducible rules with single sources. This adds more edges to the callgraph, which allows us to reduce more complex rules, until a fixpoint is reached because no more rules can be reduced. See this example (conditions omitted for clarity):
+
+```
+(1) A.
+(2) B :- A.
+(3) B :- A, B, C.
+(4) C :- A, B.
+(5) D :- A, B.
+// iteration 1: trivially reducible rules
+(1) A.
+(2) B :- A.
+// iteration 2
+(4) C :- B. // :- A
+(5) D :- B. // :- A
+// iteration 3
+(3) B :- C. // :- B :- A
+```
 
 If a rule reduction leads to more than one possible callgraph edge, there exists an ambiguity in the program that the user must resolve by adding more edges.
 

diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -1,5 +1,5 @@
-Relation-Rule Based CFG Inference
-=================================
+Relation-Rule Based Callgraph Inference
+=======================================
 
 A relational event graph is described with unpredicated rules relating events, connecting a product of `n` sources and `m` conditions to a single sink (also called the goal). The format is as follows:
 ```
@@ -9,18 +9,15 @@ means "when all events `X[1]..X[n]` have happened, and all conditions `c[1]..c[m
 
 The resulting graph is a directed hypergraph of the [B-graph](https://en.wikipedia.org/wiki/BF-graph) class, with each rule constituting a B-arc. 
 
-The task is now to manifest the relational event graph as a CFG ([control flow graph](https://en.wikipedia.org/wiki/Control-flow_graph)) that satisfies all rules. 
+The task is now to manifest the relational event graph as a callgraph (as precursor of a [control flow graph](https://en.wikipedia.org/wiki/Control-flow_graph)) that satisfies all rules. 
 
-To achieve this, we define algebraic join and meet operators `future` and `past` over two events. The _soonest shared future_ of two events `future(a, b)` is their immediate common post-dominator, and constitutes the join operation (or supremum). The _latest common past_ of two events `past(a, b)` is their immediate common dominator, and forms the meet operation (or infimum). For the rule `B :- A.`, `future(A,B) == B` and `past(A,B) == A`. Both operations are commutative, associative and satisfy absorption and idempotent identities.
+We recognize the callgraph as a transitive reduction of the hypergraph, which means all source edges of a rule are reducible to one (and only one) edge that, in the strict interpretation, is dominated by all sources reachable through existing callgraph edges.
 
-Since `A, B <-> future(A, B)`, each B-arc can be collapsed to a single directed edge if the future over all its sources is satisfiable.
+Because the callgraph is initially incomplete, we must start from trivially reducible rules with single sources. This adds more edges to the callgraph, which allows us to reduce more complex rules, until a fixpoint is reached because no more rules can be reduced.
 
-Initially, only rules with singular sources can be collapsed, which solves all linear dependencies and allows to satisfy dependent rules. We iteratively collapse all satisfiable futures until a fixpoint is reached.
+If a rule reduction leads to more than one possible callgraph edge, there exists an ambiguity in the program that the user must resolve by adding more edges.
 
-Within the iterations, graph rules must be rewritten so all edges sourcing the same event have exclusive conditions, and therefore the event's next goal is linearly decidable.
+If one or more rules remain undecidable after the fixpoint, the user should be warned as the rules would never be applied.
 
-If any B-arcs remain, then it is because no common post-dominator for their sources exists, which requires the user to insert a rule for every source with the same goal.
 
-A rule may have a data dependency on a source `X[i]` that does not dominate the future `G` (i.e. function call pattern). If `X[i]` is an immediate predecessor of `G = future(X[1],...,X[n])`, then a phi node can be used. However, if the edge distance between `X[i]` and `G` is greater than one, then `X[i]`'s data `d` must be implicitly forwarded as an option type, and the rule must add a "is option `d` set" condition.
 
-If this implicit solution is undesired (for the sake of intuitive reasoning, or simplification of the compiler), then an additional constraint can be imposed which requires any source `X[i]` to be a dominator of `G` (that is, `past(X[i],G) == X[i]`).
diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -11,7 +11,7 @@ The resulting graph is a directed hypergraph of the [B-graph](https://en.wikiped
 
 The task is now to manifest the relational event graph as a CFG ([control flow graph](https://en.wikipedia.org/wiki/Control-flow_graph)) that satisfies all rules. 
 
-To achieve this, we define algebraic join and meet operators `future` and `past` over two events. The soonest shared future of two events `future(a, b)` is their immediate common post-dominator, and constitutes the join operation (or supremum). The latest common past of two events `past(a, b)` is their immediate common dominator, and forms the meet operation (or infimum). For the rule `B :- A.`, `future(A,B) == B` and `past(A,B) == A`. Both operations are commutative, associative and satisfy absorption and idempotent identities.
+To achieve this, we define algebraic join and meet operators `future` and `past` over two events. The _soonest shared future_ of two events `future(a, b)` is their immediate common post-dominator, and constitutes the join operation (or supremum). The _latest common past_ of two events `past(a, b)` is their immediate common dominator, and forms the meet operation (or infimum). For the rule `B :- A.`, `future(A,B) == B` and `past(A,B) == A`. Both operations are commutative, associative and satisfy absorption and idempotent identities.
 
 Since `A, B <-> future(A, B)`, each B-arc can be collapsed to a single directed edge if the future over all its sources is satisfiable.
 

diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -1,26 +1,26 @@
 Relation-Rule Based CFG Inference
 =================================
 
-A relational callgraph is described with unpredicated rules relating argument-free continuations, connecting a product of `n` sources and `m` conditions to a single sink (also called the goal). The format is as follows:
+A relational event graph is described with unpredicated rules relating events, connecting a product of `n` sources and `m` conditions to a single sink (also called the goal). The format is as follows:
 ```
 Y :- X[1], X[2], ..., X[n], c[1], c[2], ..., c[m].
 ```
-means "when all continuations `X[1]..X[n]` have been called, and all conditions `c[1]..c[m]` have been met, then the goal `Y` will be called". Because the right hand side is a product, the arguments are commutative and associative, so that the rule makes no demands as to in what order the sources are called, or the conditions are evaluated.
+means "when all events `X[1]..X[n]` have happened, and all conditions `c[1]..c[m]` have been met, then the goal `Y` will happen". Because the right hand side is a product, the arguments are commutative and associative, so that the rule makes no demands as to in what order the sources are called, or the conditions are evaluated.
 
 The resulting graph is a directed hypergraph of the [B-graph](https://en.wikipedia.org/wiki/BF-graph) class, with each rule constituting a B-arc. 
 
-The task is now to manifest the relational callgraph as a CFG ([control flow graph](https://en.wikipedia.org/wiki/Control-flow_graph)) that satisfies all rules. 
+The task is now to manifest the relational event graph as a CFG ([control flow graph](https://en.wikipedia.org/wiki/Control-flow_graph)) that satisfies all rules. 
 
-To achieve this, we define algebraic join (`&`) and meet (`|`) operators over two continuations. The join of two continuations `a & b` is their immediate common dominator. The meet of two continuations `a | b` is their immediate common post-dominator. Both operations are commutative, associative and satisfy absorption and idempotent identities.
+To achieve this, we define algebraic join and meet operators `future` and `past` over two events. The soonest shared future of two events `future(a, b)` is their immediate common post-dominator, and constitutes the join operation (or supremum). The latest common past of two events `past(a, b)` is their immediate common dominator, and forms the meet operation (or infimum). For the rule `B :- A.`, `future(A,B) == B` and `past(A,B) == A`. Both operations are commutative, associative and satisfy absorption and idempotent identities.
 
-Since `A | B <-> A, B`, each B-arc can be collapsed to a single directed edge if the meet over all its sources is satisfiable.
+Since `A, B <-> future(A, B)`, each B-arc can be collapsed to a single directed edge if the future over all its sources is satisfiable.
 
-Initially, only rules with singular sources can be collapsed, which solves all linear dependencies and allows to satisfy dependent rules. We iteratively collapse all satisfiable meets until a fixpoint is reached.
+Initially, only rules with singular sources can be collapsed, which solves all linear dependencies and allows to satisfy dependent rules. We iteratively collapse all satisfiable futures until a fixpoint is reached.
 
-Within the iterations, graph rules must be rewritten so all edges sourcing the same continuation have exclusive conditions, and therefore the continuation's next goal is linearly decidable.
+Within the iterations, graph rules must be rewritten so all edges sourcing the same event have exclusive conditions, and therefore the event's next goal is linearly decidable.
 
-If any B-arcs remain, then it is because no common post-dominator for their sources exists, which requires the user to insert meet rules.
+If any B-arcs remain, then it is because no common post-dominator for their sources exists, which requires the user to insert a rule for every source with the same goal.
 
-A rule may have a data dependency on a source `X[i]` that does not dominate the meet `G` (i.e. function call pattern). If `X[i]` is an immediate predecessor of `G = meet(X[1],...,X[n])`, then a phi node can be used. However, if the edge distance between `X[i]` and `G` is greater than one, then `X[i]`'s data `d` must be implicitly forwarded as an option type, and the rule must add a "is option `d` set" condition.
+A rule may have a data dependency on a source `X[i]` that does not dominate the future `G` (i.e. function call pattern). If `X[i]` is an immediate predecessor of `G = future(X[1],...,X[n])`, then a phi node can be used. However, if the edge distance between `X[i]` and `G` is greater than one, then `X[i]`'s data `d` must be implicitly forwarded as an option type, and the rule must add a "is option `d` set" condition.
 
-If this implicit solution is undesired (for the sake of intuitive reasoning, or simplification of the compiler), then an additional constraint can be imposed which requires any source `X[i]` to be a dominator of `G` (that is, `join(X[i],G) == X[i]`).
+If this implicit solution is undesired (for the sake of intuitive reasoning, or simplification of the compiler), then an additional constraint can be imposed which requires any source `X[i]` to be a dominator of `G` (that is, `past(X[i],G) == X[i]`).
diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -21,6 +21,6 @@ Within the iterations, graph rules must be rewritten so all edges sourcing the s
 
 If any B-arcs remain, then it is because no common post-dominator for their sources exists, which requires the user to insert meet rules.
 
-A rule may have a data dependency on a source `B` that does not dominate the meet `G` (i.e. function call pattern). If `B` is an immediate predecessor of `G = meet(X[1],...,X[n])`, then a phi node can be used. However, if the edge distance between `B` and `G` is greater than one, then `B`'s data `d` must be implicitly forwarded as an option type, and the rule must add a "is option `d` set" condition.
+A rule may have a data dependency on a source `X[i]` that does not dominate the meet `G` (i.e. function call pattern). If `X[i]` is an immediate predecessor of `G = meet(X[1],...,X[n])`, then a phi node can be used. However, if the edge distance between `X[i]` and `G` is greater than one, then `X[i]`'s data `d` must be implicitly forwarded as an option type, and the rule must add a "is option `d` set" condition.
 
 If this implicit solution is undesired (for the sake of intuitive reasoning, or simplification of the compiler), then an additional constraint can be imposed which requires any source `X[i]` to be a dominator of `G` (that is, `join(X[i],G) == X[i]`).
diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -21,6 +21,6 @@ Within the iterations, graph rules must be rewritten so all edges sourcing the s
 
 If any B-arcs remain, then it is because no common post-dominator for their sources exists, which requires the user to insert meet rules.
 
-A rule may have a data dependency on a branching continuation `B` that does not dominate the goal `G` (i.e. function call pattern). If `B` is an immediate predecessor of `G`, then a phi node can be used. However, if the edge distance between `B` and `G` is greater than one, then `B`'s data `d` must be implicitly forwarded as an option type, and the rule must add a "is option `d` set" condition.
+A rule may have a data dependency on a source `B` that does not dominate the meet `G` (i.e. function call pattern). If `B` is an immediate predecessor of `G = meet(X[1],...,X[n])`, then a phi node can be used. However, if the edge distance between `B` and `G` is greater than one, then `B`'s data `d` must be implicitly forwarded as an option type, and the rule must add a "is option `d` set" condition.
 
 If this implicit solution is undesired (for the sake of intuitive reasoning, or simplification of the compiler), then an additional constraint can be imposed which requires any source `X[i]` to be a dominator of `G` (that is, `join(X[i],G) == X[i]`).
diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -9,8 +9,6 @@ means "when all continuations `X[1]..X[n]` have been called, and all conditions
 
 The resulting graph is a directed hypergraph of the [B-graph](https://en.wikipedia.org/wiki/BF-graph) class, with each rule constituting a B-arc. 
 
-We assume the graph has been rewritten so all edges sourcing the same continuation have exclusive conditions, and therefore the continuation's next goal is uniquely decidable.
-
 The task is now to manifest the relational callgraph as a CFG ([control flow graph](https://en.wikipedia.org/wiki/Control-flow_graph)) that satisfies all rules. 
 
 To achieve this, we define algebraic join (`&`) and meet (`|`) operators over two continuations. The join of two continuations `a & b` is their immediate common dominator. The meet of two continuations `a | b` is their immediate common post-dominator. Both operations are commutative, associative and satisfy absorption and idempotent identities.
@@ -19,6 +17,10 @@ Since `A | B <-> A, B`, each B-arc can be collapsed to a single directed edge if
 
 Initially, only rules with singular sources can be collapsed, which solves all linear dependencies and allows to satisfy dependent rules. We iteratively collapse all satisfiable meets until a fixpoint is reached.
 
+Within the iterations, graph rules must be rewritten so all edges sourcing the same continuation have exclusive conditions, and therefore the continuation's next goal is linearly decidable.
+
 If any B-arcs remain, then it is because no common post-dominator for their sources exists, which requires the user to insert meet rules.
 
-In addition, we require all conditions of the graph to be exclusive, so that each continuation with multiple out-edges will only take one path during evaluation.
+A rule may have a data dependency on a branching continuation `B` that does not dominate the goal `G` (i.e. function call pattern). If `B` is an immediate predecessor of `G`, then a phi node can be used. However, if the edge distance between `B` and `G` is greater than one, then `B`'s data `d` must be implicitly forwarded as an option type, and the rule must add a "is option `d` set" condition.
+
+If this implicit solution is undesired (for the sake of intuitive reasoning, or simplification of the compiler), then an additional constraint can be imposed which requires any source `X[i]` to be a dominator of `G` (that is, `join(X[i],G) == X[i]`).
diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -9,7 +9,7 @@ means "when all continuations `X[1]..X[n]` have been called, and all conditions
 
 The resulting graph is a directed hypergraph of the [B-graph](https://en.wikipedia.org/wiki/BF-graph) class, with each rule constituting a B-arc. 
 
-We assume that the graph has been rewritten so that all edges sourcing the same continuation have exclusive conditions, so that the continuation's next goal is uniquely decidable.
+We assume the graph has been rewritten so all edges sourcing the same continuation have exclusive conditions, and therefore the continuation's next goal is uniquely decidable.
 
 The task is now to manifest the relational callgraph as a CFG ([control flow graph](https://en.wikipedia.org/wiki/Control-flow_graph)) that satisfies all rules. 
 

diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -9,6 +9,8 @@ means "when all continuations `X[1]..X[n]` have been called, and all conditions
 
 The resulting graph is a directed hypergraph of the [B-graph](https://en.wikipedia.org/wiki/BF-graph) class, with each rule constituting a B-arc. 
 
+We assume that the graph has been rewritten so that all edges sourcing the same continuation have exclusive conditions, so that the continuation's next goal is uniquely decidable.
+
 The task is now to manifest the relational callgraph as a CFG ([control flow graph](https://en.wikipedia.org/wiki/Control-flow_graph)) that satisfies all rules. 
 
 To achieve this, we define algebraic join (`&`) and meet (`|`) operators over two continuations. The join of two continuations `a & b` is their immediate common dominator. The meet of two continuations `a | b` is their immediate common post-dominator. Both operations are commutative, associative and satisfy absorption and idempotent identities.

diff --git a/dril_rel_callgraph.md b/dril_rel_callgraph.md
@@ -1,16 +1,22 @@
 Relation-Rule Based CFG Inference
 =================================
 
-A relational callgraph is described with unpredicated rules relating argument-free continuations, connecting a product of `n` sources and `m` conditions to a single sink. The format is as follows:
+A relational callgraph is described with unpredicated rules relating argument-free continuations, connecting a product of `n` sources and `m` conditions to a single sink (also called the goal). The format is as follows:
 ```
 Y :- X[1], X[2], ..., X[n], c[1], c[2], ..., c[m].
 ```
-means "when all continuations `X[1]..X[n]` have been called, and all conditions `c[1]..c[m]` have been met, then `Y` will be called". Because the right hand side is a product, the arguments are commutative and associative, so that the rule makes no demands as to in what order the sources are called, or the conditions are evaluated.
+means "when all continuations `X[1]..X[n]` have been called, and all conditions `c[1]..c[m]` have been met, then the goal `Y` will be called". Because the right hand side is a product, the arguments are commutative and associative, so that the rule makes no demands as to in what order the sources are called, or the conditions are evaluated.
 
 The resulting graph is a directed hypergraph of the [B-graph](https://en.wikipedia.org/wiki/BF-graph) class, with each rule constituting a B-arc. 
 
 The task is now to manifest the relational callgraph as a CFG ([control flow graph](https://en.wikipedia.org/wiki/Control-flow_graph)) that satisfies all rules. 
 
 To achieve this, we define algebraic join (`&`) and meet (`|`) operators over two continuations. The join of two continuations `a & b` is their immediate common dominator. The meet of two continuations `a | b` is their immediate common post-dominator. Both operations are commutative, associative and satisfy absorption and idempotent identities.
 
-Since `A | B <-> A, B`, each B-arc can be collapsed to a single directed edge if the meet over all its sources is satisfiable.
+Since `A | B <-> A, B`, each B-arc can be collapsed to a single directed edge if the meet over all its sources is satisfiable.
+
+Initially, only rules with singular sources can be collapsed, which solves all linear dependencies and allows to satisfy dependent rules. We iteratively collapse all satisfiable meets until a fixpoint is reached.
+
+If any B-arcs remain, then it is because no common post-dominator for their sources exists, which requires the user to insert meet rules.
+
+In addition, we require all conditions of the graph to be exclusive, so that each continuation with multiple out-edges will only take one path during evaluation.