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<z</math>, <math>f(y)</math> is defined and <math>f(y)>0</math>.

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>.

This mathematics-related article is a stub. You can help Wikipedia by expanding it.