Environments
Although the operational semantics presented in class for the λ-calculus can be used as a basis for implementing an interpreter, it’s not necessarily the best fit. First, it may be easier to implement the big-step semantics (Exercise 5.3.8) instead of the small-step semantics.
Second, substitution might not be very practical because it modifies code. Especially if functions are compiled, it may be difficult or impossible to perform substitutions on them. Environments are an alternative to substitution that also correspond better with how functions really work in implementation.
Preliminaries
In this section, the language we work with is λNB, which combines λ and NB. We don’t need numbers and Booleans to use environments, but it does make the examples easier.
The big-step evaluation (λx. λy. x) 0 true ⇓ 0 has the
derivation:
――――――――――――――――――――― ――――― ―――――――――――――
λx. λy. x ⇓ λx. λy. x 0 ⇓ 0 λy. 0 ⇓ λy. 0
――――――――――――――――――――――――――――――――――――――――――――― ――――――――――― ―――――
(λx. λy. x) 0 ⇓ λy. 0 true ⇓ true 0 ⇓ 0
―――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――
(λx. λy. x) 0 true ⇓ 0Let’s write it again, but this time with the substitutions unsimplified:
――――――――――――――――――――― ――――― ―――――――――――――――――――――――――――――
λx. λy. x ⇓ λx. λy. x 0 ⇓ 0 [x↦0](λy. x) ⇓ [x↦0](λy. x)
――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――― ――――――――――― ―――――――――――――――――――
(λx. λy. x) 0 ⇓ [x↦0](λy. x) true ⇓ true [x↦0,y↦true]x ⇓ 0
―――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――
(λx. λy. x) 0 true ⇓ 0An implementation that worked like this would only ever deal with subterms of the original term (in practice, pointers into the code) together with a list of substitutions, called the environment. Here, we redesign our semantics to use an environment instead of substitutions.
Environments
An environment is just a list of bindings of variables to values:
ρ ::= ε
ρ ::= ρ, x ↦ vThe order of the bindings matters: if there are two bindings for
x, the one on the right wins. For example, if
ρ = a ↦ 0, b ↦ succ 0, a ↦ succ (succ 0)then ρ binds a to
succ (succ 0), not 0.
Environment-based semantics
We now define values to be
v ::= nv
true
false
[ρ]λx. tAnd we are going to define a judgement of the form
[ρ]t ⇓ v, which means “t evaluated in the
environment ρ yields value v”.
Previously, we did not have a rule B-Var for variables, but now we do. It just looks up the variable’s value in the environment.
—————————————— B-VarEq
[ρ, x↦v]x ⇓ v
[ρ]x ⇓ v
———————————————— x' ≠ x B-VarNeq
[ρ, x'↦v']x ⇓ vSince we are working with λNB, we also need the rules from NB. They aren’t very interesting, because they don’t involve variables.
———————— B-Zero
[ρ]0 ⇓ 0
—————————————— B-True
[ρ]true ⇓ true
———————————————— B-False
[ρ]false ⇓ false
[ρ]t1 ⇓ true [ρ]t2 ⇓ v2
——————————————————————————————— B-IfTrue
[ρ](if t1 then t2 else t3) ⇓ v2
[ρ]t1 ⇓ false [ρ]t3 ⇓ v3
——————————————————————————————— B-IfFalse
[ρ](if t1 then t2 else t3) ⇓ v3
[ρ]t ⇓ nv
————————————————————— B-Succ
[ρ](succ t) ⇓ succ nv
[ρ]t ⇓ 0
——————————————— B-PredZero
[ρ](pred t) ⇓ 0
[ρ]t ⇓ succ nv
———————————————— B-PredSucc
[ρ](pred t) ⇓ nv
[ρ]t ⇓ 0
———————————————————— B-IsZeroZero
[ρ](iszero t) ⇓ true
[ρ]t ⇓ succ nv
————————————————————— B-IsZeroSucc
[ρ](iszero t) ⇓ falseTake 1: no nested functions
First consider only terms that do not have lambdas inside lambdas. (This is why we included NB in our language.) Then every abstraction is evaluated in the empty environment, so the rule for abstractions would be:
————————————————— B-Abs'
[](λx. t) ⇓ λx. tAnd the rule for applications would be:
[ρ]t1 ⇓ λx. t12 [ρ]t2 ⇓ v2 [x↦v2]t12 ⇓ v
————————————————————————————————————————————— B-App'
[ρ](t1 t2) ⇓ vExample:
[]((λf. f (f 0)) (λn. succ (succ n))) ⇓ succ (succ (succ (succ 0)))
This example is large, so we write numbers in base-10 and we omit some uninteresting subtrees.
[n↦0]n ⇓ 0
――――――――――――――――――
[n↦0](succ n) ⇓ 1 [n↦2]n ⇓ 2
――――――――――――――――――――――――― ――――――――――――――――――
⋯ ⋯ [n↦0](succ (succ n)) ⇓ 2 [n↦2](succ n) ⇓ 3
――――――――――――――――――――――――――――――― ―――――――――――――――――――――――――
⋯ [f↦λn. succ (succ n)](f 0) ⇓ 2 [n↦2](succ (succ n)) ⇓ 4
―――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――
⋯ ⋯ [f↦λn. succ (succ n)](f (f 0)) ⇓ 4
―――――――――――――――――――――――――――――――――――――――――――
[]((λf. f (f 0)) (λn. succ (succ n))) ⇓ 4An implementation would traverse this tree, and at any given time, it has to remember the path to the root, which can be thought of as a stack. Each element of the stack has a term, which is always a subterm of the original term and so can be a pointer into it, and an environment, which has at most one variable and its value. A stack of code pointers and variables – that’s the same as the call stack, in programming languages like C.
Take 2: closures
Now consider our full language, which does allow nested lambdas and
therefore we have to evaluate things of the form
[ρ](λx. t). The rule doesn’t actually perform the
substitutions in ρ; that’s what we were trying to avoid. It
just evaluates the abstraction-with-environment to itself:
——————————————————————— B-Abs
[ρ](λx. t) ⇓ [ρ](λx. t)Now, for the first time, an environment appears on the right
side of ⇓. An abstraction-with-environment is called a
closure, because the abstraction might have free variables, but
the environment says what their values are. It “closes over” all the
free variables in λx. t to turn it into a closed term (= a
term with no free variables).
Finally, and most importantly, the rule for applications is:
[ρ]t1 ⇓ [ρ'](λx. t12) [ρ]t2 ⇓ v2 [ρ', x↦v2]t12 ⇓ v
——————————————————————————————————————————————————————— B-App
[ρ](t1 t2) ⇓ vThis does the following:
Evaluate
t1in the current environmentρto get a closure,[ρ'](λx. t12). Note thatρ', the environment where the function is defined, might be different fromρ, the environment where the function is applied.Evaluate
t2in the current environmentρto getv2.Next we need to evaluate
t12. Since it comes from[ρ'](λx. t12), it isρ'(notρ), extended withx↦v2, that is attached to it.
Example: (λx. λy. x) 0 true again. The derivation is
nearly identical to the “unsimplified substitutions” derivation at the
top of the page.
――――――――――――――――――――――――― ――――――― ―――――――――――――――――――――――――――――
[](λx. λy. x) ⇓ λx. λy. x []0 ⇓ 0 [x↦0](λy. x) ⇓ [x↦0](λy. x)
――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――― ――――――――――――― ―――――――――――――――――――
[]((λx. λy. x) 0) ⇓ [x↦0](λy. x) []true ⇓ true [x↦0,y↦true]x ⇓ 0
―――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――
[]((λx. λy. x) 0 true) ⇓ 0
Environments can now have any number of variables and values now. To avoid copying them over and over, they can be stored as linked lists. Each list node (known as an activation record or AR) stores a variable name and value, and a pointer (called an access link) to the rest of the environment.
The value, in turn, can be a closure, which stores a subterm (or a pointer into the original term) and another environment. So environments are much more complex structures than in a C-like language.
For example, recall that
pair ≡ (λx. λy. λf. f x y)
triple ≡ (λx. λy. λz. λf. f x y z)Here’s what triple 0 true false looks like:
This illustrates how the lambda calculus can have data structures without really having data structures – environments can be formed into linked lists, binary trees, and so on.
The downside of this is that a stack is no longer enough. If a function returns a closure, its local variables become part of the closure and cannot be popped. So they must be moved somewhere else where they can persist until they are no longer needed (the heap). Since it would be tricky to do this manually, languages that have true closures usually also have some sort of automatic memory management.