🚀 go-pugleaf

>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