Self-application is often an elegant way to introduce recursion, especially in a strict language:
(define (U f) (f f))
It is that simple, especially compared to the more complex expression for the applicative fixpoint combinator. As an example, consider a non-recursive function:
(define (fact-nr f) (lambda (n) (if (zero? n) 1 (* n ((f f) (- n 1))))))and so we can compute
((U fact-nr) 3) ==> 6 ((U fact-nr) 5) ==> 120
Yand other combinators
We will show now that the abstraction
(lambda u (u u))
can indeed express the least fixed point of any term. This
abstraction turns out not only related to the familiar
combinator but convertible to it as well.
We start by noting that
((lambda (u) (u u)) ( (lambda (f) (lambda (x) (f (x x)))) e ))is the least fixed point of an arbitrary term
e. Indeed, the following two lambda-terms:
((lambda (u) (u u)) ( (lambda (f) (lambda (x) (f (x x)))) e )) (e ((lambda (u) (u u)) ( (lambda (f) (lambda (x) (f (x x)))) e )))are inter-convertible: They reduce to an obvious common term, as they should according to Church-Rosser Theorem I.
Let's consider a term
(lambda (f) (lambda (x) (f (x x)))), which we will call a
U combinator. It has the reduction rule
U f x ==> f (x x)With this definition,
S (K (U I)) Uis the Y combinator. Indeed, applying the usual rules of the combinatorial lambda-calculus
S f g x ==> f x (g x) K c x ==> c I x ==> xyields
S (K (U I)) U e ==> U I (U e) ==> (U e) (U e) ==> e ((U e) (U e))which is the least fixed point of a term
e. The Y combinator can be replaced by the U combinator in the SKI-calculus without affecting its power or expressiveness.
(lambda (u) (u u)) discussed earlier is
(U I), or
(S I I). This form of a
fixed-point combinator appears more convenient to deal with in
a (strict) programming language.
Jon Fairbairn pointed out in a private message that the above explanation is essentially the insight behind Turing's fixed point combinator. The latter is briefly mentioned in Chap. 9, Sec. 6, Ex. 7, of
Anthony A. Aaby, ``Introduction to Programming Languages,'' 1996.
The present section is a compilation of two articles posted on comp.lang.scheme, comp.lang.functional newsgroups on Oct 15 and Oct 20, 1999.
In a simply typed lambda-calculus, the fix-point operator can be typed but cannot be expressed and so has to be introduced as a primitive. The self-application combinator cannot even be typed because it requires recursive types.
The following code presents 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
FixReferenceA in the code) and exceptions.
The code has been inspired and influenced by Omega implementations
<http://www.lri.fr/~signoles/prog/misc/lambda.ml.html> by Julien SIGNOLES.
The complete OCaml code with a few comments.
The code was mentioned in a message posted by Jacques Carette on the caml-list on Tue, 22 Nov 2005.
Defining the fix-point combinator in Haskell without the value recursion
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
cells permit defining the pure
fix, if we use
ST. Type classes and type families offer a
Haskell-specific way to write the fix-point combinator.
A polyvariadic fix-point combinator lets us obtain a mutually least fixed point of several terms. The combinator thus expresses mutual recursion, i.e.:
(letrec ((f1 e1) (f2 e2) ... (fn en) ) e)can be schematically represented as
(let ((fs (Y* (lambda (f1 f2 ... fn) e1) ... (lambda (f1 f2 ... fn) en)))) (apply (lambda (f1 f2 ... fn) e) fs))
That expression is not entirely satisfactory because it uses
... . This implies the need for a meta-language operation
-- ellipsis -- to express the mutual fixed point of several
expressions. In the following, we write the polyvariadic fixpoint
combinator in pure Haskell98, without any ellipsis construct.
As a starting point we take a polyvariadic Y written in Scheme. The following expression is different from the one by Christian Queinnec and Mayer Goldberg. Our combinator is derived by systematic simplifications:
(define (Y* . fl) (map (lambda (f) (f)) ((lambda (x) (x x)) (lambda (p) (map (lambda (f) (lambda () (apply f (map (lambda (ff) (lambda y (apply (ff) y))) (p p) )))) fl)))))
Its translation to Haskell couldn't be any simpler due to the non-strict nature of Haskell:
fix':: [[a->b]->a->b] -> [a->b] fix' fl = self_apply (\pp -> map ($ pp) fl) self_apply f = f g where g = f gThat's it. Here are a few examples. The common odd-even example:
test1 = (map iseven [0,1,2,3,4,5], map isodd [0,1,2,3,4,5]) where [iseven, isodd] = fix' [fe,fo] fe [e,o] x = x == 0 || o (x-1) fo [e,o] x = x /= 0 && e (x-1)A more involved example of three mutually-recursive functions:
test2 = map (\f -> map f [0,1,2,3,4,5,6,7,8,9,10,11]) fs where fs= fix' [\[triple,triple1,triple2] x-> x==0 || triple2 (x-1), \[triple,triple1,triple2] x-> (x/=0)&&((x==1)|| triple (x-1)), \[triple,triple1,triple2] x-> (x==2)||((x>2)&& triple1 (x-1))]
This section is based on a message Polyvariadic Y: a mutually least fixpoint combinator for several terms posted on the Haskell Cafe mailing list on Oct 27, 2003.
Y overriding self-application
Self-application as the fixpoint of
Self-quoting fix-points: Quines, in Scheme and MetaOCaml
This site's top page is http://okmij.org/ftp/
Converted from SXML by SXML->HTML