8
$\begingroup$

I'm learning about strict functions in Haskell.
A function f is strict if f ⊥ = ⊥
Some functions are strict only in the first argument (for e.g. const), others are strict in the second (for e.g. map).
I'm trying to think of a function which is strict in only both arguments at the same time, so
f x ⊥ is not bottom
f ⊥ y is not bottom
but
f ⊥ ⊥ is bottom
and I can't come up with any such function. Is this possible?

It feels like it isn't, but I'm a bit confused. Also because of currying, we can think of the function as only taking one argument at a time and then returning a function that takes the second argument. Do we only talk about strictness in one argument at a time?

$\endgroup$

1 Answer 1

17
$\begingroup$

That's a very good question! It turns out the answer is both yes and no.

A classic example of a function we'd like to write is Plotkin's parallel or. We know from basic boolean logic that both or True _ and or _ True are always true, regardless of the value of _. So we'd like to write a function or that takes two arguments, and True if either argument is True, returns False if both arguments are False, and only doesn't terminate if neither argument terminates. But can we?

It turns out that in the lambda calculus, it's impossible to write such a function. The lambda calculus is said to be inherently sequential. I've written a bit about this in the past in Why are there two not operators in lambda calculus?, on a related example.

If you think in terms of Turing machines, it is possible to write a machine that performs parallel or. Consider a machine with two inputs: a description of a machine $M_1$ that calculates the first argument, and a description of a machine $M_2$ that calculates the second argument. The machine simulates one step of $M_1$, then one step of $M_2$, then again one step of each machine in turn, until one of the machine halts. If the first machine to halt outputs True, output True and stop, otherwise keep simulating the other machine and return its output (if it ever terminates).

This illustrates an important aspect of the Church-Turing thesis. All definitions of things we'd sensibly want to call “this can be computer” turn out to be equivalent, as long as the intuition of computability is only about taking inputs and returning a result. If we throw other things into the mix, such as looking at computations in progress and giving it a meaning other than the final output, then models of computation are not equivalent. In particular, there isn't an equivalent of the Church-Turing thesis for concurrent computation: different models often have subtle differences in terms of expressivity.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.