2016/08/26

λの起源、2つの説

λ算法はなぜλなのかについては、次の説が有名である。

Alonzo Churchがλ算法を考えた時、RusselとWhiteheadが Principia Mathematicaで束縛変数を表すのにカレット^を 使っているのに倣ったが、1行でタイプする都合上カレットを前に出し ^x f(x) とし、それが λx f(x)となった。

『プログラミングGauche』でもこの話を紹介していて、そこでは出典を Peter NorvigのPAIPとしている。 この説はあちこちで見るので特に深追いしていなかった。

ところが、Churchの教え子であるProf. Dana Scottがそうではないと 語っているレクチャーがある。

http://researchblogs.cs.bham.ac.uk/thelablunch/2016/05/why-is-lambda-calculus-named-after-that-specific-greek-letter-do-not-believe-the-rumours/

He says that when Church was asked what the meaning of the λ was, he just replied "Eeny, meeny, miny, moe.", which can only mean one thing. It was a random, meaningless choice. Prof. Scott claimed that the typographical origin myth was mainly propagated by Henk Barendregt and is just pure whimsy. He asked us to stop perpetrating this silly story.

とすると^説はどこから? というわけで調べてみた。

Dov M. Gabbay, John Woods (ed.): "Logic from Russell to Church", Elsevier, 2009, p.731に次の下りがある。 (Google Books)

どうやら、Church自身が両方の説(^説と偶然説)を語っているようだ。

ここで引用されてる[Church, 1964]は "A. Church, 7 July 1964. Unpublished letter to Harald Dickson." だそうで現物を見ることは叶わず。 [Rosser 1984]の方はIEEEのDigital Libraryで読める。該当箇所:

RosserはChurch-RosserのRosserその人だから、信憑性に欠けるということはないだろうが、 Church本人から直接聞いた話なのか、上記Unpublished letterを通じて広まった話の方を 耳にしたのか、という点については明確ではない。

(あと、Rosserは^を前に出したこと自体はタイプの都合ではなく Russell&Whiteheadとは異なる用法だから、としている。 "Logic from Russell to Church"の説明もそれなので、その点は 1964年の手紙に記されていたのではないかと思われる。 「タイプの都合で前に出した」は尾鰭である可能性が高い。)

可能性としては、

• λの選択は偶然だったが、Harald Dicksonへの手紙ではジョークのつもりで もっともらしい話をでっち上げたらそれが広まってしまった
• Principia Mathematicaからインスピレーションを得たといえばそうなのだが、 記号の起源なんてどうでもいいと思っていたので後の方ではただ偶然ということにしておいた

あたりだろうか。 まあ、どちらにせよそんなにこだわるような話ではない、と少なくともChurch本人は思っていたような感じである。

Tag: Programming