From: Jim Pryor Date: Thu, 16 Sep 2010 20:46:32 +0000 (-0400) Subject: tweak week2 X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=5516c3e364df25f7ea7676e1ff3e47e037fadd1e tweak week2 Signed-off-by: Jim Pryor --- diff --git a/week2.mdwn b/week2.mdwn index 6bca0c6a..6f157990 100644 --- a/week2.mdwn +++ b/week2.mdwn @@ -60,13 +60,13 @@ In the assignment we asked you to reduce various expressions until it wasn't pos (\x. x x) (\x. x x) -As we saw above, each of the halves of this formula are the combinator ω; so this can also be written: +As we saw above, each of the halves of this formula are the combinator ω; so this can also be written: 
ω ω
-This compound expression---the self-application of ω---is named Ω. It has the form of an application of an abstract (ω) to an argument (which also happens to be ω), so it's a redex and can be reduced. But when we reduce it, we get ω ω again. So there's no stage at which this expression has been reduced to a point where it can't be reduced any further. In other words, evaluation of this expression "never terminates." (This is the standard language, however it has the unfortunate connotation that evaluation is a process or operation that is performed in time. You shouldn't think of it like that. Evaluation of this expression "never terminates" in the way that the decimal expansion of π never terminates. These are static, atemporal facts about their mathematical properties.) +This compound expression---the self-application of ω---is named Ω. It has the form of an application of an abstract (ω) to an argument (which also happens to be ω), so it's a redex and can be reduced. But when we reduce it, we get ω ω again. So there's no stage at which this expression has been reduced to a point where it can't be reduced any further. In other words, evaluation of this expression "never terminates." (This is the standard language, however it has the unfortunate connotation that evaluation is a process or operation that is performed in time. You shouldn't think of it like that. Evaluation of this expression "never terminates" in the way that the decimal expansion of π never terminates. These are static, atemporal facts about their mathematical properties.) -There are infinitely many formulas in the lambda calculus that have this same property. Ω is the syntactically simplest of them. In our meta-theory, it's common to assign such formula a special value, ⊥, pronounced "bottom." When we get to discussing types, you'll see that this value is counted as belonging to every type. To say that a formula has the bottom value means that the computation that formula represents never terminates and so doesn't evaluate to any orthodox, computed value. +There are infinitely many formulas in the lambda calculus that have this same property. Ω is the syntactically simplest of them. In our meta-theory, it's common to assign such formula a special value, ⊥, pronounced "bottom." When we get to discussing types, you'll see that this value is counted as belonging to every type. To say that a formula has the bottom value means that the computation that formula represents never terminates and so doesn't evaluate to any orthodox, computed value. From a "Fregean" or "weak Kleene" perspective, if any component of an expression fails to be evaluable (to an orthodox, computed value), then the whole expression should be unevaluable as well. @@ -76,7 +76,7 @@ However, in some such cases it seems *we could* sensibly carry on evaluation. Fo (\x. y) (ω ω) -Should we count this as unevaluable, because the reduction of ω ω never terminates? Or should we count it as evaluating to `y`? +Should we count this as unevaluable, because the reduction of (ω ω) never terminates? Or should we count it as evaluating to `y`? This question highlights that there are different choices to make about how evaluation or computation proceeds. It's helpful to think of three questions in this neighborhood: