reference_directions.bend
unified-nsga-iii@0.2.0.0 · 132 lines · 0 definitions
1# ReferenceDirections — C# Unsga3.Utilities.ReferenceDirections.
2# Das–Dennis structured points on the unit simplex.
3# Count = C(p + M - 1, M - 1); M == 1n → 1n. Points match C# recurse order
4# (first coordinate increases 0..p, DFS).
5#
6# count and das_dennis disagree at partitions == 0 when M > 1.
7# count(2, 0) = C(1, 1) = 1. das_dennis(2, 0) is Nil{} (length 0).
8# C# throws if partitions < 1. Law das_dennis_len quantifies p+1 and
9# its comment in LAWS.bend records that split. Oracles use p >= 4.
10# Do not treat count and the generator as the same function.
11
12import Base
13import unified-nsga-iii@0.2.0.0/util.bend as Util
14
15def binomial(+n: Nat, +k: Nat) -> Nat:
16 Util.binomial(n, k)
17
18def count.succ(+rest: Nat, +partitions: Nat, z: Bool) -> Nat:
19 match z:
20 case True{}:
21 1n
22 case False{}:
23 Util.binomial(Nat.add(partitions, rest), rest)
24
25def count.go(+rest: Nat, +partitions: Nat) -> Nat:
26 count.succ(rest, partitions, Nat.is_eq(rest, 0n))
27
28# Number of Das–Dennis points. M == 0n is a guard (0). M == 1n → 1.
29# M == 1n+rest → if rest == 0 then 1 else C(p + rest, rest) = C(p + M - 1, M - 1).
30def count(number_of_objectives: Nat, partitions: Nat) -> Nat:
31 match number_of_objectives:
32 case 0n:
33 0n
34 case 1n+rest:
35 count.go(rest, partitions)
36
37def to_dir(+p: Nat, comps: List<&2, Nat>) -> List<&2, F32>:
38 match comps:
39 case Nil{}:
40 Nil{}
41 case i <> rest:
42 F32.div(F32.from_nat(i), F32.from_nat(p)) <> to_dir(p, rest)
43
44def to_dirs(+p: Nat, rows: List<&2, List<&2, Nat>>) -> List<&2, List<&2, F32>>:
45 match rows:
46 case Nil{}:
47 Nil{}
48 case row <> rest:
49 to_dir(p, row) <> to_dirs(p, rest)
50
51# k-th composition of `p` into `m` parts, C# DFS order (first coord
52# increases 0..p). Enumerating `range(Count)` makes |DasDennis| = Count
53# by construction. @unsafe: Bool dispatch on `k < count(rest)` then
54# either shrinks M or advances i; fuel is a bound, not the shrink key.
55type DasCtx is Data:
56 DasCtx{
57 m: Nat
58 p: Nat
59 }
60
61def nth_comp.fallback(m: Nat, p: Nat) -> List<&2, Nat>:
62 match m:
63 case 0n:
64 Nil{}
65 case 1n:
66 [p]
67 case 1n+rd:
68 0n <> nth_comp.fallback(rd, p)
69
70@unsafe def nth_comp.go(
71 ready: Bool,
72 take: Bool,
73 fuel: Nat,
74 +m: Nat,
75 +p: Nat,
76 +k: Nat,
77 +i: Nat,
78 left: Nat,
79 c: Nat
80) -> List<&2, Nat>:
81 match ready take fuel:
82 case True{} True{} f:
83 i <> nth_comp.go(False{}, False{}, f, m, left, k, 0n, 0n, 0n)
84 case True{} False{} f:
85 nth_comp.go(False{}, False{}, f, 1n+m, p, Nat.sub(k, c), 1n+i, 0n, 0n)
86 case False{} t 0n:
87 nth_comp.fallback(m, p)
88 case False{} t 1n+f:
89 match m:
90 case 0n:
91 Nil{}
92 case 1n:
93 [p]
94 case 1n+rd:
95 +left2 = Nat.sub(p, i)
96 +c2 = count(rd, left2)
97 nth_comp.go(True{}, Nat.is_lt(k, c2), f, rd, p, k, i, left2, c2)
98
99def nth_comp(+m: Nat, +p: Nat, +k: Nat) -> List<&2, Nat>:
100 nth_comp.go(False{}, False{}, Nat.mul(Nat.add(p, 1n), Nat.add(m, 1n)), m, p, k, 0n, 0n, 0n)
101
102def nth_row(+ctx: DasCtx, +k: Nat) -> List<&2, Nat>:
103 match ctx:
104 case DasCtx{+m, +p}:
105 nth_comp(m, p, k)
106
107def comps_all(+m: Nat, +p: Nat) -> List<&2, List<&2, Nat>>:
108 Util.map_halves(~Nat, ~List<&2, Nat>, ~DasCtx, ~nth_row, DasCtx{m, p}, List.range(count(m, p)))
109
110def das_dennis.from(+m: Nat, +p: Nat, rest: Nat) -> List<&2, List<&2, F32>>:
111 match rest:
112 case 0n:
113 [[1.0]]
114 case 1n+q:
115 to_dirs(p, comps_all(m, p))
116
117def das_dennis.p0(rest: Nat) -> List<&2, List<&2, F32>>:
118 match rest:
119 case 0n:
120 [[1.0]]
121 case 1n+q:
122 Nil{}
123
124# Generate directions. M == 1n → [[1.0]]. M == 0n → Nil{}. p == 0n → Nil{} when M > 1.
125def das_dennis(number_of_objectives: Nat, partitions: Nat) -> List<&2, List<&2, F32>>:
126 match number_of_objectives partitions:
127 case 0n p:
128 Nil{}
129 case 1n+rest 0n:
130 das_dennis.p0(rest)
131 case +m 1n+q:
132 das_dennis.from(m, 1n+q, Nat.sub(m, 1n))