[转帖]The Lambda Calculus for Absolute Dummies (like myself)
Monday, May 7, 2012
The Lambda Calculus for Absolute Dummies (like myself)
Unfortunately, most people outside of programming and computer science don't know exactly what computation means. Many may have heard of Turing Machines, but these things tend to do more harm than good, because they leave strong intuitions of moving wheels and tapes, instead of what it really does: embodying the nature of computation.
The Lambda Calculus does exactly the same thing, but without wheels to cloud your vision. It might look frighteningly mathematical from a distance (it has a greek letter in it, after all!), so nobody outside of academic computer science tends to look at it, but it is unbelievably easy to understand. And if you understood it, you might end up with a much better intuition of computation.
A line of symbols is called an expression. It might look like this: λx.(xy) (ab)
We only have the following symbols:
- Single letters (like a, b, c, d...), which are calledvariables. An expression can be a single letter, or several letters in a row. More generally, we can write any two or more expressions together to get another expression.
- Parentheses: ( ). Parentheses can be used to indicate that some part of an expression belongs together (just as the braces around this part of the sentence make it belong together). Where we don't have parentheses, we look at expressions simply from left to right.
- The greek letter λ (pronounced, of course:Lambda), and the dot: . With λ and the dot, we can write functions. A function starts always with the λ and a variable, followed by a dot, and then comes an expression. The λ does not have any complicated meaning: it just says that a function starts here. The λ-variable-. part of a function is called its head, and the remainder (the expression) is called the body.
A function. |
Q: What is the value or meaning of a variable?
A: None. Variables do not stand for anything. They are just empty names. Even the name is unimportant. The only thing that matters is: when two variables have the same name, they are the same. You can rename variables all you want, without changing the expression.
Q: What does a function calculate?
A: Nothing, really. It is just a kind of expression, with a head and a body. It just stands there. The only thing we can do with it is to resolve it.
Cut & Paste
Functions can be resolved if they are followed by another expression. The resolution works by taking the variable mentioned in the head, and replacing all of its occurrences within the body with the expression after the function. Wecut the expression after the function, and paste it into the body, in every place indicated by the head. Having done that, we throw the head away, because it has served its purpose: telling us which variable to replace.
Resolving a function: Replacing all occurrences of y with the expression(ab) |
The resolution of functions is the only thing we can ever do in the Lambda Calculus. Once we have gotten rid of all the lambdas, or if there are no more expressions after the remaining functions, we cannot replace anything any more. We can go home now.
Q: Can functions contain other functions?
A: Absolutely. Functions are expressions, and expressions can contain other expressions, so functions can be parts of the bodies of other functions, or be part of the replacing expression. In fact, we have expressions like λx.λy.xzy so often that we like to abbreviate them as λxy.xzy. This means that we will try to replace the first variable in the head (x) with the first expression after the body (xzy), the second variable (y) with the next one after that, and so on.
The variables mentioned in the head (the one tagged for replacement) are called bound variables. Unmentioned variables are free variables. Because functions can be part of other functions, a variable may be both bound and free in the same expression.
Q: I find this a little bit confusing.
A: Think of it like this: Imagine you are editing a very minimalist gossip newspaper. Everything the newspaper writes about, ever, are names (we don't have articles, verbs, pronouns–just names). People don't want to be recognized in your paper, and you anonymize them by replacing all names with arbitrary pseudonyms. So, the names do not mean anything, but if two names in the same text are the same, they refer to the same person.
Minimalist Lambda Newspaper |
All text in the newspaper is arranged in text blocks. A text block is ultimately made up of nothing but names, and it may have a headline, but does not have to. Headlines are printed in bold face, and consist of a single name. All occurrences of that name within the text belonging to the headline arefamous, that is, they refer to that headline person. All names that are not headline material areordinary. Text blocks may contain other text blocks, including their headings (which work like sub-headings, or sub-sub-headings and so on). Thus, a name may be ordinary in one sub-text, but in another, it may be made famous by the headline of that sub-text.
This is exactly like the Lambda Calculus: names are variables, text blocks are expressions, and headlines are function heads, only instead of being printed in bold, they are surrounded by a λ and a dot, so we know where they begin and end.
The resolution operation is a simple find/replace operation. We find all occurrences of the bound name in a headlined text block, and replace each of them with the following text block.
By the way: we might run into a little problem if the replacing text contains names that are also mentioned in the original text that we merge it into. All names are anonymized pseudonyms, but we could have used the same pseudonym for different people in different texts. If we combine these texts now, we must make sure that different people are referred to by different pseudonyms, so perhaps we have to rename some of them.
Alternatively, we might insist that no two text blocks use the same names. (In other words: either use different variables in unrelated expressions, or make sure you do not forget to rename them during the replace operation as necessary.)
Q: What happens if a variable is bound in the head of a function, but does not occur in the body?
A: The variable is bound, of course. But during replacement, the replacing expression will simply disappear, as there are no places where it could be inserted. That is ok, really: it simplifies our result, so what is not to like?
Numbers
With all the technicalities out of the way (yay! that was easy, wasn't it?), lets see what nice tricks we can do with the Lambda Calculus. You might argue that computation should be able to do things with numbers, so let us build some. Mathematicians often like to start with natural numbers, and then go from there, by defining all sorts of operations that give us other the other number types.
The easiest way of defining all natural numbers at once works by first defining the first one (which is zero), and a successor operation. By using the successor operation on any natural number, we get another, bigger natural number, and so we can derive them all by counting forward.
Let us express zero as:
0 :⇔ λ sz.z
(Remember: this is shorthand for λs.λz.z, and it means exactly the same thing as λab.b, or λqx.x.)
This expression has an interesting property: when resolved, it will throw away the first expression after it, and keep the second one intact. The bound variable s will be replaced by nothing (it does not occur in the body), and the variable z by itself.
Similary, we can use:
1 = λ sz.s(z)
2 = λ sz.s(s(z))
3 = λ sz.s(s(s(z)))
4 = λ sz.s(s(s(s(z))))
...
In other words, our number notation works by nesting the expression s(...) around our z as often as the number says (which also means: if we resolve the number n, it will replicate the following expression n times). We can also say: we apply s n times to z.
A nice successor function is
Q: This is a very strange way of writing numbers...
A: Actually, from the point of view of mathematics, this is not stranger than using the characters 1, 2, 3... and so on, or Roman literals (I, II, III, IV, V...), or Chinese ones (一, 二, 三, 四, 五, ...), or binary notation (1, 10, 11, 100, 101...). There is no true way of writing numbers, there are only conventions. Natural numbers do not care about how we spell them.
Addition
Multiplication
Counting Backwards
Let us now apply this function n times to the starting pair (0, 0), and select the second half of the pair, which wil be our final result. You may have noticed that I just cheated a little:(0, 0) is not totally the same as (0, –1), so it is not a sparkling example of a pair (a, a-1). However, we have no negative numbers to work with yet, and for our helper functionNEXT-PAIR, it does not make any difference, because it ignores the second half of the pair anyway. Repeated application of NEXT-PAIR on (0, 0) will give us (1, 0), (2, 1), (3, 2), (4, 3) and so on.
Q: I can see how we can do subtraction: by applying the predecessor operation multiple times. But every time, we have to go back to 0 and produce all intermediate numbers with the successor operation, just to do a single predecessor operation. Isn't this very inefficient?
A: Who cares! The Lambda Calculus only claims toeffectively compute everything that can be computed–but it does not promise to do itefficiently. (Also, it is a mathematical idea, so it can run at infinite speed in some ephemeral mathematical universe.)
Logic
Conditionals
We cannot just compute logical values from other logical values. The following function tells us if a given value is equal to 0. If it is, we get TRUE, and FALSE otherwise. Such a test is very useful when writing programs.
IS-ZERO :⇔ λ a.a FALSE NOT FALSE
If we apply IS-ZERO to any value n, we get
IS-ZERO n = n FALSE NOT FALSE
This will apply the function FALSE n times to the functionNOT, and the result to the remaining FALSE. The each time, the first FALSE (= λ xy.y) erases the expression directly after it. Eventually (after n times) it gets to NOT FALSE, erases theNOT and returns the FALSE. Thus, the result of IS-ZEROn is always FALSE. (If you find this confusing, try an example.)
The only exception is when n = 0. If we apply 0 to FALSE NOT FALSE, it will erase the first expression, and only NOT FALSE = TRUE remains:
IS-ZERO 0
= λ sz.z FALSE NOT FALSE
= NOT FALSE
= TRUE
Now that we know if a number is 0, we can find out if one number is greater than or equal to (≥) another:
GREATER-OR-EQUAL n m :⇔ λ n m. IS-ZERO(n P m)
Using ≥, we can also determine equality: n = m, if n ≥ m andm ≥ n. We can express this directly now:
EQUAL n m :⇔ λ n m. AND (GREATER-OR-EQUAL(n m) GREATER-OR-EQUAL(m n))
= λ n m. AND (IS-ZERO(n P m) IS-ZERO(m P n))
Furthermore...
As you see, the Lambda Calculus is a (minimalist) programming language. As ist must be, since every possible computer program can ultimately be mapped into a Lambda function. In fact, the venerable and powerful programming language Lisp has been built directly on the idea of the Lambda calculus, mainly by tweaking the syntax in useful ways, formalizing the creation of function macros and adding a few practical data types.
Everything that is computable
(you can follow me on Twitter: https://twitter.com/Plinz)
最新文章
- 关于安装Apache之后,解析PHP的配置
- 在cmd和terminal怎么粘贴?
- .NET LINQ 元素操作
- js弹框3秒后自动消失
- jpype调用jar
- 菜鸟学Windows Phone 8开发(4)——设置应用程序样式
- LeetCode Shortest Word Distance III
- jQuery图片延迟加载插件
- Bmp 解析 (2013-09-09 19:30:41)
- 使用FileSystem自带的api读取hdfs中的文件
- python笔记:#001#python简介
- XP .Net 4.0使用Microsoft.Bcl需要安装XP补丁NDP40-KB2468871-v2-x86
- VMware vsphere client报错问题
- 虚拟机安装macos 分辨率不正常修改不了,不能全屏如何解决
- 管理git生成的多个ssh key
- 在Visual C#中使用XML指南之读取XML
- 3D Spherical Geometry Kernel( Geometry Kernels) CGAL 4.13 -User Manual
- asp.net MVC4 框架揭秘 读书笔记系列3
- ubuntu16.04+opencv3.0.0
- Python基本数据类型之列表