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.
Fix.hs [3K]
Defining the fixpoint combinator in Haskell without the value recursion
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).
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
... and are indexed by the number
of clauses, which has to be known
by the time the schema is instantiated.
We demonstrate that if the number of clauses (functions to fixpoint) is known, our polyvariadic combinator can be mechanically specialized -- obtaining the result analogous to that of instantiating the term schema, but in the typed and strict setting. The polyvariadic fixpoint combinator is hence more general, applying to both statically known and unknown number of clauses. As before, our development is in OCaml: with strictness to draw attention to divergence, and types to draw attention to mistakes.
Recall, the simplest so far polyvariadic fixpoint combinator described earlier is (in OCaml):
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
(The outer eta-expansion is needed to avoid the monomorphism restriction.)
It is a proper OCaml term, taking the list of ('a -> 'b) list -> ('a -> 'b) functions (clauses) and returning the list of their mutual
fixpoints. As befits a strict language such as OCaml, the fixpoint
combinator is applicative: the fixpoints must be 'a->'b function
values. The number of clauses (functions to fixpoint) is arbitrary and
not statically known. Here, fix is the ordinary applicative
fix-point combinator:
let rec fix : (('a -> 'b) -> ('a -> 'b)) -> ('a -> 'b) = fun f x ->
f (fun x -> fix f x) x
On the other hand, what one often sees in the literature is
tieₙ = λa.fix(λw. a (w λe₁...eₙ. e₁) ... (w λe₁...eₙ. eₙ))to be used as
tieₙ (λe₁...eₙw. w B₁ ... Bₙ) (λe₁...eₙ. A)to obtain the least mutual fixpoint of the clauses
B₁ ... Bₙ
each of which may use e₁ ... eₙ for mutual self-reference.
The fixpoints are then passed as arguments to λe₁ ... eₙ. A.
This definition is taken from Ramsdell's paper
(changing greek identifiers into
latin ones: unlike Ramsdell, we work in a typed setting,
reserving greek letters for type variables and Latin letters for term
variables.) We must stress that tieₙ is neither typed nor strict.
We also stress that B₁ ... Bₙ are open.
The tieₙ definition is schematic, as betrayed by the ellipsis
`...', the meta-term notation. Hence tieₙ defines not a single term
but a family of terms: a term for each particular n.
It contrast, fix_poly is generic: it defines the single
term that can deal with an arbitrary number of clauses.
Since tieₙ is a schema rather than a term, before use it
must first be instantiated to a particular number
of clauses, say 3:
tie₃ = λa.fix(λw. a (w λe₁e₂e₃. e₁) (w λe₁e₂e₃. e₂) (w λe₁e₂e₃. e₃))This is now a proper term, with no ellipsis.
One may argue that although fix_poly is intellectually satisfying,
tieₙ is more practically useful. Even as the programmer may define
an arbitrary number of mutually recursive definitions, once the
program is finished and submitted to the compiler, the number of
mutually recursive definitions becomes fixed and known. Compiler can
then instantiate tieₙ with that number, obtaining a specialized
fixpoint combinator, which is more efficient than the generic
fix_poly. Indeed,
comparing tie₃ with fix_poly, we see the former has no lists, no
map -- nothing but lambda-abstractions and applications.
We now demonstrate that a compiler may as well
specialize fix_poly instead -- with the additional benefit of
using the result in typed and strict languages.
We start by specializing fix_poly to the list of three clauses:
let fix3 : (('a -> 'b) list -> 'a -> 'b) list -> ('a -> 'b) list = fun l ->
fix (fun self ([i1;i2;i3] as l) ->
List.map (fun li x -> li (self l) x) [i1;i2;i3]) l
Since the structure of the list is known (although the
elements aren't), the mapping may be performed right away:
let fix3 : (('a -> 'b) list -> 'a -> 'b) list -> ('a -> 'b) list = fun l ->
fix (fun self ([i1;i2;i3] as l) ->
[(fun x -> i1 (self l) x);
(fun x -> i2 (self l) x);
(fun x -> i3 (self l) x)]) l
The list of three elements can be converted to a tuple: triple.
let fix3 = fun l ->
fix (fun self ((i1,i2,i3) as l) ->
((fun x -> i1 (self l) x),
(fun x -> i2 (self l) x),
(fun x -> i3 (self l) x))) l
The inferred type is quite a mouthful, although of clear structure
val fix3 :
(('a -> 'b) * ('c -> 'd) * ('e -> 'f) -> 'a -> 'b) *
(('a -> 'b) * ('c -> 'd) * ('e -> 'f) -> 'c -> 'd) *
(('a -> 'b) * ('c -> 'd) * ('e -> 'f) -> 'e -> 'f) ->
('a -> 'b) * ('c -> 'd) * ('e -> 'f) = <fun>
The conversion to triple gained us generality: the clauses no longer
have to have the same type. Here is a usage example:
let (three0,three1,three2) = fix3 (
(fun (three0,three1,three2) x -> x = 0 || three2 (x-1)),
(fun (three0,three1,three2) x -> x = 1 || (x > 0 && three0 (x-1))),
(fun (three0,three1,three2) x -> x = 2 || (x > 0 && three1 (x-1)))) in
three1 7
We could stop already: fix3 has no lists or mapping. It still has
tuples, though, which make using fix3 more inconvenient than
necessary. Some tuples are straightforward to eliminate, via
currying:
let fix3 = fun l ->
fix (fun self i1 i2 i3 ->
((fun x -> i1 (self i1 i2 i3) x),
(fun x -> i2 (self i1 i2 i3) x),
(fun x -> i3 (self i1 i2 i3) x))) l
The thrice-occurring (self i1 i2 i3) asks to be let-bound and shared. If we
try, however, attempting to use fix3 would diverge. The reader is
encouraged to ponder why. Mainly, there are still tuples left, to
construct and deconstruct on each recursive call.
Boehm-Berarducci encoding let us represent tuples by pure lambda-terms. It however requires first-class polymorphism: System F.
triple = Λαβγ.λ(x:α)(y:β)(z:γ).Λω.λ(w:α→β→γ→ω).w x y zOCaml does support first-class polymorphism, but naturally requires types annotations (and a record to attach these annotations to).
type ('a,'b,'c) tup3 = {s: 'w. ('a -> 'b -> 'c -> 'w) -> 'w} [@@unpack]
Incidentally, the record construction
{s = e} corresponds to Λα.e and the projection e.s to
type application. The replacement of tuples with their encoding is
straightforward:
let fix3 = fun l ->
fix (fun self i1 i2 i3 ->
{s= fun w -> w
(fun x -> i1 (self i1 i2 i3) x)
(fun x -> i2 (self i1 i2 i3) x)
(fun x -> i3 (self i1 i2 i3) x)}) l
Although tuples, as a data structures, are gone, the clauses still
receive the tuple (now encoded) of mutual fixpoints. Luckily,
currying it out has become easy:
let fix3 = fun l ->
fix (fun self i1 i2 i3 ->
{s= fun w -> w
(fun x -> (self i1 i2 i3).s (fun e1 e2 e3 -> i1 e1 e2 e3 x))
(fun x -> (self i1 i2 i3).s (fun e1 e2 e3 -> i2 e1 e2 e3 x))
(fun x -> (self i1 i2 i3).s (fun e1 e2 e3 -> i3 e1 e2 e3 x))}) l
The inferred type confirms:
val fix3 :
(('a -> 'b) -> ('c -> 'd) -> ('e -> 'f) -> 'a -> 'b) ->
(('a -> 'b) -> ('c -> 'd) -> ('e -> 'f) -> 'c -> 'd) ->
(('a -> 'b) -> ('c -> 'd) -> ('e -> 'f) -> 'e -> 'f) ->
('a -> 'b, 'c -> 'd, 'e -> 'f) tup3 = <fun>
We have obtained the three-variadic fixpoint combinator that is a pure
lambda term which is relatively easy to use. Its expression is an
eyesore, however. Surely repetition could be curbed. It can indeed:
let fix3 = fun l ->
fix (fun self i1 i2 i3 ->
let sel i x = (self i1 i2 i3).s (fun e1 e2 e3 -> i e1 e2 e3 x) in
{s= fun w -> w (sel i1) (sel i2) (sel i3)}) l
The inferred type is the same. Here is how it can be used:
(fix3
(fun three0 three1 three2 x -> x = 0 || three2 (x-1))
(fun three0 three1 three2 x -> x = 1 || (x > 0 && three0 (x-1)))
(fun three0 three1 three2 x -> x = 2 || (x > 0 && three1 (x-1)))).s @@
fun three0 three1 three2 -> three1 7
The fix3 combinator is trivial to make schematic:
fixₙ = fun l ->
fix (fun self i₁ ... ->
let sel i x = (self i₁ ...).s (fun i₁ ... -> i i₁ ... x) in
{s= fun w -> w (sel i₁) ...}) l
One may see the similarity with tieₙ. The difference, aside from
strictness and typing, is that fix_n takes closed (that is,
lambda-lifted) clauses. The schema tieₙ may be converted to take
take closed clauses as well, at the cost of introducing many
applications.
I thank John Tromp for pointing out Ramsdell's paper to me.
Appendix. The specialized fix3 derived in the article and tie₃ are
not really compatible: the former is meant for closed clauses whereas
the latter for open ones. Although closed, lambda-lifted clauses
are better for the compiler (since the compiler would probably do
lambda-lifting anyway), they are less elegant, if nothing
else. The last example is a good illustration:
(fix3
(fun three0 three1 three2 x -> x = 0 || three2 (x-1))
(fun three0 three1 three2 x -> x = 1 || (x > 0 && three0 (x-1)))
(fun three0 three1 three2 x -> x = 2 || (x > 0 && three1 (x-1)))).s @@
fun three0 three1 three2 -> three1 7
All three clauses have a common prefix: fun three0 three1 three2. Wouldn't it be nice to factor it out?
Let's go back to the first tupling example, repeated below:
let fix3 = fun l ->
fix (fun self ((i1,i2,i3) as l) ->
((fun x -> i1 (self l) x),
(fun x -> i2 (self l) x),
(fun x -> i3 (self l) x))) l
Here, l is the triple of functions of the form
((fun l x -> e1),(fun l x -> e2),(fun l x -> e3))The three functions have the common argument, which is also a triple. It can be factored out, as
fun tup -> (fun x -> e1), (fun x -> e2), (fun x -> e3)The factored-out
l is easily convertible to the original one, which
then can be substituted to fix3:
let t31 (x,y,z) = x and t32 (x,y,z) = y and t33 (x,y,z) = z
let fix3o = fun l ->
fix (fun self l ->
let i1 = fun tup -> t31 (l tup) in
let i2 = fun tup -> t32 (l tup) in
let i3 = fun tup -> t33 (l tup) in
((fun x -> i1 (self l) x),
(fun x -> i2 (self l) x),
(fun x -> i3 (self l) x))) l
The inferred type shows the factored out triple:
val fix3o :
(('a -> 'b) * ('c -> 'd) * ('e -> 'f) ->
('a -> 'b) * ('c -> 'd) * ('e -> 'f)) ->
('a -> 'b) * ('c -> 'd) * ('e -> 'f) = <fun>
The rest is inlining of let-definitions, converting to
Boehm-Berarducci encoding, currying and abstracting out similarities,
as explained above:
see the accompanying code. The result is:
let fix3o = fun l ->
fix (fun self l ->
let sel p x = (self l).s (fun e1 e2 e3 -> (l e1 e2 e3).s p x) in
{s= fun w ->
w (sel (fun e1 e2 e3 -> e1))
(sel (fun e1 e2 e3 -> e2))
(sel (fun e1 e2 e3 -> e3))}) l
to be used as
(fix3o (fun three0 three1 three2 ->
{s=fun w -> w
(fun x -> x = 0 || three2 (x-1))
(fun x -> x = 1 || (x > 0 && three0 (x-1)))
(fun x -> x = 2 || (x > 0 && three1 (x-1)))})).s @@
fun three0 three1 three2 -> three1 7
John D. Ramsdell. The Alonzo Functional Programming Language.
SIGPLAN Notices, 1989, Vol 24, N9, pp.152-157.
doi:10.1145/68127.68139
The language itself is quite unremarkable: a non-strict version of
Scheme, which, by author's admission, requires research to produce
an efficient implementation.
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.
EnumFix.hs [12K]
Enumerating all fixpoint combinators
(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.