<img src="_static/FuPy.png" alt="FuPy logo" style="float: right; margin-left: 20px; margin-bottom: 20px;">

# Fixpoints

`FuPy.fixpoints` provides definitions to obtain
fixpoints of functions and functors (parameterized types).

## Fixpoints of functions: `fix`

Given function `f` of type `Func[A, A]`,
value `a` is called a _fixpoint_ of `f`
when `f(a) == a`.

Function `fix` of type `Func[Func[A, A], A]`
returns a fixpoint of its argument,
that is, we have `f(fix(f)) == fix(f)`.

Note that under eager evaluation,
defining `fix(f) = f(fix(f))` is not going to work,
because it gives rise to an infinite recursion:
`f(f(f(...)))`.

In `FuPy.fixpoints`,
`fix` is defined as `fix(f) = f(lazy(fix)(f))`,
which rewrites to `f(Lazy(lambda: fix(f)))`,
thereby breaking the infinite recursion.

### Example of using `fix`: infinite zero-one sequence

The following examples require
```python
from FuPy.core import *

_ = x_
```
where `FuPy.core` loads `FuPy.basics`, `FuPy.laziness`, and `FuPy.fixpoints`.

Function `fix` can be used to define the infinite nested tuple
consisting of alternating zeros and ones:
```python
zero_one = fix(la('x: (0, (1, x))'))
```
Now, `zero_one` behaves like `(0, (1, (0, (1, (0, (1, ...))))))`.
We can test that by verifying, for various `n`,
```python
(first @ second ** n)(zero_one) == n % 2
```

### Example of using `fix`: factorial again

Also see [demo.py](../examples/demo.py).

The factorial function `fac` for which `fac(n) == n!`,
can be defined as follows using `fix`.
First, we define
```python
pre_fac = la('x, n: 1 if n == 0 else n * x(n - 1)')
```
Note that here, `x` has type `Func[int, int]`,
and thus `pre_fac` has type
`Func[Func[int, int], Func[int, int]]`.
Observe that `fac` is a fixpoint of `pre_fac`:
```
   pre_fac(fac)
 =   { def. pre_fac }
   lambda n: 1 if n == 0 else n * fac(n - 1)
 =   { def. fac }
   fac
```
Function `pre_fac(x)(0)` does not "use" `x`
and just returns `1`, which is `fac(0)`.
And for `pre_fac(x)(n)` with `n > 0` to "work" (return `fac(n)`),
we only need to have that `x(n - 1)` returns `fac(n - 1)`;
in particular, we _don't_ need `x(m) == fac(m)` for all `m`.
This explains why we can define
```python
fac = fix(pre_fac)
```

By the way, using the definitions in `FuPy.basics`,
we could have defined `pre_fac` by
```python
from operator import mul

pre_fac = la('x: (const(1) | mul @ (id_ & x @ (_ - 1))) @ guard(_ == 0)')
```


## Functors

To Be Provided

## Fixpoints of functors: `Fix`

To Be Provided