# Many faces of the fixed-point combinator

## Many ways to write the fixed-point combinator in a typed practical language

Although the fixed-point (a.k.a fixpoint) combinator can be given a simple or polymorphic type, it cannot be written as an expression in simply-typed lambda calculus or System F. In fact, making the fixed-point combinator inexpressible was the reason for introducing types into lambda calculus in the first place.

Originally, (untyped) lambda calculus was meant for formalizing mathematics. Then the expression, to be called `fix`, was discovered with the property `fix f = f (fix f)` for any term `f` -- including negation `neg`. In the latter case we obtain `fix neg = neg (fix neg)`: the term `fix neg` is equal to its own negation. A calculus with the liar paradox does not seem suitable as a logical foundation.

Although a fixed-point combinator, or general recursion, is logically inconsistent, it is awfully convenient for writing programs. We just have to accept the possibility of getting no result, because the program loops forever. Therefore, many practical programming languages introduced the combinator -- or the equivalent syntactic sugar such as recursive bindings -- as a primitive. After all, in System F, Hindley-Milner and many other type systems, the fixed-point combinator is typable: its introduction does not break the type system.

Built-in recursive bindings are not the only way to write the fixed-point combinator in languages like OCaml or Haskell. It turns out, there are many other ways -- more than one might have expected.

The code below demonstrates all the different ways to express the fully polymorphic fixpoint combinator in OCaml: from banal to advanced. Our approach is explicitly based on self-application. Most of the code focuses on the emulation of (equi-) recursive types via iso-recursive data types. We also explore equi-recursive types, explicit ones and those inherent in delimited continuations underlying mutations or exceptions. Along the way we describe two lesser-known expressions of the fixpoint combinator, via mutations (see `FixReferenceA` in the code) and exceptions.

Using iso-recursive data types to write `fix` also works in Haskell. On the other hand, using mutable state or exceptions does not work so well in Haskell -- at least if the goal is to write the pure `fix` rather than the monadic `mfix`. Surprisingly, however, `ST` reference cells let us write the pure `fix`, if we use the lazy `ST` monad. The pure `fix` can also be written with type classes and type families.

References
fixpoints.ml [7K]
The complete, commented OCaml code
The code has been inspired and influenced by Omega implementations written by Julien Signoles. The code was mentioned in a message posted by Jacques Carette on the caml-list on Tue, 22 Nov 2005.

Fix.hs [3K]
Defining the fixpoint combinator in Haskell without the value recursion

## Simplest poly-variadic fixpoint combinators for mutual recursion

A polyvariadic fixpoint combinator expresses mutual recursion, obtaining a mutual least fixed point of several terms. We systematically derive a polyvariadic fixpoint combinator, as the proper lambda-term, without any `ellipsis'. A fixpoint combinator is not just an academic curiosity: it transparently introduces memoization, crucial in dynamic programming and efficient parsing. We develop the polyvariadic fixpoint combinator for Scheme, OCaml and Haskell. The main derivation is in OCaml: with strictness to draw attention to divergence, and types to draw attention to mistakes. Our polyvariadic combinator is notably simpler than those developed by Queinnec and Goldberg.

In the literature a polyvariadic fixpoint combinator is often presented using "...", or ellipsis. For example,

```    (letrec
((f1 e1)
(f2 e2)
...
(fn en)
)
e)
```
is schematically represented via the explicit polyvariate fixpoint (denoted as `Y*` below) as
```    (let ((fs (Y* (lambda (f1 f2 ... fn) e1) ... (lambda (f1 f2 ... fn) en))))
(apply (lambda (f1 f2 ... fn) e) fs))
```
Surely the mutual fixed-point combinator can be written as a proper lambda-term, without resorting to the meta-language operation, ellipsis. We demonstrate such a lambda term, the simplest so far.

We start by recalling how ordinary general recursion is represented via an ordinary fixpoint combinator. A recursive function like `fact`:

```    let rec fact : int -> int = fun n -> if n <= 0 then 1 else n * fact (n-1)
```
first has to be re-written in the so-called `open recursion style', with the explicit argument for the recursive occurrence:
```    let open_fact : (int -> int) -> int -> int = fun self n ->
if n <= 0 then 1 else n * self (n-1)
```

This function is no longer recursive. The fixpoint combinator

```    val fix : (('a->'b) -> ('a->'b)) -> ('a->'b)
```
then ties the recursive knot:
```    fix open_fact;;
(* - : int -> int = <fun> *)
fix open_fact 5;;
(* - : int = 120 *)
```

We now generalize to mutual recursion, on the familiar example of determining if a natural number is even or odd:

```    let rec even : int -> bool = fun n -> n = 0  || odd (n-1)
and odd  : int -> bool = fun n -> n <> 0 && even (n-1)
```
The definition looks like two clauses of a single function, which we call `evod`:
```    type idx = int
let rec evod : idx -> int -> bool = function
| 0 -> fun n -> n = 0  || evod 1 (n-1)
| 1 -> fun n -> n <> 0 && evod 0 (n-1)
let even = evod 0 and odd = evod 1
```
The first argument (of type `idx`, integer for now) indexes the clauses. Since `evod` is an ordinary recursive function, quite like `fact`, we re-write it in the open recursion style
```    let open_evod : ((idx -> int -> bool) as 't) -> 't = fun self -> function
| 0 -> fun n -> n = 0 || self 1 (n-1)
| 1 -> fun n -> n <> 0 && self 0 (n-1)
```
and then apply the ordinary fixpoint combinator:
```    let evod = fix open_evod
(* val evod : idx -> int -> bool = <fun> *)
let even = evod 0 and odd = evod 1
(* val even : int -> bool = <fun> *)
(* val odd : int -> bool = <fun> *)
```

We thus obtain that the polyvariadic fixpoint combinator

```    let fix_poly_v1 : ('t ->'t) -> ((idx -> 'a -> 'b) as 't) = fix
```
is just an instance of the ordinary fixpoint combinator. It seems we are done. However, the interface of `fix_poly_v1` is cumbersome, requiring a function like `open_evod` with the explicitly indexed clauses. Recursive applications have to apply the index, which is error-prone and inefficient. There is another problem: all mutually recursive clauses are restricted to be of the same type. We lift the latter restriction at the end.

We now derive the mutual fixpoint combinator with a better interface and efficiency. We wish the fixpoint combinator took a list of functions in the open recursion style, returning the list of functions with their knots tied-up. Ideally, the running example should look like

```    let [even;odd] =
let open_even [even;odd] = fun n -> n = 0  || odd (n-1)
and open_odd  [even;odd] = fun n -> n <> 0 && even (n-1)
in fix_poly [open_even;open_odd]
```
Hence the polyvariadic fixpoint combinator should have the following type
```    val fix_poly : (('a -> 'b) list -> ('a -> 'b)) list -> ('a -> 'b) list
```
We develop exactly such combinator. It seems easy since `fix_poly_v1` is straightforward to adapt to the above signature. The key point is that a total function `idx -> t` with the result type `t` and the domain `[0..n-1]` for `idx` is isomorphic to the `n`-element `t list`. Writing out the conversion between the two representations explicitly gives us:
```    let fix_poly_temp : (('a -> 'b) list -> 'a -> 'b) list -> ('a -> 'b) list
= fun l ->
let n = List.length l in
let clause self idx = (List.nth l idx) (List.map self (iota n)) in
List.map (fix_poly_v1 clause) (iota n)
```
where `iota n` produces a list of integers `0` through `n-1`. This combinator has two problems: divergence and inefficiency. The former is easy to fix with the appropriate eta-expansion
```    let fix_poly_v2 : (('a -> 'b) list -> 'a -> 'b) list -> ('a -> 'b) list
= fun l ->
let n = List.length l in
let clause self idx x = (List.nth l idx) (List.map self (iota n)) x in
let tied idx x = fix clause idx x in
List.map tied (iota n)
```
giving us a polyvariadic fixpoint combinator with the desired interface. `List.nth` and `iota` strongly remind of Queinnec's `NfixN2`, described in his book ``LISP In Small Pieces''. However, not only `List.nth` (in Scheme, `list-ref`) is inefficient (indexing a list requires its traversal and hence is not constant time), it is also aesthetically displeasing. Ideally, the list of clauses should be handled as an abstract collection, using only operations like fold or map rather than random-access `List.nth`. It would be easy then to generalize to other collections, such as tuples.

We now improve the efficiency of `fix_poly_v2`, getting rid of `List.nth`. The starting point is the simpler `fix_poly_temp`: we can always fix the divergence later, with eta-expansion. Let `fl` be `fix_poly_temp l` for some appropriate list `l` of length `n` and let `clause` be `fun self idx -> (List.nth l idx)(List.map self (iota n))`. We calculate

```    fl
=== fix_poly_temp l
=== map (fix clause) (iota n)
{fixpoint}
=== map (clause (fix clause)) (iota n)
{inline the first occurrence of clause, beta-reduce}
=== map (fun idx -> List.nth l idx (map (fix clause) (iota n))) (iota n)
{Recall that (map (fix clause) (iota n)) is fix_poly_temp l, which is fl}
=== map (fun idx -> List.nth l idx fl) (iota n)
{beta-expansion}
=== map (fun idx -> (fun li -> li fl) (List.nth l idx)) (iota n)
{Recall, map (f . g) l === map f (map g l), and
map (fun idx -> List.nth l idx) (iota (List.length l)) === l }
=== map (fun li -> li fl) l
```
The result shows that `fix_poly_temp l` is an ordinary fixpoint, of `fun self -> map (fun li -> li self) l`. This expression is immediately usable in Haskell. In OCaml, we have to introduce a few eta-expansions to prevent premature looping.
```    let fix_poly : (('a -> 'b) list -> 'a -> 'b) list -> ('a -> 'b) list
= fun l -> fix (fun self l -> List.map (fun li x -> li (self l) x) l) l
```
This combinator has the desired interface and efficiency. We have achieved our goal.

The combinator `fix_poly` is straightforward to translate into Scheme. After inlining the definition of the ordinary fixpoint combinator and simplifying, we obtain the following expression for the polyvariadic fixpoint combinator. It is notably simpler than the polyvariadic combinators by Queinnec and Goldberg.

```    (define (Y* . l)
((lambda (u) (u u))
(lambda (p)
(map (lambda (li) (lambda x (apply (apply li (p p)) x))) l))))
```
Compared to the OCaml version, the functions to obtain the mutual fixpoint of do not have to have the same number of arguments (the same arity). The accompanying code shows an example.

The combinator `fix_poly` translates to Haskell trivially. Since Haskell is non-strict, no eta-expansions are needed. The result is a one-liner:

```    fix_poly:: [[a]->a] -> [a]
fix_poly fl = fix (\self -> map (\$ self) fl)
where fix f = f (fix f)

test1 = (map iseven [0..5], map isodd [0..5])
where
[iseven, isodd] = fix_poly [fe,fo]
fe [e,o] n = n == 0 || o (n-1)
fo [e,o] n = n /= 0 && e (n-1)
```

The type of `fix_poly` points out the remaining problem: all mutually dependent clauses are restricted to the same type. This is a serious limitation. The type of `fix_poly` has a curious structure, which shows a way out, through the second-order `Functor`:

```    class Functor2 c where
fmap2 :: (forall a. c1 a -> c2 a) -> c c1 -> c c2
```
for collections `c` indexed by a type constructor `c1`. Lists are such collections, and so are tuples:
```    newtype Id a = Id{unId :: a}
newtype P3 a1 a2 a3 c = P3 (c a1, c a1, c a3)
instance Functor2 (P3 a1 a2 a3) where
fmap2 f (P3 (x,y,z)) = (P3 (f x, f y, f z))
```
The general polyvariadic fixpoint combinator takes then the following form:
```    fix_gen_poly:: Functor2 c => c ((->) (c Id)) -> c Id
fix_gen_poly fl = fix (\self -> fmap2 (\x -> Id (x self)) fl)
where fix f = f (fix f)
```
The accompanying code shows an example of its use.

A different way to generalize `fix_poly` for clauses of varying types is to look back to the point where we first introduced indexing of clauses to convert mutual recursion to the ordinary recursion. One may observe then that `idx` does not have to be an integer. It could be any suitable variant type, in particular, GADT. This approach is elaborated in the reference below.

In conclusion: we have developed the simplest to date polyvariadic combinator for mutual fixpoint: `\l -> fix (\self -> map (\$ self) l)`.

Version
The current version is 2002 (Scheme version), 2003 (Haskell version), August 2013 (simple OCaml version)
References
polyvar-Y.scm [6K]
Several examples of using Y* in Scheme

PolyY.hs [2K]
Several examples of `fix_poly` in Haskell

Polyvariadic Y: a mutually least fixpoint combinator for several terms
A message posted on the Haskell Cafe mailing list on Oct 27, 2003.

Generating Mutually Recursive Definitions
The article that fully works out and explains the GADT-based approach to the general polyvariadic fixpoint combinator

Mayer Goldberg: A Variadic Extension of Curry's Fixed-Point Combinator
Higher-Order and Symbolic Computation, v18, N3-4, pp 371-388, 2005

## Fixpoint combinators are infinitely many and recursively-enumerable

We present a simpler proof that in the untyped lambda calculus there are infinitely many fixpoint combinators and they are all effectively countable, that is, recursively enumerable. We implement the proof as a Haskell program that produces all fixpoint combinators, one-by-one. The proof is a simpler version of that by Mayer Goldberg (2005). It is based on the well-known proof that the set of all halting programs is recursively enumerable (or, `listable'). The proof also relies on the fact that the beta-eta equality of two lambda-terms can be confirmed in finite time.

As common (see Goldberg 2005 for references), we call a closed lambda-term `F` a fixpoint combinator if the following equation holds for any term `e`:

```    F e =*= e (F e)
```
where `(=*=)` is the beta-eta equality: the smallest congruence that includes beta- and eta-reductions. The well-known `Y` combinator is one example of the fixpoint combinator. There are infinitely many more. For instance, if `F` is a fixpoint combinator, `G = \f g e x -> e (f (g e))` and `(.)` is the functional composition, then `F . F (G F)` is a fixpoint combinator, not equal to `F`.

The set of fixpoint combinators, albeit infinite, is effectively countable, or recursively enumerable. There exists an effective process, a program, that produces all fixpoint combinators one by one, without duplicates.

For the proof, we take the inspiration from the well-known demonstration that the set of all halting programs (or, all normalizable lambda-terms) is recursively enumerable. This fact does not imply that termination or normalization are decidable since the complement set -- of non-terminating terms -- is not recursively enumerable. The recursive enumerability of normalizable terms can be demonstrated as a simple non-deterministic program:

```    list_normalizable :: MonadPlus m => m Exp
list_normalizable = do
term <- a_term
check_normalization term
return term

check_normalization :: MonadPlus m => Exp -> m ()
check_normalization term =
check_NF term `mplus` (reduce_one_step term >>= check_normalization)
where
check_NF term = if is_normal_form term then return () else mzero
```
Here `a_term :: MonadPlus m => m Exp` non-deterministically generates a lambda-term (represented as a value of the data type `Exp`). One can always write such a procedure since the set of all lambda-terms is recursively enumerable. The total function `is_normal_form :: Exp -> Bool` tests if a term is in normal form, and a function `reduce_one_step :: MonadPlus m => Exp -> m Exp` non-deterministically picks a redex and contracts it, returning the reduced term. Both operations can be done in finite time. The decision tree for the `list_normalizable` program is infinite. Normalizable terms are at the leaves of the tree, at a finite distance from the root: By definition, a term is normalizable if it can be reduced to a normal form in a finite number of steps. A complete search procedure (such as breadth-first search) will traverse the tree, listing all leaves in some order.

The second key idea of our proof of the recursive enumerability of fixpoint combinators is that the equality of two lambda-terms can be confirmed in finite time. For example, by using the Church-Rosser theorem: Given two terms `M` and `N`, we non-deterministically apply 0 or more reduction steps to `M` and 0 or more reduction steps to `N`. If `M` and `N` are beta-eta-equal, the results (which are not necessarily normal forms) will be identical modulo alpha-renaming. This procedure does not imply that beta-eta-equality is decidable since the disequality of terms cannot be, in general, established in finite time. Putting these facts together, we obtain the proof: non-deterministically generate a closed term `F`, and check that `F e` is beta-eta-equal to `e (F e)` where `e` is a fresh variable.

The enclosed code is the complete proof -- the program that produces all fixpoint combinators one-by-one. Here is the key part:

```    list_fix :: MonadPlusOnce m => m Exp
list_fix = do
term <- a_term
let fixe = A term e
once \$ check_equal fixe (A e fixe)
return term
```

As before, `a_term` non-deterministically picks a lambda-term, in De Bruijn notation. The function `check_equal :: MonadPlus m => Exp -> Exp -> m ()` checks if two terms are beta-eta equal (by checking the congruence, rather than using Church-Rosser theorem). Two terms may be equal in more than one way; any one way is sufficient. The search combinator `once` prunes the further, redundant search once the equality has been confirmed.

References
Mayer Goldberg: On the Recursive Enumerability of Fixed-Point Combinators
BRICS Report RS-05-1, University of Aarhus
<http://www.brics.dk/RS/05/1/BRICS-RS-05-1.pdf>

EnumFix.hs [12K]
Enumerating all fixpoint combinators

## Self-application and recursion: the U combinator

The familiar applicative fixpoint combinator, suitable for call-by-value languages, is quite a mouthful:
```    (define (Y f)
((lambda (u) (u u))
(lambda (p) (lambda (x) ((f (p p)) x)))))
```
In contrast, the self-application combinator, typically called `delta`, expresses the explicit fixpoint quite more concisely:
```    (define delta (lambda (u) (u u)))

(define (fact-nr self)   ; non-recursive!
(lambda (n) (if (zero? n) 1 (* n ((self self) (- n 1))))))

((delta fact-nr) 5) ; ==> 120
```

We now describe the simple inter-relationship between the `Y` combinator and the self-application combinator that we call `U`:

```    (define U (lambda (f) (lambda (x) (f (x x)))))
```
Clearly, `delta` is a particular case of `U`, namely, `U` applied to the identity function. The combinator `U` can express a fixpoint of any term. Indeed, keeping in mind the reduction rule of the combinator
```    U f x ==> f (x x)
```
we immediately see that for any term `e`:
```    (U e) (U e) ==>  e ((U e) (U e))
```
Furthermore, `(U e) (U e)` is the reduction of `S U U e`, where `S` is one of the basic combinators. We thus obtain that `S U U` is a fixpoint combinator. In fact, it is beta-eta-equal to `Y`.

The combinator `U` can be expressed in terms of the basic `S`, `K` and `I` combinators;

```    U = Q (S I I)
```
where `Q` is the composition with the flipped arguments, also expressible via `SKI`.

Indeed, keeping in mind the re-writing rules of the combinator calculus

```    S f g x  ==> f x (g x)
K c x    ==> c
I x      ==> x
Q f g x  ==> g (f x)
```
we see
```    U f x = Q (S I I) f x ==> f (S I I x) ==> f (I x (I x)) ==> f (x x)
```

Jon Fairbairn pointed out in a private message that the above explanation is essentially the insight behind Turing's fixed point combinator.

Version
The current version is October 1999, see comp.lang.scheme, comp.lang.functional