previous   next   up   top

Many faces of the fixed-point combinator

 


 

Writing the fixed-point combinator in a typed language

In simply typed lambda-calculus, the fix-point combinator can be typed but cannot be expressed and so has to be introduced as a primitive. The self-application combinator \x -> x x cannot even be assigned any simple type. Practical typed languages like OCaml and Haskell have enough features to write the fix-point combinator without resorting to the built-in recursive binding. In fact, one can write the fix-point combinator in these languages in quite a few different ways.

The code below demonstrates all the different ways to express the fully polymorphic fix-point 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 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 fix-point combinator: via mutations (see FixReferenceA in the code) and exceptions.

Some of the ML techniques, such as using iso-recursive data types to define fix, easily transfer to Haskell. The side-effecting approaches (e.g., relying on exceptions) do not work so well if our goal is to write the pure fix, rather than the monadic mfix. Surprisingly, ST reference cells let us write the pure fix, if we use the lazy ST monad. Type classes and type families offer a Haskell-specific way to express the fix-point combinator.

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 fix-point combinator in Haskell without the value recursion

 

Simplest poly-variadic fix-point combinators for mutual recursion

A polyvariadic fix-point combinator expresses mutual recursion, obtaining a mutual least fixed point of several terms. We systematically derive a polyvariadic fix-point combinator, as the proper lambda-term, without any `ellipsis'. A fix-point combinator is not just an academic curiosity: it transparently introduces memoization, crucial in dynamic programming and efficient parsing. We develop the polyvariadic fix-point 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 fix-point combinator is often presented using "...", or ellipsis. For example,

     (letrec
        ((f1 e1)
         (f2 e2)
         ...
         (fn en)
        )
      e)
is schematically represented via the explicit fix-point 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 the ordinary fix-point combinator such as Y. 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 a 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 fix-point 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 fix-point 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 fix-point combinator

     let fix_poly_v1 : ('t ->'t) -> ((idx -> 'a -> 'b) as 't) = fix
is just an instance of the ordinary fix-point 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 that restriction at the end.

We now derive a mutual fix-point combinator with the better interface and efficiency. We wish the fix-point 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 fix-point 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 some 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 fix-point 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 and let clause = 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 clause, beta-reduce}
     === map (fun idx -> List.nth l idx (map (fix clause) (iota n))) (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 (map (fix clause) (iota n))) l
     === {recall what fix_poly_temp l is}
     === map (fun li -> li (fix_poly_temp l)) l

The result shows that fix_poly_temp l is an ordinary fix-point, of fun self -> map (fun li -> li self) l. The result 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 fix-point combinator and simplifying, we obtain the following expression for the polyvariadic fix-point 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 fix-point 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 the 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 fix-point 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.

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

Version
The current version is 2002 (Scheme version), 2003 (Haskell version), August 2013 (simple 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.

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

 

Fix-point combinators are infinitely many and recursively-enumerable

We present a simpler proof that in the untyped lambda-calculus there are infinitely many fix-point combinators and they are all effectively countable, that is, recursively enumerable. We implement the proof as a Haskell program that produces all fix-point 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 fix-point combinator if the following equation holds for any term e:

     F e =*= e (F e)
where (=*=) is the beta-eta equality. That is, two lambda-terms M and N are beta-eta equal iff there exists a term L to which they both reduce in 0 or more steps. Even divergent terms (which have no normal form) can be determined equal. The well-known Y combinator is one example of the fix-point combinator. There are infinitely many more. For instance, if F is a fix-point combinator, so is F . I, where I is the identity and (.) is the functional composition. Less trivially, if F is a fix-point combinator and G = \f g e x -> e (f (g e)), then F . F (G F) is a fix-point combinator.

The set of fix-point combinators, albeit infinite, is effectively countable, or recursively enumerable. There exists an effective process, a program, that produces all fix-point 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 fix-point combinators is that the equality of two lambda-terms can be confirmed in finite time. 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 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 fix-point 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 deBruijn notation. The function check_equal :: MonadPlus m => Exp -> Exp -> m () checks if two terms beta-eta equal. 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 [7K]
Enumerating all fix-point combinators

 

Self-application and recursion: the U combinator

The familiar applicative fix-point 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 fix-point 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 fix-point 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)) 
Since S U U e reduces to (U e) (U e), we obtain a concise expression for the fix-point combinator: S U U. It is easy to see that S U U is beta-eta-equal to the familiar Y.

The combinator U can be expressed in terms of S, K and I: U = S (CSC) (KI), where C = S (KS) K is the composition combinator. 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
     C f g x  ==> f (g x)
we see
     U f x = S (CSC) (KI) f x ==> C S C f (K I f) x ==> S (C f) I x 
     ==> C f 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.


Last updated August 1, 2013

This site's top page is http://okmij.org/ftp/

oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!

Converted from HSXML by HSXML->HTML