1 <!-- λ Λ ∀ ≡ α β γ ρ ω Ω ○ μ η δ ζ ξ ⋆ ★ • ∙ ● ⚫ 𝟎 𝟏 𝟐 𝟘 𝟙 𝟚 𝟬 𝟭 𝟮 ⇧ (U+2e17) ¢ -->
6 The goal for these notes is to introduce the Reader Monad, and present
7 two linguistic applications: binding and intensionality. Along the
8 way, we'll continue to think through issues related to order, and a
9 related notion of flow of information.
11 At this point, we've seen monads in general, and three examples of
12 monads: the Identity monad (invisible boxes), the Option/Maybe monad (option
13 types), and the List monad.
15 We've also seen an application of the Option/Maybe monad to safe division.
16 The starting point was to allow the division function to return an `int
17 option` instead of an `int`. If we divide `6` by `2`, we get the answer `Some
18 3`. But if we divide `6` by `0`, we get the answer `None`.
20 The next step was to adjust the other arithmetic functions to teach
21 them what to do if they received `None` instead of a boxed integer.
22 This meant changing the type of their input from `int`s to `int option`s.
23 But we didn't need to do this piecemeal; rather, we "lift"ed the
24 ordinary arithmetic operations into the monad using the various tools
25 provided by the monad.
27 We'll go over this lifting operation in detail in the next section.
29 ## Tracing the effect of `safe_div` on a larger computation
31 So let's see how this works in terms of a specific computation.
34 \tree ((((+) (1)) (((*) (((/) (6)) (2))) (4))))
37 (+ 1 (* (/ 6 2) 4)) in tree format:
52 No matter what order we evaluate it in, this computation
53 should eventually reduce to `13`. Given a specific reduction strategy,
54 we can watch the order in which the computation proceeds. Following
55 on the evaluator developed during the previous homework, let's
56 adopt the following reduction strategy:
58 > In order to reduce an expression of the form (head arg), do the following in order:
60 > 1. Reduce `head` to `head'`
61 > 2. Reduce `arg` to `arg'`.
62 > 3. If `(head' arg')` is a redex, reduce it.
64 There are many details left unspecified here, but this will be enough
65 for today. The order in which the computation unfolds will be
67 > 1. Reduce head `(+ 1)` to itself
68 > 2. Reduce arg `((* ((/ 6) 2)) 4)`
69 > 1. Reduce head `(* ((/ 6) 2))`
70 > 1. Reduce head `*` to itself
71 > 2. Reduce arg `((/ 6) 2)`
72 > 1. Reduce head `(/ 6)` to itself
73 > 2. Reduce arg `2` to itself
74 > 3. Reduce `((/ 6) 2)` to `3`
75 > 3. Reduce `(* 3)` to itself
76 > 2. Reduce arg `4` to itself
77 > 3. Reduce `((* 3) 4)` to `12`
78 > 3. Reduce `((+ 1) 12)` to `13`
80 This reduction pattern follows the structure of the original
81 expression exactly, at each node moving first to the left branch,
82 processing the left branch, then moving to the right branch, and
83 finally processing the results of the two subcomputation. (This is
84 called a depth-first postorder traversal of the tree.)
86 [diagram with arrows traversing the tree]
88 It will be helpful to see how the types change as we make adjustments.
91 type contents = Num of num | Op2 of (num -> num -> num)
92 type tree = Leaf of contents | Branch of tree * tree
94 Never mind that these types will allow us to construct silly
95 arithmetric trees such as `+ *` or `2 3`. Note that during the
96 reduction sequence, the result of reduction was in every case a
97 well-formed subtree. So the process of reduction could be animated by
98 replacing subtrees with the result of reduction on that subtree, until
99 the entire tree is replaced by a single integer (namely, `13`).
101 Now we replace the number `2` with `0`:
104 \tree ((((+) (1)) (((*) (((/) (6)) (0))) (4))))
120 When we reduce, we get quite a ways into the computation before things
123 > 1. Reduce head `(+ 1)` to itself
124 > 2. Reduce arg `((* ((/ 6) 0)) 4)`
125 > 1. Reduce head `(* ((/ 6) 0))`
126 > 1. Reduce head `*` to itself
127 > 2. Reduce arg `((/ 6) 0)`
128 > 1. Reduce head `(/ 6)` to itself
129 > 2. Reduce arg `0` to itself
130 > 3. Reduce `((/ 6) 0)` to ACKKKK
132 This is where we replace `/` with `safe_div`. `safe_div` returns not an `int`, but an `int option`. If the division goes
133 through, the result is `Some n`, where `n` is the integer result.
134 But if the division attempts to divide by zero, the result is `None`.
136 We could try changing the type of the arithmetic operators from `int
137 -> int -> int` to `int -> int -> int option`; but since we now have to
138 anticipate the possibility that *any* argument might involve division by
139 zero inside of it, it would be better to prepare for the possibility
140 that any subcomputation might return `None` here. So our operators should have
141 the type `int option -> int option -> int option`. Let's bring that about
142 by just changing the type `num` from `int` to `int option`, leaving everying else the same:
144 type num = int option
145 type contents = Num of num | Op2 of (num -> num -> num)
146 type tree = Leaf of contents | Branch of tree * tree
148 The only difference is that instead of defining our numbers to be
149 simple integers, they are now `int option`s; and so `Op` is an operator
152 At this point, we bring in the monadic machinery. In particular, here
153 is the `⇧` and the `map2` function from the notes on safe division:
157 map2 (f : 'a -> 'b -> 'c) (xx : 'a option) (yy : 'b option) =
163 | Some y -> Some (f x y))
165 Then we lift the entire computation into the monad by applying `⇧` to
166 the integers, and by applying `map2` to the operators. Only, we will replace `/` with `safe_div`, defined as follows:
168 safe_div (xx : 'a option) (yy : 'b option) =
175 | Some y -> Some ((/) x y))
178 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (⇧0))) (⇧4))))
185 map2 + ⇧1 _____|_____ ⇧4
194 With these adjustments, the faulty computation now completes smoothly:
196 > 1. Reduce head `((map2 +) ⇧1)`
197 > 2. Reduce arg `(((map2 *) ((safe_div ⇧6) ⇧0)) ⇧4)`
198 > 1. Reduce head `((map2 *) ((safe_div ⇧6) ⇧0))`
199 > 1. Reduce head `(map2 *)`
200 > 2. Reduce arg `((safe_div ⇧6) ⇧0)`
201 > 1. Reduce head `(safe_div ⇧6)`
203 > 3. Reduce `((safe_div ⇧6) ⇧0)` to `None`
204 > 3. Reduce `((map2 *) None)`
206 > 3. Reduce `(((map2 *) None) ⇧4)` to `None`
207 > 3. Reduce `(((map2 +) ⇧1) None)` to `None`
209 As soon as we try to divide by `0`, `safe_div` returns `None`.
210 Thanks to the details of `map2`, the fact that `None` has been returned
211 by one of the arguments of a `map2`-ed operator guarantees that the
212 `map2`-ed operator will pass on the `None` as its result. So the
213 result of each enclosing computation will be `None`, up to the root
216 It is unfortunate that we need to continue the computation after
217 encountering our first `None`. We know immediately at the result of
218 the entire computation will be `None`, yet we continue to compute
219 subresults and combinations. It would be more efficient to simply
220 jump to the top as soon as `None` is encoutered. Let's call that
221 strategy Abort. We'll arrive at an `Abort` operator later in the semester.
223 So at this point, we can see how the Option/Maybe monad provides
224 plumbing that allows subcomputations to send information from one part
225 of the computation to another. In this case, the `safe_div` function
226 can send the information that division by zero has been attempted
227 upwards to the rest of the computation. If you think of the plumbing
228 as threaded through the tree in depth-first, postorder traversal, then
229 `safe_div` drops `None` into the plumbing half way through the
230 computation, and that `None` travels through the rest of the plumbing
231 till it comes out of the result faucet at the top of the tree.
234 ## Information flowing in the other direction: top to bottom
236 We can think of this application as facilitating information flow.
237 In the `safe_div` example, a subcomputation created a message that
238 propagated upwards to the larger computation:
241 message: Division by zero occurred!
256 (The message was implemented by `None`.)
258 We might want to reverse the direction of information flow, making
259 information available at the top of the computation available to the
277 We've seen exactly this sort of configuration before: it's exactly
278 what we have when a lambda binds a variable that occurs in a deeply
279 embedded position. Whatever the value of the argument that the lambda
280 form combines with, that is what will be substituted in for free
281 occurrences of that variable within the body of the lambda.
286 So our next step is to add a (primitive) version of binding to our
287 computation. We'll allow for just one binding dependency for now, and
288 then generalize later.
290 Binding is independent of the safe division, so we'll return to a
291 situation in which the Option/Maybe monad hasn't been added. One of the nice
292 properties of programming with monads is that it is possible to add or
293 subtract layers according to the needs of the moment. Since we need
294 simplicity, we'll set the Option/Maybe monad aside for now.
296 So we'll go back to the point where the num type is simple `int`, not
301 And we won't be using the `map2` or `⇧` from the Option/Maybe monad anymore.
303 As you might guess, the technique we'll use to arrive at binding will
304 be to use the Reader monad, defined here in terms of `mid`/`⇧` and `mbind`/`>>=`:
307 type <u>α</u> = int -> α
309 xx >>= k = \n. k (xx n) n
310 map f xx = \n. f (xx n)
311 ff ¢ xx = \n. (ff n) (xx n)
312 map2 f xx yy = map f xx ¢ yy = \n. f (xx n) (yy n)
315 A boxed type in this monad will be a function from an integer to an
316 value in the original type. The `mid`/`⇧` function lifts a value `x` to
317 a function that expects to receive an integer, but throws away the
318 integer and returns `x` instead (most values in the computation don't
319 depend on the input integer).
321 The `mbind`/`>>=` function in this monad takes a monadic value `xx`, a function
322 `k` taking non-monadic values into the monad, and returns a function
323 that expects an integer `n`. It feeds `n` to `xx`, which delivers a
324 result in the orginal type, which is fed in turn to `k`. `k` returns
325 a monadic value, which upon being fed an integer, also delivers a result
328 The `map`, `¢`, and `map2` functions corresponding to this `mbind` are given
329 above. They may look familiar --- we'll comment on this in a moment.
331 Lifing the computation into the monad, we have the following adjusted
334 type num = int -> int
336 That is, `num` is once again replaced with the type of a boxed `int`.
337 When we were dealing with the Option/Maybe monad, a boxed `int` had type `int
338 option`. In this monad, a boxed int has type `int -> int`.
341 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (x))) (⇧4))))
348 map2 + ⇧1 ____|_____ ⇧4
357 It remains only to decide how the variable `n` will access the input value supplied
358 at the top of the tree. The input value is supposed to be the
359 value that gets used for the variable `n`. Like every leaf in the tree
360 in argument position, the code we want in order to represent the
361 variable will have the type of a boxed `int`, namely, `int -> int`. So
362 we have the following:
364 var_n = fun (n : int) -> n
366 That is, variables in this system denote the identity function!
368 The result of evaluating this tree will be a boxed integer: a function
369 from any integer `n` to `(+ 1 (* (/ 6 n)) 4)`.
371 Take a look at the definition of the Reader monad again. The
372 `mid` takes some object `x` and returns `\n. x`. In other words,
373 `⇧x = Kx`, for our familiar combinator **K**, so `⇧ = K`. Likewise, the `map` operation
374 is just function composition, and the `mapply`/`¢` operation is our friend the **S** combinator. `map2 f xx yy` for the Reader monad is `(f ○ xx) ¢ yy` or `S (f ○ xx) yy`.
376 We've seen this before as a strategy for translating a binding
377 construct into a set of combinators. To remind you, here is a part of
378 the general scheme for translating a lambda abstract into Combinatory
379 Logic. The translation function `[.]` translates a lambda term into a
380 term in Combinatory Logic:
384 [\a.M] = K[M] (assuming a not free in M)
385 [\a.(MN)] = S[\a.M][\a.N]
387 The reason we can make do with this subset of the full translation
388 scheme is that we're making the simplifying assumption that there is
389 at most a single lambda involved. So once again we have the identity
390 function **I** as the translation of the bound variable, **K** as the function
391 governing expressions that don't contain an instance of the bound
392 variable, **S** as an operation that manages `¢`, that is, the applicative combination of complex expressions.
395 ## Jacobson's Variable Free Semantics as a Reader Monad
397 We've designed the presentation above to make it as easy as possible
398 to show that Jacobson's Variable Free Semantics (e.g., Jacobson 1999,
399 [Towards a Variable-Free
400 Semantics](http://www.springerlink.com/content/j706674r4w217jj5/))
401 implements a Reader monad.
403 More specifically, it will turn out that Jacobson's geach combinator
404 *g* is exactly our `map` operator, and her binding combinator *z* is
405 exactly our `mbind` (though with the arguments reversed).
407 Jacobson's system contains two main combinators, *g* and *z*. She
408 calls *g* the Geach rule, and *z* performs binding. Here is a typical
409 computation. This implementation is based closely on email from Simon
410 Charlow, with beta reduction as performed by the on-line evaluator:
413 ; Jacobson's analysis of "Everyone_i thinks he_i left"
414 let g = \f xx. \n. f (xx n) in ; or `f ○ xx`
415 let z = \k xx. \n. k (xx n) n in ; or `S (flip k) xx`, or `Reader.(>>=) xx k`
417 let everyone = \P. FORALL i (P i) in
419 everyone (z thinks (g left he))
421 ~~> FORALL i (thinks (left i) i)
424 Two things to notice: First, pronouns once again denote identity
425 functions, just as we saw in the reader monad in the previous section.
427 Second, *g* plays the role of transmitting a binding dependency for an
428 embedded constituent to a containing constituent.
430 The basic recipe in Jacobson's system is that you transmit the
431 dependence of a pronoun upwards through the tree using *g* until just
432 before you are about to combine with the binder, when you finish off
433 with *z*. Here is an example with a longer chain of *g*'s:
436 ; "Everyone_i thinks that Bill said he_i left"
438 everyone (z thinks (g (T bill) (g said (g left he))))
439 ; or `everyone (thinks =<< T bill ○ said ○ left ○ I)`
441 ~~> FORALL i (thinks (said (left i) bill) i)
444 If you compare Jacobson's values for *g* and *z* to the functions in
445 the reader monad given above, you'll see that Jacobson's *g*
446 combinator is exactly our `map` operator. Furthermore, Jacobson's *z*
447 combinator is identical to our Reader `>>=`, except with the order of the
448 arguments reversed (i.e., `(z k xx) == (xx >>= k)`).
450 (The `T` combinator in the derivations above is given by `T x <~~> \f. f x`;
451 it handles situations in which English word order reverses
452 the usual function/argument order. `T` is what Curry and Steedman call this
453 combinator. Jacobson calls it "lift", but it shouldn't be confused with the
454 `mid` and `map` operations that lift values into the Reader monad we're focusing
455 on here. It does lift values into a *different* monad, that we'll consider in
459 Jacobson's variable-free semantics is essentially a Reader monad.
461 One of the peculiar aspects of Jacobson's system is that binding is
462 accomplished not by applying *z* to the element that will (in some
463 pre-theoretic sense) bind the pronoun, here, *everyone*, but rather by
464 applying *z* instead to the predicate that will take *everyone* as an
465 argument, here, *thinks*.
468 ## The Reader monad for intensionality
470 Now we'll look at using the Reader monad to do intensional function application.
472 In Shan (2001) [Monads for natural
473 language semantics](http://arxiv.org/abs/cs/0205026v1), Ken shows that
474 making expressions sensitive to the world of evaluation is conceptually
475 the same thing as making use of the Reader monad.
476 This technique was beautifully re-invented
477 by Ben-Avi and Winter (2007) in their paper [A modular
479 intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf),
480 though without explicitly using monads.
482 All of the code in the discussion below can be found here: [[code/intensionality-monad.ml]].
483 To run it, download the file, start OCaml, and say
485 # #use "intensionality-monad.ml";;
487 Note the extra `#` attached to the directive `use`.
489 First, the familiar linguistic problem:
493 Ann believes that Bill left.
494 Ann believes that Cam left.
496 We want an analysis on which the first three sentences can be true at
497 the same time that the last sentence is false. If sentences denoted
498 simple truth values or booleans, we have a problem: if the sentences
499 *Bill left* and *Cam left* are both true, they denote the same object,
500 and Ann's beliefs can't distinguish between them.
502 The traditional solution to the problem sketched above is to allow
503 sentences to denote a function from worlds to truth values, what
504 Montague called an intension. So if `s` is the type of possible
505 worlds, we have the following situation:
509 Extensional types Intensional types Examples
510 -------------------------------------------------------------------
514 VP e->t (s->e)->s->t left
515 Vt e->e->t (s->e)->(s->e)->s->t saw
516 Vs t->e->t (s->t)->(s->e)->s->t thought
519 This system is modeled on the way Montague arranged his grammar.
520 There are significant simplifications compared to Montague: for
521 instance, determiner phrases are thought of here as corresponding to
522 individuals rather than to generalized quantifiers.
524 The main difference between the intensional types and the extensional
525 types is that in the intensional types, the arguments are functions
526 from worlds to extensions: intransitive verb phrases like *left* now
527 take so-called "individual concepts" as arguments (type `s->e`) rather than plain
528 individuals (type `e`), and attitude verbs like *think* now take
529 propositions (type `s->t`) rather than truth values (type `t`).
530 In addition, the result of each predicate is an intension.
531 This expresses the fact that the set of people who left in one world
532 may be different than the set of people who left in a different world.
534 Normally, the dependence of the extension of a predicate to the world
535 of evaluation is hidden inside of an evaluation coordinate, or built
536 into the the lexical meaning function, but we've made it explicit here
537 in the way that the intensionality monad makes most natural.
539 The intensional types are more complicated than the extensional
540 types. Wouldn't it be nice to make the complicated types available
541 for expressions like attitude verbs that need to worry about
542 intensions, and keep the rest of the grammar as extensional as
543 possible? This desire is parallel to our earlier desire to limit the
544 concern about division by zero to the division function, and let the
545 other functions, like addition or multiplication, ignore
546 division-by-zero problems as much as possible.
548 So here's what we do:
550 In OCaml, we'll use integers to model possible worlds. `char`s (characters in the computational sense, i.e., letters like `'a'` and `'b'`, not Kaplanian characters) will model individuals, and OCaml `bool`s will serve for truth values:
560 let left1 (x : e) = true
561 let saw1 (y : e) (x : e) = x < y
564 saw1 bill ann (* true *)
565 saw1 ann bill (* false *)
567 So here's our extensional system: everyone left, including Ann;
568 and Ann saw Bill (`saw1 bill ann`), but Bill didn't see Ann. (Note that the word
569 order we're using is VOS, verb-object-subject.)
571 Now we add intensions. Because different people leave in different
572 worlds, the meaning of *leave* must depend on the world in which it is
575 let left (x : e) (w : s) = match (x, w) with ('c', 2) -> false | _ -> true
576 left ann 1 (* true: Ann left in world 1 *)
577 left cam 2 (* false: Cam didn't leave in world 2 *)
579 This new definition says that everyone always left, except that
580 in world 2, Cam didn't leave.
582 Note that although this general *left* is sensitive to world of
583 evaluation, it does not have the fully intensionalized type given in
584 the chart above, which was `(s->e)->s->t`. This is because
585 *left* does not exploit the additional resolving power provided by
586 making the subject an individual concept. In semantics jargon, we say
587 that *leave* is extensional with respect to its first argument.
589 We will adopt the general strategy of defining predicates
590 in a way that they take arguments of the lowest type that will allow
591 us to make all the distinctions the predicate requires. When it comes
592 time to combine this predicate with monadic arguments, we'll have to
593 make use of various lifting predicates.
595 Likewise, although *see* depends on the world of evaluation, it is
596 extensional in both of its syntactic arguments:
598 let saw (y : e) (x : e) (w : s) = (w < 2) && (x < y)
599 saw bill ann 1 (* true: Ann saw Bill in world 1 *)
600 saw bill ann 2 (* false: no one saw anyone in world 2 *)
602 This (again, partially) intensionalized version of *see* coincides
603 with the `saw1` function we defined above for world 1; in world 2, no
606 Just to keep things straight, let's review the facts:
609 World 1: Everyone left.
610 Ann saw Bill, Ann saw Cam, Bill saw Cam, no one else saw anyone.
611 World 2: Ann left, Bill left, Cam didn't leave.
615 Now we are ready for the intensionality monad:
618 type 'a intension = s -> 'a
619 let mid x = fun (w : s) -> x
620 let (>>=) xx k = fun (w : s) -> let x = xx w in let yy = k x in yy w
621 (* or just `fun w -> k (xx w) w` *)
624 Then the individual concept `mid ann` is a rigid designator: a
625 constant function from worlds to individuals that returns `'a'` no
626 matter which world is used as an argument. This is a typical kind of
627 thing for a monadic `mid` to do.
629 Then combining a predicate like *left* which is extensional in its
630 subject argument with an intensional subject like `mid ann` is simply `mbind`
633 (mid ann >>= left) 1 (* true: Ann left in world 1 *)
634 (mid cam >>= left) 2 (* false: Cam didn't leave in world 2 *)
636 As usual, `>>=` takes a monadic box containing Ann, extracts Ann, and
637 feeds her to the function *left*. In linguistic terms, we take the
638 individual concept `mid ann`, apply it to the world of evaluation in
639 order to get hold of an individual (`'a'`), then feed that individual
640 to the predicate *left*.
642 We can arrange for a transitive verb that is extensional in both of
643 its arguments to take intensional arguments:
646 let map2' f xx yy = xx >>= (fun x -> yy >>= (fun y -> <span class=ul>f x y</span>))
649 This is almost the same `map2` predicate we defined in order to allow
650 addition in our division monad example. The *difference* is that this
651 variant operates on verb meanings that take extensional arguments but
652 returns an intensional result. Thus the original `map2` predicate
653 has `mid (f x y)` where we have just <code><span class=ul>f x y</span></code> here.
655 The use of `>>=` here to combine *left* with an individual concept,
656 and the use of `map2'` to combine *see* with two intensional
657 arguments closely parallels the two of Montague's meaning postulates
658 (in PTQ) that express the relationship between extensional verbs and
659 their uses in intensional contexts.
662 map2' saw (mid bill) (mid ann) 1 (* true *)
663 map2' saw (mid bill) (mid ann) 2 (* false *)
666 Ann did see Bill in world 1, but Ann didn't see Bill in world 2.
668 Finally, we can define our intensional verb *thinks*. *Think* is
669 intensional with respect to its sentential complement (it takes complements of type `s -> t`), though still extensional
670 with respect to its subject (type `e`). (As Montague noticed, almost all verbs
671 in English are extensional with respect to their subject; a possible
672 exception is *appear*.)
674 let thinks (p : s->t) (x : e) (w : s) =
675 match (x, p 2) with ('a', false) -> false | _ -> p w
677 In every world, Ann fails to believe any proposition that is false in world 2.
678 Apparently, she stably thinks we may be in world 2. Otherwise, everyone
679 believes a proposition iff that proposition is true in the world of evaluation.
681 (mid ann >>= thinks (mid bill >>= left)) 1 (* true *)
683 So in world 1, Ann thinks that Bill left (because in worlds 1 and 2, Bill did leave).
685 But although Cam left in world 1:
687 (mid cam >>= left) 1 (* true *)
689 he didn't leave in world 2, so Ann doesn't in world 1 believe that Cam left:
691 (mid ann >>= thinks (mid cam >>= left)) 1 (* false *)
694 **Small project**: add intersective (*red*) and non-intersective
695 adjectives (*good*) to the fragment. The intersective adjectives
696 will be extensional with respect to the nominal they combine with
697 (using `mbind`), and the non-intersective adjectives will take
698 intensional arguments.
700 **Connections with variable binding**: the rigid individual concepts generated by `mid ann` and the like correspond to the numerical constants, that don't interact with the environment in any way, in the variable binding examples we considered earlier on the page. If we had any non-contingent predicates that were wholly insensitive to intensional effects, they would be modeled using `map2` and would correspond to the operations like `map2 (+)` in the earlier examples. As it is, our predicates *lift* and *saw*, though only sensitive to the *extension* of their arguments, nonetheless *are* sensitive to the world of evaluation for their `bool` output. So these are somewhat akin, at the predicate level, to expressions like `var_n`, at the singular term level, in the variable bindings examples. Our predicate *thinks* shows yet a further kind of interaction with the intensional structures we introduced: namely, its output can depend upon evaluating its complement relative to other possible worlds. We didn't discuss analogues of this in the variable binding case, but they exist: namely, they are expressions like `let x = 2 in ...` and `forall x ...`, that have the effect of supplying their arguments with an environment or assignment function that is shifted from the one they are themselves being evaluated with.
702 notes: cascade, general env