{
localUrl: '../page/church_encoding.html',
arbitalUrl: 'https://arbital.com/p/church_encoding',
rawJsonUrl: '../raw/6qb.json',
likeableId: '3750',
likeableType: 'page',
myLikeValue: '0',
likeCount: '1',
dislikeCount: '0',
likeScore: '1',
individualLikes: [
'PatrickStevens'
],
pageId: 'church_encoding',
edit: '1',
editSummary: '',
prevEdit: '0',
currentEdit: '1',
wasPublished: 'true',
type: 'wiki',
title: 'Church encoding',
clickbait: 'How can you represent things like numbers as lambda expressions?',
textLength: '7020',
alias: 'church_encoding',
externalUrl: '',
sortChildrenBy: 'likes',
hasVote: 'false',
voteType: '',
votesAnonymous: 'false',
editCreatorId: 'DylanHendrickson',
editCreatedAt: '2016-12-06 01:55:46',
pageCreatorId: 'DylanHendrickson',
pageCreatedAt: '2016-12-06 01:55:46',
seeDomainId: '0',
editDomainId: 'AlexeiAndreev',
submitToDomainId: '0',
isAutosave: 'false',
isSnapshot: 'false',
isLiveEdit: 'true',
isMinorEdit: 'false',
indirectTeacher: 'false',
todoCount: '0',
isEditorComment: 'false',
isApprovedComment: 'false',
isResolved: 'false',
snapshotText: '',
anchorContext: '',
anchorText: '',
anchorOffset: '0',
mergedInto: '',
isDeleted: 'false',
viewCount: '37',
text: 'In [-6ld], the only objects we can work with are $\\lambda$ expressions, which represent functions. So how can we talk about, and perform computations on, more familiar objects like [54y numbers]? We'll have to come up with a way to encode numbers, and operations on them, as $\\lambda$ expressions.\n\n# [45h Natural numbers]\n\nLet's figure out how to express the natural numbers $0,1,2,\\dots$ in $\\lambda$ calculus. First of all, they shouldn't have any free variables; we don't want numbers to depend on some undefined $x$. So, like any $\\lambda$ expression with no free variables, they need to start with a $\\lambda$. That is, they need to be functions.\n\nSay they only take in one input, so they're $\\lambda x.M$, where $M$ is a $\\lambda$ expression (that varies with the number encoded) containing only the variable $x$. What could $M$ look like? The obvious things to try look like $x\\ (x\\ (x\\ x))$ and $((x\\ x)\\ x)\\ x$. To encode $0$, we would use the simplest version of this: just $x$. So the examples listed earlier would encode for $3$.\n\nWhile it's possible to use one of those definitions for numbers, they don't work that well. What type of object is $x$ supposed to be? Should it be a function, or the input to a function? (Yes, everything in $\\lambda$ calculus can be both, but it can still help to think of those two types differently.) Instead, we'll have each natural number be a function on two inputs, of the form $\\lambda f.\\lambda x.M$, where we think of $f$ as a "function" and $x$ as an "object."\n\nSo what should $0$ be? How about it does nothing to its inputs, and just returns $x$, so $0=\\lambda f.\\lambda x.x$. What about $1$? We have a function and an object, so the natural thing to do is apply the one to the other: $1=\\lambda f.\\lambda x.f\\ x$. At this point it should be clear how we're going to continue:\n\n- $2=\\lambda f.\\lambda x.f\\ (f\\ x)$\n- $3=\\lambda f.\\lambda x.f\\ (f\\ (f\\ x))$\n- $4=\\lambda f.\\lambda x.f\\ (f\\ (f\\ (f\\ x)))$\n\nAnd so on, so $n$ is the function that, on inputs $f$ and $x$, applies $f$ to $x$ $n$ times. Informally, we could write $n=\\lambda f.\\lambda x.f^n(x)$.\n\n# Operations on numbers\n\nWe've defined natural numbers, but so far they aren't doing anything. We expect numbers to be able to be added and multiplied, so let's figure out how to express those in $\\lambda$ calculus. We'll start easy: with the successor function $S(n)=n+1$.\n\n## [successor]\n\nOn to defining $S$. It's a function that takes in a number, so let's start with $\\lambda n$. What should it return? Another number, of course, which starts $\\lambda f.\\lambda x$. Now we should use $n$, which applies $f$ to $x$, $n$ times. But we want $n+1$, so we want to apply $f$ to $x$, $n+1$ times. If we apply $f$ $n$ times, and then once more, we can achieve this:\n\n$$S=\\lambda n.\\lambda f.\\lambda x.f\\ (n\\ f\\ x).$$\n\nHere $(n\\ f\\ x)$ gives us $f^n(x)$, so $f\\ (n\\ f\\ x)$ is $f(f^n(x))=f^{n+1}(x)$. We could do these applications in the other order, first taking $f\\ x$ and then applying $f$ to that $n$ times, so\n\n$$S^\\prime=\\lambda n.\\lambda y.\\lambda x.n\\ f\\ (f\\ x).$$\n\nWhile $S$ and $S^\\prime$ are equivalent when $n$ is a natural number, they aren't equal; if we plug in $\\lambda a.\\lambda b.a$ for $n$, we have\n\\begin{align}\n S\\ (\\lambda a.\\lambda b.a) &= \\lambda f.\\lambda x.f\\ ((\\lambda a.\\lambda b.a)\\ f\\ x) \\newline\n &= \\lambda f.\\lambda x.f\\ f\n\\end{align}\nbut\n\\begin{align}\n S^\\prime\\ (\\lambda a.\\lambda b.a) &= \\lambda f.\\lambda x.(\\lambda a.\\lambda b.a)\\ f\\ (f\\ x)) \\newline\n &= \\lambda f.\\lambda x.f\n\\end{align}\nwhich is a different function.\n\nTo check that $S$ works as we want, let's verify that $S\\ 3=4$. For these worked examples, it's probably much more informative if you work through them yourself; they're provided here so you can check that you did it right.\n\n%%hidden(Worked example: successor):\n\\begin{align}\n S\\ 3 &= (\\lambda n.\\lambda f.\\lambda x.f\\ (n\\ f\\ x))\\ (\\lambda f.\\lambda x.f\\ (f\\ (f\\ x))) \\newline\n &= (\\lambda f.\\lambda x.f\\ ((\\lambda f.\\lambda x.f\\ (f\\ (f\\ x)))\\ f\\ x)) \\newline\n &= (\\lambda f.\\lambda x.f\\ (f\\ (f\\ (f\\ x))) \\newline\n &= 4\n\\end{align}\n%%\n\n## [addition]\n\nNow that we know how to add $1$, let's figure out how to add arbitrary numbers. Suppose we have two numbers $m$ and $n$; remember $m$ means "on inputs $f$ and $x$, apply $f$ to $x$ $m$ times," and similarly for $n$. We want $m+n$ to apply $f$ to $x$ $m+n$ times, so how can we accomplish that? If we apply $f$ to $x$ $n$ times, and then $m$ more times, it should have the desired effect. Writing this as a $\\lambda$ term,\n\n$$+=\\lambda m.\\lambda n.\\lambda f.\\lambda x.m\\ f\\ (n\\ f\\ x)$$\n\nAgain $n\\ f\\ x$ is $f$ of $x$ $n$ times, and the $m\\ f$ in front applies $f$ to the result $m$ more times. We could of course swap $m$ and $n$, since addition is [3jb commutative].\n\nLet's verify that $2+3=5$. We have to write $2+3$ as $+\\ 2\\ 3$ because we haven't defined infixes in $\\lambda$ calculus (though we could define $m+n$ to mean $+\\ m\\ n$.\n\n%%hidden(Worked example: addition):\n\\begin{align}\n +\\ 2\\ 3 &= (\\lambda m.\\lambda n.\\lambda f.\\lambda x.m\\ f\\ (n\\ f\\ x))\\ (\\lambda f.\\lambda x.f\\ (f\\ x))\\ (\\lambda f.\\lambda x.f\\ (f\\ (f\\ x))) \\newline\n &= \\lambda f.\\lambda x.(\\lambda f.\\lambda x.f\\ (f\\ x))\\ f\\ ((\\lambda f.\\lambda x.f\\ (f\\ (f\\ x)))\\ f\\ x) \\newline\n &= \\lambda f.\\lambda x.(\\lambda f.\\lambda x.f\\ (f\\ x))\\ f\\ (f\\ (f\\ (f\\ x))) \\newline\n &= \\lambda f.\\lambda x.f\\ (f\\ (f\\ (f\\ (f\\ x)))) \\newline\n &= 5\n\\end{align}\n%%\n\n## [multiplication]\n\nMultiplication might seem a bit harder. Now, given two numbers $m$ and $n$, we want to apply some function $f$ to $x$ $m\\times n$ times. If we take a function that applies $f$ $n$ times, and then apply that function $m$ times, we should get something that applies $f$ $n$ times, $n$ times, which is the same as applying $f$ $m\\times n$ times. That is, $(f^n)^m(x)=f^{m\\times n}(x)$. The intermediate function that applies $f$ $n$ times is $\\lambda x.n\\ f\\ x$, or using [eta_convesion $\\eta$-conversion], simply $n\\ f$. We just need to apply $n\\ f$, $m$ times, so we can define\n\n$$\\times=\\lambda m.\\lambda n.\\lambda f.\\lambda x.m\\ (n\\ f) x$$\n\nor, using $\\eta$-conversion again,\n\n$$\\times=\\lambda m.\\lambda n.\\lambda f.m\\ (n\\ f).$$\n\nAgain multiplication is commutative, so we could swap $m$ and $n$ to get an equally good definition.\n\nWe should have $\\times\\ 2\\ 3=6$; let's check this.\n\n%%hidden(Worked example: multiplication):\n\\begin{align}\n \\times\\ 2\\ 3 &= (\\lambda m.\\lambda n.\\lambda f.m\\ (n\\ f))\\ (\\lambda f.\\lambda x.f\\ (f\\ x))\\ (\\lambda f.\\lambda x.f\\ (f\\ (f\\ x))) \\newline\n &= \\lambda f.(\\lambda f.\\lambda x.f\\ (f\\ x))\\ ((\\lambda f.\\lambda x.f\\ (f\\ (f\\ x)))\\ f) \\newline\n &= \\lambda f.(\\lambda f.\\lambda x.f\\ (f\\ x))\\ (\\lambda x.f\\ (f\\ (f\\ x))) \\newline\n &= \\lambda f.\\lambda x.(\\lambda x.f\\ (f\\ (f\\ x)))\\ ((\\lambda x.f\\ (f\\ (f\\ x)))\\ x) \\newline\n &= \\lambda f.\\lambda x.(\\lambda x.f\\ (f\\ (f\\ x)))\\ (f\\ (f\\ (f\\ x))) \\newline\n &= \\lambda f.\\lambda x.f\\ (f\\ (f\\ (f\\ (f\\ (f\\ x)))))) \\newline\n &= 6\n\\end{align}\n%%\n\n##(this page is unfinished)',
metaText: '',
isTextLoaded: 'true',
isSubscribedToDiscussion: 'false',
isSubscribedToUser: 'false',
isSubscribedAsMaintainer: 'false',
discussionSubscriberCount: '1',
maintainerCount: '1',
userSubscriberCount: '0',
lastVisit: '',
hasDraft: 'false',
votes: [],
voteSummary: 'null',
muVoteSummary: '0',
voteScaling: '0',
currentUserVote: '-2',
voteCount: '0',
lockedVoteType: '',
maxEditEver: '0',
redLinkCount: '0',
lockedBy: '',
lockedUntil: '',
nextPageId: '',
prevPageId: '',
usedAsMastery: 'false',
proposalEditNum: '0',
permissions: {
edit: {
has: 'false',
reason: 'You don't have domain permission to edit this page'
},
proposeEdit: {
has: 'true',
reason: ''
},
delete: {
has: 'false',
reason: 'You don't have domain permission to delete this page'
},
comment: {
has: 'false',
reason: 'You can't comment in this domain because you are not a member'
},
proposeComment: {
has: 'true',
reason: ''
}
},
summaries: {},
creatorIds: [
'DylanHendrickson'
],
childIds: [],
parentIds: [],
commentIds: [],
questionIds: [],
tagIds: [],
relatedIds: [],
markIds: [],
explanations: [],
learnMore: [],
requirements: [],
subjects: [],
lenses: [],
lensParentId: '',
pathPages: [],
learnMoreTaughtMap: {},
learnMoreCoveredMap: {},
learnMoreRequiredMap: {},
editHistory: {},
domainSubmissions: {},
answers: [],
answerCount: '0',
commentCount: '0',
newCommentCount: '0',
linkedMarkCount: '0',
changeLogs: [
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '22739',
pageId: 'church_encoding',
userId: 'DylanHendrickson',
edit: '0',
type: 'newEditGroup',
createdAt: '2017-09-02 03:25:44',
auxPageId: 'AlexeiAndreev',
oldSettingsValue: '669',
newSettingsValue: '1'
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '20598',
pageId: 'church_encoding',
userId: 'DylanHendrickson',
edit: '1',
type: 'newEdit',
createdAt: '2016-12-06 01:55:46',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
}
],
feedSubmissions: [],
searchStrings: {},
hasChildren: 'false',
hasParents: 'false',
redAliases: {},
improvementTagIds: [],
nonMetaTagIds: [],
todos: [],
slowDownMap: 'null',
speedUpMap: 'null',
arcPageIds: 'null',
contentRequests: {}
}