Xref: utzoo comp.lang.functional:727 comp.theory:1788
Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!samsung!spool.mu.edu!munnari.oz.au!brolga!uqcspe!cs.uq.oz.au!farrell
From: farrell@cs.uq.oz.au (Friendless)
Newsgroups: comp.lang.functional,comp.theory
Subject: Re: Applications for lazy functional languages
Keywords: strict
Message-ID: <618@uqcspe.cs.uq.oz.au>
Date: 8 Apr 91 00:50:54 GMT
References: <8413@skye.cs.ed.ac.uk> <6853@rex.cs.tulane.edu> <4705@osc.COM> <6922@rex.cs.tulane.edu>
Sender: news@cs.uq.oz.au
Reply-To: farrell@cs.uq.oz.au
Followup-To: comp.lang.functional
Distribution: comp
Lines: 12

In <6922@rex.cs.tulane.edu> fs@rex.cs.tulane.edu (Frank Silbermann) writes:
>How does the _theory_ of typed lambda calculus deal with this issue?

  Typed or not, lambda calculus expressions are strict in at most one
argument, which you can identify by calculating the head normal form, the
answer being the head variable. For typed lambda calculus, there is always a
head normal form, proved by Barendregt in his book. For more information on
strictness of the pure lambda calculus, see the paper by Prateek Mishra in
Information Processing Letters in 1988.


John