non_dominated_sort.bend checks

raw source on the hub · import 0xa2f9d6ef8c474468bf1de15ebe70c512/non_dominated_sort.bend as Non_dominated_sort

NonDominatedSort — C# Unsga3.Core.NonDominatedSort. Fast non-dominated sorting by peeling (Deb et al.). sort uses Deb constraint-domination: feasible beats infeasible; both infeasible and unequal CV → smaller CV; equal CV is mutual non-domination (objectives are not compared). Both feasible → Pareto. dominates stays the Pareto predicate (law dominates_irreflexive). Zero constraints (cv 0) keeps today's Pareto fronts.

Layout (Bend guide: Arrays cannot ride a fork tree; List.get is a cons walk): one sequential pass materializes Row{index, objectives, cv} so the peel never List.gets a fat Individual. Per-candidate split still mid-splits a b = f(lo) f(hi) (same front/leftover order as the tail-first walk). Inner is_dominated stays a sequential OR so a first hit skips the rest. Same ranks and index order when every cv is 0.

3 imports

import Base
import ./individual.bend as Ind
import ./util.bend as Util

Types

type Row source · line 22 · raw

Data

One sort-row: population index plus the objective vector. Built once per sort; leftover peels reuse the same rows (no re-index).

Row

@i:Nat -> @f:List<&2, F32> -> @cv:F32 -> Row

type Split source · line 189 · raw

Data

Split

@ff:List<&2, Nat> -> @ot:List<&2, Row> -> Split

Definitions

def row_idx source · line 29 · raw

@r:Row -> Nat

def row_f source · line 34 · raw

@r:Row -> List<&2, F32>

def row_cv source · line 39 · raw

@r:Row -> F32

def rows_of.go source · line 44 · raw

@pop:List<&2, 0xa2f9d6ef8c474468bf1de15ebe70c512/individual.Individual> -> @+i:Nat -> List<&2, Row>

def rows_of source · line 51 · raw

@+pop:List<&2, 0xa2f9d6ef8c474468bf1de15ebe70c512/individual.Individual> -> List<&2, Row>

def row_idxs source · line 54 · raw

@rs:List<&2, Row> -> List<&2, Nat>

def verdict.a source · line 61 · raw

@bb:Bool -> Nat

def verdict.b source · line 68 · raw

@bb:Bool -> Nat

def verdict source · line 76 · raw

@ab:Bool -> @bb:Bool -> Nat

Minimization: 0n = mutual non-domination, 1n = a dominates b, 2n = b dominates a.

def compare_pareto.go source · line 83 · raw

@a:List<&2, F32> -> @b:List<&2, F32> -> @ab:Bool -> @bb:Bool -> Nat

def compare_pareto source · line 97 · raw

@a:List<&2, F32> -> @b:List<&2, F32> -> Nat

def compare_cd.infeas source · line 103 · raw

@+cva:F32 -> @+cvb:F32 -> @a_lt:Bool -> @b_lt:Bool -> Nat

Equal CV among infeasible points: 0. Deb does not Pareto-compare. C# CompareConstraintDominated on published main falls through to Pareto; this tree does not (Deb / constraint-domination target).

def compare_cd.feas source · line 117 · raw

@+fa:List<&2, F32> -> @+fb:List<&2, F32> -> @+cva:F32 -> @+cvb:F32 -> @a_feas:Bool -> @b_feas:Bool -> Nat

0 mutual, 1 a dominates b, 2 b dominates a. Feasible (cv ≤ 0) beats infeasible. Both feasible → Pareto, including unequal objective lengths (mutual non-domination).

def compare_cd source · line 135 · raw

@+fa:List<&2, F32> -> @+fb:List<&2, F32> -> @+cva:F32 -> @+cvb:F32 -> Nat

def compare_constraint source · line 138 · raw

@+a:0xa2f9d6ef8c474468bf1de15ebe70c512/individual.Individual -> @+b:0xa2f9d6ef8c474468bf1de15ebe70c512/individual.Individual -> Nat

def dominates.is1 source · line 141 · raw

@p:Nat -> Bool

def dominates.fin source · line 148 · raw

@c:Nat -> Bool

def dominates source · line 157 · raw

@a:0xa2f9d6ef8c474468bf1de15ebe70c512/individual.Individual -> @b:0xa2f9d6ef8c474468bf1de15ebe70c512/individual.Individual -> Bool

Pareto only. Irreflexivity is closed in PROOF.bend on this predicate. sort uses compare_cd, not this function.

def dominates_ff source · line 160 · raw

@+fa:List<&2, F32> -> @+fb:List<&2, F32> -> Bool

def dominates_cd source · line 163 · raw

@+fa:List<&2, F32> -> @+cva:F32 -> @+fb:List<&2, F32> -> @+cvb:F32 -> Bool

def is_dominated source · line 169 · raw

@+all:List<&2, Row> -> @+i:Nat -> @+fi:List<&2, F32> -> @+cvi:F32 -> Bool

Sequential OR so a first hit can skip the rest. Candidate-level parallelism lives in split_walk (coarse mid-split). Walks all rows directly — no List.get into the population.

def row_dom source · line 181 · raw

@+all:List<&2, Row> -> @+r:Row -> Bool

def split_put source · line 195 · raw

@+r:Row -> @s:Split -> @dominated:Bool -> Split

def split_cat source · line 204 · raw

@a:Split -> @b:Split -> Split

def split_walk.go source · line 211 · raw

@+all:List<&2, Row> -> @+fuel:Nat -> @cand:List<&2, Row> -> Split

Per-candidate split is independent given all. Mid-split then concatenate fronts / leftovers so order matches the tail-first walk.

def split_walk source · line 227 · raw

@+all:List<&2, Row> -> @+cand:List<&2, Row> -> Split

def split_ne source · line 232 · raw

@+r:Row -> @+rest:List<&2, Row> -> @s:Split -> Split

Empty first front (unreachable on a finite Pareto set) keeps the head so peel stays a partition.

def split_front source · line 241 · raw

@remaining:List<&2, Row> -> Split

def split_fst source · line 248 · raw

@s:Split -> List<&2, Nat>

def split_snd source · line 253 · raw

@s:Split -> List<&2, Row>

def peel source · line 258 · raw

@fuel:Nat -> @remaining:List<&2, Row> -> List<&2, List<&2, Nat>>

def sort source · line 270 · raw

@population:List<&2, 0xa2f9d6ef8c474468bf1de15ebe70c512/individual.Individual> -> List<&2, List<&2, Nat>>

def front_index_count source · line 278 · raw

@fronts:List<&2, List<&2, Nat>> -> Nat