Lambda Calculus - Computerphile

Summary

このビデオスクリプトでは、コンピューターサイエンスの興味深いトピックであるラムダ計算について語られています。アルンゾ・チャーチが発明したこの概念は、計算からの関数の考え方を表しています。チャーチとアラン・チューリングの博士論文の間に興味深い歴史があります。ラムダ計算は純粋な数学的関数であり、関数型プログラミング言語の基礎となっています。また、現在ではJavaやC#など、多くの主なプログラミング言語に組み込まれています。さらに、論理値のエンコードや再帰を実現するYコンビネータなどの例を通じて、ラムダ計算の応用範囲を示しています。最後に、生物学とラムダ計算の間の興味深い関係について触れています。

Takeaways

• 📚 ラムダ計算はコンピューターサイエンスの重要なトピックの一つであり、関数の計算的观点からの定義を提供します。
• 👨‍🏫 アロンゾ・チャーチはラムダ計算を考案し、関数の純粋な数学的定義を提供したプリンストン大学の数学者です。
• 🤝 ラムダ計算とチューリングマシンは異なる概念ですが、計算能力において等価であり、これらは教会チューリング仮説によって関連しています。
• 🔲 ラムダ計算における関数はブラックボックスであり、内部状態を持たず、純粋な数学的関数です。
• 📝 ラムダ計算では、簡単な記法を使用して関数を定義し、変数、ラムダ記法、関数の適用の3つの要素のみから成り立ちます。
• 🔄 ラムダ計算は変数の代入という基本プロセスに基づいて動作し、関数を適用することで結果を得られます。
• 💡 ラムダ計算は、いかなる計算もエンコードできる強力なモデルであり、チューリングマシンと同様に様々なプログラムを表現できます。
• 🌐 ハスケルのような関数型プログラミング言語は、ラムダ計算に基づいており、そのコア言語はラムダ計算に類似しています。
• 🚀 現代の主要なプログラミング言語は、JavaやC#など、ラムダ計算を組み込んでおり、コンピューターサイエンスの基礎知識として重要です。
• 🔧 ラムダ計算では、データ型や再帰などのコントロール構造が組み込まれていないので、それらをエンコードする必要があります。
• 🔄 Yコンビネータはラムダ計算における再帰のエンコードに重要な役割を果たし、ハスケル言語の名前の由来であるハスケル・カレーによって考案されました。
• 🧬 ラムダ計算と生物学には興味深い関係があり、DNAのダブルヘリックス構造とYコンビネータの構造には類似性があります。

Q & A

ラムダ計算とは何ですか？

ラムダ計算は、計算の概念を関数の観点から捉えたもので、数学者であるアルンゾ・チャーチによって発明されました。関数をブラックボックスとして扱い、入力を与えられたときにどのような出力が得られるかを定義する理論です。

アルンゾ・チャーチとアラン・チューリングにはどのような関係がありますか？

アルンゾ・チャーチはアラン・チューリングの博士号指導教員であり、二人は計算に関する異なるアプローチを提唱しました。チャーチはラムダ計算を、チューリングはチューリングマシンをそれぞれ考案しました。

チューリングマシンとラムダ計算はどのように関連していますか？

チューリングマシンとラムダ計算は、どちらも計算の基本モデルとして考えられており、教会-チューリング仮説により等価とされています。つまり、どちらのモデルでも同じ計算が可能であるとされています。

ラムダ計算における関数の定義方法を教えてください。

ラムダ計算では、ギリシャ文字のラムダ記号を使って関数を導入し、その後に入力変数の名前を記述し、ドットを使い出力がどのように計算されるかを記述します。例えば、単純なインクリメント関数は 'λx. x + 1' と表記されます。

ラムダ計算における関数の適用はどのように行われますか？

関数の適用は、関数に入力を与えることによって行われます。例えば、インクリメント関数 'λx. x + 1' を5に適用すると、5が関数の本体に代入され、5 + 1 となり、最終的に6が結果として得られます。

ラムダ計算はなぜ有用なのですか？

ラムダ計算は、あらゆる計算をエンコードできるという基本的なコンピューテーショナルアイデアを持っており、また関数型プログラミング言語の基礎となっています。近年では、JavaやC#などの主要なプログラミング言語にもラムダ計算が組み込まれています。

関数型プログラミング言語におけるラムダ計算の役割は何ですか？

関数型プログラミング言語では、ラムダ計算が基本的な構文として使用され、関数の定義や適用に使われます。例えば、Haskellのような高度な言語は、ラムダ計算に基づいたコア言語にコンパイルされます。

ラムダ計算で真偽値TRUEとFALSEをどのように表現するのですか？

TRUEは 'λx λy. x' と表現され、入力を2つ受け取りそのうちの1つを選んで返します。FALSEは 'λx λy. y' と表現され、2つを受け取り2番目の値を返します。これにより、選択の概念に基づいて真偽値をエンコードできます。

ラムダ計算でNOT演算子を定義するにはどうすればよいですか？

NOT演算子は 'λb. b FALSE TRUE' と定義されます。これは、真偽値を引数に取り、それを使ってTRUEとFALSEの間で選択します。例えば、NOTをTRUEに適用すると、TRUEは2つの引数を受け取り1つ目を選ぶため、FALSEが返ります。

Yコンビネータとは何ですか？

Yコンビネータは、ラムダ計算における非常に有名な式で、再帰のエンコードに鍵となる要素です。再帰を定義する基本的なメカニズムを提供し、関数型プログラミングにおける再帰の実現に欠かせません。

Yコンビネータと生物学的自己繁殖にはどのような関係があると言えますか？

Yコンビネータは再帰をエンコードする際に、構造的に二つの同じ要素を並べた形で表現されます。これはDNAのダブルヘリックス構造と似ており、自己繁殖を可能にする要素と見なすことができます。これは哲学的な観点からの興味深い観察です。

Outlines

00:00

📚 ラムダ計算の基礎と由来

この段落では、コンピューターサイエンスの重要なトピックであるラムダ計算について紹介しています。ラムダ計算は、関数を計算的观点から捉えたもので、アルンゾ・チャーチによって発明されました。チャーチは、関数をブラックボックスとして扱い、入力と出力の関係性を定義するという考え方を提案しました。また、チャーチはアラン・チューリングの博士指導教員であり、チューリングマシンとラムダ計算は異なるが等価な計算モデルであるという教会-チューリング仮説につながります。関数の定義方法や応用方法についても説明しています。

05:02

🤖 ラムダ計算の有用性と実践的例子

第二段落では、ラムダ計算がどんなに有用であるかを説明しています。ラムダ計算は、あらゆる計算をエンコードできるという基本的な考え方から始まります。チューリングマシンと同様に、ラムダ計算でも何でも表現が可能とされています。また、ラムダ計算は関数型プログラミング言語の基礎となっています。具体例として、Haskellのような高度な言語がラムダ計算に基づいていると紹介されています。さらに、JavaやC#などの主要プログラミング言語にもラムダ計算が組み込まれていることから、コンピューターサイエンス分野において重要な概念であることが強調されています。

10:05

🧬 ラムダ計算における論理値と再帰の表現

最後の段落では、ラムダ計算における論理値のエンコード方法と再帰の実現方法について解説しています。ラムダ計算には組み込みのデータ型がなく、関数と変数のみから成り立っています。論理値TRUEとFALSEをラムダ式を使って表現し、それに基づいて論理否定NOTを定義する例を紹介しています。さらに、再帰を実現するための有名なYコンビネータについても触れており、これは関数型プログラミングにおける再帰を実現する鍵となる要素です。最後に、生物学とラムダ計算の間の興味深い類似点を指摘しています。

Keywords

💡ラムダ計算

ラムダ計算は、コンピュータサイエンスの基礎概念の一つであり、計算の観点からの関数の概念を定義するものです。このビデオでは、関数をブラックボックスとして扱い、入力を処理し出力を生成するという考え方を紹介しています。ラムダ計算は、関数型プログラミング言語の基礎であり、様々なプログラミング言語に組み込まれていると同時に、計算の可能性を示すチューリング完全性を持つとされています。

💡アルンゾ・チャーチ

アルンゾ・チャーチは、プリンストン大学の数学者であり、ラムダ計算の創始者です。彼は計算の観点からの関数の概念に興味を持ち、その答えとして今から知られるラムダ計算を考案しました。チャーチはまた、コンピュータサイエンスの巨匠であるアラン・チューリングの博士号指導教官でもあります。

💡チューリングマシン

チューリングマシンは、アラン・チューリングによって考案された計算モデルであり、状態に基づく基本的な計算の概念を捉えています。ビデオでは、チューリングマシンとラムダ計算が異なる概念であるにもかかわらず、計算能力においては等価であるというチューリング完全性を説明しています。

💡関数

ビデオでは関数をブラックボックスとして扱い、外部からは中身が見えず、入力を与えられた時に出力が生成されるという性質を持っています。関数は純粋であり、内部状態を持たないという特徴があります。これは、チューリングマシンにおける内部状態を持つ計算モデルとは対照的です。

💡ラムダ記法

ラムダ記法は、ラムダ計算で関数を定義する際に使用される記法です。ギリシャ文字の小文字ラムダを用いて、入力変数、ドット、そして出力の計算方法を記述します。例えば、インクリメント関数は'lambda x, x + 1'という形で表現されます。

💡関数の適用

関数の適用は、定義された関数に入力を与え、その関数が持つ効果を適用するプロセスです。ビデオでは、インクリメント関数を5に適用することで、5を関数の中身に置換し、結果として6が生成されるという例を説明しています。

💡関数型プログラミング

関数型プログラミングは、関数とその適用を中心に据えたプログラミングパラダイムです。ビデオでは、ラムダ計算が関数型プログラミング言語、特にHaskellの基礎にあると紹介しています。関数型プログラミング言語は純粋な関数と高階関数を活用し、状態の変化を最小限に抑える特徴があります。

💡チューリング完全性

チューリング完全性は、ある計算モデルが他のすべての計算モデルと等価である計算能力を持つという概念です。ビデオでは、ラムダ計算とチューリングマシンがチューリング完全であると説明されており、これによりどんな計算もこれらのモデルで行うことができるとされています。

💡Yコンビネータ

Yコンビネータは、ラムダ計算における有名な表現であり、再帰を可能にします。ラムダ計算自体には再帰や制御構造はなく、全ての機能を関数としてエンコードする必要があります。Yコンビネータは再帰を表現する鍵であり、このビデオでは生物学とコンピュータサイエンスの間の興味深い類似性にも触れています。

💡ブール値

ブール値は、真偽値を表すデータ型であり、真(TRUE)または偽(FALSE)の2つの値を取ることができます。ビデオでは、TRUEとFALSEをラムダ計算でエンコードし、それらを使って論理演算子を定義する方法を紹介しています。例えば、NOT演算子はブール値を引数に取り、その反対の値を返す関数として定義されます。

Highlights

Lambda Calculus 是计算机科学中的一个重要话题，由 Alonzo Church 发明。

Lambda Calculus 与 Alan Turing 的图灵机在计算能力上是等价的，这被称为 Church-Turing 假说。

函数在 Lambda Calculus 中被视为黑盒，只通过输入和输出进行交互。

Lambda Calculus 中的函数是纯粹的，没有内部状态。

Lambda Calculus 的基本语法包括 lambda 符号、输入名称和输出计算方式。

Lambda Calculus 通过替换过程来应用函数。

Lambda Calculus 由变量、函数构建方式和函数应用方式组成。

Lambda Calculus 能够编码任何计算，与图灵机等价。

Lambda Calculus 是函数式编程语言如 Haskell 的基础。

现代主要编程语言如 Java、C# 等都包含了 Lambda Calculus 的元素。

Lambda Calculus 中没有内置的数据类型，需要通过编码实现。

TRUE 和 FALSE 在 Lambda Calculus 中通过选择操作进行编码。

NOT 操作符可以通过 Lambda Calculus 中的 TRUE 和 FALSE 编码来定义。

Lambda Calculus 可以用来定义逻辑运算符，如 AND 和 OR。

Y combinator 是 Lambda Calculus 中实现递归的关键表达式。

Lambda Calculus 中的递归编码与生物学中的自我复制有相似之处。

Y combinator 在数学和计算机科学中的重要性，有人将其纹在身上。

Transcripts

Today we're going to talk about one of my favorite topics in Computer Science,

which is the Lambda Calculus. And in particular, we're going to talk about

three things: we're going to think what actually is it, why is it useful, and

where did it actually come from? So we're going to start with the last

question here - where did it actually come from? This is Alonzo Church, who was

a mathematician at Princeton University in the United States, and he

was the person who invented the Lambda Calculus. And what he was interested in

is what is the notion of a function from a computational perspective. And his

answer to this question is what we now know as the Lambda Calculus. And there's

an interesting piece of history here, which many people don't know.

So, it turns out that Alonzo Church was the PhD supervisor of someone very

famous in computer science -- Alan Turing. And of course Alan Turing,

amongst many other things which he did, he invented Turing machines -- which

Computerphile has done a number of videos on -- and Turing machines capture a basic

state-based model of computation. It's interesting that his PhD supervisor,

Alonzo Church, he captured a basic functional notion of computation with

his Lambda Calculus. And it turns out that these two, quite different notions,

one functional and one state-based, turn out to be equivalent -- and this is what's

called the Church-Turing hypothesis, or part of the Church-Turing hypothesis.

So for Church, a function was a black box, but you're not allowed to look inside.

And what it does is it takes some input, so maybe it takes a number like x, and it's

going to process it in some way, and it's going to produce an output. So maybe it

produces the output x + 1. So this would be a function that takes a single

input, a number called x, processes in some way, and then produces a single

output, which is the number x + 1. And we could have a slightly more

interesting example. Maybe we have a box with two inputs, x

and y, and we process them in some way, and maybe we produce their sum as the

output. So this would be a function which takes two inputs, x and y, processes

them in some way, and then produces their sum, x + y. And there's two important

things about functions in this sense. The first is that they're black boxes; you're

not allowed to look inside, and you can't see the mechanics of what's going on

inside that box, all you can do it put something in and observe what comes out

the other side. And the second important thing is that these functions are pure,

they have no internal state; so all that happens when you map x across to x + 1,

is the magic goes on inside the box, and there's no internal state, there's no

hidden information that we can use. And this is quite different from the notion of

computation that Alan Turing was interested in with his Turing machines -- he had

internal state -- there's no internal state, these are pure mathematical functions. Now

we can think how do you actually define functions in the Lambda Calculus. And

there is a very, very simple syntax for this, which I'll introduce to you now. So

let's think about the increment function in the Lambda Calculus. What you do is

you write down a lambda symbol -- so this is the Greek lower-case letter lambda, and

that says we're introducing a function at this point. And then you just write

down the name of the input, so that was x. And then you have a dot, and then

you say how the output is calculated in terms of the input, that's x + 1. So we

could do the same with addition, you just need two lambdas, and write lambda x,

dot, lambda y, dot, x + y. So this is the function that takes two inputs, x

and y, and then delivers the result x + y. And this is written down formally in

Church's Lambda Calculus exactly like this. So, when you've got a function,

what can you do with it? Well, all you can do is give it some input, let it do its

thing, and it will give you some output. So let's have a simple example of this.

If we take a function like increment, which was lambda x, x + 1, and we

apply it to a number like 5, what actually happens? It's a basic process of

substitution; we're essentially substituting the number 5 here into the body of

this lambda expression and then x becomes 5, so we get 5 + 1,

and then we get the result 6 on the other side. And this is basically all

there is to the Lambda Calculus. It's only got three things: it's got variables,

like x, y and z; and it's got a way of building functions -- this lambda notation;

and it's got a way of applying functions. This is the only three things that you

have in the setting. What is actually the point of the Lambda

Calculus? We've introduced this very simple notation, why should you be

interested in learning about it? I think there's three answers which I would give

to this. The first point I'd make is that the Lambda Calculus can encode any

computation. If you write a program in any programming language, which has ever

been invented, or ever will be invented, or really any sequential programming

language, it can in some way be encoded in the Lambda Calculus. And of course it

may be extremely inefficient when you do that, but that's not the point -- this is a

basic idea of computation, and we want to think how many and what kind of programs

can we encode this, and actually you can encode anything. And this is really the

kind of Church-Turing hypothesis which I mentioned. Alan Turing, you can encode

anything in his Turing machines, and in Church's Lambda Calculus, you can encode

anything. And actually these two systems are formally equivalent -- any Turing

machine program can be translated into an equivalent Lambda Calculus program, and

vice versa. They are formally equivalent. The

second point I would make is that Lambda Calculus can also be regarded as the

basis for functional programming languages like Haskell. So these are

becoming increasingly popular these days. And actually a very sophisticated

language like Haskell is compiled down to a very small core language, which is

essentially a glorified form of Lambda Calculus. So if you're interested in

functional programming languages like Haskell, or the ML family,

these are all fundamentally based on the Lambda Calculus -- it's just kind of a

glorified syntax on top of that. The third point which I would make, is that

the Lambda Calculus is actually now present in most major programming

languages. So this wasn't the case 10 or 15 years ago, but it is the case today. So if

you look at languages like Java, like C#, even Visual Basic, F#, and so

on, all of these languages now encode Lambda Calculus, or include Lambda

Calculus, as a fundamental component. So every computer scientist today needs to

know about Lambda Calculus. What I'd like to end up with is

a couple of little examples of what you can do with it. So, the Lambda Calculus has

basically got nothing in it: it's got variables, it's got a way of building functions, and it's

got a way of applying functions. It doesn't have any built-in data types

like numbers, logical values, recursion and things like that. So if you want to

do these things in the Lambda Calculus, you need to encode them. So I'll end

up showing you a simple encoding, and the encoding which I'm going to show you is

the logical values TRUE and FALSE. And the key to this is to think what do you

do with logical values in a programming language? And the basic observation is

that you use them to make a choice between doing two things -- you say if

something is TRUE do one thing, if something is FALSE do another thing, and

we're going to use this idea of making a choice between two things to actually

encode TRUE and FALSE. So the trick is for TRUE, you write down this lambda

expression. So what it does is it takes two things, x and y, and then it chooses

the first. And FALSE does the opposite. It's going to take two things, and it's

going to choose the second. So we've got two lambda expressions here, both of

which take two inputs, x and y, and one chooses the first one, x, and one chooses the

second one, y. So fair enough, what can we actually

do with this? Well, let's think how we could define a little logical operator.

So, NOT is the most simple logical operator which I could think of. It's going

to flip TRUE to FALSE, and FALSE to TRUE. It's logical negation. Based upon this

encoding, how could I actually define the NOT operator or the NOT function. It's

very easy to do. I will take in a logical value, or a Boolean as it normally called

in Computer Science, after George Boole, who first studied a kind of formal logic. So

we take a Boolean, which will be one of TRUE or FALSE, and here's what we do. We apply

it to FALSE, and we apply it TRUE. And I claim that this is a valid definition

for a NOT function. But I can very easily convince you that it's the case,

because I can do a little calculation. So, let's check, if we apply NOT to TRUE,

that we actually get FALSE. And in just a few steps, using the Lambda Calculus magic,

we'll find that this actually works out. So what can we do here?

Well the only thing we can do is start to expand

definitions. So, we know what the definition of NOT is. It was lambda b, b applied to

FALSE and TRUE, and then we just copy down the TRUE. So all I've done in the

first step here, is I've expanded my definition of NOT -- NOT was defined to be

this Lambda Calculus expression here. Now, I've got a function, which is this thing,

and it's applied to an input, so i can just apply it.

OK, and the function says if I take in a b, I just apply that b to FALSE and TRUE.

So, the thing I'm applying it to is TRUE here, so i just do the little

substitution. Rather than b, I write TRUE, and then I copy down the FALSE, and copy

down the TRUE, and I get down to here. And at this point, you might quite

rightly be thinking this looks like complete rubbish.

I've just written TRUE FALSE TRUE. What does that mean? It means absolutely

nothing. But it means something in the Lambda Calculus, because we continue to

expand. So, what we can do now, is expand the definition of TRUE. We said that TRUE

takes two things, and chooses the first one. So, let's expand it out. So, TRUE is

lambda x, lambda y, x. So, it chooses the first thing of two things, and then we just

copy down the two inputs, FALSE AND TRUE. And you can see what's going to

happen now -- we've got a function here which takes two things and chooses the first

thing. Here the first thing is FALSE, so when we apply the function, we just get

back FALSE. So what you see has happened here, in just

a few steps, we've shown how using this encoding of TRUE and FALSE, and not, we

can actually get the desired behavior. And it's very easy to check for yourself,

if you apply NOT to FALSE, you'll get TRUE. And I'd like to set you a little kind of

puzzle at this point -- think how you could define logical AND,

or logical OR, in this style as well. And I'm interested to see what kind

of definitions people come up with in the comments. So, the very last thing I'd

like to show you is this lambda expression here, which is a very famous

Lambda Calculus expression called the Y combinator, or the Y operator. And actually,

this is the key to doing recursion in the Lambda Calculus. So, as I mentioned,

Lambda Calculus has basically nothing in it, or it's only got three things in it:

variables x, y and z, and so on; a way of building functions; and a way of applying

functions. It's got no other control structures, no other data types, no anything.

So, if you want to do recursion, which is the basic mechanism for

defining things in terms of themselves -- again Computerphile's had videos on this --

you need to encode it. And it turns out that this expression here is the key to

encoding recursion in the Lambda Calculus. And this expression was

invented by someone called Haskell Curry, and this is the Haskell that gives

his name to the Haskell programming language. And he was a PhD student of

David Hilbert, who's a very famous mathematician. The last observation

I'd like to leave you with here, is something that's interested me for many

years. I think there's a connection between this piece of kind of abstract computer

science, or abstract mathematics, and biology. If you look at human DNA, you

have this double helix structure; you have two copies of the same thing,

side-by-side, and this is the key to allowing DNA to self-replicate. If you

look at the structure of this lambda expression here, we have two copies of

the same thing side-by-side. You have lambda x, f applied to x x, and exactly the

same here. This is the key to doing recursion, which is kind of related to

self-replication in a programming language, or in the Lambda Calculus. And

for me, I don't think this is a coincidence -- I think it's kind of

interesting philosophical observation. The Lambda Calculus has this kind of

very clever way of doing recursion, which would take a video on its own to explain

how it actually works, but you can look it up on Wikipedia. And there's a link here,

I think, to biology. Somebody actually found the Y Combinator

so interesting, that they've had it tattooed permanently on their arm, and

you can find a picture of this if you do a quick web search. What would people search for?

The Y combination -- the Y combinator in mathematics or computer science.

And tattoo I'm guessing. Yup!