🚀 go-pugleaf

>>		The Scott domain D described by:
>>				D =~ (Int + Bools + D->D )_bot
>>		does indeed contain a (curried) parallel-OR.
>>		However, the Scott domain D described by:
>>				D =~ (D->D)
>>		contains no Boolean functions at all.  In fact,
>>		this domain lacks even the base Boolean values TRUE and FALSE!

Adapted from <3859@moondance.cs.uq.oz.au> by paul@batserver.cs.uq.oz.au:

>	Thanks for pointing out the need for a Bool type to make
>	parallel-or etc. meaningful.  Nevertheless, Ints, Bools, etc.
>	can be simulated in lambda-calc. without any sort of complicated
>	interpretation e.g. ``TRUE'' and ``FALSE'' can be ``declared'' as
>	...
>		(lam x.(lam y. x)) <<called T below>>
>		(lam x.(lam y. y)) <<called F below>>
>
>	These exist in pure, untyped lambda-calc, in the D =~ D->D domain.
>	What's stopping a parallel-or ...?	Paul Bailes

Since the pure untyped lambda calculus is Turing equivalent,
you can indeed simulate any computable function, even parallel-or.
But nobody says it has to be easy!
The dove-tailing required to ensure fairness
(e.g. regularly swapping left and right arguments)
will probably be mucho ugly (and inefficient).
The suggested encodings for TRUE and FALSE were chosen for
their simplicity _under the assumption_ that sequential-or sufficed.

Aside from the difficulties of simulating parallelism,
note that if you erroneously apply your encoding of TRUE to an object,
it will happily compute a value, whereas I would want the result
to be undefined (BOTTOM), or perhaps a special error code.

The right typed lambda calculi will avoid
the need for difficult encodings.
The disadvantage of a more complex system
is that proofs become more complicated.

	Frank Silbermann	fs@rex.cs.tulane.edu