home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #18 / NN_1992_18.iso / spool / comp / lang / scheme / 2024 < prev    next >
Encoding:
Text File  |  1992-08-13  |  3.5 KB  |  124 lines
  1. Newsgroups: comp.lang.scheme
  2. Path: sparky!uunet!gatech!bloom-beacon!INTERNET!dont-send-mail-to-path-lines
  3. From: stone@hilbert.math.grin.EDU (John David Stone)
  4. Subject: Church numerals
  5. Message-ID: <9208131348.AA08840@HILBERT.MATH.GRIN.EDU>
  6. Sender: daemon@athena.mit.edu (Mr Background)
  7. Organization: The Internet
  8. Date: Thu, 13 Aug 1992 13:48:34 GMT
  9. Lines: 113
  10.  
  11.         Here's the classic approach to arithmetic with Church numerals:
  12.  
  13. (define zero
  14.   (lambda (x)
  15.     (lambda (y) y)))
  16.  
  17. (define successor
  18.   (lambda (u)
  19.     (lambda (x)
  20.       (lambda (y) (x ((u x) y))))))
  21.  
  22. (define one (successor zero))
  23.  
  24. (define add
  25.   (lambda (m)
  26.     (lambda (n)
  27.       (lambda (f)
  28.         (lambda (x) ((m f) ((n f) x)))))))
  29.  
  30. (define mult
  31.   (lambda (m)
  32.     (lambda (n)
  33.       (lambda (f) (m (n f))))))
  34.  
  35. (define power
  36.   (lambda (m)
  37.     (lambda (n) (n m))))
  38.  
  39.         And for direct definition of recursive functions (without Y,
  40. incidentally!):
  41.  
  42. (define constant
  43.   (lambda (x)
  44.     (lambda (y) x)))
  45.  
  46. (define ordered-pair
  47.   (lambda (x)
  48.     (lambda (y)
  49.       (lambda (z) ((z (constant y)) x)))))
  50.  
  51. The idea of the ordered-pair notation is that ((ordered-pair x) y) is a
  52. function that yields x when applied to zero and y when applied to any other
  53. Church numeral, thus giving the effect of a test for equality with zero.
  54.  
  55. (define extender
  56.   (lambda (y)
  57.     (lambda (v)
  58.       ((ordered-pair (successor (v zero))) ((y (v zero)) (v one))))))
  59.  
  60. You can think of extender as a function that takes a function y and an
  61. ordered pair v, where v's two elements are a counter and a previously
  62. generated value, and yields an ordered pair consisting of the counter
  63. incremented once and a value obtained by applying y to the old value of
  64. the counter and the previously generated value.
  65.  
  66. (define recurser
  67.   (lambda (x)
  68.     (lambda (y)
  69.       (lambda (u)
  70.         (((u (extender y)) ((ordered-pair zero) x)) one)))))
  71.  
  72. Recurser takes an initial value x, a transition function y, and a Church
  73. numeral u and delivers the result of applying the transition function to
  74. the initial value u times in succession.  (Actually, you think of y as
  75. applying to two arguments to give its value -- the count of the number
  76. of times it's been applied previously, and the value resulting from those
  77. earlier applications.)
  78.  
  79.         Now recursive definitions simply fall out of applications of
  80. recurser:
  81.  
  82. (define recursive-add
  83.   (lambda (n) ((recurser n) (constant successor))))
  84.  
  85. (define recursive-multiply
  86.   (lambda (n) ((recurser zero) (constant (recursive-add n)))))
  87.  
  88. (define recursive-power
  89.   (lambda (m)
  90.     (lambda (n) (((recurser one) (constant (recursive-multiply m))) n))))
  91.  
  92. (define factorial
  93.   ((recurser one) (lambda (x) (recursive-multiply (successor x)))))
  94.  
  95.         In testing these, you may find the following Scheme procedures
  96. useful:
  97.  
  98. (define int->Church
  99.   (lambda (n)
  100.     (if (zero? n)
  101.         zero
  102.         (successor (int->Church (- n 1))))))
  103.  
  104. (define Church->int
  105.   (lambda (numeral)
  106.     ((numeral (lambda (x) (+ 1 x))) 0)))
  107.  
  108. as in:
  109.  
  110. (Church->int (factorial (int->Church 4)))
  111.  
  112. (Church->int ((recursive-power (int->Church 5)) (int->Church 3)))
  113.  
  114. which yield 24 and 125 respectively.
  115.  
  116.         I found the idea behind extender and recurser in Hindley and
  117. Seldin's _Introduction to Combinators and the Lambda-Calculus_, where it is
  118. ascribed to the logician P. Bernays.
  119.  
  120. ------  John David Stone - Lecturer in Computer Science and Philosophy  -----
  121. --------------  Manager of the Mathematics Local-Area Network  --------------
  122. --------------  Grinnell College - Grinnell, Iowa 50112 - USA  --------------
  123. --------  stone@math.grin.edu - (515) 269-3181 - stone@grin1.bitnet  --------
  124.