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

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:

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,

(first @ second ** n)(zero_one) == n % 2

Example of using fix: factorial again

Also see demo.py.

The factorial function fac for which fac(n) == n!, can be defined as follows using fix. First, we define

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

fac = fix(pre_fac)

By the way, using the definitions in FuPy.basics, we could have defined pre_fac by

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