From c359efaee71b34e8db4e7527c75766fde6c0e8fa Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Fri, 17 Sep 2010 16:37:40 -0400 Subject: [PATCH] tweak week2 Signed-off-by: Jim Pryor --- week2.mdwn | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/week2.mdwn b/week2.mdwn index 992c8c89..77459bfd 100644 --- a/week2.mdwn +++ b/week2.mdwn @@ -161,7 +161,8 @@ One important advantage of normal-order evaluation in particular is that it can Indeed, it's provable that if there's *any* reduction path that delivers a value for a given expression, the normal-order evalutation strategy will terminate with that value. -An expression is said to be in **normal form** when it's not possible to perform any more reductions. (EVEN INSIDE ABSTRACTS?) There's a sense in which you *can't get anything more out of* ω ω, but it's not in normal form because it still has the form of a redex. +An expression is said to be in **normal form** when it's not possible to perform any more reductions (not even inside abstracts). +There's a sense in which you *can't get anything more out of* ω ω, but it's not in normal form because it still has the form of a redex. A computational system is said to be **confluent**, or to have the **Church-Rosser** or **diamond** property, if, whenever there are multiple possible evaluation paths, those that terminate always terminate in the same value. In such a system, the choice of which sub-expressions to evaluate first will only matter if some of them but not others might lead down a non-terminating path. -- 2.11.0