The $(\mu+1)$ GA and the function $\mathrm{Jump}_k$

Lax343628.Algorithm · concepts/Lax343628/Algorithm.lean · lax-343628

definition

Loading review…

Natural Language Statement

Definition

For $x\in\{0,1\}^n$ , let $|x|_1$ be its number of ones. For a jump size $k\in\{1,\dots,n\}$ , the function $\mathrm{Jump}_k\colon\{0,1\}^n\to\mathbb N$ is

\mathrm{Jump}_k(x)=\begin{cases}k+|x|_1 & \text{if } |x|_1=n \text{ or } |x|_1\le n-k,\\ n-|x|_1 & \text{otherwise.}\end{cases}

The $(\mu+1)$ genetic algorithm with crossover probability $p_c\in[0,1]$ maintains a population, a multiset of $\mu$ individuals from $\{0,1\}^n$ . One iteration, maximizing a fitness function $f$ , proceeds as follows:

With probability $p_c$ , choose two parents $x,y$ uniformly at random with replacement from the population. Create the offspring $z$ by uniform crossover of $x$ and $y$ , which takes each bit from $x$ or $y$ independently with probability $1/2$ , followed by standard bit mutation, which flips each bit independently with probability $1/n$ .
Otherwise, choose a parent $x$ uniformly at random and create $z$ by standard bit mutation of $x$ .
Add $z$ to the population and remove an individual with the lowest fitness, breaking ties uniformly at random.

Concept map

1 concept; 3 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Data.PNat.Basic
2	import Mathlib.Probability.Distributions.Uniform
3	import Mathlib.Probability.ProbabilityMassFunction.Constructions
4
5	/-!
6	---
7	title: The $(\mu+1)$ GA and the function $\mathrm{Jump}_k$
8	type: definition
9	---
10	For $x\in\{0,1\}^n$ , let $\|x\|_1$ be its number of ones. For a jump size $k\in\{1,\dots,n\}$ ,
11	the function $\mathrm{Jump}_k\colon\{0,1\}^n\to\mathbb N$ is
12	$\mathrm{Jump}_k(x)=\begin{cases}k+\|x\|_1 & \text{if } \|x\|_1=n \text{ or } \|x\|_1\le n-k,\\ n-\|x\|_1 & \text{otherwise.}\end{cases}$
13
14
15	The $(\mu+1)$ genetic algorithm with crossover probability $p_c\in[0,1]$ maintains a
16	population, a multiset of $\mu$ individuals from $\{0,1\}^n$ . One iteration, maximizing a
17	fitness function $f$ , proceeds as follows:
18
19	1. With probability $p_c$ , choose two parents $x,y$ uniformly at random with replacement from
20	the population. Create the offspring $z$ by uniform crossover of $x$ and $y$ , which takes
21	each bit from $x$ or $y$ independently with probability $1/2$ , followed by standard bit
22	mutation, which flips each bit independently with probability $1/n$ .
23	2. Otherwise, choose a parent $x$ uniformly at random and create $z$ by standard bit mutation
24	of $x$ .
25	3. Add $z$ to the population and remove an individual with the lowest fitness, breaking ties
26	uniformly at random.
27	-/
28
29	namespace Lax343628.Algorithm
30
31	open scoped ENNReal Classical BigOperators
32
33	noncomputable section
34
35	/-- A string in $\{0,1\}^n$ . `Fin n` indexes positions $0,\ldots,n-1$ ;
36	`Fin 2` consists of the values zero and one. -/
37	abbrev BitString (n : ℕ) := Fin n → Fin 2
38
39	/-- A population of positive size $\mu$ , with entries indexed separately even when equal.
40	An iteration writes the offspring into the slot of the deleted entry, or discards it if it
41	is deleted itself; up to the order of entries, this is adding it and then deleting. -/
42	abbrev Population (n : ℕ) (μ : ℕ+) := Fin (μ : ℕ) → BitString n
43
44	/-- The number of one-bits in a string. -/
45	def ones {n : ℕ} (x : BitString n) : ℕ :=
46	∑ j : Fin n, (x j : ℕ)
47
48	/-- The function $\mathrm{Jump}_k$ with jump size `k`, usually considered for $n\ge2$ and
49	$1\le k\le n/2$ . Fitness values are real numbers; natural-number subtraction is truncated
50	at zero. -/
51	def jump {n : ℕ} (k : ℕ) (x : BitString n) : ℝ :=
52	if ones x ≤ n - k ∨ ones x = n then (k + ones x : ℕ) else (n - ones x : ℕ)
53
54	/-- The all-one string $1^n$ , the unique optimum of $\mathrm{Jump}_k$ when $1\le k\le n$ . -/
55	def optimum (n : ℕ) : BitString n := fun _ ↦ 1
56
57	/-- A Bernoulli bit, equal to one with probability $p$ for $0\le p\le1$ .
58	Outside this interval it always returns the bit 0; all algorithm claims use valid probabilities. -/
59	def coin (p : ℝ) : PMF (Fin 2) :=
60	if h : 0 ≤ p ∧ p ≤ 1 then
61	PMF.ofFintype (fun b : Fin 2 ↦ ENNReal.ofReal (if b = 1 then p else 1 - p))
62	-- Lean checks this proof that the probabilities sum to one; readers can skip it.
63	(by simp_all [Fin.sum_univ_two, ← ENNReal.ofReal_add])
64	else PMF.pure 0
65
66	/-- Independent Bernoulli bits, each equal to one with probability $p$ : a string $x$ has
67	probability $\prod_j \Pr[\text{coin}=x_j]$ , which is $p^{\|x\|_1}(1-p)^{n-\|x\|_1}$ for
68	$0\le p\le1$ . Here `coin p b` is the probability that the coin shows the bit `b`. -/
69	def independentBits (n : ℕ) (p : ℝ) : PMF (BitString n) :=
70	PMF.ofFintype (fun x ↦ ∏ j, coin p (x j))
71	-- Lean checks this proof that the probabilities sum to one; readers can skip it.
72	(by
73	have h := (coin p).tsum_coe
74	rw [tsum_fintype] at h
75	rw [← Fintype.prod_sum]
76	simp [h])
77
78	/-- Uniform crossover: at each position an independent fair mask bit selects one parent.
79	Sampling the mask uniformly among all bit strings gives independent fair choices. -/
80	def crossover {n : ℕ} (x y mask : BitString n) : BitString n :=
81	fun j ↦ if mask j = 1 then x j else y j
82
83	/-- Flip exactly the positions where the mutation mask is one. -/
84	def mutate {n : ℕ} (x mask : BitString n) : BitString n :=
85	fun j ↦ if mask j = 1 then 1 - x j else x j
86
87	/-- Uniform deletion among the $\mu+1$ entries of minimal `fitness`, including the offspring.
88	The minimum exists because the enlarged population is finite and nonempty. -/
89	def deletionIndex {n : ℕ} (fitness : BitString n → ℝ) {μ : ℕ+}
90	(Q : Fin ((μ : ℕ) + 1) → BitString n) : PMF (Fin ((μ : ℕ) + 1)) :=
91	PMF.uniformOfFinset
92	(Finset.univ.filter fun i ↦ ∀ j, fitness (Q i) ≤ fitness (Q j))
93	-- Lean checks this proof that a minimal entry exists; readers can skip it.
94	(by simpa [Finset.filter_nonempty_iff] using Finite.exists_min fun j ↦ fitness (Q j))
95
96	/-- One iteration of the $(\mu+1)$ GA, maximizing `fitness`.
97	Crossover parents are independent uniform draws with replacement; the mutation-only
98	parent is uniform. Mutation flips each bit independently with probability $1/n$ .
99	The offspring is inserted even if it equals an existing entry, before a worst entry is deleted.
100	Each `←` draws a sample from the distribution on its right. -/
101	def step {n : ℕ} (fitness : BitString n → ℝ) {μ : ℕ+} (p_c : ℝ) (P : Population n μ) :
102	PMF (Population n μ) := do
103	let useCrossover ← coin p_c
104	-- `z'` is the uniform crossover of the parents `P u` and `P v`, or the parent `P u` itself.
105	let z' ← if useCrossover = 1 then do
106	let (u, v) ← PMF.uniformOfFintype (Fin (μ : ℕ) × Fin (μ : ℕ))
107	let crossMask ← PMF.uniformOfFintype (BitString n)
108	pure (crossover (P u) (P v) crossMask)
109	else do
110	let u ← PMF.uniformOfFintype (Fin (μ : ℕ))
111	pure (P u)
112	let flipMask ← independentBits n (1 / (n : ℝ))
113	let z := mutate z' flipMask
114	-- `Q` lists the μ + 1 entries: the population `P`, followed by the offspring `z`.
115	let Q := Fin.lastCases z P
116	let d ← deletionIndex fitness Q
117	-- Deleting an old entry puts z into its slot; deleting the offspring (the last entry of
118	-- `Q`) leaves P unchanged.
119	pure (if h : d.val < (μ : ℕ) then Function.update P ⟨d.val, h⟩ z else P)
120
121	end
122	end Lax343628.Algorithm
123

Builds on

none

Used by

Lax343628.Runtime

From Mathlib

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

The $(\mu+1)$ GA and the function $\mathrm{Jump}_k$

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments

The (μ+1)(\mu+1)(μ+1) GA and the function Jumpk\mathrm{Jump}_kJumpk​

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

The $(\mu+1)$ GA and the function $\mathrm{Jump}_k$