🚀 go-pugleaf

fs@rex.cs.tulane.edu (Frank Silbermann) writes:


>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!
>So, please explain again why you don't believe
>this domain D =~ (D->D) is not a fully abstract model
>of the pure untyped lambda calculus.

> ...

>In programming languages, we usually assume the existence of
>base atomic values (e.g. integers, booleans or other atoms),
>so D =~ (D->D) is rarely the appropriate domain.
>Therefore, the pure-untyped-lambda-calculus
>is not the best basis for programming language design.
>Mulmuley and Plotkin use typed lambda calculi,
>whose fully abstract models (their corresponding domains)
>contain the kinds of values desired.

Thanks for pointing out the need for a Bool type to make
parallel-or etc. meaningful. The only thing that still
troubles me is that, of course, Ints, Bools, etc. can be
simulated in lambda-calc. without any sort of complicated
interpretation e.g. ``1'' can be ``declared'' in lambda-calc
as

	(lam f.(lam x.f x))

Likewise true and false as respectively

	(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

	parallel-or T ? ->> T
	parallel-or ? T ->> T
	parallel-or F F ->> F

where ? means anything (incl ``bottom''), from existing in the domain?

Thanks in advance for your help

Paul Bailes