Return-Path: <kfoury@cs.bu.edu> Received: from cs.bu.edu (cs [128.197.12.2]) by cs3.bu.edu (8.12.11/8.12.11) with ESMTP id i9FFX6WF014372; Fri, 15 Oct 2004 11:33:06 -0400 Received: from cs.bu.edu (kfoury@fiddle [128.197.10.114]) (authenticated bits=0) by cs.bu.edu (8.12.2/8.12.2) with ESMTP id i9FFX3dF021553; Fri, 15 Oct 2004 11:33:03 -0400 (EDT) Sender: kfoury@cs.bu.edu Message-ID: <416FEDA7.25EDDEDB@cs.bu.edu> Date: Fri, 15 Oct 2004 11:32:55 -0400 From: "Assaf J. Kfoury" <kfoury@cs.bu.edu> Organization: Boston University X-Mailer: Mozilla 4.78 [en] (X11; U; SunOS 5.8 sun4u) X-Accept-Language: en To: Hsueh-Szu Yang <alvin@cs.bu.edu> CC: cs520@cs.bu.edu Subject: Re: A question about fix point function References: <Pine.SOL.4.20.0410151110190.18566-100000@csa.bu.edu> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Spam-HitLevel: X-Spam-DCC: dcc.uncw.edu: cs3.bu.edu 1201; Body=2 Fuz1=2 Fuz2=2 X-Spam-Checker-Version: SpamAssassin 3.0.0 (2004-09-13) on cs3.bu.edu X-Spam-Level: X-Spam-Status: No, score=-3.2 required=10.0 tests=ALL_TRUSTED,AWL,BAYES_00 autolearn=ham version=3.0.0 X-Spam-Pyzor: Reported 0 times. Status: X-Mozilla-Status: 8011 X-Mozilla-Status2: 00000000 X-UIDL: 411f69ec00001394
No fixed-point combinator is typable. All such
combinators include a self-application of the
form (x x) somewhere, which is not typable
in a system of simple types (as well as in most
other type systems).
In an untyped programming language, we can
use fixed-point combinators to define recursively
defined functions. See [Pierce, pp 65-66].
In SML, OCaml, and other strongly-typed languages
we cannot use fixed-point combinators, because they
are not typable. But we need to do recursion (or some
form of repetitive computation). So, instead, we introduce
a new constructor in the language, typically called "fix",
which will simulate recursion. See [Pierce, Section 11.11].
Note that "fix" is NOT a name for any of the fixed-point
combinators, but is a constructor (or reserved symbol)
that is used in a particular way.
I hope this answers your question.
Assaf
Hsueh-Szu Yang wrote:
> Hi Professor,
>
> Is it possible to define a fix point function by using a typeable
> language, such as OCaml ? According to the book, the fix point function
> is:
>
> fix = lambda f . (lambda x. f( lambda y . x x y))
> (lambda x. f( lambda y . x x y));
>
> However, the term "x x" in non-typeable. So, I am wondering if we can
> define such a function in a typeable language?
>
> Thanks,
> Hsueh-Szu
This archive was generated by hypermail 2b29 : Fri Nov 19 2004 - 17:00:43 EST