5. Advanced Rule Classification & Semantic Analysis

5.1 Final Rules vs. Illegal Subchain Rules

The efficiency of airline schedule generation depends on classifying rules correctly:

Final Rule Definition: A rule $r$ is a Final Rule if, whenever $r$ is violated for a candidate sub-trip node $n$, no possible continuation subnode $n_s \in s(n)$ can ever be legal under $r$: $$\forall n \left( \neg r(n) \implies \neg \exists n_s \in s(n) : r(n_s) \right)$$
Illegal Subchain Rule Definition: A rule $r$ is an Illegal Subchain Rule if, when $r$ is violated for a candidate node $n$, there may still exist a legal continuation subnode $n_s \in s(n)$: $$\exists n \left( \neg r(n) \land \exists n_s \in s(n) : r(n_s) \right)$$

Consequences of Misclassification

Final Rule misclassified as Illegal Subchain: The solver explores dead-end subtrees, causing severe computational slowdowns.
Illegal Subchain Rule misclassified as Final: The solver prematurely prunes valid branches, missing feasible or cost-optimal pairings entirely.

5.2 Conditionality & The `is_closed` Keyword

To prevent Illegal Subchain Rules from prematurely pruning search branches, Rave introduces conditional rule checking via the valid clause and the is_closed solver state variable.

rule trip_must_end_at_base =
  valid is_closed;
  first(leg(trip), leg.%dep_airport%) = last(leg(trip), leg.%arr_airport%);
end

The keyword is_closed evaluates to False while the generator is actively expanding an incomplete candidate trip, and evaluates to True only when evaluating a completed candidate trip.

5.3 Monotonicity & Abstract Interpretation

By analyzing the mathematical properties of expressions at compile-time, the Rave compiler can automatically infer whether a rule is a Final Rule or an Illegal Subchain Rule.

Definition: Monotonic Sum

A sum expression $S = \sum e_i$ is a monotonic sum if the subexpression $e_i$ is guaranteed to be non-negative ($\ge 0$). As candidate flight legs are appended to a trip during generation, $S$ is strictly non-decreasing ($S_{k+1} \ge S_k$).

Direction in Legality

Non-increasing in Legality (NiL): A rule expression $E$ is NiL if, once it evaluates to False for a candidate trip, no continuation can ever evaluate to True.
Theorem: Any rule comparing a non-decreasing monotonic sum against a constant upper bound ($S \le C$) is Non-increasing in Legality and is therefore statically proven to be a Final Rule.
Non-decreasing in Legality (NdL): A rule expression $E$ is NdL if, once it evaluates to True, all continuations remain True ($S \ge C$). Such rules are Illegal Subchain Rules.

5.4 Type & Attribute Inference Framework

The Rave compiler uses an abstract interpretation and attribute propagation pass over the Abstract Syntax Tree (AST):

flowchart TD
    Op["Relational Operator (<=)<br><b>[Inferred: Non-increasing in Legality &rarr; FINAL RULE]</b>"]
    Sum["sum(leg(duty), e)<br><i>[Inferred: Non-decreasing]</i>"]
    Const["Constant Bound (08:00)<br><i>[Inferred: DepOnlyConst]</i>"]
    Var["leg.%flight_time%<br><i>[Inferred: Non-negative]</i>"]

    Op --- Sum
    Op --- Const
    Sum --- Var

Attribute Propagation Rules:

Range Inference: e1 : NonNegative, e2 : NonNegative => e1 + e2 : NonNegative e : NonNegative => sum(e) : NonDecreasing
Direction in Legality Inference: e1 : NonDecreasing, e2 : DepOnlyConst => (e1 <= e2) : NonIncreasingInLegality (NiL) Rule(E : NiL) => Final Rule (Safe to Prune Search Tree)