English
The fix function transforms a partial function f : α →. β ⊕ α into a partial function α →. β, by repeatedly applying f and returning the first β encountered, if any.
Русский
Функция fix преобразует частичную функцию f : α →. (β ⊕ α) в частичную функцию α →. β, возвращая первый встреченный β или оставаясь неопределённой.
LaTeX
$$$\\mathrm{fix}(f) : \\alpha \\to^. \\beta \\text{ is defined as in the given recursive construction}$$$
Lean4
/-- First return map. Transforms a partial function `f : α →. β ⊕ α` into the partial function
`α →. β` which sends `a : α` to the first value in `β` it hits by iterating `f`, if such a value
exists. By abusing notation to illustrate, either `f a` is in the `β` part of `β ⊕ α` (in which
case `f.fix a` returns `f a`), or it is undefined (in which case `f.fix a` is undefined as well), or
it is in the `α` part of `β ⊕ α` (in which case we repeat the procedure, so `f.fix a` will return
`f.fix (f a)`). -/
def fix (f : α →. β ⊕ α) : α →. β := fun a =>
Part.assert (Acc (fun x y => Sum.inr x ∈ f y) a) fun h =>
WellFounded.fixF
(fun a IH =>
Part.assert (f a).Dom fun hf =>
match e : (f a).get hf with
| Sum.inl b => Part.some b
| Sum.inr a' => IH a' ⟨hf, e⟩)
a h
