From 52b49c352b3d56d1a929694f22b0b94577e28ee3 Mon Sep 17 00:00:00 2001 From: jim Date: Sat, 7 Feb 2015 13:23:07 -0500 Subject: [PATCH] refine notes --- topics/week2_lambda_advanced.mdwn | 21 +++++++++------------ 1 file changed, 9 insertions(+), 12 deletions(-) diff --git a/topics/week2_lambda_advanced.mdwn b/topics/week2_lambda_advanced.mdwn index 1372e436..dbc62e76 100644 --- a/topics/week2_lambda_advanced.mdwn +++ b/topics/week2_lambda_advanced.mdwn @@ -1,4 +1,4 @@ -## Fine points concerning the lambda calculus ## +## Advanced notes on the Lambda Calculus ## Hankin uses the symbol → for one-step contraction, @@ -7,10 +7,7 @@ zero-or-more step reduction. Hindley and Seldin use ⊳1 and ⊳. -As we said in the main notes, when M and N are such that there's some P that M -reduces to by zero or more steps, and that N also reduces to by zero or more -steps, then we say that M and N are **beta-convertible**. We write that like -this: +As we said in the main notes, when `M` and `N` are such that there's some `P` that `M` reduces to by zero or more steps, and that `N` also reduces to by zero or more steps, then we say that `M` and `N` are **beta-convertible**. We write that like this: M <~~> N @@ -31,11 +28,11 @@ when discussing the metatheory. Instead we'll use `<~~>` as we said above. When we want to introduce a stipulative definition, we'll write it out longhand, as in: -> T is defined to be `(M N)`. +> `T` is defined to be `(M N)`. or: -> Let T be `(M N)`. +> Let `T` be `(M N)`. We'll regard the following two expressions: @@ -92,7 +89,7 @@ what (c) reduces to. So if we took (b) to reduce to `\y. y y`, we'd wrongly be counting (b) to be equivalent to (c), instead of (a). To reduce (b), then, we need to be careful to that no free variables in what -we're substituting in get captured by binding λs that they shouldn't be +we're substituting in get "captured" by binding λs that they shouldn't be captured by. In practical terms, you'd just replace (b) with (a) and do the unproblematic substitution into (a). @@ -147,7 +144,7 @@ furthermore lack any notion of a bound position. ## Review: syntactic equality, reduction, convertibility ## -Define N to be `(\x. x y) z`. Then N and `(\x. x y) z` are syntactically equal, +Define `N` to be `(\x. x y) z`. Then `N` and `(\x. x y) z` are syntactically equal, and we're counting them as syntactically equal to `(\z. z y) z` as well. We'll express all these claims in our metalanguage as: @@ -158,16 +155,16 @@ This: N ~~> z y -means that N beta-reduces to `z y`. This: +means that `N` beta-reduces to `z y`. This: M <~~> N -means that M and N are beta-convertible, that is, that there's something they both reduce to in zero or more steps. +means that `M` and `N` are beta-convertible, that is, that there's something they both reduce to in zero or more steps. The symbols `~~>` and `<~~>` aren't part of what we're calling "the Lambda Calculus". In our mouths, they're just part of our metatheory for talking about it. In the uses of the Lambda Calculus as a formal proof theory, one or the other of these -symbols (or some notational variant of them) is added to the object language. +symbols (or some notational variant of them) is added to the object language. But only in outermost contexts. It's like the "sequent" symbol (written `=>` or ⊢) in [Gentzen-style proof systems](https://en.wikipedia.org/wiki/Sequent_calculus) for logic. You can't embed the `~~>` or `<~~>` symbol inside lambda terms. See Hankin Sections 2.2 and 2.4 for the proof theory using `<~~>` (which he writes as `=`). He discusses the proof theory using `~~>` in his Chapter 3. -- 2.11.0