ラムダ計算 #3 マクロ, 不動点結合子と再帰関数

ラムダ計算セルフブログリレー3日目です. 今日は異常運転, くまちゃんです. 2日目はこちら.
kumachan-math.hatenablog.jp

あれ, 2日目をさっき書いた気がしなくもないんですけど, まあいいです. 昨日(確かに昨日, うん)は, ラムダ式の簡約について書きましたが, 今日はマクロと不動点結合子, 再帰関数を扱います.

マクロとは, ラムダ式であって自由変数を1つも持たないものをいいます.

3.1. ブーリアン

まず手始めに, $\overline{\mathrm{if}}$ を定義しましょう. if文には条件, then節, else節の3つがあればいいです. そこで,

$\overline{\mathrm{if}} := \lambda bte.bte$

と定義しておきましょう.
これに従うと, 条件であるブーリアンについて次が満たされていれば良いことがわかります.

trueはthen節とelse節の2つを入力として, then節を返せば良い.
trueはthen節とelse節の2つを入力として, else節を返せば良い.

すなわち,

$\overline{\mathrm{true}} := \lambda tf.t$
$\overline{\mathrm{false}} := \lambda tf.f$

とすればいいことがわかります.

さらに $\overline{\mathrm{not}}$ , $\overline{\mathrm{and}}$ , $\overline{\mathrm{or}}$ も一気に定義してしまいましょう.

$\overline{\mathrm{not}} := \lambda b.b~\overline{\mathrm{false}}~\overline{\mathrm{true}}$
$\overline{\mathrm{and}} := \lambda b_1b_2.b_1 ~(b_2~\overline{\mathrm{true}}~\overline{\mathrm{false}}) ~\overline{\mathrm{false}}$
$\overline{\mathrm{or}} := \lambda b_1b_2.b_1 ~\overline{\mathrm{true}} ~(b_2~\overline{\mathrm{true}}~\overline{\mathrm{false}})$

この $\overline{\mathrm{and}}$ , $\overline{\mathrm{or}}$ だと, $b_1$ の評価結果に応じて, $b_2$ が評価されたりされなかったりします. すなわち, CやJavaでいうところの2重記号のand(&&)とor(||)に対応することになります. もし必ず両方評価されるもの, すなわち単体のand(&)とor(|)を定義しようとすると, 次のようになるでしょうか.

$\overline{\mathrm{and}} := \lambda b_1b_2. b_1 ~(b_2~\overline{\mathrm{true}}~\overline{\mathrm{false}}) ~(b_2~\overline{\mathrm{false}}~\overline{\mathrm{false}})$
$\overline{\mathrm{or}} := \lambda b_1b_2. b_1 ~(b_2~\overline{\mathrm{true}}~\overline{\mathrm{true}}) ~(b_2~\overline{\mathrm{true}}~\overline{\mathrm{false}})$

3.2. 整数

ブーリアンと論流演算が定義できたので, 次に整数と算術演算を定義しておきましょう.

$\overline{\mathrm{0}} := \lambda sz.z$
$\overline{\mathrm{1}} := \lambda sz.sz$
$\overline{\mathrm{2}} := \lambda sz.s(sz)$
$\overline{\mathrm{3}} := \lambda sz.s(s(sz))$
...
$s$ は1を足す関数, $z$ はゼロだと思ってみてください.

このとき, $\overline{\mathrm{add}}$ と $\overline{\mathrm{mul}}$ は次のように定義されます.
$\overline{\mathrm{add}} := \lambda mn.(\lambda sz.ms(nsz))$
イメージ的には, 0に1をn回足したものに1をm回足せばmとnの和になるよねといった次第です.
$\overline{\mathrm{mul}} := \lambda mn.(\lambda sz.m(ns)z))$
$\overline{\mathrm{mul}}$ はなんと括弧を付け替えただけです. イメージ的には0に「1をn足す操作をしたもの」をm回足す操作をしたものはmとnの積になるよねといった次第です.

最後に指数です. 指数 $m^n = \overline{\mathrm{exp}}~\overline{\mathrm{m}}~\overline{\mathrm{n}}$ は次のように定義されます.
$\overline{\mathrm{exp}} = \lambda mn.(\lambda sz.nmsz)$
超単純！ビビるこれはビビる！えーまあみていきましょう.
$\overline{\mathrm{m}}~\overline{\mathrm{n}} = \lambda sz. \underbrace{m(m(\cdots m(}_{n個}s)\cdots))z$
となります. これを踏まえると,
$\overline{\mathrm{exp}}~\overline{\mathrm{m}}~\overline{\mathrm{n}} \to m (\overline{\mathrm{exp}}~\overline{\mathrm{m}}~\overline{\mathrm{n - 1}}) z$

先の $\overline{\mathrm{mul}}$ の定義のときにみたように, $\lambda sz.m(ns)z$ は $n$ を $m$ 倍したものに対応したのですから, 上の式は
$m^n = m \times m^{n-1}$
に対応しそうだということが想像できます.

次に確認しておくべきは, この漸化式の出発点
$\overline{\mathrm{exp}}~\overline{\mathrm{m}}~\overline{\mathrm{0}} = \overline{\mathrm{1}}$
です.
$\lambda sz.(\overline{\mathrm{exp}}~\overline{\mathrm{m}}~\overline{\mathrm{0}})sz \to \lambda sz.(\lambda sz.z)\overline{\mathrm{m}}sz \to \lambda sz. sz =: \overline{\mathrm{1}}$

したがって, $\overline{\mathrm{exp}} = \lambda mn.(\lambda sz.nmsz)$ は $m^n$ を表しうることがわかりました.

3.3. 不動点結合子と再帰関数

次に不動点結合子ですが, 結論からいきましょう.

命題3.1 不動点結合子
$\overline{\mathrm{Y}} := \lambda f.(\lambda x. f(xx))(\lambda x. f(xx))$
は符号点結合子である. すなわち, $\overline{\mathrm{Y}}F$ は $F$ の不動点を与え, $F(\overline{\mathrm{Y}}F) = \overline{\mathrm{Y}}F$ を満たす.

証明 :
$\overline{\mathrm{Y}}F \to (\lambda x. F(xx) )(\lambda x. F(xx))\to (F(xx) )[x\mapsto (\lambda x. F(xx) )] \to F( (\lambda x. F(xx) )(\lambda x. F(xx) ) ) \equiv F(\overline{\mathrm{Y}}F)$

次に, 再帰関数を考えていきましょう. $\overline{\mathrm{pre}}$ を整数を引数にとり1つ小さい整数を返すマクロとします. 定義は煩雑なので省略します. この時次のラムダ式を考えます.

$\overline{\mathrm{F}} := \lambda g. \lambda n. \overline{\mathrm{if}}~(\overline{\mathrm{iszero}} ~n) ~\overline{\mathrm{1}} ~(\overline{\mathrm{mul}}~n~(g(\overline{\mathrm{pre}}~n)))$

ここで, $\overline{\mathrm{iszero}}$ は与えられた整数が $\overline{\mathrm{0}}$ なら $\overline{\mathrm{true}}$ , それより大きければ, $\overline{\mathrm{false}}$ を与えるマクロであって次で定義されます

$\overline{\mathrm{iszero}} := \lambda n. n~(\lambda x. \overline{\mathrm{false}})~\overline{\mathrm{true}}$

整数の $z$ , すなわちゼロのところに $\overline{\mathrm{true}}$ を, $s$ , すなわち1を足す関数のところに, 問答無用で $\overline{\mathrm{false}}$ を返す関数 $\lambda x.\overline{\mathrm{false}}$ を差し込んだものです.

さて, 上の $\overline{\mathrm{F}}$ を不動点結合子を食わせたもの $\overline{\mathrm{Fact}} := \overline{\mathrm{Y}}~ \overline{\mathrm{F}}$ は, 階乗関数になります. それは簡単に確認することができます.

$\overline{\mathrm{Fact}}$ は[ $\overline{\mathrm{F}}$ の不動点ですから,
$\overline{\mathrm{Fact}} = \overline{\mathrm{F}}~\overline{\mathrm{Fact}}$
ところが,
$\overline{\mathrm{F}}~\overline{\mathrm{Fact}} \to \lambda n.\overline{\mathrm{if}}~(\overline{\mathrm{iszero}} ~n) ~\overline{\mathrm{1}} ~(\overline{\mathrm{mul}}~n~(\overline{\mathrm{Fact}}(\overline{\mathrm{pre}}~n)))$
ですから, 結局
$\lambda n.\overline{\mathrm{Fact}}~n = \lambda n.\overline{\mathrm{if}}~(\overline{\mathrm{iszero}} ~n) ~\overline{\mathrm{1}} ~(\overline{\mathrm{mul}}~n~(\overline{\mathrm{Fact}}(\overline{\mathrm{pre}}~n)))$
を得ました. と, こんな感じで, 不動点結合子を使うと簡単に再帰関数を表現できることになります.

3.4. フラグ回収

ここから先は, 著者と同じ講義を受けている人向けの内輪ネタです. はじめの方の講義で, 木構造を集合として扱ったことを覚えているでしょうか. 木構造を
$T_{n + 1} = I_A(T_n) := \{\bot\} + A \times T_n \times T_n$
で再帰的に定義していって,
$\displaystyle T := \bigcup_{n\in \mathbb{N}} T_n$
と膨らませていったものは, $I_A$ の不動点になったのでした. これとラムダ計算の講義資料34ページをよーーーく見比べてみてください. 全く同じことを言っていることがわかるかと思います. さすが頭の良い教員だけあってこの辺りのフラグ建築が一級品ですよね.