型のないλ式

前置き

もう一度言いますが、はじめにでも述べているように、このサイトの製作者（算散士）は 型理論をあまりよく知りません。ですから、本格的に知りたい人は他をあたった方がいいと思います。

型のないλ式

いきなり型の付いたλ式を説明すると、初めての人は複雑に見えるかもしれないので、まずは型のないλ式の定義を述べようと思います。以下の１．２．３．は

高橋正子　「計算論」　近代科学社

のｐ．６３の定義２．１．１です。

変数、ｘ_０，ｘ_１，．．．はλ式である。
Ｍがλ式で、ｘが変数のとき（λｘ．Ｍ）はλ式である。
ＭとＮがλ式のとき（ＭＮ）はλ式である。

そして、上記の１．２．３．のみによって作られる式を（型のない）λ式と呼びます。また、２．における（λｘ．Ｍ）をｘに関するＭの関数抽象（functional abstraction）と呼び、３．における（ＭＮ）をＭのＮに対する関数適用（functional applicatoin）と呼びます。これらの言葉を使うなら、（型のない）λ式というのは、変数に関数抽象と関数適用を繰り返し行うことによって得られる式ということになります。

あと、上記の定義でそのままλ式を書くと、括弧が多すぎて大変見づらくなるので、次のような略記法を用います。

一番外側の括弧は省略する。
（λｘ_１．（λｘ_２．（・・・（λｘ_ｎ．Ｍ）・・・）））は λｘ_１ｘ_２・・・ｘ_ｎ．Ｍと略す。
（（・・・（（Ｍ_１Ｍ_２）Ｍ_３）・・・）Ｍ_ｎ）はＭ_１Ｍ_２Ｍ_３・・・Ｍ_ｎと略す。
関数適用の結合力よりも、関数抽象の結合力の方が弱いものとする。つまり、 λｘ．Ｍ_１Ｍ_２と書いたときは、（λｘ．Ｍ_１）Ｍ_２ではなく、 λｘ．（Ｍ_１Ｍ_２）を意味するものとする。

以上の定義から最初に思ってほしいのは、「λ式というのは何らかのルールに沿った単なる文字列なんだな」ということです。

λ式を単なる文字列という目で見ることはとても大事なので決して忘れないでください。ですが、それだけではアルファ同値とか、ベータ変換（ベータ簡約？）等の気持ちがわからなくなるので、 λ式の気持ちも説明しておこうと思います。

λ式の気持ちをわかりやすく説明するために、上記の１．２．３．から外れた式も使用したいと思います。高校までの数学では、ｘ^２＋３などの式で、ｘの関数を表現したりします。しかしこれが、ｘ^２＋ｘ・ｙのような式になると、ｘの関数なのか、ｙの関数なのか、それとも関数の値なのか、そのままでは区別がつかなくなります。そこで、ｘ^２＋ｘ・ｙをｘの関数として見るときは（λｘ．ｘ^２＋ｘ・ｙ）と書き、ｙの関数として見るときは（λｙ．ｘ^２＋ｘ・ｙ）と書くことにするのです。これが、上記２．の記法の気持ちです。

次は３．です。ｆを（引数が）ｘの１変数関数とするときに、関数ｆの引数ｘに４を代入した値をｆ（４）などと表記します。これを括弧をはずし、単に並べてｆ４と書く。これが上記３．の記法の気持ちです。すぐ上で説明した２．の気持ちとあわせて具体例を示しましょう。
ｆを（λｘ．ｘ^２＋３）とするなら、

　　　ｆ４＝（λｘ．ｘ^２＋３）４＝４^２＋３＝１９

です。

すると、λ式の記法の仕方では1変数しか表現できないように思えるかもしれませんが、そうではありません。次の具体例を見てください。

　　　（（λｘ．（λｙ．ｘ^２＋ｘ・ｙ））３）４＝（λｙ．３^２＋３・ｙ）４＝３^２＋３・４＝９＋１２＝２１

これはｘ^２＋ｘ・ｙをｘとｙの2変数関数と見て、ｘ＝３、ｙ＝４を代入した計算になっています。一般的に、Ｍ_１Ｍ_２Ｍ_３・・・Ｍ_ｎと書いた場合、気持ち的にはＭ_１のみが関数で、残りのＭ_２、Ｍ_３、・・・、Ｍ_ｎは関数Ｍ_１に代入されるものなのです。

実は、上記の１．２．３．で定義されたλ式に、上記の計算例ａ．ｂ．のような書き換えをすることをベータ変換といいます。具体的には、

　　　（λｘ．ｘｙ）（λｘ．ｘ）＝（λｘ．ｘ）ｙ＝ｙ

です。これを使ってアルファ同値について説明しましょう。λｘ．ｘｙを上記で説明した気持ちで解釈すると、ｘの関数になっているわけですが、関数という機能に着目した場合、λｘ．ｘｙにおける文字ｘは、代入する場所を教える役割しかありません。つまり、文字ｘをｚに変えても、上記の計算（ベータ変換）の結果は同じになります。やって見ましょう。

　　　（λｚ．ｚｙ）（λｘ．ｘ）＝（λｘ．ｘ）ｙ＝ｙ

そこで、λｘ．ｘｙにおける文字ｘのような文字を束縛変数と呼び、束縛変数だけが違うλ式は、アルファ同値といって、同じλ式であるとみなすのです。ですから、λｘ．ｘｙなるλ式を、何かの都合でλｚ．ｚｙに書き換えるというようなことは頻繁に行います。（結局、λ式における束縛変数というのは、上記２．において、λで指定される変数のことです。）

ただし、λｘ．ｘｙにおける文字ｘをｙに変えることはアルファ同値とは言いません。もしそれをおこなうと、λｘ．ｘｙはλｙ．ｙｙになってしまうわけですが、それでは上記の計算の結果が変わってしまいます。やってみましょう。

　　　（λｙ．ｙｙ）（λｘ．ｘ）＝（λｘ．ｘ）（λｘ．ｘ）＝λｘ．ｘ

つまり、λ記号で指定されている文字を変更しても、関数としての機能が同じ場合なら、アルファ同値とするのです。

さらに、束縛変数でない変数は、自由変数と呼びます。少し具体例を示しましょう。

　　　（λｘｙ．ｘｚ（ｙｚ））（λｚ．ｚ（λｙ．ｘｙｚ））

上記ｇ．のλ式において、文字ｘは3箇所に現れていますが、左から1番目と2番目のｘは束縛変数ですが、一番右の変数ｘは自由変数です。このように、同じ文字でも場所によって束縛変数だったり、自由変数だったりします。そこで、「左から1番目と2番目のｘは束縛されているが、一番右の変数ｘは自由である」というような言い方もします。他の文字ｙ、ｚに関しては、ｙはすべて束縛されていますし、ｚは場所によって束縛されているのと自由なものがあります。（ちなみに、右から１，２，３番目のｚが束縛されています。）

以上のことは精密に定義しようとすると、たいしたことではないのに読むのが苦痛になるような長い定義になるので、これくらいで勘弁してください。また、このサイトでCoqで遊ぶ上では、上記のベータ変換よりも、アルファ同値の方を頭に入れて置いてください。というのも、Coqは証明の段階で、よく勝手に束縛変数の書き換えをするからです。

もどる