.. _RecursiveFunctions:
.. raw:: html
.. |--| unicode:: U+2013 .. en dash
.. |---| unicode:: U+2014 .. em dash, trimming surrounding whitespace
:trim:
.. This file is part of the OpenDSA eTextbook project. See
.. http://algoviz.org/OpenDSA for more details.
.. Copyright (c) 2012-13 by the OpenDSA Project Contributors, and
.. distributed under an MIT open source license.
.. avmetadata::
:author: David Furcy and Tom Naps
Recursive Functions
===================
The Y Fixed-point Combinator
----------------------------
To turn the :math:`\lambda` calculus into a "real" programming
language, we need to be able to manipulate, we saw in the previous
section that we could appropriately define boolean constants (true,
false), conditionals (if-then-else), logical operators (and, or, not),
integers (0, 1, 2, 3, etc.), and arithmetic operators (:math:`+`,
:math:`-`, etc.).
However, one thing is missing. We still need to be able to define
recursive functions (factorial, etc.). But to recur, we need a "name"
by which we can refer to the function we are creating within the
function we are creating. And the :math:`\lambda` calculus does not
give us global names. Instead we only have a variable that represents
the parameter in a function abstraction. So is there a way out of
this dilemma? The answer is "yes", and it's called a **fixed point
combinator**.
For any :math:`f` and :math:`x`, if :math:`f(x) = x` then :math:`x` is
called a **fixed point** of the function :math:`f`.
Examples to consider when the functions are functions of real numbers:
#. Can you find one or more fixed points for the function
:math:`f(t) = t^2`?
#. Can you find one or more fixed points for the function
:math:`f(t) = 1`?
#. Can you find one or more fixed points for the function
:math:`f(t) = t+1`?
When we are dealing with functions of real numbers, the "algorithm" to
find a fixed point to solve the equation :math:`f(x) = x`.
If a solution can be found, the function has a fixed point; otherwise it doesn't.
fixed point of any numerical function?
Is there a similar technique to find the fixed point of any
:math:`\lambda` calculus function? Consider a function that we call :math:`Y`
for historical reasons. It is defined as follows:
.. math:: Y = \lambda h.(\lambda x.(h \; (x \; x)) \lambda x.(h \; (x \; x)))
:math:`Y` will find the *fixed point* of any function F. That is, for any
function F, :math:`(F \; (Y \; F)) = (Y \; F)`. To see this, note that the substitution dictated by
:math:`\beta` reduction leads us to:
.. math:: (Y \; F) = (\lambda h.(\lambda x.(h \; (x \; x)) \; \lambda x.(h \; (x \; x))) \; F) = (\lambda x.(F \; (x \; x)) \; \lambda x.(F \; (x \; x))) = (F \; (\lambda x.(F \; (x \; x)) \; \lambda x.(F \; (x \;x)))) = (F \; (Y \; F))
Now using the IF-THEN-ELSE, MULT, ISZERO, and PRED functions that were defined within the :math:`\lambda` calculus in the previous section, we can define a new function:
.. math:: \lambda g. \lambda n.(IF \; (ISZERO \; n) \; THEN \; 1 \; ELSE \; (MULT \; n \; (g \; (PRED \; n))))
This new function resembles what we would normally think of as a
recursively defined factorial function *except* it uses a parameter
:math:`g` instead of a globally defined name :math:`g`. Hence it is a
valid definition in the :math:`\lambda` calculus. Although valid, it
is also unfortunately not a recursive factorial function. The amazing thing, however, is that, if we apply :math:`Y` to this function, that is:
.. math:: (Y \; \lambda g. \lambda n.(IF \; (ISZERO \; n) \; THEN \; 1 \; ELSE \; (MULT \; n \; (g \; (PRED \; n)))))
we get the factorial function. It may take awhile to convince yourself of this. Try carrying out the :math:`\beta` reductions that would come into play when
.. math:: ((Y \; \lambda g. \lambda n.(IF \; (ISZERO \; n) \; THEN \; 1 \; ELSE \; (MULT \; n \; (g \; (PRED \; n))))) \; THREE)
is evaluated, and you should see how the Church numeral :math:`SIX` is eventually produced.
Identifying Fixed Point Combinators
-----------------------------------
Although the function :math:`Y` defined above is a famous fixed-point combinator, there are also many other fixed-point combinators, that is, functions :math:`Z` with the property that:
.. math:: (F \; (Z \; F)) = (Z \; F)
for all functions :math:`F`.
This problem will give you practice with identifying other fixed-point combinators.
To reduce syntactic clutter in this problem, we will take some
shortcuts in writing :math:`\lambda` expressions. First, we will drop
all but the first :math:`\lambda` and all but the last dot for
(curried) functions with two or more parameters. So, for example, we
will use:
.. math::
\lambda abcd.E
as an abbreviation for:
.. math::
\lambda a.\!\lambda b.\!\lambda c.\!\lambda d.E
Second, to cut down on parentheses, we will use :math:`(u\ v\ w\ x\ y\
z)` as an abbreviation for :math:`(((((u\ v)\ w)\ x)\ y)\ z)`. In
essence, we are making function application left-associative. **This
notation is to be used only for this review problem. Do NOT use it
for any assignments, exams, or other review problems.**
.. avembed:: Exercises/PL/FixedPointCombinators.html ka
:module: RecursiveFunctions
:points: 1.0
:required: True
:threshold: 3
:exer_opts: JXOP-debug=true&JOP-lang=en&JXOP-code=java_generic
:long_name: Identifying Fixed Point Combinators