From: Jim Date: Sun, 1 Feb 2015 10:35:30 +0000 (-0500) Subject: update week1 notes X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=a29220f7cb8b5963e5819de0fb091f399a8ad952 update week1 notes --- 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 ###