“Introduction to Lambda Calculus” メモ

Intruduction to Lambda Calculus — ftp://ftp.cs.ru.nl/pub/CompMath.Found/lambda.pdf

著者はこちらと同じ、 “L.i.S.P” では The “bible” of λ-calculus begins with として示されています、 The Lambda Calculus: Its Syntax and Semantics - Hendrik Pieter Barendregt - Google Books — https://books.google.co.jp/books?id=KbZFAAAAYAAJ&dq=editions:ISBN0444875085

自分なりの注釈を入れてみています。

2.3 CONVENTION.
(i) x, y, z, ... denote arbitrary variables; M, N, L, ... denote arbitrary λ-terms. Outermost parentheses are not written.
(ii) M ≡ N denotes that M and N are the same term or can be obtained from each other by remaning bound variables. E. g.
...
(iii) We use the abbreviations
…

定義が非常にシンプルなので、この入門で説明される中の慣習を陽に記述してくれているのが非常に助かります。

2.4 VARIABLE CONVENTION.
If M₁, ... ,Mₙ occur in a certain mathmatical context (e.g. definition, proof), then in these terms all bound variables are chosen to be different from the free variables.

一見、定義の裏返しのように見えるのだけれども、 … and y ∉ FV(N) をも考慮するようになっているのが注意する所でしょうか。ここでは x が free variable である、とあらかじめ先に言及していたとしても無理が起きないようにしている、とも考えられます。

2.13 EXAMPLE. (i)

$\begin{array} & \exists G \; \forall X \; GX = SGX. \mbox{ ; Indeed} \\ \forall X \; GX = SGX \\ ⇐ Gx = SGx \\ ⇐ G = λx.SGx \\ ⇐ G = (λgx.Sgx)G \mbox{ ; (注記)ここで不動点が出てきたので、} \\ ⇐ G ≡ Y(λgx.Sgx). \\ \end{array}$

$f x = x$ となる $x$ を関数 $f$ の不動点という。ここで関数 $f$ を入力として取って、その不動点を返す関数 $Y$ があるとすると、関数 $f$ の不動点は $Yf$ と表現できます。これをそのまま $G = (λgx.Sgx)G$ に当てはめています。

(ii)

$\begin{array} & \exists G \; \forall X \; GX = GG: \\ \mbox{take } G ≡ Y(λgx.gg). \\ \end{array}$

さらっと $Y$ を使った $G$ の式として書かれているのだけれども、 $GX = GG$ から $G$ の式にするのを目指してみます。

$\begin{array} & GX = GG \\ ⇒ Gx = (λx.GG)x \\ ⇒ G = λx.GG \\ ⇒ G = (λgx.gg)G \\ \end{array}$

ここでも不動点が出てきた。
$FX = X$ となる $X$ は関数 $F$ の不動点である。$F = YF.$
ここで、
$(λgx.gg)G = G$ となる $G$ はある関数 $(λgx.gg)$ の不動点である。ゆえに

$G ≡ Y(λgx.gg)$

これを、 $Y$ を使わずに表現するとすると。

$\begin{array} & GX = GG \\ \mbox{; GG の式を G の式にするとすると} \\ ⇒ GG = (SII)G \\ ⇒ G ≡ SII \\ \end{array}$

検算するとすると、

$\begin{eqnarray} SIIG \quad & ; & [S:=λxyz.xz(yz)] ⇒ \\ (λxyz.xz(yz))IIG \quad & ; & [x:=I] ⇒ \\ (λyz.Iz(yz))IG \quad & ; & [y:=I] ⇒ \\ (λz.Iz(Iz))G \quad & ; & [z:=G] ⇒ \\ IG(IG) \quad & ; & ⇒ \\ IGG \quad & ; & ⇒ \\ GG.\quad \\ \end{eqnarray}$

$IGG$ が $(IG)G$ という評価されることが最初はピンと来ないのだけれども、 Functions of more arguments の所の説明で納得できた後に見返すと腑に落ちます。複数の引数がある関数の評価は、繰り返し一引数の関数を評価することで値を得ることができるというもの、 currying です。

Functions of more arguments の所では、括弧を使って複数引数を表現されているものを、使わない形へと変形していきます。一見括弧を使った方がより自然なもののような気もするのですけれども、一旦腑に落ちると、どちらも不自然でもないと感じられるようになりました。括弧を使わない場合には当然、テキストに現れる要素は少なくて済みます（少しですが）。

最初に一見したところ、言い替えると過去の自分は、括弧を使って表現した方が見慣れているからか、より自然な気がしていた、ということです。

$f(x,y)$ を例に以下のように説明されています。

... If $f(x,y)$ depends on two arguments, one can define:

$\begin{eqnarray} F_{x} & = & λy.f(x,y), \\ F & = & λx.F_{x}. \\ \mbox{Then} \\ (Fx)y & = & F_{x}y = f(x,y). \\ \mbox{...} \\ Fxy & = & f(x,y) \\ \end{eqnarray}$

そして、一般に、 application と abstraction はそれぞれ次のように説明されます。

...
it is convenient to use association to the left for iterated application:
$FM_{1}…M_{n}$ denotes $(…((FM_{1})M_{2})…M_{n})$

...
Dually, iterated abstraction uses association to the right:
$λx_{1}…x_{n}.f(x_{1},…,x_{n})$ denotes $λx_{1}.(λx_{2}.(…(λx_{n}.f(x_{1},…,x_{n}))))$

これは 2.3 CONVENTION の (iii) に挙げられている所のものでもあります。(iii) では括弧を使用しないものなので、それぞれ以下のように。

(iii) We use the abbreviations

$\begin{eqnarray} FM_{1}…M_{n} & ≡ & (…((FM_{1})M_{2})…M_{n}) \\ \mbox{and} \\ λx_{1}…x_{n}.M & ≡ & λx_{1}(λx_{2}(…(λx_{n}.M))) \\ \end{eqnarray}$