|A summary of this article appears in Lambda calculus.|
|This article is of interest to the following WikiProjects:|
- 1 Moved
- 2 Scheme Example
- 3 Name
- 4 Haskell functions
- 5 Relationship to Gödel numbering
- 6 External implementations
- 7 Zero-predicate
- 8 Currying
- 9 Mention Peano axioms?
- 10 Added an explanation of predecessor
- 11 Clean up
- 12 Division and negative numbers
- 13 External links modified
- 14 Church encoded boolean logic operators and
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 SidawayTalk 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.--18.104.22.168 07:23, 15 August 2006 (UTC)
I see no reason why not to include the Scheme code. There may be readers of this article that do not know Haskell but do know Scheme. However I would reformat the above Scheme code in a more readable form such as:
(define (natural-number->church-numeral n) (if (zero? n) (lambda (f) (lambda (x) x))) (lambda (f) (lambda (x) (f (((natural-number->church-numeral (- n 1)) f) x)))))) (define (church-numeral->natural-number n) ((n (lambda (x) (+ x 1))) 0))
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)
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)
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. --LambiamTalk 07:15, 16 November 2006 (UTC)
The term (\n.((n(\x.F))(\x.T))) [n], where [n] is the Church numeral of n, equals T if n is zero and F is n is not zero. Should the predicate Zero?=\n.((n(\x.F))(\x.T)) not be added to the numerical functions like Plus, Pred, etc? Jos.koot (talk) 10:17, 1 April 2009 (UTC)
Mention Peano axioms?
Are Peano axioms at all related to Church encodings for numbers and addition? If so, they ought to at least be referenced. —Preceding unsigned comment added by Indil (talk • contribs) 04:27, 12 May 2011 (UTC)
Added an explanation of predecessor
I found the explanations found elsewhere hard to follow. I hope this is more accessible.
I am considering some cosmetic changes to this page to write the lambda calculus using the Extension:Math - MediaWiki. If anyone has a strong affection for the current layout please tell me and I will desist. I really like MathJax option in preferences for displaying math. I have never had any problem with it and it is much clearer. Also it zooms when you click on it :). I use x\ y for application, which looks good but is a little cumbersome to write.
Division and negative numbers
I added division and signed numbers. Its overkill in terms of demonstrating the Church-Turing thesis, but some people appear to be curious about how negative number may be implemented. The best source I have found on signed numbers is,
but its really a high level summary answer to a question. I don't know if it is appropriate to add it as a reference. Other sites were hard to understand and or coded in Scheme.
The best I found for division is Lloyd Allison's site,
His implementation of DIVMOD allows both divisor and remainder to be defined. I haven't used exactly that definition because it is harder to understand and it uses MINUS (MONUS) twice, which takes many beta reductions. However the description I have given doesn't seem that good to me. I will think on it.
Hello fellow Wikipedians,
I have just modified one external link on Church encoding. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:
- Added archive https://web.archive.org/web/20160304083208/http://tromp.github.io/cl/LC.pdf to http://tromp.github.io/cl/LC.pdf
When you have finished reviewing my changes, please set the checked parameter below to true or failed to let others know (documentation at
An editor has reviewed this edit and fixed any errors that were found.
- If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
- If you found an error with any archives or the URLs themselves, you can fix them with this tool.
Church encoded boolean logic operators and 
Someone brought up the two definitions for boolean negation in #haskell, talking about the definitions and in this section.
No one seemed to know why there were two and the definitions seemed to work both in haskell and in python so I don't understand the difference. It doesn't seem to have anything to do with strict v. lazy -- as opposed to what the notes seem to say -- since both work in both a strict and a lazy language.