Talk:Church encoding

Moved

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)

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)

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))

Jos.koot (talk) 16:22, 1 April 2009 (UTC)

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)

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)

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)

I agree. Comparing it to Peano arithmetic seams better. —Preceding unsigned comment added by 67.188.108.234 (talk) 06:45, 3 July 2010 (UTC)

External implementations

I have written a Python implementation of Church lists using higher order functions, when I was bored. Feel free to reference it, if you like. --Ertugrul S. (talk) 01:26, 26 January 2009 (UTC)

Zero-predicate

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)

Currying

Shouldn't the functions here be the same as those in the lambda calculus article? Phantom Hoover (talk) 14:44, 19 December 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.

Thepigdog (talk) 05:30, 3 November 2013 (UTC)

Clean up

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.

Thepigdog (talk) 17:26, 4 December 2013 (UTC)

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,

• representing-negative-and-complex-numbers-using-lambda-calculus

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,

• Lambda Calculus Integers

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.

Thepigdog (talk) 12:29, 25 March 2014 (UTC)

External links modified

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 {{Sourcecheck}}).

Y 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.

Cheers.—InternetArchiveBot (Report bug) 14:12, 24 November 2016 (UTC)

Church encoded boolean logic operators $not_{1}$ and $not_{2}$

Someone brought up the two definitions for boolean negation in #haskell, talking about the definitions $not_{1}$ and $not_{2}$ 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.

Clarification or correction of the article would be much appreciated. 2A02:1810:2505:BF00:EC76:4D29:7CE7:51FB (talk) 23:19, 23 December 2018 (UTC)anon

Agreed, the notes are definitely incorrect. I'm removing them, and if there are relevant actual differences between the two they can be added in the future. Ebf526 (talk) 01:02, 20 July 2021 (UTC)

Church numeral division

There exists a much smaller term for division:

   divide = \n.\m.\f.\x.n (\x.\f.f x) (\d.x) (n (\t.m (\x.\f.f x) (\c.f (c t)) (\x.x)) x)

References

Too many list representations

I think the "Two pairs as a list node" representation could be left out.

The Scott encoding should be considered the standard representation, the right folding is of interest in its own right, and the "single pair as a list node" achieves the greatest overall simplicity.

Compared to he latter, "Two pairs as a list node" just seems unnecessarily complicated in every way.