Talk:Church encoding

From Wikipedia, the free encyclopedia

The following discussion was moved here from Talk:Church numeral as a result of that page being merged into this one. --David Wahler (talk) 15:53, 25 October 2005 (UTC)

Contents 1 Scheme Example 2 Name 3 Haskell functions 4 Relationship to Gödel numbering

[edit] Scheme Example

Isn't the scheme implementation backwards?

That is, shouldn't it be:

(define zero (lambda (f) (lambda (x) x)))
(define one  (lambda (f) (lambda (x) (f x))))
(define two  (lambda (f) (lambda (x) (f (f x)))))
(define three (lambda (f) (lambda (x) (f (f (f x))))))

This would be in line with both the top-of-page explanatory text and the Haskell, not to mention the examples given on the lambda calculus page. Actually, why make it as hard to read as it is? Just say:

(define (zero f) (lambda (x) x))
(define (one f) (lambda (x) (f x)))
(define (two f) (lambda (x) (f (f x))))
(define (three f) (lambda (x) (f (f (f x)))))

The unchurch examples also become less obscure:

(define (add1 x) (+ x 1))
(define (unchurch c) ((c add1) 0))

However, I fail to see what the scheme example adds at this point. The Haskell is already clean, and above all matches the English text. Also, the Haskell allows you to define all the church integers at one swoop, whereas the scheme example only shows a few examples (because the scheme equivalent of the "church" function is just too ugly).

Scrap the scheme. It adds nothing to the article and just gets in the way of understanding what church numbers are.

• I agree with erasing the scheme example. It is worse than the Haskell one. If someone wants to do it in pure lambda calculus, that would be worthwhile. Brighterorange 16:40, 2 Jun 2005 (UTC)

I know no Haskell, and I know nobody who knows Haskell. I don't even know, for sure, what Haskell is. The Scheme I understand. It's been around forever and it's well understood. --Tony Sidaway^Talk 18:25, 4 August 2005 (UTC)

A Scheme example should be added... I'd be willing to take it a little further as well, showing what addition and multiplication of Church numerals look like. Hundreds of students are introduced to this concept each year using Scheme (if only through Abelson and Sussman's book, used in 6.001 at MIT) -- it makes no sense to me not to have Scheme examples and some discussion along with them. --Cityintherain 02:47, 29 June 2006 (UTC)

There are two possible encodings of church numerals; one has the successor function as the first parameter, the other takes the zero value first. I think the article ought to simply give the lambda-calculus versions and let students of each language make their own translations as appropriate. --bmills 21:37, 24 October 2005 (UTC)

The haskell code here is *awful*. While the scheme code "adds" less, the entire point of adding "less" is that it makes the underlying concepts clearer to those who don't already have full understanding or otherwise need reminding at 3 in the morning while drunk and arguing with somebody about something they haven't thought about in years -- scheme is intentionally "simple". As is, an argument could be made for C. The haskell code relies on several DWIMs of haskell such that translation to a language that isn't haskell relies on very particular knowledge of Haskell's currying and parenthesizing rules, which is *not* a feature for a "get a clue" encyclopedia article (haskell hackers, please stop doing this; it's not the first time I've seen a straightforward concept obscured by "see how wonderful haskell is?"). Scheme code for church/unchurch that is explicitly single argument lambda calculus with all the parens in the right place is:

(define (church n)
  (if (zero? n)
      (lambda (f)
        (lambda (x)
          x)))
      (lambda (f)
        (lambda (x)
          (f (((church (- n 1)) f) x))))))
(define (unchurch n)
  ((n (lambda (x) (+ x 1))) 0))

The rest is left as an exercise if it doesn't already exist in the article history. Somebody less annoyed than me please feel welcome to rework the articule as needed to get what seems saner than what is written.--66.92.73.217 07:23, 15 August 2006 (UTC)

[edit] Name

I think this article should be called "church numerals"; that's the name we always use in school. Church "integer" is incorrect, because this encoding only represents the natural numbers, not the integers (which may be negative). Is there some historic precedent for "church integers"? Brighterorange 16:40, 2 Jun 2005 (UTC)

Well, it should be "Church numeral" (singular) as I understand the Wikipedia convention. It's astonishing that someone would apparently invent such a mistaken term as "Church integer" and to redirect from the previously correct name! (These are a kind of numeral, definitely not a kind of integer, for crying out loud.) Trouble is, there are now a zillion links to the incorrect name, and I'm too new to editing to know how to fix them all economically. --r.e.s. (Talk) 17:36:15, 2005-08-04 (UTC)

Because a study of Church numerals generally also includes other Church encodings (such as Church booleans), and concepts from one greatly aid understanding of others, I'm proposing that this page be merged into Church encoding. --bmills 21:39, 24 October 2005 (UTC)

[edit] Haskell functions

The Haskell functions are elegant. But I can't help noticing that if you use extended Haskell, you can write the types as

church :: Integer -> (forall a. Church a)
unchurch :: (forall a. Church a) -> Integer

This shows the isomorphism (actually, with natural numbers, not Integer) a little more clearly. But then others might complain that this isn't (yet) Haskell. —Ashley Y 11:33, 2 December 2005 (UTC)

I'm more of an ML person myself, but aren't both of those pretty much the same? forall a. Church a just eliminates the prenex restriction on the type of the function, if Haskell even has a prenex restriction. I don't suppose it really matters much either way. --bmills 22:30, 4 December 2005 (UTC)

The type signature for "church" is exactly the same, as you say, but the one for unchurch isn't. (church,unchurch) is not an isomorphism between the naturals and "Church Integer", but it is an isomorphism between the naturals and "forall a. Church a". However, I don't intend to change it. —Ashley Y 10:38, 5 December 2005 (UTC)

[edit] Relationship to Gödel numbering

The intro states: "Many students of mathematics are familiar with Gödel numbering members of a set; Church encoding is an equivalent operation defined on lambda abstractions instead of natural numbers." Doesn't this needlessly obfuscate things? What meaning of "equivalent" is this? I think it is best to delete this sentence.  --Lambiam^Talk 07:15, 16 November 2006 (UTC)