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