Mu operator
|
|
In computability theory, the μ-operator is the operator which when applied to a given computable function f is a computable function returning the first value for which f is zero.
For a given function
- <math>f:\mathbb{N}\rightarrow\mathbb{Z}<math>,
- <math>\mu y\left[f(y)=0\right]=z<math>
- <math>f(z)=0<math> and
- for every <math>y
Using similar definitions, this idea can be extended to a μ-formula for any well-formed formula φ of one free variable, written
- <math>\mu y\left[\phi(y)\right]<math>.Template:Math-stub