Subscribed unsubscribe Subscribe Subscribe

さけるチーズを避けるチーズによるラムダ計算・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では関数適用はコンビネータの直後に引数を置くだけで行えるということが、この翻訳の原理になっています。

さけるチーズを避けるチーズで作る関数型言語

最近、「裂けてるさけるチーズを裂けて避けるチーズが載ってる裂けてる地図を裂けて避けるチーズ」が話題になりました。
togetter.com

「さけるチーズを避けるチーズ」において、チーズがさけるチーズを避けた結果、残るのはチーズ。
「さけるチーズを避けるチーズを避ける地図」において、さけるチーズとチーズが避けられた結果、残るのは地図。
では「裂けてるさけるチーズを裂けて避けるチーズが載ってる裂けてる地図を裂けて避けるチーズ」の「事の果て」には、何が残るのか?
この記事では、そのような疑問を追うこと、つまりさけるチーズや地図が従う法則を追う行為によって、チューリング完全な純粋関数型言語「さけるチーズ」を構成します。

(具体的には、Lazy Kと呼ばれる言語に束縛変数を導入することでラムダ計算風にし、自然言語的に意味が通るように中置記法に改めたものです。)

例えば以下は、さけるチーズで記述した素数を無限に出力し続けるプログラムです。

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

The Lazy K Programming LanguageのSample Codeをさけるチーズに変換しました。)

このチーズ達の「せめぎ合い」の果てに何が残るのか、それを探す過程が素数を求める事に対応するのです。
さけるチーズはチューリング完全であるため、これほど単純な文法を持ちながら、素数計算に限らず、計算機上で実行できるいかなる計算も実行することができます。

自然数すら現れないこのコードで、なぜ素数が計算できるのか…?本当にそうなのか?という疑問に答えるため、この記事では上記のコードを実際に実行するために必要なツールを用意しました。「さけるチーズ」は「Lazy K」と呼ばれる言語をベースにしているため、今回はさけるチーズ → Lazy K 翻訳器と Lazy K → さけるチーズ翻訳器を構成しました。上記のコードを実際に実行するには、翻訳器によってさけるチーズをLazy Kに翻訳し、Lazy Kインタプリタ(たとえば http://lazy-k.appspot.com/ など)を使用して下さい。(インタプリタ作成は今回は割愛しました。)翻訳器はGitHub - woodrush/ski2cheese: 純粋関数型言語「さけるチーズ」とLazy Kの相互翻訳器に載せています。

では、さけるチーズとはどのような言語なのでしょうか。

さけるチーズにおける4つの法則

世の中には数多の言語が存在し、それぞれ複雑な構文や規則を持っています。しかし、さけるチーズに存在するのはたった4つの構文です。
それは、

1. 「さけるチーズを避けるチーズ」
2. 「裂けてるチーズ」
3. 「Xに捧げるY」
4. 「チーズとさけるチーズと地図のある地、伊豆」

の4つです。
そしてこの言語の唯一の原則は、以上の語句が現れたタイミングで、自然の摂理に従った置き換えを行うという事です。

第一法則:さけるチーズを避けるチーズ

まずは「さけるチーズを避けるチーズ」。
「Yを避けるX」という語句が現れたら、「X」に置き換えます。
なぜならば、YはXに避けられ、結果としてXが残るからです。これが第一の法則です。

例えば

「「Yを避けるX」を避けるZ」を避ける「Aを避ける「Bを避けるC」」

という構造物は、第一の法則に従って

「「Yを避けるX」を避けるZ」を避ける「Aを避ける「Bを避けるC」」
= 「Aを避ける「Bを避けるC」」
= 「Bを避けるC」
= C

のように変形できるため、「「Yを避けるX」を避けるZ」を避ける「Aを避ける「Bを避けるC」」の実行結果(評価結果)はCという事になります。

第二法則:裂けてるチーズ

続いて、「裂けてるチーズ」です。
「裂けてるX」という語句が現れたら、「X」に置き換えます。
なぜならば、裂けたXはやがて自らの力で修復され、元に戻るからです。これが第二の法則です。

例えば、

「「Yを避けるX」を避けるZ」を避ける「裂けてる「Aを避ける「「裂けてるB」を避ける「裂けてるC」」」」

は、第一・第二の法則を合わせて

「「Yを避けるX」を避けるZ」を避ける「裂けてる「Aを避ける「「裂けてるB」を避ける「裂けてるC」」」」
= 「裂けてる「Aを避ける「「裂けてるB」を避ける「裂けてるC」」」」
= 「Aを避ける「「裂けてるB」を避ける「裂けてるC」」」
= 「裂けてるB」を避ける「裂けてるC」
= 「裂けてるC」
= C

となり、「「Yを避けるX」を避けるZ」を避ける「裂けてる「Aを避ける「「裂けてるB」を避ける「裂けてるC」」」」の実行結果はCとなります。

第三法則:Xに捧げるY

さて、ここで事態は少し複雑になります。
この構文を説明する前に、この世界(言語)に関する重要な定めについて話す必要があります。それは、この世界には触れてはならぬ禁断の者が3人存在するということです。彼らはすなわち、「さけるチーズ」「チーズ」「地図」です。
そして実は、先ほどの第一、第二の法則、そして続く第四の法則では、これら禁断の者本人が存在する場合、置き換えを行ってはなりません。
例えば、

「Aを避ける「Bを避けるチーズ」」
= 「Bを避けるチーズ」
≠ チーズ  (※禁断の者を含む構造物を変形してはいけない!)

と変形されます。
まず、一行目から二行目の変形は許されています。「Bを避けるチーズ」は禁断の者本人ではないため、「Aを避ける「Bを避けるチーズ」」は変形が可能なのです。
しかし、第二行目において「チーズ」は禁断の者であることから、これ以上変形ができません。

同様に、

裂けてる「「裂けてるチーズ」を避ける「Aを避ける「「裂けてるチーズ」を避けるチーズ」」」
= 「裂けてるチーズ」を避ける「Aを避ける「「裂けてるチーズ」を避けるチーズ」」
= 「Aを避ける「「裂けてるチーズ」を避けるチーズ」」
= 「裂けてるチーズ」を避けるチーズ
≠ チーズ  (※禁断の者を含む構造物を変形してはいけない!)

のようになります。最後の一つ手前の行では、構造物が禁断の者チーズを含んでいるためこれ以上変形できません。

さて、ここで「Xを捧げるY」という構文が登場します。
「Xを捧げるY」は、「Xに含まれる最強の禁断の者を、Yで置き換える」という規則です。
禁断の者たちの強さの順番は、禁断の者の強さの順は「チーズ>さけるチーズ>地図」となっています。

例えば、

「さけるチーズを避けるチーズ」に捧げるXに捧げるY
= 「さけるチーズを避けるX」に捧げるY
= 「Yを避けるX」
= X

となり、この構造物の値はXとなります。
また、

「Aを避ける「Bを避けるチーズ」」に捧げるX
= 「Bを避けるチーズ」に捧げるX
= 「Bを避けるX」
= X

となります。
1行目から2行目の変形では、第一項(「Aを避ける「Bを避けるチーズ」」)の最上層部には禁断の者は存在しないため、「に捧げるX」は発動しません。
第二項内部の第二項「チーズ」は、1行目の最上層には存在しないため、禁断の者としてカウントされません。
しかし2行目にたどり着くと、第一項(「Bを避けるチーズ」)が変形できない形になっています。
ここで、「に捧げるX」という構文によって、2行目から3行目にかけて禁断の者チーズがXに置き換えられました。
そして第一の法則によって、最終的にこの値はXとなっています。

また、捧げ物同士で捧げあってはいけません。例えば、

「さけるチーズを避けるチーズ」に捧げるXに捧げるY
= Yを避けるX  (※正しい変形)

「さけるチーズを避けるチーズ」に捧げるXに捧げるY
≠ 「さけるチーズを避けるチーズ」に捧げる「Xに捧げるY」 (※間違い!)
= さけるチーズを避ける「Xに捧げるY」 (※結果が正しい変形の場合と異なってしまっている)

ということです。(つまり、「〜に捧げる」は左結合な演算子です。)

(補足)
禁断の者を、以下のように空欄で置き換えると、この法則が明快になります。

「裂けてる「「裂けてるチーズ」を避ける「さけるチーズを避ける「さけるチーズを避けるチーズ」」」」に捧げるXに捧げるY
↓
「裂けてる「「裂けてる__1」を避ける「__1を避ける「__2を避ける__1」」」」に捧げるXに捧げるY

この構造物は、

「裂けてる「「裂けてる__1」を避ける「__1を避ける「__2を避ける__1」」」」に捧げるXに捧げるY
= 「「裂けてる__1」を避ける「__1を避ける「__2を避ける__1」」」に捧げるXに捧げるY
= 「__1を避ける「__2を避ける__1」」に捧げるXに捧げるY
= 「Xを避ける「__2を避ける__1」」に捧げるY
= 「__2を避ける__1」に捧げるY
= 「__2を避けるY」

と変形されます。
つまり、禁断の者に関するルールは、最上層に空欄が存在する構造物は変形してはいけないという事になります。

第四法則:「チーズとさけるチーズと地図のある地、伊豆」

さて、この法則がさけるチーズにおいて最も複雑な法則になります。
神聖なる地、伊豆では、古来から物を捧げる文化が発達してきました(要出典)。
そんな伊豆にまつわる第四の法則における変換規則は

「XとYとZのある地、伊豆」
= Xに捧げるZに捧げる「Yに捧げるZ」

です。
例えば、

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

となり、答えは「裂けてるチーズ」となります。

さけるチーズによるプログラミング

さけるチーズの全ての文法が出揃った所で、さけるチーズによる実際のプログラミング方法を解説しながら、さけるチーズで実際にプログラミングが可能であることを示したいと思います。
具体的には、

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

を扱います。
続きは、次の記事で!
woodrush.hatenablog.com

Configuring and Installing TensorFlow for Non-Titan GPUs

TensorFlow officially supports GPUs with versions greater than the GeForce GTX TITAN. However, it is possible to configure and install TensorFlow for GPUs before Titan, such as the GeForce GTX 960 (which I have used for verification) by using "unofficial settings" that are not tested and supported (but is mentioned on the official installation instructions).

TensorFlow's official GPU compatibility is mentioned in the "Optional: Install CUDA (GPUs on Linux)" section in the TensorFlow installation instructions
https://www.tensorflow.org/get_started/os_setup.html#installation-for-linux:

TensorFlow GPU support requires having a GPU card with NVidia Compute Capability >= 3.5. Supported cards include but are not limited to:

However, as mentioned in the "Enabling Cuda 3.0" section, we can configure and install TensorFlow for non-Titan GPUs by using "unofficial settings" during the configuration.

Caution: as it is called as "unofficial," this method is "largely untested and unsupported," meaning that the installation may be glitchy. This is mentioned in the following message that appears during the `./configure` part in the installation:

WARNING: You are configuring unofficial settings in TensorFlow. Because some
external libraries are not backward compatible, these settings are largely
untested and unsupported.

A Japanese version of this entry can be found here: http://qiita.com/woodrush/items/67703153541ce869e3dc

Installation

Build from source, according to the official installation guide
https://www.tensorflow.org/versions/master/get_started/os_setup.html:

  1. Follow each step in the "Installing from sources" section before the "Configure the installation" step
  2. Follow the "Enabling Cuda 3.0" section and ./configure the "unofficial settings"
  3. Follow the "Create the pip package and install" to create a pip wheel and install TensorFlow from the wheel
    • (This step is required only when installing in virtual python environments such as pyenv, virtualenv, etc. When installing TensorFlow for the system's Python environment, follow the instructions in "Build your target with GPU support" section instead.)

I used a Geforce GTX 960, Ubuntu 15.04 PC setup for verifying these steps. I tested the "Neural Art in TensorFlow" repo for testing functionality: woodrush/neural-art-tf · GitHub.

tmuxの使い方:一晩サーバーに仕事を投げて、翌日結果を見たい!

「一晩サーバーに仕事を投げて、翌日結果を見たい!」
「学校でサーバーにタスクを投げて、後で家で確認したい!」
Windows Updateが始まってssh接続が切れてしまった…つらい…」

こんな場面はしばしばあります。普通にssh接続をしている場合、接続を切るとタスクが止まってしまいます。すると上記のような場合、sshで接続している自機を一晩中つけておいたり、学校から家までsshの接続をずっと保っておくわけには行きません。Windows Updateなどで強制的にsshが切られたらもっと嫌です。

そんな時にはtmuxを使います。tmuxはかなり多くの機能があるのですが、上記の用途だけなら2, 3個コマンドを覚えるだけで十分です。

tmuxの詳しい動作原理はtmuxを使い始めたので基本的な機能の使い方とかを整理してみた - 完熟トマトの「tmux利用のイメージ図」がわかりやすいです。ごく簡単に言うと、tmuxはサーバー側に仮想端末を包み込んだ(アタッチした)プロセスを走らせておきます。この仮想端末はsshを切っても裏で動き続けてくれるので、一晩寝ていても裏でタスクを走らせ続けることができるのです。

tmuxの使い方については主に下記のサイトを参考にしました。
tmuxを使い始めたので基本的な機能の使い方とかを整理してみた - 完熟トマト
www.task-notes.com

1. サーバー側でtmuxをインストール

まずはターミナルからtmuxをインストールします。

Ubuntuの場合、下記でインストールします:

sudo apt-get install tmux

これでインストール出来ない場合はtmux installation steps for Ubuntu · GitHubが参考になるかもしれません。

Mac OS Xの場合、Homebrewをインストールした状態で下記でインストールします:

brew install tmux

また、tmuxを使い始めたので基本的な機能の使い方とかを整理してみた - 完熟トマトによると、RHELLinuxでは「EPELリポジトリにパッケージが存在しますのでyumでパッケージをインストールできます」:

yum install http://dl.fedoraproject.org/pub/epel/6/x86_64/tmux-1.6-3.el6.x86_64.rpm

また、tmuxの基本的な使い方とコマンドのまとめ - TASK NOTESによると、CentOSの場合は「EPELリポジトリを追加してインストールします」:

rpm -i http://ftp.riken.jp/Linux/fedora/epel/6/x86_64/epel-release-6-8.noarch.rpm
yum -y install tmux

2. 作業開始:tmuxを起動

いよいよtmuxを使います。まず、sshで処理を行いたいサーバーへ接続します。そして、

tmux

を実行します。すると、仮想端末(セッション)が開始します。

仮想端末は閉じたり開いたりするので、名前をつけておきます。そのためには「Control - b」「$」と続けて押します。(Controlで操作するのはemacsに似ていますね。)その後、セッション名を入力してEnterで名前がつきます。

tmux起動と同時にセッションに名前を付けるには

tmux new-session -s <session-name>

とします。

さて、名前のついたセッションを起動しました。セッションは普通の端末と同じように使えるので、一晩投げたいタスクをここで実行します。

3. 作業中断:セッションのデタッチ

タスクも実行開始した所で、いよいよ一晩寝る時がやってきました。セッションをデタッチするには、「Control - b」「d」と続けて押します。すると、仮想端末から抜けて普通の端末に戻ります。
しかし、裏ではtmuxの仮想端末がちゃんと動いています。この普通の端末で

tmux ls

を実行してみましょう。すると、先ほど名前をつけた端末が裏で走っています。

デタッチしたセッションを再びアタッチするには、

tmux a -t <session-name>

とします。これで、先ほどの処理の実行途中でも、その端末の様子を見ることが出来ます。

ここでサーバーとのssh接続を切って、再び接続し、同じくtmux lsを実行しても、やはり裏で仮想端末が走り続けてくれています。
これで、安心して一晩寝ることが出来ます。

4. 作業復帰:セッションのアタッチ

新しい朝がやって来ました。進捗確認のため、サーバーにsshで接続し、先ほどのように

tmux a -t <session-name>

を実行します。セッション名を忘れたらtmux lsで確認すれば大丈夫です。

これで一晩寝られる!

これで、あなたもサーバーにタスクを投げて一晩寝られるようになりました。

tmuxにはここで紹介した他にも色々な便利な機能があります。詳しくは、
tmuxを使い始めたので基本的な機能の使い方とかを整理してみた - 完熟トマト
tmuxの基本的な使い方とコマンドのまとめ - TASK NOTES
が大変参考になります。

Installing Torch (OpenBLAS) on Ubuntu 15.04 with Skylake CPUs

As I encountered a problem installing Torch in Ubuntu 15.04 probably because of using Skylake CPUs (Intel Core i7 6600), I would like to share how I have managed installing it on my system. The main reasons were installation errors of OpenBLAS and luacrypto.

My system setup is as follows:
MB: z170 Extreme 6 (with z170 chipset)
CPU: Intel Core i7 6600
OS: Ubuntu 15.04 Japanese Remix

I was installing Torch as said on its official website:
Torch | Getting started with Torch
Installation failed on the following command:

curl -s https://raw.githubusercontent.com/torch/ezinstall/master/install-deps | bash

With the following error indicating OpenBLAS was not compiled:

Cloning into 'OpenBLAS'...
remote: Counting objects: 17300, done.
remote: Compressing objects: 100% (8/8), done.
remote: Total 17300 (delta 2), reused 0 (delta 0), pack-reused 17292
Receiving objects: 100% (17300/17300), 14.80 MiB | 3.03 MiB/s, done.
Resolving deltas: 100% (11998/11998), done.
Checking connectivity... done.
getarch_2nd.c: In function ‘main’:
getarch_2nd.c:12:35: error: ‘SGEMM_DEFAULT_UNROLL_M’ undeclared (first use in this function)
printf("SGEMM_UNROLL_M=%d\n", SGEMM_DEFAULT_UNROLL_M);
^
getarch_2nd.c:12:35: note: each undeclared identifier is reported only once for each function it appears in
getarch_2nd.c:13:35: error: ‘SGEMM_DEFAULT_UNROLL_N’ undeclared (first use in this function)
printf("SGEMM_UNROLL_N=%d\n", SGEMM_DEFAULT_UNROLL_N);
^
getarch_2nd.c:14:35: error: ‘DGEMM_DEFAULT_UNROLL_M’ undeclared (first use in this function)
printf("DGEMM_UNROLL_M=%d\n", DGEMM_DEFAULT_UNROLL_M);
^
getarch_2nd.c:15:35: error: ‘DGEMM_DEFAULT_UNROLL_N’ undeclared (first use in this function)
printf("DGEMM_UNROLL_N=%d\n", DGEMM_DEFAULT_UNROLL_N);
^
getarch_2nd.c:19:35: error: ‘CGEMM_DEFAULT_UNROLL_M’ undeclared (first use in this function)
printf("CGEMM_UNROLL_M=%d\n", CGEMM_DEFAULT_UNROLL_M);
^
getarch_2nd.c:20:35: error: ‘CGEMM_DEFAULT_UNROLL_N’ undeclared (first use in this function)
printf("CGEMM_UNROLL_N=%d\n", CGEMM_DEFAULT_UNROLL_N);
^
getarch_2nd.c:21:35: error: ‘ZGEMM_DEFAULT_UNROLL_M’ undeclared (first use in this function)
printf("ZGEMM_UNROLL_M=%d\n", ZGEMM_DEFAULT_UNROLL_M);
^
getarch_2nd.c:22:35: error: ‘ZGEMM_DEFAULT_UNROLL_N’ undeclared (first use in this function)
printf("ZGEMM_UNROLL_N=%d\n", ZGEMM_DEFAULT_UNROLL_N);
^
getarch_2nd.c:67:50: error: ‘SGEMM_DEFAULT_Q’ undeclared (first use in this function)
printf("#define SLOCAL_BUFFER_SIZE\t%ld\n", (SGEMM_DEFAULT_Q * SGEMM_DEFAULT_UNROLL_N * 4 * 1 * sizeof(float)));
^
getarch_2nd.c:68:50: error: ‘DGEMM_DEFAULT_Q’ undeclared (first use in this function)
printf("#define DLOCAL_BUFFER_SIZE\t%ld\n", (DGEMM_DEFAULT_Q * DGEMM_DEFAULT_UNROLL_N * 2 * 1 * sizeof(double)));
^
getarch_2nd.c:69:50: error: ‘CGEMM_DEFAULT_Q’ undeclared (first use in this function)
printf("#define CLOCAL_BUFFER_SIZE\t%ld\n", (CGEMM_DEFAULT_Q * CGEMM_DEFAULT_UNROLL_N * 4 * 2 * sizeof(float)));
^
getarch_2nd.c:70:50: error: ‘ZGEMM_DEFAULT_Q’ undeclared (first use in this function)
printf("#define ZLOCAL_BUFFER_SIZE\t%ld\n", (ZGEMM_DEFAULT_Q * ZGEMM_DEFAULT_UNROLL_N * 2 * 2 * sizeof(double)));
^
make: *** [getarch_2nd] Error 1
Makefile:131: *** OpenBLAS: Detecting CPU failed. Please set TARGET explicitly, e.g. make TARGET=your_cpu_target. Please read README for the detail.. 中止.
Error. OpenBLAS could not be compiled

I found the following issue at the OpenBLAS repo:
The build system doesn't know about SkyLake · Issue #632 · xianyi/OpenBLAS · GitHub

martin-frbg commented 25 days ago

"TARGET=BROADWELL" should work on the "develop" branch (which you will probably want to try rather than the already somewhat dated 0.2.14 release)
(Edited to add: judging from cpuid_x86.c, Broadwell cpu is simply mapped to Haswell even in the develop branch, but you will probably still want all the fixes that went in since the 0.2.14 release)

xianyi commented 23 days ago

@yuyichao , I didn't optimize skylake yet. Therefore, please use haswell kernels. make TARGET=HASWELL

So I did

curl -s https://raw.githubusercontent.com/torch/ezinstall/master/install-deps > installtorch.sh

and edited it to create a custom installation shellscript: (edit: deleted lines that specified to use the `develop` branch)

diff installtorch.sh installtorch-new.sh 
14,16c14,16
<         make NO_AFFINITY=1 USE_OPENMP=0 USE_THREAD=0
<     else
<         make NO_AFFINITY=1 USE_OPENMP=1
---
>         make NO_AFFINITY=1 USE_OPENMP=0 USE_THREAD=0 TARGET=HASWELL
>     else 
>         make NO_AFFINITY=1 USE_OPENMP=1 TARGET=HASWELL

This shellscript let OpenBLAS compile correctly, letting the command that failed to pass.

Installing luacrypto

I encountered another failure on the third command,

cd ~/torch; ./install.sh

and got the following error:

Missing dependencies for itorch:
lbase64
luacrypto
uuid
lzmq >= 0.4.2

Using https://raw.githubusercontent.com/rocks-moonscript-org/moonrocks-mirror/master/lbase64-20120820-1.src.rock... switching to 'build' mode
Do not use 'module' as a build type. Use 'builtin' instead.
gcc -O2 -fPIC -I/home/woodrush/torch/install/include -c lbase64.c -o lbase64.o
gcc -shared -o base64.so -L/home/woodrush/torch/install/lib lbase64.o
Updating manifest for /home/woodrush/torch/install/lib/luarocks/rocks
lbase64 20120820-1 is now built and installed in /home/woodrush/torch/install/ (license: Public domain)

Using https://raw.githubusercontent.com/rocks-moonscript-org/moonrocks-mirror/master/luacrypto-0.3.2-1.src.rock... switching to 'build' mode

Error: Failed installing dependency: https://raw.githubusercontent.com/rocks-moonscript-org/moonrocks-mirror/master/luacrypto-0.3.2-1.src.rock - Could not find expected file openssl/evp.h, or openssl/evp.h for OPENSSL -- you may have to install OPENSSL in your system and/or pass OPENSSL_DIR or OPENSSL_INCDIR to the luarocks command. Example: luarocks install luacrypto OPENSSL_DIR=/usr/local

I found the following issue on a different OpenSSL problem:
cmake not able to find openssl - Stack Overflow

so I did

    sudo apt-get install libssl-dev

to make sure I installed luacrypto I also did (may not be necessary)

    sudo apt-get install libssl-dev
    sudo apt-get install luarocks
    source .bashrc       # This was after I failed installing torch with the third command: this seems to have the effect of enabling luarocks
    luarocks install luacrypto

and the rest of the Torch installation finished successfully.

Survey: Marschner, et al. (2003), Light scattering from human hair fibers (The Marschner Model)

As I had an opportunity to read and implement Marschner's paper [1] on the Marschner Model, I would like to share the details and points I have stumbled upon on reading the paper. The Marschner Model is a model proposed in 2003, that describes how light is scattered (reflected and transmitted) in human hair. It is used to implement shaders for human hair models, and rendering realistic hair.
[1] MARSCHNER, S. R., et al., 2003. Light scattering from human hair fibers. ACM Trans. Graph. 22, 3, 780–791. http://www.graphics.stanford.edu/papers/hair/

For conducting this survey, I've also referenced the following blog post:
Marschner Shader Part II | Real-Time Hair Simulation and Rendering



Overview

The Marschner Model is essentially a scattering function {S(\omega_i,\omega_r)}, which lets you find how much light is redirected from one direction to another. Simply put, it is the ratio of incoming light intensity from direction {\omega_i} against the outcoming light intensity from direction {\omega_r}. Given an outcoming direction {\omega_r}, it can be used as

{
\bar L_r(\omega_r) = D \int
S(\omega_i, \omega_r)
L_i(\omega_i)
\cos \theta_i\,
d \omega_i,
}

to determine the amount of light emitted in that direction.

  • Here, {\bar L} is the intensity per *length* (which is different from ordinary *radiance*, which is intensity per *area*), which they call as *curve intensity*.
  • {D} is the diameter of the hair - which implies that outcoming light increases for thicker hair, i.e. thicker hairs are more shiny.
  • One novel point of the Marschner Model is that {S} is a function of only the *direction* of incidence, and not the *position* of incidence, meaning that the hair's thickness is *taken out of thought*. In the derivation, the hair's thickness (the position of ray-hair intersection) is explicitly considered, but is effectively ignored in its final form.


f:id:woodrush:20150923200321p:plain

Figure 1. The coordinate system. Image cited from Marschner, et al. (2003) [1]

One important point that I've stumbled upon is the coordinate system. Although at first sight it seems like an ordinary spherical system with {w} as the {z} direction, that is actually not the case. Here, {\theta_i} and {\theta_r} are measured as the inclination to the {w}-{v} plane. Therefore,

{
\begin{align}
\theta_i &:= \frac \pi 2 - \cos^{-1} (\omega_i \cdot u), \\
\phi_i &:= \tan^{-1} \left(\frac{\omega_i \cdot w}{\omega_i \cdot v}\right). \\
\end{align}
}

The same holds for {\omega_r}.


In the paper, the hair is modeled as an elliptic cylinder with a bumpy surface (which models cuticles). They first start with an ideal, smooth cylinder case, where {S} is given as

{
S(\phi_i, \theta_i ; \phi_r, \theta_r) = \delta(\theta_r + \theta_i) N(\eta'(\theta); \phi_i, \phi_r) / \cos^2 \theta.
}

Where {\delta} is the delta function.
The term {\delta(\theta_r + \theta_i)} implies that scattering only occurs when {\theta_r = \theta_i}, which ultimately implies that an incoming straight ray is emitted in the shape of a cone.

We can see that {S} is decomposed into {\theta}-dependent parts and {\phi}-dependent parts. This is one of the important features of this model, derived from the symmetry of the cylindric geometry of the hair.

The actual Marschner Model is an extention of this equation,

{ 
\begin{align}
S(\phi_i, \theta_i ; \phi_r, \theta_r)
&=M_{R}  (\theta_h) N_{R}  (\eta'(\eta,\theta_d); \phi) / \cos^2 \theta_d \\
&+M_{TT} (\theta_h) N_{TT} (\eta'(\eta,\theta_d); \phi) / \cos^2 \theta_d \\
&+M_{TRT}(\theta_h) N_{TRT}(\eta'(\eta^*(\phi_h),\theta_d); \phi) / \cos^2 \theta_d.
\end{align}
}

Although there are more terms, all emitted light is still contained in a single cone. The 3 terms represent the 3 modes of scattering that are considered (all modes are in the same cone). We can recognize that one major extension is the replacement of {\delta(\theta_r + \theta_i)} with {M(\theta_h)}.

  • {\eta '} is one of the difficult parts of this paper. In this paper, simply put, *3D Fresnel effects are evaluated as 2D Fresnel effects with an augmented index of refraction,* thanks to the symmetry of hair (c.f. p. 6). We know that in Fresnel reflections/refractions, all light paths are contained in one plane. Obviously, this plane does not necessarily run parallel to the surface normal of the hair, and can be tilted (i.e., the plane may not cross the hair orthogonally). In this paper, the "3D" light path (on the tilted plane) is projected on to the plane perpendicular to the hair surface. Then, the Fresnel equations are evaluated *on the projected plane*, and then *projected back to the original tilted plane*. The augmented index of refraction, used on the projected plane, is {\eta '} - which only depends on {\theta} due to the projection.

The Model

{M} is a "unit-integral, zero-mean lobe function with width {\beta}" (c.f. p.8), i.e. simply a probability distribution {g}:

{ 
\begin{align}
M_{R}  (\theta_h) &= g(\alpha_{R}  , \beta_{R}  ;\theta_h) \\
M_{TT} (\theta_h) &= g(\alpha_{TT} , \beta_{TT} ;\theta_h) \\
M_{TRT}(\theta_h) &= g(\alpha_{TRT}, \beta_{TRT};\theta_h) 
\end{align}
}

In the paper, {g(\alpha, \beta, x)} is given as a normalized Gaussian function with mean {\alpha} and standard deviation {\beta}:
{ 
g(\alpha, \beta, x) = \frac 1 {\sqrt{2 \pi \beta^{2}}}
\exp \left(-\frac{(x - \alpha)^2}{2\beta^{2}}
\right).
}

  • The notation for the dependency of {\alpha} on {g} is changed for clarity.

{N} is complicated to find. First, as a notation, the paths {R, TT, TRT} are given an index {p=0,1,2}, respectively. Then:

{ 
\begin{align}
N_p(\eta'(\eta,\theta_d),p,\phi) &:= \sum_{\gamma_i \in \Gamma} A(p,h(p,\gamma_i,\phi))
\left|
	2 \frac {d\hat\phi} {dh}(p, h(p,\gamma_i,\phi))
\right|^{-1}.
\end{align}
}

Here, {\phi := \phi_i - \phi_t}. This means that {N_p} depends on the azimuths through only their *difference*.

  • We have additionally written the {\eta'(\eta,\theta_d)}-dependency of {N_p} and {h}.
  • The notation of the sum and the arguments of {h} were changed for clarity.
  • Confusingly, in the original paper there is a *variable* {\phi := \phi_i - \phi_t/2} and a *function* {\phi(p,\gamma_i)} which are different quantities. {\phi(p,\gamma_i)} is a trigonometric function (c.f. p.6) and is later approximated as {\hat \phi(p,\gamma_i)} (c.f. p.8). For brevity, we will write {\hat \phi} in place of the original function {\phi(p,\gamma_i)}.

Below, we will study the actual forms of each term.


Definition of {\eta'}, {\eta''}:

{\eta'}, {\eta''} are the corrected values of {\eta}:

{ 
\begin{align}
	\eta'(\eta, \varphi)  &:= \sqrt{\eta^2 - \sin^2 \varphi} \Big/ \cos \varphi\\
	\eta''(\eta, \varphi) &:= \eta^2 \cos \varphi \Big/ \sqrt{\eta^2 - \sin ^2 \varphi}
\end{align}
}

Here, {\eta} is a constant (c.f. p.8).

Definition of {F}:

{F} is the corrected Fresnel reflectance function, computed with the corrected refraction indices {\eta', \eta''}.

We know the ordinary Fresnel reflectance functions are given as:

{ 
\begin{align}
	F_s(\eta_1, \eta_2, \varphi)
	&:=
	\frac
	{\eta_1 \cos \varphi - \eta_2 \cos \varphi'}
	{\eta_1 \cos \varphi + \eta_2 \cos \varphi'} \\
	F_t(\eta_1, \eta_2, \varphi)
	&:=
	\frac
	{\eta_1 \cos \varphi' - \eta_2 \cos \varphi}
	{\eta_1 \cos \varphi' + \eta_2 \cos \varphi} \\
	\varphi' &:= \sin^{-1}\left(\frac{\eta_1}{\eta_2}\sin \varphi \right)
\end{align}
}

The corrected Fresnel function {F} is then defined as
{ 
\begin{align}
	F(\eta', \eta'', \varphi)
	&:=
	\frac
	{F_s(1,\eta'(\varphi),\varphi)^2 + F_t(1,\eta''(\varphi),\varphi)^2}
	2.
\end{align}
}

c.f. p.12:

...factor for oblique incidence may be computed from the projected angles by using {\eta'} for the perpendicular component of the reflectance and a second index, {\eta''}.

Finding {\gamma_i} and {h, \gamma_t}:

{\gamma_i} is found by solving a cubic equation. First define


{ 
\begin{align}
\theta_d &:= \frac{(\theta_r - \theta_i)} 2 \\
\eta' &:= \eta'(\eta,\theta_d) \\
c &:= \sin^{-1}(1/\eta') \\
%    \phi(p,h) &:= 2p\gamma_t - 2\gamma_i + p\pi  \\
\hat \phi(p,\gamma_i) &:= \left( \frac{6pc} \pi - 2 \right) \gamma_i - \frac{8pc}{\pi^3} \gamma_i^3 + p \pi
\end{align}
}

{\gamma_i} is then the solution of the equation

{ 
\hat \phi(p,\gamma_i) - \phi = 0.
}

Let {\gamma_i \in \Gamma} be all of the solutions of {\gamma_i}. (Recall that {\Gamma} is a symbol newly defined in this blog post.)

  • It is mentioned (c.f. p.6) that for {p \geq 2}, there may be one or three solutions to this equation, i.e. for the path {TRT} there may be multiple incident directions that end up being emitted in a specific direction.

For each solution of {\gamma_i}, we finally calculate {h} and {\gamma_t}:

{ 
\begin{align}
	h &:= h(p, \gamma_i, \phi) := \sin \gamma_i \\
	\gamma_t &:= \sin^{-1}\frac h {\eta'} \\
\end{align}
}

Finding {A}:

{A} is the attenuation factor:

{ 
\begin{align}
T(\sigma_a, h) &:= \exp\left(-\sigma_a(2 + 2\cos 2\gamma_t)  \right) \\
\sigma'_a &:= \sigma_a/\cos \theta_t \\
	A(p,h) &:=
	\begin{cases}
		F(\eta',\eta'',\gamma_i) & p = 0 \\
		\left(1 - F(\eta',\eta'',\gamma_i) \right)^2 
		F\left(
		\frac 1 {\eta'},
		\frac 1 {\eta''},
		\gamma_t
		\right)^{p-1}
		T(\sigma'_a,h)^p
		 & p > 0 \\
	\end{cases}
\end{align}
}

Where {\theta_t} is the "inclination to the axis" (c.f. p.7). Although this symbol is newly defined here in this sentence, we can infer that {\theta_t = \theta_d}, since {\theta_d} is the inclination used to determine the effective index of refraction {\eta'}.

Finding {d\hat\phi/dh}:

Using the approximation,

{ 
\begin{align}
	\frac{d\hat\phi}{dh}
	&=
	\frac{d\hat\phi}{d\gamma_i}
	\frac{d\gamma_i}{dh} \\
	&=
	\frac
	{\left( \frac{6pc} \pi - 2 	\right) - \frac{24pc}{\pi^3} \gamma_i^2}
	{\sqrt{1 - h^2}}.
\end{align}
}

Finding {N_p}:

Let us finally recall the form of {N_p}:

{ 
\begin{align}
N_p(p,\phi) &:= \sum_{\gamma_i \in \Gamma} A(p,h(p,\gamma_i,\phi))
\left|
	2 \frac {d\hat\phi} {dh}(p, h(p,\gamma_i,\phi))
\right|^{-1}.
\end{align}
}

One important fact is that the sum on the right hand side is taken over all solutions {\gamma_i \in \Gamma}, i.e. for all paths corresponding to the azimuth {\phi}.


The Grand Result

If we shall write the explicit form of one mode {M_pN_p} for the sake of reference (which becomes quite messy),

{ 
\begin{align}
&M_p  (\theta_h) N_p(\eta'(\eta,\theta_d),p,\phi) \\
=&
\frac 1 {\sqrt{2 \pi \beta_p^{2}}}
\exp \left(-\frac{(x - \alpha_p)^{2}}{2\beta_p^{2}}
\right) \times \\
&\sum_{\gamma_i \in \Gamma}
\left[
%A(p,h(p,\gamma_i,\phi))
\left(
	\begin{cases}
		F(\eta',\eta'',\gamma_i) & p = 0 \\
		\left(1 - F(\eta',\eta'',\gamma_i) \right)^{2} 
		F\left(
		\frac 1 {\eta'},
		\frac 1 {\eta''},
		\gamma_t
		\right)^{p-1}
		T(\sigma'_a,h)^p
		 & p > 0 \\
	\end{cases}
\right) \times \right.\\
&
\left.\left|
	2
	\frac
	{\left( \frac{6pc} \pi - 2 	\right) - \frac{24pc}{\pi^3} \gamma_i^{2}}
	{\sqrt{1 - h^{2}}}
\right|^{-1}\right],
\end{align}
}

where {\gamma_i \in \Gamma} are defined by the solutions for the cubic equation
{ 
\left( \frac{6pc} \pi - 2 \right) \gamma_i - \frac{8pc}{\pi^3} \gamma_i^3 + p \pi - \phi = 0.
}

{S(\omega_i, \omega_r)} is then a sum of the modes over the paths {p \in \{0,1,2\}}:
{ 
S(\omega_i, \omega_r) = \sum_p M_pN_p.
}

An intuitive explanation for the "Russian Roulette" sampling technique in ray tracing

The "Russian Roulette" sampling technique (which is creepily named, but is known officially as so) is a sampling technique used in ray tracing to reduce the number of samples for evaluating some value, while maintaining the convergence. It was very mystifying at first sight, but became very intuitive when I came up of a graphical explanation.

Shortly put, the Russian Roulette sampling technique can be interpreted as making "copies" of high-order terms, to use in place of the dropped off terms that were not evaluated in other samples. This can be described graphically using the following figure.

f:id:woodrush:20150725201736p:plain

Let us consider a problem where we want to evaluate 4 orders of some value, with 5 samples. In ray tracing, this could be evaluating the radiance using terms of up to 4 reflections with 5 samples, for instance. In the figure above, the colors correspond to the orders of the value, and the number n in the circle indicates that it is the n-th sample.

The leftmost figure shows a direct method of evaluating this value, that is to just simply evaluate all of the orders in all of the samples. However, in ray tracing it can be time-consuming to do such evaluations.

This is where the Russian Roulette sampling technique comes in. In the Russian Roulette technique, we aim to evaluate only a few high-order terms. Basically, before evaluating each order of terms, we roll some dice - and proceed to evaluate high order terms at only a given probability, or else halt the evaluation and move on to the next samples. Each higher order term must survive this judgement before it gets evaluated, or otherwise the "game" (higher-term evaluation) ends and moves on to the next round (sample) - therefore, the name "Russian Roulette." In this figure, we've assumed a 50% probability of proceeding to evaluate the next higher order. The figure on the center shows the actually calculated terms in each sample, for the Russian Roulette. In other words, the circles in the figure are the circles that "survived" the Roulette. Notice that the number of evaluations is reduced to around half of that in the left figure, and many high orders are dropped off.

Now, since we have excluded many orders, we don't have enough circles (terms) to add up to calculate the average. (i.e., simply taking the average of all of the terms (circles) provides an inaccurate estimate of the true value, compared to the estimator shown on the left figure.) Specifically, each n-th order term shows up at a ratio of (1/2)^(n-1) compared to the number of them in the left figure.

How do we calculate the average with such few circles (terms)? The answer, which is the Russian Roulette sampling technique, is to use copies of other circles (terms) as placeholders. Mathematically, the technique is to divide the value of each evaluated term by the probability of its appearance when taking the grand average. This obscure technique can be understood by observing the right side of the figure. Dividing the term by its survival probability p is equivalent to considering as if 1/p copies of that term has existed in the evaluation. This is the whole idea of the sampling technique, and is depicted in the figure above as copies of the circle. (Copies are indicated by red index numbers.) By making "copies" in such a way, the number of samples of each order approximately match that of the direct technique shown in the left side of the first figure. Although the number of circles differ from its true value (they are short in the 3rd order and excessive in the 2nd and 4th order), if we take a sufficient number of samples, the law of large numbers helps us to diminish those discrepancies to an ignorable level. Therefore, the "magic" of dividing higher order terms in the Russian Roulette technique, can be interpreted as making the "right number of copies" of that term, so that it properly compensates for the higher order terms that did not survive to be evaluated (i.e. dropped in the sampling process).