はじめに

この記事は株式会社ACCESS Advent Calendar 2020 の13日目の記事になります。

弊社では有志で集まって本を読む会というのをやっています。
そこでは本ごとにいくつかチームがあり、僕のチームでは Types and Programming Languages (いわゆる TaPL と呼ばれる本)を読んでいます。

まだ6章までしか読めていませんが、λ項の無名表現というのを初めて知りました。これを使って自然数とλ項の間に全単射を作り、自然数をチューリング完全にします。

この記事ではTaPLに倣い、自然数に 0 を含むものとして扱います。一応 $\mathbb{N}_0$ と書いておきます

λ項の無名表現

よくあるλ式の書き方は λx. λy. x y のように変数に x, y などの名前をつけて書く方法です。
無名表現では、この名前を取り除いて変数が束縛された順の逆順に番号を振り、この番号でもって変数を表現します。

例えば
λx. λy. x y は λ. λ. 1 0
λx. (λy. x) (λy. y) は λ. (λ. 1) (λ. 0)
となります。

束縛変数がスタックに積まれていて、今の文脈でスタックの何番目にいるか、という番号だと思うとわかりやすいかもしれません。

無名λ項の定義

無名λ項は、以下の3種類として定義されます:

term ::=
  n
  λ. t1
  (t1 t2)

1つめは変数で、n には任意の自然数が入ります
2つめはラムダ抽象で、 t1 の部分には任意の term が入ります
3つめは関数適用で、t1, t2 の部分には任意の term が入ります

無名λ項の評価

評価については色々方法があったり面倒な話が結構あるのですが、長くなってしまうので今回は割愛します。詳しくはTaPLの6章を参照。

例えば (λ. λ. 0 1) (λ. 1) という項を評価すると
λ. 0 (λ. 2) とならなければなりません。

(適当に名前をつけて考えると (λx. λy. y x)(λz. p) => λy. y (λz. p) です)

手順としては、(λ. (...)) (λ. 1) を評価するために (...) の部分の束縛変数(今の段階では0) を λ. 1 に置き換えようとするのですが、中身を見ると (λ. 0 1) であり、さらにλによる束縛が入ります。なので置き換えるべき束縛変数は 1 になり、λ. 0 (置き換えたもの) としたくなるのですが、λ. 1 をそのまま書いてしまうともともと自由変数だった 1 が束縛変数になってしまいます。なのでさらに番号をずらして λ. 0 (λ. 2) となるわけです。

この「ずらす」という操作と「置き換える」という操作をまず関数として定義します。

d-シフト

自由変数の番号をずらす関数です。
$\uparrow^d_c$ の $d$ はずらしたい差分で、$c$ はλの入れ子の中にいるときに「今まで何個の変数が束縛されたか」をカウントしたもので、 $c$ 未満の変数は束縛変数ということになります(一番外側にある $0$ は自由変数で、 $λ. 0$ となって初めて束縛変数となることに注意)。

\begin{eqnarray}
\uparrow^d_c(n) &=& \left\{\begin{array}{ll} n & \text{if}~~ n < c \\ n + d & \text{if}~~ n ≥ c\end{array}\right.\\
\uparrow^d_c(λ.t_1) &=& λ.\uparrow^d_{c+1}(t_1)\\
\uparrow^d_c(t_1~t_2) &=& (\uparrow^d_c(t_1)~\uparrow^d_c(t_2))\\
\\
\uparrow^d(t) &=& \uparrow^d_0(t)
\end{eqnarray}

代入

項 t の中で変数 j を項 s に置き換える代入 $[j \mapsto s]t$ は以下で定義できます:

\begin{eqnarray}
[j \mapsto s]k &=&\left\{\begin{array}{ll} s & \text{if}~~ k =  j \\ k & \text{otherwise}\end{array}\right. \\
[j \mapsto s](λ.t_1) &=& λ.[j+1 \mapsto \uparrow^1(s)]t_1\\
[j \mapsto s](t_1~t_2) &=& ([j \mapsto s]t_1~[j\mapsto s]t_2)
\end{eqnarray}

評価

シフトと代入を使うことで、(1-stepの)評価を以下で定義出来ます:

\begin{eqnarray}
\text{eval1}(n) &=& n\\
\text{eval1}(λ.t_1) &=& λ.t_1\\
\text{eval1}(n ~ t') &=& n ~ \text{eval1}(t')\\
\text{eval1}((λ. t_1)~t') &=& \uparrow^{-1}([0\mapsto \uparrow^1(t')]t_1)\\
\text{eval1}((t_1~t_2)~t') &=& (\text{eval1}(t_1~t_2)~t')\\
\end{eqnarray}

自然数への埋め込み

無名λ項の定義を見ると、無名λ項の集合の濃度が $\aleph_0$ であることがすぐにわかります。
これはいかにも自然数への全単射を作ってくださいと言わんばかりではありませんか。作ります。

まず項が3種類なので、それぞれ 3 で割ったあまりが 0, 1, 2 のものに写します。

変数 n は単に 3 * n で良いでしょう。

ラムダ抽象 λ. t1 は、 t1 を自然数 m に写せたものとして 3 * m + 1 とすれば良さそうです。

関数適用 (t1 t2) が問題ですが、t1 が m、 t2 が n に写せたものとして (m, n) を全単射 $\mathbb{N}_0 \times \mathbb{N}_0 → \mathbb{N}_0$ に渡すことで無理やり写します。

N^2 から N への全単射

全単射 $\mathbb{N}_0 \times \mathbb{N}_0 \rightarrow \mathbb{N}_0$ も色々なものが知られていますが、今回は以下の写像で写します:

$f (m, n) = \frac{(m + n)(m + n + 1)}{2} + m$

(0, 0) => 0, (0, 1) => 1, (1, 0) => 2, (0, 2) => 3, (1, 1) => 4, (2, 0) => 5, ...
という感じで、「2つの数の和でソートした上で、左側の数の順にならべた番号」になっています。

$\frac{k(k + 1)}{2}$ が 1 から k までの総和なので、 $\frac{(m + n)(m + n + 1)}{2}$ が 1 から m + n までの総和になります。そこに m を足せばこの数が出てくるという寸法です。

逆関数は結構面倒です。

$\frac{k(k + 1)}{2}$ という指標を使いたいのですが、写す前の数を写した後の m + n で分けると 0 | 1 2 | 3 4 5 | ... という分かれ方になり数が合いません。そこで、最初に + 1 をして 1 | 2 3 | 4 5 6 | ... という分かれ方になるようにします。

自然数 $l$ に対して $l' = l + 1$ とし、 $\frac{k(k + 1)}{2} < l' ≤ \frac{(k + 1)(k + 2)}{2}$ を満たす k を求めれば、 k = m + n になります。
ここで $l' - \frac{k(k+1)}{2} - 1$ をすれば m が出てきて、k - m が n となります。

そしてこの k を求める方法ですが、まず上記の不等式を二次不等式として解くと、

$\frac{-1-\sqrt{1 + 8l'}}{2} < k < \frac{-1+\sqrt{1 + 8l'}}{2} \land (k ≤ \frac{-3-\sqrt{1+8l'}}{2} \lor \frac{-3+\sqrt{1+8l'}}{2} ≤ k)$
となります。k, l が自然数であることを考えると(特に $l'≥1$ に注意)
$\frac{-3+\sqrt{1+8l'}}{2} ≤ k < \frac{-1+\sqrt{1+8l'}}{2}$
これを満たす自然数 $k$ を求めればよいので、最左辺を天井関数(ceil)に食わせれば良さそうですね。

実装

ということで数式が出揃ったので実装してみます。言語は何でも良いのですが、僕の使いなれた大嫌いで大好きな JavaScript で書くことにします:

LambdaOnNat.js

const vr = (m) => 3 * m;

const lambda = (t1) => 3 * t1 + 1;

const apply = (t1, t2) => (
  3 * ((t1 + t2) * (t1 + t2 + 1) / 2 + t1) + 2
);

const unvr = (t) => t / 3;

const unlambda = (t) => (t - 1) / 3;

const decomposeApply = (t) => {
  const l = (t - 2) / 3 + 1;
  const k = Math.ceil((-3 + Math.sqrt(1 + 8 * l)) / 2);
  const t1 = l - k * (k + 1) / 2 - 1;
  return [t1, k - t1];
};

const shift = (d, t, cutoff = 0) => {
  switch (t % 3) {
    case 0:
      return unvr(t) < cutoff ? t : vr(unvr(t) + d);
    case 1:
      return lambda(shift(d, unlambda(t), cutoff + 1));
    case 2:
      const [t1, t2] = decomposeApply(t);
      return apply(shift(d, t1, cutoff), shift(d, t2, cutoff));
  }
};

const substitute = (s, t, k = 0) => {
  switch (t % 3) {
    case 0:
      return unvr(t) === k ? s : t;
    case 1:
      return lambda(substitute(shift(1, s), unlambda(t), k + 1));
    case 2:
      const [t1, t2] = decomposeApply(t);
      return apply(substitute(s, t1, k), substitute(s, t2, k));
  }
}

const eval1 = (t) => {
  if (t % 3 !== 2) return t;
  const [t1, t2] = decomposeApply(t);
  switch (t1 % 3) {
    case 0:
      return apply(t1, eval1(t2));
    case 1:
      return shift(-1, substitute(shift(1, t2), unlambda(t1)));
    case 2:
      return apply(eval1(t1), t2);
  }
};

const toLambdaString = (t) => {
  switch (t % 3) {
    case 0:
      return unvr(t).toString();
    case 1:
      return `λ. ${toLambdaString(unlambda(t))}`;
    case 2:
      const [t1, t2] = decomposeApply(t);
      return [
        t1 % 3 === 1 ? `(${toLambdaString(t1)})` : toLambdaString(t1),
        t2 % 3 === 0 ? toLambdaString(t2) : `(${toLambdaString(t2)})`,
      ].join(' ');
  }
};

var が予約語なので vr としました…。

明示的にλ項を表すようなデータ構造を作ったわけではなく、自然数を自然数のまま扱っています。

とはいえ数だけだと何が起こってるのか分からないので、数を無名λ項としての文字列へ変換する関数 toLambdaString も用意しています。

実際に評価してみましょう

$ node
> .load LambdaOnNat.js

> eval1(131)
14
> eval1(14)
1
> eval1(1)
1
> toLambdaString(131)
'(λ. 0 0) (λ. 0)'
> toLambdaString(14)
'(λ. 0) (λ. 0)'
> toLambdaString(1)
'λ. 0'

> eval1(57299)
1717
> toLambdaString(57299)
'(λ. λ. 0 1) (λ. 1)'
> toLambdaString(1717)
'λ. 0 (λ. 2)'

ちゃんと評価出来ていますね！やったぜ。