さけるチーズを避けるチーズによるラムダ計算・Lazy K入門

純粋関数型言語「さけるチーズ」とは、難解プログラミング言語「Lazy K」の文法に束縛変数を導入することでラムダ計算風にし、自然言語的に意味が通るように文法を直した言語です:
woodrush.hatenablog.com

この記事では、「さけるチーズ」を用いてチャーチエンコーディングによる自然数やリストの表現について説明し、最後にさけるチーズ(というよりもLazy K)を用いたHello, world!プログラムの書き方を解説します。この記事は前回の記事の続きでもあり、また筆者自身のラムダ計算・Lazy K入門の過程をまとめた記事でもあります。Lazy Kはとても面白い言語なのですが資料が少ないので、この記事をラムダ計算・Lazy K入門の副読記事として活用して頂ければ幸いです。

ここでは、

  • 自然数の表現
  • 加算と累乗
  • リストの表現
  • Hello, World!プログラム

について解説します。

さけるチーズとLazy Kの相互翻訳法については、記事末尾の付録にて解説しています。

自然数の表現

まずはプログラミング上最も重要なデータの一つ、数を表現してみます。数字を含まない文法しか持たないさけるチーズで、どのようにして自然数を表現するのでしょうか?

さけるチーズでは、自然数をチャーチエンコーディング究極の関数型言語による至高のHello, world! - Life Goes On参照)によって表現します。
これは端的に言うと、自然数Nを、「任意の構造物fとXを捧げられた時、XにfをN回捧げた物を返す構造物」で表すという事です。
つまり「Nに捧げるfに捧げるX」が

Nに捧げるfに捧げるX
= fに捧げる「fに捧げる「fに捧げる…「fに捧げるX」」」」…」」」」  (fがN回登場)

に変換されるような構造物Nで、自然数Nを表します。

具体的には、これは以下のような構造物で実現できます:

0 = 「さけるチーズを避ける「裂けてるチーズ」」
1 = 「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」に捧げる「さけるチーズを避ける「裂けてるチーズ」」」
2 = 「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」に捧げる「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」に捧げる「さけるチーズを避ける「裂けてるチーズ」」」」
…

例えば

0に捧げるfに捧げるX
= 「さけるチーズを避ける「裂けてるチーズ」」に捧げるfに捧げるX
= 「fを避ける「裂けてるチーズ」」に捧げるX
= 「裂けてるチーズ」に捧げるX
= X

となり、確かにfにXを0回捧げた結果が返ってきます。
また、ここでは長くなるので割愛しますが、「2に捧げるfに捧げるX」という構造物を評価すると、実際に「fに捧げる「fに捧げるX」」となることが確認できます。

実はこの表現には規則性があり、後者関数

SUCC = 「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」

を定義すると、

0 = 「さけるチーズを避ける「裂けてるチーズ」」
1 = SUCCに捧げる0
2 = SUCCに捧げる1
3 = SUCCに捧げる2
…

のように計算できます。

このような数の表現方法(チャーチエンコーディング)におけるポイントは、どの数の表現の最上層部にも禁断の者が存在しているため、これ以上の変形ができないという事です。例えば 0 = 「さけるチーズを避ける「裂けてるチーズ」」では禁断の者さけるチーズがいます。また、1 = SUCCに捧げる0 では、SUCCがさけるチーズとチーズという2人の禁断の者を含んでいることから、0を捧げても禁断の者さけるチーズが残り、これ以上の変形ができません。
変形ができないことから、「最終的に計算結果の答えとして残す」ような使い方ができるのです。

加算と累乗

このような数の表し方の下で、数同士の演算も行うことができます。

まずX+Yという計算は、「XにSUCCをY回適用する」ことによって表すことができます。
そしてY自身、「与えられた関数をY回適用する」という機能を持つため、

「Yに捧げるSUCCに捧げるX」
= 「SUCCに捧げる「SUCCに捧げる…「SUCCに捧げるX」」」」」…」  (SUCCがY回登場)

となります。
ここで、

ADD = 「「裂けてるチーズ」と「さけるチーズを避けるSUCC」と地図のある地、伊豆」

を定義すると、

ADDに捧げるXに捧げるY
= 「「裂けてるチーズ」と「さけるチーズを避けるSUCC」と地図のある地、伊豆」に捧げるXに捧げるY
= 「「裂けてるチーズ」と「さけるチーズを避けるSUCC」とXのある地、伊豆」に捧げるY
= 「裂けてるチーズ」に捧げるXに捧げる「「さけるチーズを避けるSUCC」に捧げるX」に捧げるY
= 「裂けてるX」に捧げる「「Xを避けるSUCC」」に捧げるY
= Xに捧げるSUCCに捧げるY
= 「SUCCに捧げる「SUCCに捧げる…「SUCCに捧げるX」」」」」…」  (SUCCがY回登場)

となり、捧げ物をすることで足し算が行える構造物を得ることができました。

ここで、3を表す構造物に2を捧げたらどうなるでしょうか?
「3に捧げるfに捧げるX」=「fに捧げる「fに捧げる「fに捧げるX」」」であることから、

3に捧げる2に捧げるfに捧げるX
= 「2に捧げる「2に捧げる「2に捧げるf」」」に捧げるX  (3の直後の捧げ物を2つ取るため、Xは余る)
= 2に捧げる「2に捧げる「2に捧げるf」」に捧げるX
= 「「2に捧げる「2に捧げるf」」に捧げる「「2に捧げる「2に捧げるf」」に捧げるX」」  (※1)
= 「「2に捧げる「2に捧げるf」」に捧げる「2に捧げる「2に捧げるf」に捧げるX」」
= 「「2に捧げる「2に捧げるf」」に捧げる「「2に捧げるf」に捧げる「「2に捧げるf」に捧げるX」」」
= 「「2に捧げる「2に捧げるf」」に捧げる「2に捧げるfに捧げる「「2に捧げるf」に捧げるX」」」
= 「「2に捧げる「2に捧げるf」」に捧げる「2に捧げるfに捧げる「2に捧げるfに捧げるX」」」
= 「「2に捧げる「2に捧げるf」」に捧げる「2に捧げるfに捧げる「fに捧げる「fに捧げるX」」」」
= 「「2に捧げる「2に捧げるf」」に捧げる「fに捧げる「fに捧げる「fに捧げる「fに捧げるX」」」」」  (※1)

A = 「fに捧げる「fに捧げる「fに捧げる「fに捧げるX」」」」とおくと、
= 「「2に捧げる「2に捧げるf」」に捧げるA

※1、※2より、
「「2に捧げる「2に捧げるf」」に捧げるA
= 「fに捧げる「fに捧げる「fに捧げる「fに捧げるA」」」」
となることがわかる。よって、Aを代入して

= 「fに捧げる「fに捧げる「fに捧げる「fに捧げる「fに捧げる「fに捧げる「fに捧げる「fに捧げるX」」」」」」」」

これは、Xにfを8回捧げたものになっています。
よって、「3に捧げる2」は、さけるチーズ言語でいう8に等しいことになります。
ここでいう8は2の3乗を表しています。「与えられた物を3回捧げる」機能を持つものに「与えられた物を2回捧げる」機能を持つものを与えた結果、2×2×2回捧げることになった、というわけです。

リストの表現

さて、これまでで一つの数を表すことができました。しかし、文字列や数の列を扱うには、列の概念、つまりリストの概念が必要です。

まず、

PAIRに捧げるXに捧げるYに捧げるf
= fに捧げるXに捧げるY

となるような構造物PAIRを考えます。
PAIRは、具体的には

PAIR = 「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「「さけるチーズを避ける「さけるチーズを避けるチーズ」」と「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「「さけるチーズを避ける「「裂けてるチーズ」とさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と地図のある地、伊豆」と地図のある地、伊豆」と地図のある地、伊豆」と「さけるチーズを避ける「さけるチーズを避けるチーズ」」と地図のある地、伊豆」

と表すことができます。(証明はとても長いのでここでは省略します。)

ここで、PAIRにXとYのみを捧げ、fを捧げず

PAIRに捧げるXに捧げるY

で捧げ物を止めてみましょう。この構造物にはfを捧げる余地の為の禁断の者が1人含まれるため、これ以上変形できません。
これは、XとYの組(X . Y)を表しています。

A,B,C,Dのリストを作る場合、

「PAIRに捧げるAに捧げる「PAIRに捧げるBに捧げる「PAIRに捧げるCに捧げる「PAIRに捧げるDに捧げるEND」」」」

これは、(A . (B . (C . (D . END))))という、入れ子になったペアを表しています。
ここで、ENDはリストの終わりを表す特別な構造物です。冒頭にて述べたように、さけるチーズはLazy Kをベースにしているため、ENDには256を用います。
(リストに関して、詳しくは究極の関数型言語による至高のHello, world! - Life Goes On参照。)

Hello, World!

さて、ここまでの知識が揃うと、いよいよHello, World!プログラムを書くことができます。

さけるチーズでは、実行結果として残った構造物をASCII文字コードの入ったリストとして解釈し、文字列として表示します。
つまり、Hello, World!を出力するには、

(72 . (101 . (108 . (108 . (111 . (44 . (32 . (119 . (111 . (114 . (108 . (100 . (33 . 256)))))))))))))
= 「PAIRに捧げる72に捧げる「PAIRに捧げる101に捧げる「…に捧げる256」」」」…」」」」

という構造物を作れば良いのです。

ここでややこしいことに、さけるチーズ(というよりもLazy K)では「プログラムに標準入力の値が捧げられる」ため、実行時には

「PAIRに捧げる72に捧げる「PAIRに捧げる101に捧げる「…に捧げる256」」」」…」」」」に捧げる標準入力

という構造物が評価されてしまいます。
そこで、この標準入力を右から左へ受け流すため、

「さけるチーズを避けるHELLO_WORLD」

というプログラムを書きます。これによって、

「さけるチーズを避けるHELLO_WORLD」に捧げる標準入力
= 「標準入力を避けるHELLO_WORLD」
= HELLO_WORLD
⇒ Hello, World!

のように、無事Hello, World!を表示することができます。

また、数を効率的に表現するために2進法を使います:

4 = 2に捧げる2
8 = 3に捧げる2 = (2+1)に捧げる2
16 = 4に捧げる2 = (2^2)に捧げる2
32 = 5に捧げる2 = (2^2+1)に捧げる2
64 = 2に捧げる8

72 = ADDに捧げる64に捧げる8
101 = ADDに捧げる64に捧げる「ADDに捧げる32に捧げる「ADDに捧げる4に捧げる1」」
…

このようにして書いたさけるチーズによるHello, World!プログラムが以下です:

「さけるチーズを避ける「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「さけるチーズを避ける「「「裂けてるチーズ」と「さけるチーズを避ける「「「裂けてるチーズ」と「さけるチーズを避ける「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」」」と地図のある地、伊豆」と「さけるチーズを避ける「「「裂けてるチーズ」と「さけるチーズを避ける「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズと
さけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「裂けてるチーズ」」」」」と地図のある地、伊豆」と「さけるチーズを避ける「「「裂けてるチーズ」と「さけるチーズを避ける「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ
」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」」」」」と地図のある地、伊豆」と「さけるチーズを避ける「「「裂けてるチーズ」と「さけるチーズを避ける「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」」」」」と地図のある地、伊豆」と「さけるチーズを避ける「「「裂けてるチーズ」と「さけるチーズを避ける「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と
地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」のある地、伊豆」に捧げる「裂けてるチーズ」」」」」」」と地図のある地、伊豆」と「さけるチーズを避ける「「「裂けてるチーズ」と「さけるチーズを避ける「「「「
「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」」」」と地図のある地、伊豆」と「さけるチーズを避ける「「「裂けてるチーズ」と「さけるチーズを避ける「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」」と地図のある地、伊豆」と「さけるチーズを避ける「「「裂けてるチーズ」と「さけるチーズを避ける「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを
避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」のある地、伊豆」に捧げる「裂けてるチーズ」」」」」」」と地図のある地、伊豆」と「さけるチーズを避ける「「「裂けてるチーズ」と「さけるチーズを避ける「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と
「裂けてるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」のある地、伊豆」に捧げる「裂けてるチーズ」」」」」」」と地図のある地、伊豆」と「さけるチーズを避ける「「「裂けてるチーズ」と「さけるチーズを避ける「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける
「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」」」」」と地図のある地、伊豆」と「さけるチーズを避ける「「「裂けてるチーズ」と「さけるチーズを避ける「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチー
ズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」」」」」と地図のある地、伊豆」と「さけるチーズを避ける「「「裂けてるチーズ」と「さけるチーズを避ける「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」と「「「さけるチーズを避け
る「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」」」」と地図のある地、伊豆」と「さけるチーズを避ける「「「裂けてるチーズ」と「さけるチーズを避ける「「「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」に捧げる「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」に捧げる「裂けてるチーズ」」」と地図のある地、伊豆」と「さけるチーズを避ける「「裂けてるチーズ」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と「「「さけるチーズを避ける「チーズとさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と「裂けてるチーズ」と地図のある地、伊豆」のある地、伊豆」のある地、伊豆」」と地図のある地、伊豆」」と地図のある地、伊豆」」と地図のある地、伊豆」」と地図のある地、伊豆」」と地図のある地、伊豆」」と地図のある地、伊豆」」と地図のある地、伊豆」」と地図のある地、伊豆」」と地図のある地、伊豆」」と地図のある地、伊豆」」と地図のある地、伊豆」」と地図のある地、伊豆」」と地図のある地、伊豆」」と地図のある地、伊豆」とさけるチーズと地図のある地、伊豆」」と「さけるチーズを避けるチーズ」と地図のある地、伊豆」と地図のある地、伊豆」」


結論:さけるチーズを避けるチーズでプログラミングをすることができる

あとがき

今回は、さけるチーズによる自然数の表現、加算と累乗計算、リストの表現、そしてHello, World!プログラムについて解説しました。
累乗以外にも加減乗除など様々な演算を行うことができます。さけるチーズはチューリング完全であるため、数にまつわる演算ならばいかなるものでも行うことができます。今回、Lazy Kの計算能力や方法には度々驚かされました。特に、404 Blog Not Found:Math - 言語はどこまで小さくなれるか - (unlambda|iota|jot) のすすめ究極の関数型言語による至高のHello, world! - Life Goes Onなどが非常に参考になります。

さけるチーズやLazy K自体を書くことは難しいのですが、究極の関数型言語による至高のHello, world! - Life Goes Onにあるように、Scheme内のDSLで記述したプログラムに対応するLazy Kコードを出力するプログラムがあり、それを用いると非常にさけるチーズ(Lazy K)開発が捗ります。

また、この記事の執筆にあたって筆者が最も嵌ったのは、Lazy Kではチャーチ数そのものを出力に用いることができず、単一の数字でも、必ずリストに入れて出力しなければいけないという事です。
例えば、65という数字(ASCIIのAに対応)を出力したい時、チャーチ数の65を使うと出力されず、

PAIRに捧げる65に捧げるEND

という65を唯一の要素に持つリストを出力しなければなりません。
これは仕様にしっかりと書いてあることなのですが、そもそもSKIコンビネータ計算におけるリストとは何なのか、という点から調べる必要があり、苦労しました。

付録 - さけるチーズとLazy Kの相互翻訳

まず、Lazy Kからさけるチーズに翻訳する場合、

1. SXYZ → 「XとYとZのある地、伊豆」
2. KXY → 「Yを避けるX」  (※YとXが逆な事に注意!これは、演算子の日本語的な意味を保存するため)
3. IX → 「裂けてるX」
4. (式)XYZ → 「「式」に捧げるAに捧げるBに捧げるC」

4つ目の式が一番特徴的で、関数適用を「に捧げる」の文法で表しています。

これを踏まえた上で、さけるチーズからLazy Kに翻訳する場合、

  • 「XとYと地図のある地、伊豆」 → (SXY)
  • 裂けてる「Xを避けるチーズ」 → I(KX)
  • 「XとYと地図のある地、伊豆」に捧げるZ → (SXY)Z

のように、禁断の者(チーズ、さけるチーズ、地図)を空のコンビネータで置き換えることで翻訳が可能になります。
最後の「に捧げる」を用いた翻訳が最大のポイントで、これはコンビネータSXY(つまりラムダ式 λ a. SXYa )にZを適用したものであるためこうなっています。言い換えると、禁断の者がラムダ計算における束縛変数を表していて(つまり「XとYと地図のある地、伊豆」 = λ Z. SXYZ)、更にLazy Kでは関数適用はコンビネータの直後に引数を置くだけで行えるということが、この翻訳の原理になっています。