From d2f7232f5c6124a53eb3889a690bd700ee4ce1ce Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Thu, 16 Sep 2010 18:09:18 -0400 Subject: [PATCH] merge lists, numbers Signed-off-by: Jim Pryor --- lists.mdwn => lists_and_numbers.mdwn | 0 numbers.mdwn | 32 -------------------------------- 2 files changed, 32 deletions(-) rename lists.mdwn => lists_and_numbers.mdwn (100%) delete mode 100644 numbers.mdwn diff --git a/lists.mdwn b/lists_and_numbers.mdwn similarity index 100% rename from lists.mdwn rename to lists_and_numbers.mdwn diff --git a/numbers.mdwn b/numbers.mdwn deleted file mode 100644 index 8d554245..00000000 --- a/numbers.mdwn +++ /dev/null @@ -1,32 +0,0 @@ - -Church figured out how to encode integers and arithmetic operations -using lambda terms. Here are the basics: - -0 = \f\x.fx -1 = \f\x.f(fx) -2 = \f\x.f(f(fx)) -3 = \f\x.f(f(f(fx))) -... - -Adding two integers involves applying a special function + such that -(+ 1) 2 = 3. Here is a term that works for +: - -+ = \m\n\f\x.m(f((n f) x)) - -So (+ 0) 0 = -(((\m\n\f\x.m(f((n f) x))) ;+ - \f\x.fx) ;0 - \f\x.fx) ;0 - -~~>_beta targeting m for beta conversion - -((\n\f\x.[\f\x.fx](f((n f) x))) - \f\x.fx) - -\f\x.[\f\x.fx](f(([\f\x.fx] f) x)) - -\f\x.[\f\x.fx](f(fx)) - -\f\x.\x.[f(fx)]x - -\f\x.f(fx) -- 2.11.0