fs@rex.cs.tulane.edu (Frank Silbermann) (04/08/91)
>In article <6853@rex.cs.tulane.edu> fs@caesar.cs.tulane.edu (Frank Silbermann) >writes: >>By the way, does the _formal_ theory of typed lambda calculus accept >>constructor-based primitive functions defined via rewrite-rules? >>For example, in the lambda-notation of denotational semantics, >>one can _force_ any primitive function `f: A->B' to be strict >>simply by defining f(BOT_A) = BOT_B. In article <4705@osc.COM> jgk@osc.COM (Joe Keane) writes: > It's not that simple. In general you can't define f(BOT_A). David Schmidt seems to do this in his book, _Denotational Semantics_ (of course, any such definition must maintain continuity). > If don't want to be fully lazy you can make it less determined. > You can never make it more determined. > Really this is a semantic argument. > I would say that strictness is a property > of specific strict primitive combinators > that force evaluation of some expression, > (even if you don't use its value), > rather than something you can specify in your type system. Strictness means only that bottom is mapped to bottom, nothing more. I did not ask whether this could be made part of the _type system_. I asked whether this can be taken care of within the context of typed lambda _calculus_. Certainly there must be more to typed lambda calculus than type theory alone. If typed lambda calculus is to be the basis of functional programming, then its expressions must be executable/simplifiable. If the lambda calculus permits primitive combinators (e.g. strict ones), then the calculus must take into account some sort of rewriting mechanism to simplify expressions using the primitive combinators. How does the _theory_ of typed lambda calculus deal with this issue? Frank Silbermann fs@cs.tulane.edu Tulane University New Orleans, Louisiana USA
farrell@cs.uq.oz.au (Friendless) (04/08/91)
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