home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #18 / NN_1992_18.iso / spool / comp / lang / scheme / 2021 < prev    next >
Encoding:
Text File  |  1992-08-12  |  3.3 KB  |  101 lines
  1. Newsgroups: comp.lang.scheme
  2. Path: sparky!uunet!caen!news.cs.indiana.edu!mayer@moose.cs.indiana.edu
  3. From: Mayer Goldberg <mayer@moose.cs.indiana.edu>
  4. Subject: church numerals ...
  5. Message-ID: <1992Aug12.201701.18392@news.cs.indiana.edu>
  6. Organization: Computer Science, Indiana University
  7. Date: Wed, 12 Aug 1992 20:16:55 -0500
  8. Lines: 91
  9.  
  10. Here are my 2 cents worth of church numeral stuff:
  11.  
  12. It would really be neat if we had a successor and a zero. If we did,
  13. we could say the following (in either LC or Scheme):
  14.  
  15. Let z be our zero combinator; let s be our successor combinator:
  16.  
  17. zero == z
  18. one == (s z)
  19. two == (s (s z))
  20. etc.
  21.  
  22. But unfortunately we con't have s and z in any obvious way, and so we
  23. abstract over the two, defining our numerals as follows:
  24.  
  25. zero == \sz.z
  26. one == \sz.(s z) == \x.x
  27. two == \sz.(s (s z))
  28.  
  29. etc.
  30.  
  31. We want a successor.
  32. If we had a successor "add1" combinator, we could have: (add1 five) -> six.
  33. and in general (add1 'n') -> 'n+1', where 'n' is our church numeral
  34. representation for n, and 'n+1' is our church numeral rep for n+1,
  35. both quasi-quoted. If we had s and z, all we'd need is one more
  36. application of s:
  37.  
  38. (s ('n' s z))   or the less obvious:
  39. ('n' s (s z))
  40.  
  41. where 'n' is the rep for our n'th church numeral.
  42. But we don't have s and z and so we abstract them out, getting:
  43.  
  44. 'n+1' == \sz.(s ('n' s z)) or the less obvious:
  45. 'n+1' == \sz.('n' s (s z))
  46.  
  47. By abstracting over 'n' we can define add1 as follows:
  48.  
  49. add1_version1 == \nsn.(s (n s z)) or the less obvious:
  50. add1_version2 == \nsz.(n s (s z)).
  51.  
  52. We'll use version1 here because it's the easiest to prove things
  53. about.
  54.  
  55. A church numeral is an abstraction over the n'th composition of a
  56. function, hence for some function f: ('n' f) -> f^n
  57. (right-associated).
  58.  
  59. This means that for example (three add1) is just: 
  60.                     \x.(add1 (add1 (add1 x)))
  61. So so we clearly have:
  62.          ('n' add1 'm') -> 'n+m'.
  63. Remeber that in LC and CL we auto-left-associate, and so (a b c)
  64. is really ((a b) c) ... side note ...
  65.  
  66. So we get addition by abstracting over 'n' and 'm':
  67. add == \nm.(n add1 m)
  68. where add1 is just a placeholder for the text of the add1 combinator,
  69. and a simple substitution can take place, yielding a formal mess.
  70.  
  71. (add five) is the procedure which adds 5 to anything ...
  72. (four (add five)) is thus: \x.(add5 (add5 (add5 (add5 x)))). If
  73. we apply it to zero we get twenty. In general:
  74.                         ('n' (add 'm') zero) -> 'n*m'
  75. so we abstract over 'n' and 'm' getting:
  76. mul == \nm.(n (add m) zero)
  77.  
  78. (mul three) is the procedure which multiplies something by three ...
  79. (two (mul three)) is thus: \x.(mul3 (mul3 x)). If we apply this to one
  80. we get 3^2 -> 9. In general:
  81.                           ('m' (mul 'n')) -> 'n^m'
  82. We abstract over 'n' and 'm' and thus get exponentiation:
  83. exp == \nm.(m (mul n) one)
  84.  
  85. This can go on all the way to ackerman and above. Ackermann is gotten
  86. through exponentiating the lambda expression taking the
  87. super-n-exponent and returning the super-n+1-exponent and applying it
  88. to exponentiation ... :)
  89.  
  90. Another interesting point is that exponentiation on church numerals is
  91. just \nm.(m n) or if you are willing to cope with a change of order in
  92. the arguments, it's just the identity \x.x. This is so because composition
  93. and exponentiation are governed by a similar algebraic structure.
  94.  
  95. Church numerals are a lot of fun!
  96.  
  97. Mayer.
  98.  
  99.  
  100.  
  101.