How can I represent state or environment in the $\lambda$-Calculus?

I have seen in different tutorials how to represent numbers and booleans in the pure $\lambda$-Calculus, and how to define some arithmetic and logic operations. But what if I want to represent other constructs, not usually encouraged in pure functional languages, like state (assignment of values to variables) and sequencing (evaluating $e_1$ before $e_2$)?

For example, how would I encode an assignment "$v := e$" (where $v$ is a variable and $e$ an environment)? And what about encoding "$x := 2; y := y + x$"? (The point is that there is a dependency among statements, and they should be evaluated/executed in the correct order.)

Such a thing is, for the most part, impossible in the pure lambda calculus: all variables represent immutable values.

However, you can fake it in a number of ways.

The simplest is parameter passing. For a function which has a "state", you give it an extra parameter, which is a data structure mapping variables to their values. Any time you alter a variables value, you just create a new store with the updated value, and use it as the new parameter.

This pattern of passing the state to each computation in sequence can be abstracted using a State monad, or something similar. A state monad provides a pattern where the machinery of creating a new store, updating its values, and correctly passing it to future functions.

Monads provide a sequencing operator, which allow for the ordered evaluation that you mention.

There exists calculi which have mutation built into them, but first off, they aren't the pure calculus as you asked for, and in such cases, you don't encode mutation, you add it as a primitive operation.

• The parameter passing way is interesting. Is there a "usual", or "standard" way of doing it using Church (or Scott) encoding? I don't remember having seen that as part of the usual treatment of this topic.
– Jay
Mar 31 '16 at 10:53
• Usually, if you need something this detailed, you don't use a lambda calculus, you use a real language like Scheme or Haskell. But if you insist on using the LC, I would encode variable names as Church Numerals, and use Church Encoding to make pairs. You can encode linked-lists as pairs. Your store is then a list of pairs, with the first element the number representing a variable, and the second element its value. Mar 31 '16 at 18:47