TETRA'S MATH

数学と数学教育
<< タイプ理論ってなんだろう? | main | 補足1>λ記号 >>

ちょっとだけλ(ラムダ)記号に慣れておく

 金子洋之『ダメットにたどりつくまで』のp58に、λq.q(p)という表記がごく簡単な説明つきで出てきます。これを目にしたとき、清水義夫『圏論による論理学 高階論理とトポス』の最初の数ページを読んでおいてよかったなぁ〜と思いました。だたし、記号に見覚えがあってよかったというだけで、実際に本文を読もうとすると目がまわりそうになります。

 で、そろそろ『ダメットにたどりつくまで』にもどろうと思うのですが、その前にちょっとだけこのλ(ラムダ)を使った表記に慣れておくことにします。なお、清水義夫『圏論による論理学 高階論理とトポス』のp13、14を参考にさせていただいていますが、私はこういうふうに理解したということで、かなり我流に書きます。
 さて、関数には入力と出力があり、中学数学や高校数学では、関数を表す式を y=2x+1 や f(x)=3x^2+5x+2 のように表すことが多いかと思います。y=2x+1において、x=3を入力すれば、出力yは2×3+1=7だし、f(x)を使う表記の場合はかっこの中に入力するものを入れて、f(1)=10 のような書き方ができます。

 ほんでもって、ここはひとつ数教協のブラックボックス風()に、「フタ」を入れたら「ブタ」が出て、「カラス」を入れたら「ガラス」が出てくるような入力-出力の関係を考えてみます。

 この関数がどのようなものかは、たった2つの入力-出力ではわかりませんが、とりあえず、フタを入れたらブタが出て、カラスを入れたらガラスが出てくるような、そのような働きを表わす関数になっているので、この関数のことを、

       [フタ][ブタ]    [カラス][ガラス]

のように、入力と出力の組み合わせで表現してもわるいということはなさそうです。(ちなみに[ ]は私が勝手に持ち出してきました)

 これを y=2x+1 や f(x)=3x^2+5x+2 に適用するならば、[x][2x+1]、[x][3x^2+5x+2]ということになります。でも、こんなふうに並べるだけでは混乱をきたすので、入力部分をλと.ではさんで示そうというのが、λ記号なのだと思います。この記号を使うと、「λフタ.ブタ」、「λカラス.ガラス」と表せます。

 で、面白いなぁと思うのは、「λフタ.ブタ」で表されるものそのものが関数なのだということ。つまり、λx.f(x)=fであるということ。y=2x+1 や f(x)=3x^2+5x+2 は等式の形をしていますが、λx.f(x)の中にはイコールがないというのが、私にとっては新鮮でした。なお、おそらく「λフタ.ブタ」は、「最初の1文字に濁点をつける」という働きをしめす関数である可能性が高いですが(もちろん、この2つの組み合わせだけではわからないけれど)、こういうふうに式で表せない関数も、入力-出力の組み合わせで関数として記号化できるというのは面白いなぁ、と思いました。ちなみにもちろんのこと、本にフタ→ブタは出てきていません、はい。(^^;

 したがって、f(x)=(λx.f(x))(x)、f(a)=(λx.f(x))(a)となります。

 なお、λ記号は「関数抽象子」(function abstractor)呼ばれることもあるそうです。

 本に例題がのっているので、=のあとを白文字にして引用させていただきます。

〔例題〕

 1) (λx.x)a=a
 2) (λx.3x+y)5=15+y
 3) (λx.xy)a=ay
 4) (λx.xz)(λy.y)=(λy.y)z=z
 5) (λx.x(y+1))(λy.y)=(λy.y)(y+1)=y+1

※ すべての答えの最後に「.」がついているのですが、これは句点としてのピリオドだと判断して省略しました。いいのかな…いいんだよな…

補足1補足2  
圏論 | permalink
  

サイト内検索