Parallel or

Every (imperative) programmer knows the usefulness of a shortcircuiting or operation, that is, a binary operation that doesn't evaluate it's second argument if the first one is True. To a functional programmer this is only natural: the function or is lazy in it's second argument.

> or True  _ = True
> or False x = x

Wouldn't it be nice to have a parallel or that evaluates to True if either of it's arguments is True. That is, a function por satisfying

> por :: Bool -> Bool -> Bool
> por True  _    === True
> por _     True === True

even if _ were undefined or a non-halting computation. As it turns out, a function like this cannot be implemented in lambda calculus. Let's prove this.

We will restrict our selves to simply-typed lambda calculus with three constants, True, False :: Bool and if :: Bool -> a -> a obeying the following reduction rules:

> if True  M N ==> M
> if False M N ==> N

Recall that the basic reduction rule of lambda calculus was beta-reduction, that is, function application.

We will additionally allow for fixpoints, as otherwise we wil not be able to define most functions at all. (Strictly speaking, we will need one fixpoint operator per type, but type annotations will be ommitted in the future for brevity.) The definition of fix (if you don't understand it, just take for granted that fix let's us do recursion or see these posts):

> fix_a :: (a -> a) -> a
> fix_a ==> \f -> f (fix f)

Our evaluation order will be normal order, that is: we apply beta-reduction (function application) and our custom reduction rules at the lefternmost possible part of the expression. (This evaluation scheme is confluent, i.e. it always produces a unique normal form if such exists)

Now, because of it's type, por must have form

> por = \x -> \y -> E

for some E. Let us assume that E is in normal form (if it is not, it can be reduced without changing the semantics of por). We will also assume that both x and y appear in E as this is only natural.

Now then, buried in E there must be some reduction opportunities that can only be taken when something is substituted for x and y. Because x and y are variables, they must be distinct parts of E. That is, when we substitute something for x and y, these somethings will not overlap. By symmetry we can assume that x is left of y in E. Let E[A,B] denote E with A replaced for y and B for x. Now then if A reduces to A' in one step, E[A,B] reduces to E[A',B] in one step because A was our lefternmost reduction opportunity.

Now we note that fix (\x -> x) reduces to itself in two steps:

> fix (\x -> x) ==> (\f -> f (fix f)) (\x -> x) ==> (\x -> x) (fix (\x -> x))
>   ==> fix (\x -> x)

And thus

> por (fix (\x -> x)) B === E[fix (\x -> x),B]

can have no normal form regardless of B. Especially por (fix (\x -> x)) True =/= False.

A taste of domain theory

Scott models, also known as domains, are a way of obtaining denotational semantics for lambda calculi. Denotational semantics mean a mapping of the structures of the language to mathematical objects (functions, sets) of some sort.

Long story short, we consider a more-defined-than ordering of values. For simple types such as Bool and Nat (the natural numbers), there are just two levels to this ordering: the completely undefined value _|_ (pronounced "bottom"), and the defined values (1,2,True,...). The intuistic reason for using these orders is that a (computable) function must map a more-defined argument to a more-defined result. That is, functions must be monotonic wrt. the orderings of it's argument and result types.

An example is in place. Consider a function f :: Nat -> Bool with

> f undefined === True

now clearly f 4 must be True as well because f couldn't have inspected it's argument. Similarily, if

> f 4 === undefined

f undefined must be undefined also.

To be exact, for simple types (here Bool and Nat) the ordering is defined by

1. _|_ <= x for all x
2. x and y are not comparable if neither is _|_

The monotonicity requirement can now be formulated as: if a <= x then f a <= f x.

The cliff hanger

If we expand the definition of monotonicity to two arguments in the most natural way, that is

> a <= x && b <= y ==> f a b <= f x y

we find out that partial or is monotonic: this can be easily ascertained by either checking all cases or reasoning that making either argument to por less defined will never make the result more defined. So, por cannot be told apart from the defineable functions in our semantic model.

In the next post we will investigate what happens when we introduce por as a constant into our lambda calculus. Be warned, it might take a while as there's a lot to handle and I'm leaving for the alps after the weekend.