From a29220f7cb8b5963e5819de0fb091f399a8ad952 Mon Sep 17 00:00:00 2001 From: Jim Date: Sun, 1 Feb 2015 05:35:30 -0500 Subject: [PATCH] update week1 notes --- week1.mdwn | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/week1.mdwn b/week1.mdwn index 983c18c0..24d606b2 100644 --- a/week1.mdwn +++ b/week1.mdwn @@ -600,7 +600,11 @@ evaluates to? Well, consider the right-hand side of the second binding: This expression evaluates to `(1, 2)`, because it uses the outer binding of `x` to `0` for the right-hand side of its own binding `x match x + 1`. That gives us a new binding of `x` to `1`, which is in place when we evaluate `(x, 2*x)`. That's why the whole thing evaluates to `(1, 2)`. So now returning to the outer expression, `y` gets bound to `1` and `z` to `2`. But now what is `x` bound to in the final line,`([y, z], x)`? The binding of `x` to `1` was in place only until we got to `(x, 2*x)`. After that its scope expired, and the original binding of `x` to `0` reappears. So the final line evaluates to `([1, 2], 0)`. -This is very like what happens in ordinary predicate logic if you say: ∃ `x. F x and (` ∀ `x. G x ) and H x`. The `x` in `F x` and in `H x` are governed by the outermost quantifier, and only the `x` in `G x` is governed by the inner quantifier. +This is very like what happens in ordinary predicate logic if you say: + +∃ `x. F x and (` ∀ `x. G x ) and H x` + +The `x` in `F x` and in `H x` are governed by the outermost quantifier, and only the `x` in `G x` is governed by the inner quantifier. ### That's enough ### -- 2.11.0