patternMinor
What is meant when we say that divergence is the only side-effect of the lambda-calculus?
Viewed 0 times
effectmeantthewhatcalculussidesaythatdivergencewhen
Problem
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?
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?
Solution
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:
-
You can extend the calculus with new primitives, for example primitive operations
-
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.
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:
-
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.-
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.
Context
StackExchange Computer Science Q#116377, answer score: 8
Revisions (0)
No revisions yet.