In the simply typed lambda-calculus, I was told that behavioral equivalence is taken in terms of divergence because "divergence is the only side-effect of such language".

How should I understand this quotation? What does it mean that divergence is a side-effect? Perhaps that it is a phenomenon that is not directly encoded in the evaluation rules? But then, how do we know there are no other kinds of side-effects?

  • 2
    $\begingroup$ Before I try to answer your question, please give us some context about your background. Are you familiar with side effects in programming languages? Can you name some standard computational effects that a typical language has, or is this totally new to you? $\endgroup$ – Andrej Bauer Oct 27 '19 at 20:19
  • $\begingroup$ my background is a course in lambda-calculus going on following pierce's TAPL book. i'm familiar with general-purporse programming languages. it is true that if you go to that level, side-effects would be writing in memory, printing something...i still lack of an understanding of how to implement side-effects in lambda-calculus (i will cover it shortly) @AndrejBauer $\endgroup$ – Rodrigo Oct 28 '19 at 13:59

I think it is better to speak of computational effects than side effects, as some of them are not really on the side but rather directly in your face.

Computational effects are aspects of a program which are not just "mathematical computing", i.e., not just internal processing of data: I/O, access to mutable memory, exceptions, etc. The notion is a bit open-ended and difficult to make completely precise (because people invent new ways of computing things -- in 1970 nobody would have thought to include quantum super-position into the list of possible side-effects). Nevertheless, any sort of interaction between a program and the external environment is usually counted as a compuational effect.

Is program divergence, i.e., running forever, a side effects? In a sense it is, because it definitely is a form of "interaction" with the external environment, albeit a very annoying and useless one. Waiting forever to find out the result of a computation has several side effects, such as a high electricity bill, death of one's pets, and the thermal death of the universe. There are also deeper theoretical reasons why divergence should be counted as a side effect, but you did not explicitly ask about that.

You stated that the pure simply-typed $\lambda$-calculus has only one computational effect, namely divergence. But this is not the case! In the simply-typed $\lambda$-calculus every program terminates! You have to pass to the untyped $\lambda$-calculus to get divergence.

You also ask how to implement computational effects in $\lambda$-calculus. There are two ways:

  1. You can extend the calculus with new primitives, for example primitive operations print, read, etc. You then have to give an operational account of what these operations do. ML-style languages do this.

  2. You can simulate effects using the calculus. For example, instead of actually printing things, you can collect the things that would get printed in a list (suitably implemented in $\lambda$-calculus). Most effects can be simulated in such a way. In this approach your language is still pure, but your programs look like they are using computational effects. Haskell does this.

  • $\begingroup$ Can you give a pointer to those "deeper theoretical reasons why divergence should be counted as a side effect"? ... there, I asked ;P $\endgroup$ – Apiwat Chantawibul Oct 28 '19 at 15:42
  • 2
    $\begingroup$ Lookup the "partiality monad". It's a monad which accounts for non-termination. $\endgroup$ – Andrej Bauer Oct 28 '19 at 18:02
  • $\begingroup$ I think of "program X diverges" as saying that its semantically bottom and the fact that it takes forever to compute as being a sub-structural property. Effects seem quite different to me however. Is the claim just that all sub-strucutral properties are effectual in some sense? Or is it just that you can gate operations that cause Turing completeness into a monad? $\endgroup$ – Jake Oct 29 '19 at 5:19
  • $\begingroup$ @jake Presumably you would consider the raising of an exception to be an effect. Considered as a mathematical function of its argument, there is no difference between a function application that diverges because it runs forever and one that diverges because it raises an InvalidArgument exception. They are both undefined at that argument. $\endgroup$ – Mark Dominus Nov 16 '19 at 15:17

A common operational definition of side effect is that it's an aspect of the behavior of a program that depends on when you execute it. A program that is effect-free always has the same behavior no matter when you execute it.

This is most useful when you consider subprograms. If subprograms A and B are effect-free, you can execute A before B, or B before A, or A and B in parallel: the behavior of the overall program will be the same. If subprogram A is effect-free, you can execute A a different number of times, which is something optimizers often do.

In particular, if A is effect-free, and the overall program happens not to depend on the value of A, then A does not need to be executed at all. In other words, effect-free subprograms can be optimized away. Programs that have side effects usually cannot be optimized away.

Going by this definition, divergence (i.e. non-termination) is a side effect. Suppose that subprogram A has no external side effect (e.g. consuming input, displaying output, or modifying the content of a memory location that is also used by some other part of the program) but does not terminate. And suppose that the overall program does not use the value of A, and terminates if you don't evaluate A. Then removing the evaluation of A does make a difference to the program's behavior: it goes from not terminating, to terminating. This wouldn't happen if A was not effect-free.

There are other possible definitions of side effects. Typically, anything that is part of the semantics of an expression and that isn't the expression's type or value is considered a side effect. This includes modifying a memory store, interacting with external entities (input/output), etc. Going by this definition, a subprogram whose value is not used can be replaced by another subprogram which has a different value, but the same side effects.

With denotational or big-step semantics, the non-termination of a program is apparent in the semantics and you can't simply replace a terminating subprogram by a non-terminating program or vice versa. But with small-step semantics, the non-termination of a program is not directly apparent in the semantics. So it's possible to replace a terminating subprogram by a non-terminating program or vice versa without changing the possible reduction steps apart from reduction inside the subprogram.

In the usual semantics of the lambda calculus, the usual semantics is a small-step semantics (beta-reduction), where the only thing that matters is what a term reduces to. There is no store, no I/O, or anything else that looks like a side effect. Therefore most semanticists say that the lambda-calculus has no side effect — there are no side effects according to the definitional definition of ”side effect“.

However, the lambda calculus does have a side effect in the operational sense that I described above: if you replace a non-terminating term by a terminating one, you get a term with a different semantics, since its set of possible reductions (its Böhm tree) has a different shape. For example, $M = (\lambda x. y) \Omega$ and $N = (\lambda x. y) z$ have different Böhm trees, since $M \to_\beta M$ but $N$ only reduces to $z$. Even though the value of the argument of $(\lambda x. y)$ is not used, its termination matters, so its termination is a side effect in this sense.

Non-termination is often used to characterize the equivalence of terms because it's a way to observe the behavior of a program without looking at the program itself. There are many useful equivalence relation on programs. Some of these equivalences are directly based on the evaluation rules of the program. For example beta-equivalence is defined by the existence of a chain of beta-reductions (each reduction in either direction) between two terms. But why should we think that this is a useful characterization of lambda terms? For example, all lambda terms (in the pure lambda calculus) are functions. Is it true that if two lambda terms are beta-equivalent, then applying them to the same argument yields beta-equivalent terms? Yes (trivially). Is the converse true? No: you need to add eta-conversion. Is this enough? Yes (in a sense that I won't go into). How can you tell what an equivalence does other than by describing it in terms of its definition? By looking at whether terms diverge. A divergent term is definitely different from a non-divergent term. A term that causes a context to diverge (a context is a program with one hole in it) is definitely different from another term that causes the same context not to diverge.

In the simply typed lambda calculus, all terms converge: the simply typed lambda calculus is strongly normalizing. (So are many typed lambda calculi, because typed lambda calculi are often defined for use in logic and non-termination is pretty much anathema to logic because it translates to being able to prove anything.) So simply typed lambda terms are effect-free even by the more restrictive definition.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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