Editing Fixed-point combinator (section)

===Verification===
The following calculation verifies that <math>Y g</math> is indeed a fixed point of the function <math>g</math>:
:{| cellpadding="0"
| <math>Y\ g\ </math>
| <math>= (\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x)))\ g\ \ \  </math>
| by the definition of <math>Y</math>
|-
|
| <math>= (\lambda x.g\ (x\ x))\ (\lambda x.g\ (x\ x))\ </math>
| by [[β-reduction]]: replacing the formal argument ''f'' of ''Y'' with the actual argument ''g''
|-
|
| <math>= g\ ((\lambda x.g\ (x\ x))\ (\lambda x.g\ (x\ x)))\ </math>
| by β-reduction: replacing the formal argument ''x'' of the first function with the actual argument <math>(\lambda x.g\ (x\ x))</math>
|-
|
| <math>= g\ (Y\ g)</math>
| by second equality, above
|}

The lambda term <math>g\ (Y\ g)</math> may not, in general, [[Β-reduction|β-reduce]] to the term <math>Y\ g</math>. However, both terms β-reduce to the same term, as shown.