Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
To: info-hol@ted.cs.uidaho.edu
Subject: Re: letrec-expressions
In-Reply-To: Your message of "Tue, 25 May 93 10:11:21 +0700." <9305250832.AA08363@ted.cs.uidaho.edu>
Date: Fri, 28 May 93 02:38:53 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:157760:930528013901"@cl.cam.ac.uk>


Klaus Schneider says:

> Let-Expressions in HOL are very readable and convenient and
> moreover they allow a structure sharing which can save exponential
> costs. However, in these expressions do not allow any form of
> recursion. One way to circumvent this is to introduce a fixpoint
> operator which can be used to "unrecursivize" the recursive definition.
> Has anybody done this before or are there other proposals for
> simulation letrec expressions?

This seems a good idea. How about the following analogous development:

  let x = s in t                        letrec x = s in t

                 is surface syntax for

  LET (\x. t) s                         LETREC (\x. t) (@x. x = s)

                 which is equivalent to

  (\x. t) s                             (\x. t) (@x. x = s)

However if this were to work nicely it would be useful to have ways of
automatically unravelling a wide class of recursive definitions, otherwise
these terms could prove very hard to eliminate. Unlike the LET case, this would
involve nontrivial proof. I can't see a clean way of encoding the fact that the
recursion equation is satisfiable.

Incidentally, it's often stated that in functional languages, let-expressions
are just syntax for lambda-expressions. But in SML:

  Standard ML of New Jersey, Version 0.93, February 15, 1993

this isn't true because you can use local polymorphism like this in lets:

  - let val f = fn x:'a => x in (f 1,f true) end;
  val it = (1,true) : int * bool

whereas the corresponding lambda-term won't typecheck:

  - (fn f => (f 1,f true))(fn x:'a => x);
  std_in:3.10-3.21 Error: operator and operand don't agree (tycon mismatch)
    operator domain: int
    operand:         bool
    in expression:
      f true
  std_in:3.1-3.36 Error: operator and operand don't agree (type mismatch)
    operator domain: int -> 'Z
    operand:         'aU -> 'aU
    in expression:
      ((fn f => (<exp>,<exp>))) ((fn <pat> : 'aU => x))

I notice that "Classic" ML has a special case in typechecking to treat the
latter as the former (see Description 5.3.1), so here it works:

  #(\f. (f 1,f true))(\x:*. x);;
  (1, true) : (int # bool)

John.