English
This is a wrapper that implements a maximum-depth option for a depth-first-like search procedure. If no maximum depth is specified, it delegates to the underlying procedure; if a maximum depth d is specified, it augments each state with a depth counter, prunes any exploration whose depth exceeds d, continues exploring with depth increased by one, and finally projects the results back to the original state space.
Русский
Это обертка, которая реализует ограничение глубины для процедуры поиска: если ограничение по глубине не задано, используется исходная процедура; если задано максимальное значение глубины d, к каждому состоянию добавляется счётчик глубины, исследования глубиной более d обрезаются, далее по стеках с глубиной увеличивается на единицу, и результат возвращается в исходном пространстве состояний.
LaTeX
$$$\displaystyle \text{implMaxDepth}(maxSize,\; maxDepth,\; f,\; a) = \begin{cases} \text{impl}(\text{prio},\; \varepsilon,\; maxSize,\; f)(a), & \text{if } maxDepth = \text{none}, \\[6pt] \\ \, \text{proj}_1\Bigl( \text{impl}\bigl(p \mapsto \text{prio}(p.1),\; q \mapsto \varepsilon(p.1),\; maxSize,\; f',\; (a,0)\bigr)\Bigr) , & \text{if } maxDepth = \text{some } \text{max}, \end{cases} \\[6pt] \text{where } f'(a,n) = \begin{cases} \varnothing, & \text{if } max < n, \\ \{ (a',n+1) : a' \in f(a) \}, & \text{otherwise}. \end{cases} $$$
Lean4
/-- Wrapper for `impl` implementing the `maxDepth` option.
-/
def implMaxDepth (maxSize : Option Nat) (maxDepth : Option Nat) (f : α → MLList m α) (a : α) : MLList m α :=
match maxDepth with
| none => impl prio ε maxSize f a
| some max =>
let f' : α ×ₗ Nat → MLList m (α × Nat) := fun ⟨a, n⟩ => if max < n then nil else (f a).map fun a' => (a', n + 1)
impl (fun p : α ×ₗ Nat => prio p.1) (fun p : α ×ₗ Nat => ε p.1) maxSize f' (a, 0) |>.map (·.1)
