《工匠の直感》ループの手順と注意点、対戦相手の立場で知っておくべきこと（おまけでモダンベルチャーの《紅蓮術士の昇天》ループも）

どうもAaronです。

今回は趣味のMtGの話です。

「神河:輝ける世界」で《隔離用構築物/Contaiment Construct》が登場したことで、《工匠の直感/Artificer's Intuition》と《ライオンの瞳のダイアモンド/Lion's Eye Diamond》と《不死の霊薬/Eixir of Imortaliry》を用いた無限マナ無限ライフコンボが注目されています。このコンボは従来のループとはやや趣の異なるループ手順であり、その手順も難解であるため、使用しようと思っている方だけでなく対戦相手側としてもループの手順や条件を知っておくことが重要です。なお今回のループ手順はMOパンダ

（Twich:

https://www.twitch.tv/mopandaa 

YouTube:

https://www.youtube.com/c/mopanda_MTG

)様の配信で勉強させていただきました。MOパンダ様ありがとうございます。

 

なお今回の記事は僕の独自研究によります。誤りなどがある可能性があることにご留意ください。

《工匠の直感》ループについて

ループの条件

以下の通り。

1.戦場に《隔離用構築物》（以下構築物）、《工匠の直感》（以下直感）がある。

2.手札に《ライオンの瞳のダイヤモンド》（以下LED）1枚か他のアーティファクトが1枚あり、残りのLED全てと《不死の霊薬》（以下霊薬）がライブラリーにある。手札にあるのがLEDか《水蓮の花びら/Lotus Petal》か《オパールのモックス/Mox Opal》（ただし自身を入れて金属術達成が条件）の場合は青2マナ、それ以外の場合は青3マナの浮きマナが必要。

 

ループ手順

二種類考えれれる。第一の手順でのループは1ループにつき任意の色の2マナが生成する。第二の手順でのループは1ループで任意の色の3マナが生成する（《水蓮の花びら》2枚か自身込みで金属術を達成する《オパールのモックス》3枚がデッキ内にあれば後述の無限サーチをこれに充てることで4マナが生成する）上にほぞの無限サーチがおまけについてくるため、基本的には第二のループを用いるべきである。ただしライブラリーの中に他のほぞが二枚以上ない場合は第二のループは不可能の為、第一のループしか使えない。

 

第一のループ手順

(0. 手札のアーティファクトを直感で捨てて、1枚目のLEDをサーチする。このとき構築物の効果でそれを追放しておき、《水蓮の花びら》、《オパールのモックス》の場合はそれをサーチ後すぐに唱える。

戦場:構築物、直感　手札:LED他　マナ:(青)(青)(マナアーティファクト込み))

1. 1枚目のLEDを直感で捨てて2枚目のLEDをサーチ。このとき構築物の効果でそれを追放しておき、サーチ後すぐに唱える。

戦場:構築物、直感、LED　手札:LED他　マナ:(青)

2. 2枚目のLEDを直感で捨て、そのスタックで1枚目のLEDを(青)を出して砕く。3枚目のLEDをサーチ。サーチ後2枚目のLEDを唱える。

戦場:構築物、直感、LED　手札:LED　マナ:(青)(青)(青)

3. 3枚目のLEDを直感で捨て、そのスタックで2枚目のLEDを(青)を出して砕く。霊薬をサーチ。サーチ後3枚目のLEDを唱える。

戦場:構築物、直感、LED　手札:霊薬　マナ:(青)(青)(青)(青)(青)

4. 霊薬を直感で捨て、そのスタックで3枚目のLEDを任意の色のマナを出して砕く。4枚目のLEDをサーチ。サーチ後霊薬を4枚目のLEDから出したマナから唱える。

戦場:構築物、直感、霊薬　手札:LED　マナ:(青)(青)(青)(青)(任意)(任意)

5. 4枚目のLEDを直感で捨て、そのスタックで青マナから霊薬を起動してLED3枚と霊薬がライブラリーに戻る。ライブラリーに戻ったLEDの一枚をサーチ。サーチ後捨てたLEDを唱えると任意の色マナが2つ増えてライフが5点増えたことを除き1.の終了後と同じ状態に戻る。注意点としてマッドネスと異なり構築物の能力は誘発型能力なのでいったん墓地を経由する。従ってこれを行う場合は先に構築物の誘発を解決してから、霊薬を起動しないと捨てたLEDが追放されずにライブラリーに戻ってしまう。

戦場:構築物、直感、LED　手札:LED　マナ:(青)(任意)(任意)

6. 2.-5.を繰り返して無限マナ、無限ライフ発生。必要な分だけマナが出たらサーチ先を《歩行バリスタ/Walking Ballista》などに変更してフィニッシュ。

 

第二のループ手順

(0.手札のアーティファクトを直感で捨てて、1枚目のLEDをサーチする。このとき構築物の効果でそれを追放しておき、《水蓮の花びら》、《オパールのモックス》の場合はそれをサーチ後すぐに唱える。

戦場:構築物、直感　手札:LED他　マナ:(青)(青)(マナアーティファクト込み))

1. 1枚目のLEDを直感で捨てて2枚目のLEDをサーチ。このとき構築物の効果でそれを追放しておき、サーチ後すぐに唱える。

戦場:構築物、直感、LED　手札:LED他　マナ:(青)

2. 2枚目のLEDを直感で捨て、そのスタックで1枚目のLEDを(青)を出して砕く。3枚目のLEDをサーチ。サーチ後2枚目のLEDを唱える。

戦場:構築物、直感、LED　手札:LED　マナ:(青)(青)(青)

3. 3枚目のLEDを直感で捨て、そのスタックで2枚目のLEDを(青)を出して砕く。4枚目のLEDをサーチ。サーチ後3枚目のLEDを唱える。

戦場:構築物、直感、LED　手札:LED　マナ:(青)(青)(青)(青)(青)

4. 4枚目のLEDを直感で捨て、そのスタックで3枚目のLEDを(青)を出して砕く。霊薬をサーチ。サーチ後4枚目のLEDを唱える。

戦場:構築物、直感、LED　手札:霊薬　マナ:(青)×7

5. 霊薬を直感で捨て、そのスタックで4枚目のLEDを任意の色のマナを出して砕く。任意のほぞをサーチ。サーチ後青マナから霊薬を唱える。霊薬をそのまま青マナから起動。LED4枚と霊薬がライブラリーに戻る。

戦場:構築物、直感　手札:任意のほぞ　マナ:(青)(青)(青)(任意)(任意)(任意)

6. 0.に戻る。0.で捨てる（5.でサーチした）ほぞは構築物の効果で唱えられるため、無限サーチ無限マナ無限ライフが成立。デッキ内にほぞがなくなってしまう場合は1.で捨てるときに構築物の効果を適用しないことを選択すればOK（追放は任意）。1.のループ手順に切り替えるか《水蓮の花びら》、《オパールのモックス》をサーチして砕くorレジェンドルールで落とすことでも解決。《水蓮の花びら》2枚か《オパールのモックス》3枚を使えば1ループにつき4マナでるのでMOでのクリックも多少軽減されるかもしれない（誤差だと思うが。）。

 

デッキ内にLEDが3枚しかない場合でも第二のループの手順を利用すれば無限サーチ無限マナ無限ライフが可能である。他の条件は同じで手順は以下の通り。

 

LED3枚でのループ手順

(0.手札のアーティファクトを直感で捨てて、1枚目のLEDをサーチする。

戦場:構築物、直感　手札:LED他　マナ:(青)(青))

1. 1枚目のLEDを直感で捨てて2枚目のLEDをサーチ。このとき構築物の効果でそれを追放しておき、サーチ後すぐに唱える。

戦場:構築物、直感、LED　手札:LED他　マナ:(青)

2. 2枚目のLEDを直感で捨て、そのスタックで1枚目のLEDを(青)を出して砕く。3枚目のLEDをサーチ。サーチ後2枚目のLEDを唱える。

戦場:構築物、直感、LED　手札:LED　マナ:(青)(青)(青)

3. 3枚目のLEDを直感で捨て、そのスタックで2枚目のLEDを(青)を出して砕く。霊薬をサーチ。サーチ後3枚目のLEDを唱える。

戦場:構築物、直感、LED　手札:霊薬　マナ:(青)(青)(青)(青)(青)

4. 霊薬を直感で捨て、そのスタックで3枚目のLEDを任意の色マナを出して砕く。任意のほぞをサーチ。サーチ後青マナから霊薬を唱える。霊薬をそのまま3枚目のLEDから出した色マナで起動。LED3枚と霊薬がライブラリーに戻る。

戦場:構築物、直感　手札:任意のほぞ　マナ:(青)(青)(青)(任意)

5. 0.に戻る。0.で捨てる（5でサーチした）ほぞは構築物の効果で唱えられるため、無限サーチ無限マナ無限ライフが成立。

 

ほぞがライブラリー内に1枚しかなく、かつLEDが3枚の場合はさらに難解になります。

 

LEDが3枚かつほぞがライブラリー内と手札合わせて1枚の場合のループ手順

1. 1枚目のLEDを直感で捨てて2枚目のLEDをサーチ。このとき構築物の効果でそれを追放しておき、サーチ後すぐに唱える。

戦場:構築物、直感、LED　手札:LED他　マナ:(青)

2. 2枚目のLEDを直感で捨て、そのスタックで1枚目のLEDを(青)を出して砕く。3枚目のLEDをサーチ。サーチ後2枚目のLEDを唱える。

戦場:構築物、直感、LED　手札:LED　マナ:(青)(青)(青)

3. 3枚目のLEDを直感で捨て、そのスタックで2枚目のLEDを(青)を出して砕く。霊薬をサーチ。サーチ後3枚目のLEDを唱える。

戦場:構築物、直感、LED　手札:霊薬　マナ:(青)(青)(青)(青)(青)

4. 霊薬を直感で捨て、そのスタックで3枚目のLEDを任意の色マナを出して砕く。ほぞをサーチ。サーチ後青マナから霊薬を唱える。霊薬をそのまま3枚目のLEDから出した色マナで起動。LED3枚と霊薬がライブラリーに戻る。

戦場:構築物、直感　手札:ほぞ　マナ:(青)(青)(青)(任意)

5. ほぞを直感で捨てて、戻った1枚目のLEDをサーチする。このとき構築物の効果は使用しないで墓地に送る（0マナで唱えてそのまま墓地に行ける場合はそうしてもよいが）。

戦場:構築物、直感　手札:LED　マナ:(青)(青)(任意)

6. 1枚目のLEDを直感で捨てて2枚目のLEDをサーチ。このとき構築物の効果でそれを追放しておき、サーチ後すぐに唱える。

戦場:構築物、直感、LED　手札:LED　マナ:(青)(任意)

7. 2枚目のLEDを直感で捨て、そのスタックで1枚目のLEDを(青)を出して砕く。霊薬をサーチ。サーチ後2枚目のLEDを唱える。

戦場:構築物、直感、LED　手札:霊薬　マナ:(青)(青)(青)(任意)

8. 霊薬を直感で捨て、そのスタックで2枚目のLEDを(青)を出して砕く。3枚目のLEDをサーチ。サーチ後青マナから霊薬を唱える。

戦場:構築物、直感、霊薬　手札:LED　マナ:(青)(青)(青)(青)(任意)

9. 3枚目のLEDを直感で捨て、そのスタックで青マナから霊薬を起動してLED2枚と霊薬とほぞがライブラリーに戻る。ライブラリーに戻ったLEDの一枚をサーチ。サーチ後捨てたLEDを唱えると任意の色マナが1つ増えてライフが10点増えたことを除き1.の終了後と同じ状態に戻る。

戦場:構築物、直感、LED　手札:LED　マナ:(青)(任意)

10. 2.-9.を繰り返して無限マナ、無限ライフ発生。

 

なお手札にほぞがある場合は5.からループに入ることが出来ます。

 

対戦する側としてはLED2枚以下では無限マナは不可能であること、LED3枚での無限マナはライブラリー内に他のほぞが1枚以上必須なことを覚えておきましょう。

但し、LED2枚でも《水蓮の花びら》2枚か《オパールのモックス》3枚（ただし現在の戦場と《オパールのモックス》での金属術達成が条件。）がある場合、およびLED3枚かつ他のほぞがない場合でも無限ライフは成立します。

手順はそれぞれ下のようになっています。

 

LED2枚+《水蓮の花びら》2枚か《オパールのモックス》3枚での無限ライフループ

(0.手札のアーティファクトを直感で捨てて、1枚目のLEDをサーチする。

戦場:構築物、直感　手札:LED他　マナ:(青)(青))

1. 1枚目のLEDを直感で捨てて2枚目のLEDをサーチ。このとき構築物の効果でそれを追放しておき、サーチ後すぐに唱える。

戦場:構築物、直感、LED　手札:LED他　マナ:(青)

2. 2枚目のLEDを直感で捨て、そのスタックで1枚目のLEDを(青)を出して砕く。霊薬をサーチ。サーチ後2枚目のLEDを唱える。

戦場:構築物、直感、LED　手札:霊薬　マナ:(青)(青)(青)

3. 霊薬を直感で捨て、そのスタックで3枚目のLEDを(青)を出して砕く。《水蓮の花びら》か《オパールのモックス》をサーチ。サーチ後青マナから霊薬を唱え、そのまま起動。LED2枚と霊薬がライブラリーに戻る。

戦場:構築物、直感　手札:《水蓮の花びら》か《オパールのモックス》　マナ:(青)(青)

4. 《水蓮の花びら》か《オパールのモックス》を直感で捨て、ライブラリーに戻った1枚目のLEDをサーチ。その後捨てた《水蓮の花びら》か《オパールのモックス》を唱えてそのままそこから(青)を出す。

戦場:構築物、直感　手札:LED　マナ:(青)(青)

5. 1.に戻る。1.-4.を繰り返して無限ライフ。ここで《水蓮の花びら》の場合は2周目以降の3.で、1周前の4.で砕かれた《水蓮の花びら》がライブラリーに戻るので3周目以降のループが回り、《オパールのモックス》の場合は2周目以降の4.でレジェンドルールによって《オパールのモックス》が墓地に落ち、3周目以降の3.でそれが回収されるので4周目以降のループが回る。

 

LED3枚での無限ライフループ

1. 1枚目のLEDを直感で捨てて2枚目のLEDをサーチ。このとき構築物の効果でそれを追放しておき、サーチ後すぐに唱える。

戦場:構築物、直感、LED　手札:LED他　マナ:(青)

2. 2枚目のLEDを直感で捨て、そのスタックで1枚目のLEDを(青)を出して砕く。霊薬をサーチ。サーチ後2枚目のLEDを唱える。

戦場:構築物、直感、LED　手札:霊薬　マナ:(青)(青)(青)

3. 霊薬を直感で捨て、そのスタックで2枚目のLEDを(青)を出して砕く。3枚目のLEDをサーチ。サーチ後霊薬を青マナから唱える。

戦場:構築物、直感、霊薬　手札:LED　マナ:(青)(青)(青)(青)

4. 3枚目のLEDを直感で捨て、そのスタックで青マナから霊薬を起動してLED2枚と霊薬がライブラリーに戻る。山札に戻ったLEDの一枚をサーチ。サーチ後捨てたLEDを唱えるとライフが5点増えたことを除き1.の終了後と同じ状態に戻る。

戦場:構築物、直感、LED　手札:LED　マナ:(青)

 

なお、これらの無限ライフループも《大霊堂の信奉者/Disciple of the Vault》などがいれば当然キルループになります

 

これらのループの存在から《外科的摘出/Surgical Extraction》などでループパーツを根絶やしにできる場合を除き、ほぞやLEDを何枚か追放することでサーチが回らなくなることを期待するのは難しいです。

 

またLEDのデメリットで手札をディスカードするにもかかわらず、構築物の効果で護身を構えることが出来るのはうっかりしがちなので気を付けましょう。ただし手札自体はなくなっているため《意志の力/Force of Will》や《誤った指図/Misdirection》のような、いわゆるピッチスペルとはかみ合わない部分は弱点と言えるでしょう。

 

（おまけ:同じくMOパンダ様の配信の中で行われたモダンベルチャーのサブプラン、《紅蓮術士の昇天》を用いた無限ループのまとめ）

モダンベルチャーの《紅蓮術士の昇天》ループについて

前提

《小道の再交差/Recross the Paths》を唱えた際、ライブラリーに土地が一枚もない場合、完全にライブラリーの中を自由に積み込むことが出来る。最初から一枚も土地を採用しないベルチャーであれば《小道の再交差》は事実上(2)(緑)の完全なライブラリー操作呪文になる。

積み込みの順番

上から順に以下のように積む。

1. 《紅蓮術士の昇天/Piromancer Ascension》

2. 《魔力変/Manamorphose》

3. 《魔力変》

4. 《魔力変》

5. 《魔力変》

6. 《バーラ・ゲドの復活/Bala Ged Recovery》

7. 《捨て身の儀式/Desperate Ritual》

8. 《バーラ・ゲドの復活》

9. 《捨て身の儀式》

10.《一攫千金/Strike It Rich》

11. フィニッシャー

12以降. 任意

 

この中にまた手札（もしくは《紅蓮術士の昇天》の場合は場）に既にあるカードがある場合はその部分を省いて上に詰めてください。

また6.と7.は逆でもよく、9.-11.は順不同です。

コンボの条件

少なくとも次の二ターンの間(赤)含む2マナが出せる状態(2T目は緑でも可)で、《小道の再交差》を唱え、ライブラリーをこの順に積む。

コンボ手順

 

ループにつなぐまでの手順

1. 《小道の再交差》を唱えて積み込む。ドローとマナがあれば次に進む、なければここでターンを返す。

2. 《紅蓮術士の昇天》（以下昇天）を唱える。ドローとマナがあれば次に進む、なければここでターンを返す。

3. 《魔力変》を3連打する（連打するために出すマナは(赤)か(緑)を含むこと）。ここで3回目の《魔力変》で昇天が起動。

4. 4回目の《魔力変》を打つ。昇天によるコピーと合わせて《バーラ・ゲドの復活》（以下復活）と《捨て身の儀式》（以下捨て身）が手札に入る。マナは(赤)(赤)(緑)(緑)を出しておくとよいだろう。

手札:復活、捨て身　マナ:(赤)(赤)(緑)(緑)　墓地:《魔力変》×4

5. 赤マナから捨て身を唱える。コピーと合わせて(赤)6マナ生成。

手札:復活　マナ:(赤)×6(緑)(緑)　墓地:《魔力変》×4、捨て身

6. 復活を唱えてコピーと合わせて《魔力変》を二枚回収。そのまま連打。このときに(緑)を一つ以上残しておく。以下では簡単のため一つだけ残したとする。最終的に4枚引くので復活、捨て身、《一攫千金》、フィニッシャーを引くことになる。

手札:復活、捨て身、《一攫千金》、フィニッシャー　マナ:(赤)×8(緑)　墓地:《魔力変》×4、復活、捨て身

 

無限(赤)ループ

以下全てのループでは起動した状態の昇天が戦場にあるのを前提とする。また以下の全てのループは復活が手札と墓地に1枚づつあることが重要である。

(0. 手札は復活、捨て身×2、《一攫千金》+α、墓地は復活+αからスタートする。初動必要マナは(2)(赤)(赤)である。また必要な手札が墓地にある場合は、復活でコピーと合わせて墓地の復活とその必要なカードを回収することで、(緑)含む3マナにつき1枚必要札を回収できる。上の手順からこのループに突入する場合はまず(赤)(赤)(緑)から捨て身を上記の手段で回収する。すると(赤)×6が残るため、ループに突入できることがわかる。この回収の手法は他のループでも使える。

手札:復活、捨て身×2、《一攫千金》　マナ:(2)(赤)(赤)　墓地:復活)

1. 赤マナと不特定マナから1枚目の捨て身に2枚目を連繋して唱える。コピーと合わせて(赤)12マナが生成。

手札:復活、捨て身、《一攫千金》　マナ:(赤)×12　墓地:復活、捨て身

2. 《一攫千金》を唱える。コピーと合わせて宝物が2個生成。

手札:復活、捨て身　マナ:(赤)×11、宝物×2　墓地:復活、捨て身、《一攫千金》

3. 宝物から(緑)を出して復活を唱える。コピーと合わせて墓地の復活と捨て身を回収。

手札:復活、捨て身×2　マナ:(赤)×9、宝物×1　墓地:復活、《一攫千金》

4. 宝物から(緑)を出して復活を唱える。コピーと合わせて墓地の復活と《一攫千金》を回収。3.と4.は逆でも可。不特定マナが(赤)に変わり、(赤)が3つ増えた以外は1.開始前に戻ったので1.-4.を繰り返して(赤)の無限マナ。

手札:復活、捨て身×2、《一攫千金》　マナ:(赤)×7　墓地:復活

 

無限宝物ループ

上記で無限(赤)、無限ストームであるため、大抵勝利できるがターンを返さなくてはならないフィニッシャー（《巣穴からの総出/Empty the Warrens》など）を用いる場合などは相手ターンに対抗手段を構えるなどの理由からこのルート及び次の無限ドローループも知っておくとよい。

(0. 手札は復活、《一攫千金》+α、墓地は復活+αからスタートする。事前に赤の無限マナが出ている状態からスタートする。

手札:復活、《一攫千金》　マナ:(赤)×∞　墓地:復活)

1. 《一攫千金》を唱える。コピーと合わせて宝物が2個生成。

手札:復活　マナ:(赤)×(∞-1)、宝物×2　墓地:復活、《一攫千金》

2. 宝物から(緑)を出して復活を唱える。コピーと合わせて墓地の復活と《一攫千金》を回収。

手札:復活、《一攫千金》　マナ:(赤)×(∞-3)、宝物×1　墓地:復活

3. 1.-2.を繰り返すと(赤)(赤)(赤)が宝物1つに変わることを何度でも行える。

 

無限ドローマナ増幅ループ

１枚ではフィニッシュできないフィニッシャーを用いる場合や、防御手段が必要な場合はこちらを使うことになる。ライブラリーが切れかかったら無限マナループに切り替えることも可能である。なお、無限(赤)ループを経由せずにこちらからループに入るには、まず「ループにつなぐ手順」で最後に出すマナを(赤)×7(緑)(緑)にしておき、無限(赤)ループの手順同様、最初に復活で拾った儀式を連繋で打ってから、復活で復活と魔力変を拾って2.からループに入ればよい。

(0. 手札は復活、捨て身×2、《魔力変》+α、墓地は復活+αからスタートする。初動必要マナは(2)(赤)(赤)である。。

手札:復活、捨て身×2、《魔力変》　マナ:(2)(赤)(赤)　墓地:復活)

1. 赤マナと不特定マナから1枚目の捨て身に2枚目を連繋して唱える。コピーと合わせて(赤)12マナが生成。

手札:復活、捨て身、《魔力変》　マナ:(赤)×12（上記の手順で2.からループに入る場合は11）　墓地:復活、捨て身

2. 《魔力変》を唱える。コピーと合わせて2枚引きつつ、出すマナは(任意)(任意)(緑)(緑)である。

手札:復活、捨て身　マナ:(赤)×9か10 (緑)(緑)(任意)(任意)　墓地:復活、捨て身、《魔力変》

3. (赤)(赤)(緑)から復活を唱える。コピーと合わせて墓地の復活と捨て身を回収。

手札:復活、捨て身×2　マナ:(赤)×7か8 (緑)(任意)(任意)　墓地:復活、《魔力変》

4. (赤)(赤)(緑)から復活を唱える。コピーと合わせて墓地の復活と《魔力変》を回収。3.と4.は逆でも可。これで2枚引いて不特定マナが任意の色マナに変わり、(赤)が4つ増えたこと以外は1.の直前と同状態に戻ったため、以降は繰り返して無限ドロー。ただし、偶数枚の無限ドローの為、最後の1枚が引けない可能性があることに注意。

手札:復活、捨て身×2、《魔力変》　マナ:(赤)×5か6 (任意)(任意)　墓地:復活

 

対戦する側で知っておくべきことは（すでに昇天にカウンターが置かれている場合や対戦相手の手札とマナベースが潤沢な場合を除き）、《魔力変》が4枚全てライブラリーに必要なこと、全ての《一攫千金》がフラッシュバックなどで墓地にすらない場合、最後に紹介した無限ドローマナ増幅ループによるライブラリー枚数に依存したマナ数しか出せないことです。

 

以上になります。長文にお付き合いいただきありがとうございました。

 

間違いやご質問がありましたらtwitter:@sanjtsu_yuまでよろしくお願いいたします。

ラムダ計算でコーディング

どうもAaronです。

今回はみんな大好きラムダ計算です。

早速行ってみよう！

1. 計算モデルについて

今回の記事中この章のみラムダ計算に関する話題ではなく、理論計算機科学で使われる計算モデルという概念についてになっています。若干連続性に欠けますが、僕は何か話をするとき、それがどんな理論に位置づけられるのかとか、別の理論での対応物は何かという話を最初にするのが好きなので今回もそういうことにします。

1.1 計算モデル

ラムダ計算は一般に計算モデルの一つとして多くの論理学や計算理論の教科書に登場します。

では計算モデルというのは何かという事になりますが、これは物理的な実装やその他外部状況に影響されない計算機や計算手順、アルゴリズムなどを記述する数理モデルのことを言います。少し比喩的に言ってしまえば非常に理想化されたプログラム言語の仕様のようなものだと思ってもよいです。

しかしここで問題なのが計算モデルという言葉は恐らく形式的に定義される語ではないということです。少なくとも僕の知っている講義・資料・和文英文Wikipediaなどから形式的な定義と呼べるものは見つけられませんでした（もし「あるよ」って方がいたら教えてください）。

これがなぜかというと多くの計算モデルは

  1. ある決まった種類の対象から同じ種類の対象への関数、またはその対象に関する述語を、
  2. あらかじめ定められた、直感的に言って人間、あるいは既存のコンピュータが容易に行えそうないくつかの操作の、
  3. 一定の形式の組み合わせ（関数としてみるなら合成）や繰り返し（いわゆる再帰）によって定義する定義方法の枠組みである。

という程度の共通点を持っていますが、

1.に関して、そもそもその「同じ種類の対象」（計算モデルの上で定義される関数の定義域）は計算モデルごとに全く異なります。比較的有名なところでいえば

  • Turing機械ならば、任意の長さの（典型的には）\{0,1\}が刻まれたテープ。
  • 今回扱うラムダ計算ならば、ラムダ項と呼ばれるある種類の項。
  • （計算モデルかは怪しいが）Kleeneの公理化された再帰関数なら自然数。
  • （有限型、プッシュダウン、線形拘束…）オートマトンでは固定された文字からなる文字列。

等見事にバラバラです。

2.や3.に関してもそもそも定義域が決まっていない状況で、「（その定義域上の対象に対する）直感的に人間や既存のコンピュータが容易に行えそうな操作」や、「その合成や再帰の一定の形式」を特徴づけるのはやはり無理があるようです。

このような理由から計算モデルという言葉自体の定義は難しく、割とふわっとつかわれるようです。

一方で計算モデルの具体的な例はこの世に数えきれないほどあげる（or 作る）ことができます。というのも上で上げたものの他、殆どのプログラミング言語はある程度の修正や抽象化の元に計算モデルと思うことができるし、既に知られた計算モデルに記号を追加するなどしたマイナーチェンジ版も無数に作ることができるからです。

そこで我々は何が計算モデルなのかを議論するより、与えられた二つの計算モデルの間の関係を定義して議論した方が実りがあります。計算モデル全体が上手く定義できずとも、二つの計算モデルが与えられたときにそれらを「比較」することができるからです。

次の節ではそれを行うことにします。

1.2 解釈可能性、エミュレート可能性

前節でお話しした通り、計算モデルによる関数定義の仕方自体に共通の特徴を洗い出すのは難しいので、ここでは計算モデルの枠組みで定義された関数や述語とその定義域を用いて、三個組

A=(C_A,F_A,P_A)

(ただし
\displaystyle F_A\subset\bigcup_n Map(\underbrace{C_A\times C_A\times\cdots\times C_A}_{n-times},C_A\cup\{\uparrow\})\\P_A\subset\bigcup_n Map(\underbrace{C_A\times C_A\times\cdots\times C_A}_{n-times},\{true,false,\uparrow\})
を満たす。）
をして計算モデルと呼ぶことにします。ここで唐突に出てきた記号\uparrowは直感的にはプログラムが無限ループを引き起こすことを表し、普通の文脈で出てくる関数や述語に比べて無限ループを起こす可能性がある分だけある意味拡張された概念になっています。

ここでちょっとした問題があり、計算モデル上の関数や述語は、例え関数、述語として外延的に等しくても*1、定義の仕方（プログラムでいう実装やアルゴリズム）の違いにも着目することが自然であるため、F_A,P_A上の等号は集合論的なそれとは違うと考えないとうまくいかないことがあり*2、どう定義したものか悩ましいのです。その意味で上の\displaystyle\bigcup_n Map(\underbrace{C_A\times C_A\times\cdots\times C_A}_{n\ times},C_A\cup\{\uparrow\}) や\displaystyle\bigcup_n Map(\underbrace{C_A\times C_A\times\cdots\times C_A}_{n\ times},\{true,false,\uparrow\})の部分集合というのは非厳密な言い方ですし、正式にどう定義するかは難しいのですが、正直に白状すればこの記事は全体を通して、割とその点を誤魔化しています。

またここで用いた定義ではF_AとP_Aを分けていますが、この辺の区別も計算モデルによるところが大きく、一般に「～オートマトン」と呼ばれるような種類の多くの計算モデルは定義に受理状態と拒否状態を含むことで述語を陽に扱いますし、多くのプログラム言語を計算モデルとみた場合ならばAの中にプリミティブなBool値（の対応物）を持っているでしょうからそれで表現するかもしれませんし、Kleeneの再帰関数や今回扱うラムダ計算では陽に述語を扱う機構もプリミティブなBool値も持たないため体系内の特定の値をBool値のコードとして用います（体系内にプリミティブなBool値やBool値のコーディングを持つ計算モデルではF_A\supset P_Aと見做せることになります。）。

さて補足と脱線で長くなりました。そろそろ本題に入りましょう。

A=(C_A, F_A, P_A), B=(C_B, F_B, P_B)をそれぞれ計算モデルとしたとき、ある関数の三個組\mathcal{I}=({}^{I_C}:C_A\cup\{\uparrow\}\to C_B\cup\{\uparrow\},\ {}^{I_F}:F_A\to F_B,\ {}^{I_P}:P_A\to P_B)が

\forall a\in C_A\cup\{\uparrow\}.a^{I_C}=\uparrow\iff a=\uparrow

\forall a,b\in C_A.a^{I_C}=b^{I_C}\Rightarrow a=b

\forall \vec{a}=(a_0,\ a_1,...,\ a_{n-1})\in \underbrace{C_A\times C_A\times\cdots\times C_A}_{n\ times},\ f\in F_A.f^{I_F}(\vec{a}^{I_C})=(f(\vec{a}))^{I_C}

\forall \vec{a}=(a_0,\ a_1,...,\ a_{n-1})\in \underbrace{C_A\times C_A\times\cdots\times C_A}_{n\ times},\ p\in P_A.p^{I_P}(\vec{a}^{I_C})\iff p(\vec{a})

(但しここで\vec{a}=(a_0,\ a_1,...,\ a_{n-1})\in \underbrace{C_A\times C_A\times\cdots\times C_A}_{n\ times}に対して\vec{a}^{I_C}=(a_0^{I_C},\ a_1^{I_C},...,\ a_{n-1}^{I_C})とする。)

を満たすとき\mathcal{I}をAのBでの解釈と呼び、そのような\mathcal{I}が存在するとき、AはBで解釈可能であるという事にします。

更にもう一歩進めて今度は五個組

\mathcal{E}=(\varphi_F,\varphi_P,\ {}^{E_C}:C_A\cup\{\uparrow\}\to C_B\cup\{\uparrow\},\ {}^{E_F}:F_A\to C_B,\ {}^{E_P}:P_A\to C_B)

（\varphi_F,\varphi_PはそれぞれF_B,P_Bに属する関数、述語の列でその第n項を\varphi_{F,n},\varphi_{P,n}と書けば、

\varphi_{F,n}\in F_B\cap Map(\underbrace{C_B\times C_B\times\cdots\times C_B}_{n+1\ times},C_B\cup\{\uparrow\})\\\varphi_{P,n}\in P_B\cap Map(\underbrace{C_B\times C_B\times\cdots\times C_B}_{n+1\ times},\{True,False,\uparrow\})

を満たす。但し

F_A\cap Map(\underbrace{C_A\times C_A\times\cdots\times C_A}_{n\ times},C_B\cup\{\uparrow\})=\emptyset

の時に限り、\varphi_{F,n}=undefinedとなることを許す。\varphi_{P,n}についても同様。）

が

 \forall a\in C_A\cup\{\uparrow\}.a^{E_C}=\uparrow\iff a=\uparrow

\forall a,b\in C_A.a^{E_C}=b^{E_C}\Rightarrow a=b

\forall \vec{a}=(a_0,\ a_1,...,\ a_{n-1})\in \underbrace{C_A\times C_A\times\cdots\times C_A}_{n\ times},\ f\in F_A.\varphi_{F,n}(f^{E_F},\vec{a}^{E_C})=(f(\vec{a}))^{E_C}

\forall \vec{a}=(a_0,\ a_1,...,\ a_{n-1})\in \underbrace{C_A\times C_A\times\cdots\times C_A}_{n\ times},\ p\in P_A.\varphi_{P,n}(p^{E_P},\vec{a}^{E_C})\iff p(\vec{a})

を満たすならば、\mathcal{E}をAのBでのエミュレータと呼び、そのような\mathcal{E}が存在するとき、AはBの中でエミュレート可能という事にします。実際に特定のAを固定して考えるときは、より多くの条件を課したエミュレータを考えるのが自然です。例えばAが関数合成や部分適用に閉じているならば、それらによって得られる関数fのf^{E_F}がBの中でもととなる関数や値から計算できることを要求したり、Aが帰納的に関数を定めるような系であるなら各インダクティブステップに対応する変換がBの中で計算可能であることを要求するのは自然でしょう。

容易にわかるように計算モデルが部分適用に閉じている（即ち

f(x_0,...x_{n-1})\in F_B\to\forall c\in B.\forall m\lt n.f(x_0,...x_{m-1},c,x_{m+1},...,x_{n-1})\in F_B\\p(x_0,...x_{n-1})\in P_B\to\forall c\in B.\forall m\lt n.p(x_0,...x_{m-1},c,x_{m+1},...,x_{n-1})\in P_B

を満たす）限りエミュレート可能性は解釈可能性よりも強い条件です。

解釈とエミュレートの関係は、言語間のトランスパイルと一方の言語を他方の言語で作られたヴァーチャルマシン上で実行することとの関係とほぼ同じなのです。

特にある計算モデルは自分自身を自明な方法で解釈できますが、エミュレートできるかどうかは相当非自明であることに注意してください。すなわち、ほかの言語をエミュレートするためにはまず自分自身がヴァーチャルマシンを構築するのに足りるだけの強さを持たなくてはならないのです。次の節ではこの事実が主要な役割を果たします。

1.3 Church-Turingの提唱

前節で定義された解釈可能性やエミュレート可能性によって知られている計算モデル同士を比較すると興味深いことがわかります。

実は「自然な」計算モデルのうち、かなりの大部分は互いに互いをエミュレート可能であり*3、残りはその大部分の計算モデルによってエミュレートされるが、逆にそれのクラスを解釈することはできないという意味でより弱いものであることがわかっているのです。言い換えると自然な計算モデル（≒人間にできる計算）に対して、既に性能の限界が経験的に知られており、それより真に弱いものを作ることはできても、強いものを作ることはできないとされているのです。「経験的に」というのは重要で、再三繰り返すように計算モデル自体には明確な定義がないので、これは何らかの数学的事実では（今のところ）ないのです。

この（繰り返すようにあくまで経験的な）事実に基づいてその「大部分のクラス」の計算モデルによって定義できる関数を計算可能関数と呼ぼう、と提唱したのがChurchとTuringで（実はこのあたり歴史的には結構ややこしいのですが）、この提唱による計算可能関数の「定義」をChurch-Turingの提唱と呼んでいます。

さて、実は先ほどから急に主役を張り出したこの「大部分の計算モデルのクラス」にはTuring完全クラスという名前がついています。このTuring完全クラスには以下のような特徴づけで定義することができます。

Def.1.3.1 (Turing完全)

\text{計算モデル}A\text{がTuring完全}\iff\text{Turing機械と}A\text{は、}I_C\text{が互いに逆関数となるような解釈で相互に解釈可能}

 「Turing機械」のところは単なる基準なので、お好きなTuring完全性がメタ的に既知である計算モデルに変更できます（定食屋さんのメニューに書いてある「セットの麺物は以下からお好きな物に変更できます」のイントネーションでお読みください）。


この条件を満たすクラスが節の冒頭で言った通り相互にエミュレート（解釈よりも強いに注意）できるのは以下のように証明できます。

Prop.1.3.2 Turing機械は自身をE_C=idであるようなエミュレータでエミュレート可能。

証明)略（Turing機械で実際にプログラムを書くことになる。難しくはないが非常に時間と紙幅がかかる。）。

Cor.1.3.3 AがTuring機械で解釈可能ならば、Turing機械でエミュレート可能。

証明)上の命題からTuring機械上の自身のエミュレータ

\mathcal{E}=(\varphi_F,\ \varphi_P,\ id,\ {}^{E_F},\ {}^{E_P})

がとれる。

また仮定からAのTuring機械上での解釈

\mathcal{I}=({}^{I_C},\ {}^{I_F},\ {}^{I_P})

が取れる。

そこで\mathcal{E}'=(\varphi_F,\ \varphi_P,{}^{I_C},\ {}^{E_F}\circ{}^{I_F},\ {}^{E_P}\circ{}^{I_P})

とするとこれはTuring機械上でのAのエミュレータである。

実際

\varphi_{F,n}( (f^{I_F})^{E_F},\vec{x}^{I_C})=f^{I_F}(\vec{x}^{I_C})=f(\vec{x})^{I_C}

\varphi_{P,n}( (p^{I_P})^{E_P},\vec{x}^{I_C})\iff p^{I_P}(\vec{x}^{I_C})\iff p(\vec{x})

Lem.1.3.4 AがTuring機械と、I_Cが互いに逆関数となるような解釈によって相互に解釈可能ならば、AはE_C=idであるようなエミュレータで自身をエミュレート可能。

Turing機械上でのAの解釈を

\mathcal{I}=({}^{I_C},\ {}^{I_F},\ {}^{I_P})、

A上でのTuring機械の解釈を

\mathcal{I}'=({}^{I_C^{-1}},\ {}^{I'_F},\ {}^{I'_P})、

Turing機械の自己エミュレータを

\mathcal{E}=(\varphi_F,\ \varphi_P,\ id,\ {}^{E_F},\ {}^{E_P})

とすると、
\mathcal{E}'=(\varphi_F^{I'_F},\ \varphi_P^{I'_P},id,\ {}^{I_C^{-1}}\circ{}^{E_F}\circ{}^{I_F},\ {}^{I_C^{-1}}\circ{}^{E_P}\circ{}^{I_P})

はAの自己エミュレータである。

実際

\varphi_{F,n}^{I'_F}( ( (f^{I_F})^{E_F})^{I_C^{-1}},\vec{x})\\(=\varphi_{F,n}^{I'_F}( ( (f^{I_F})^{E_F})^{I_C^{-1}},(\vec{x}^{I_C})^{I_C^{-1}}))\\=(\varphi_{F,n}( (f^{I_F})^{E_F},\vec{x}^{I_C}))^{I_C^{-1}}\\=(f^{I_F}(\vec{x}^{I_C}))^{I_C^{-1}}\\=(f(\vec{x})^{I_C})^{I_C^{-1}}=f(\vec{x})

\varphi_{P,n}^{I'_P}( ( (f^{I_P})^{E_P})^{I_C^{-1}},\vec{x})\\(\iff\varphi_{P,n}^{I'_P}( ( (p^{I_P})^{E_P})^{I_C^{-1}},(\vec{x}^{I_C})^{I_C^{-1}}))\\\iff \varphi_{P,n}( (p^{I_P})^{E_P},\vec{x}^{I_C})\\\iff p^{I_P}(\vec{x}^{I_C})\iff p(\vec{x})

Lem.1.3.5 AがBで解釈可能で、BがCでエミュレート可能ならばAはCでエミュレート可能。

証明)Cor.1.3.4を用いれば、Cor.1.3.3とほとんど同様の証明に帰着する。

Thm.1.3.6 A,BがTuring完全なら相互にエミュレート可能。

証明)1.3.2-1.3.5から直ちに従う。

 
結果であるThm.1.3.6は勿論ですが、Lem1.3.4やLem1.3.5も極めて重要な性質です。特にLem.1.3.4の性質はTuring完全な計算モデルの際立った特徴だと言われます。

またLem.1.3.5からわかるように自分自身をエミュレートできる体系AでBが解釈できるなら、実際にはBはAでエミュレートもできるのでエミュレート可能性と解釈可能性の違いに注目するべきなのはTuring完全よりも能力の小さい計算モデルを研究するときに限られます。

さて、今回扱うラムダ計算もTuring完全であることが知られています。

従ってラムダ計算でのコーディング手法を知れば全ての計算可能な関数を理論上は定義することができるわけです。

2. ラムダ計算

2.1 構文とその直感的意味

ラムダ計算のオリジナル版はChurchによって導入されました。その後現在に至るまで、多くの拡張や亜種が定義されたり、これから紹介する「λ抽象」と呼ばれる独特な関数定義のノーテーションが便利な記法として（ある意味ではここで紹介するような理論的なラムダ計算の議論とはほとんど独立に）使われたり*4してきましたが、その中でもオリジナル版のラムダ計算は極端なまでに簡潔な文法を持ちます。なんと構文はたった三種類しかないのです。すなわちBNFで書けば

<lambda term>=
<variable>
| "("<lambda term><lambda term>")"
| "(""λ"<variable>"."<lambda term>")"

となります。ただしここで<variable>と書いているのは「プリミティブな記号」の意味で、普通は可算無限個用意されていると考えます。ほかの用途で使う"λ"や"."や"(",")"はここに含まれてはいけません。

次に上で定義される構文の直感的意味を説明しますが、その前に一つ重要な注意として、ラムダ計算においては、全ての項や変数は「（高階）関数」であるとみなされ（得）ることを指摘しておきます。誤解を恐れず言えば、「自然数」とか「実数」といった「それ以上分解できない値」という概念が存在せず、定義された値は全て関数として（も）見られるのです。その為、前章で使ったノーテーションで言えばC_Aがラムダ項の（この記事のかなり後のほうで見るある条件を満たす）集合になっていて、C_A\subset F_A\supset P_Aという構図になります。これを念頭に次を読んでください。

上で上げた各構文は左から順にそれぞれ「原子項」、「関数適用」、「λ抽象」と呼ばれることがあります。これが各構文の直感的意味を表していて、

  1. 原子項は、変数一個のみによる構文がラムダ項であること
  2. 関数適用はそのまま、前者のラムダ項を関数とみて、後者のラムダ項をその引数に与えるという構文が新たな項を与えること

をそれぞれ意味します。ラムダ計算の文脈では関数に引数を与えることに括弧を使わない慣例があることを知っておいてください。（e.g.fにxを引数として与えるときはfxのように書く。f(x)とはしない。）

λ抽象はややとっつきにくい概念です。まず次の例を見てみてください。

f(x)=x^2

だれしもが高校生のころ、こんな式を見たことがあると思います。ここで「xが関数の仮引数を意味する」というのを左辺のxが表しているわけです。

f(2)=4

のように書くことと比較すれば、これは一種のパターンマッチングによる定義だという事もできます。

更に別の言い方をすれば、パターンマッチによって変数xが「fの仮引数」という意味を込めて「抽象化（つまりある決められた値のためのプレースホルダーでなく、あらゆる値が入りうる仮引数として働くことを明示）」されているわけです。fと常にともにあるというニュアンスで「束縛」と呼ぶ人もいます。

ラムダ計算では変数の抽象化（≒関数定義）にこの種のパターンマッチを用いるのではなく\lambda x.T（Tはラムダ項）のように書きます。これでラムダ項Tを関数と見て、xが仮引数として働く、という意味になります。例えば\lambda x.xはラムダ項であり、それが意味するところはxを受け取って、xを返す関数、即ち恒等関数になるわけです。そして\lambda x.の後に出てきたxはこの関数の仮引数として「抽象化」されているわけですが、ここでのxのように抽象化された変数を「束縛変数」、そうでない変数を「自由変数」とよびます。


いくつか合法なラムダ項の例をのせてこの節を終わりましょう。

x

(xy)

( (xy)z)

(\lambda x.x)

(\lambda z.(xy) )

( ( (\lambda z.(xy) )z)x)

2.1.1 略記

前節の最後の例でわかる通り、ラムダ項を完全に構文的に正しく書くのは大変な手間です*5。
そこで標準的には以下の四つの略記を用います。

  • 最外の項およびλ抽象の直後の項の括弧は省いてよい。

(e.g.(xy)\to xy,\lambda x.(xy)\to\lambda x.xy)

  • 関数適用が連続するときに括弧を省いたなら、それは左結合だったものと読む。

(e.g.( (xy)z)\to xyz,(x(yz) )\not\to xyz)

  • 反復適用に関する略記、\underbrace{T(T(\dots(T}_{n\text{-}times\ T}U)\dots)\to T^nU。特に勝手なTに対してU\to T^0U。
  • 連続したλ抽象があるなら、最初以外のλ(と括弧)を省略してよい。

e.g)(\lambda x.(\lambda y.(\lambda z.( (xy)z) ) ) )\to\lambda x.y.z.xyz

これらの省略法のうち、一番目と二番目は文字通りの意味で略記/省略ですが、三番目と四番目は意味づけの上で自然になるような工夫でもあります。

三番目の略記はラムダ計算が扱うオブジェクトが関数で、関数適用が「前者の項に後者の項を適用する」という意味であったことを思い出せば、

\underbrace{f(f(\dots(f}_{n\text{-}times\ f}(x))\dots)

を

f^n(x)

と略記するのと同じノリであることがわかります。

最後の略記は実は極めて重要な考え方を示唆していますので、それを次節で説明しましょう。

2.1.2 Curry化された多変数関数

ここまで一通りラムダ計算の定義を読んできた中で、もしかしたらこんな風に疑問に思われた方がいるかもしれません。

「λ抽象の構文は<variable>を一つしかとらなくていいの<variable>+じゃないの？多変数関数表現できなくない？」

と。

答えは「とらなくていいし、この条件でも多変数関数を表現する方法はある」のです。

これを説明するために、まずラムダ計算の事はいったんこちらにおいて一般的な集合論を考えてみます。

集合論でMap(X,Y)をY^Xと書くことがあります。

ここでちょっとしたメタ読みをしてみましょう。なぜ指数の形の記号を使うのでしょう？答えは簡単で指数法則を（ある意味で）満たすからなのです。

すなわち

  1. X^{Y_1\sqcup Y_2}\simeq X^{Y_1}\times X^{Y_2}
  2. X^{(Y_1\times Y_2)}\simeq(X^{Y_1})^{Y_2}

が成り立つのです。ここでA\simeq BはA,B間にいい感じの全単射が生えることを意味しています。いい感じってなんやねんという話ですが、多分両辺をXに関する自己関手と見た時、自然同型とかで定式化できそうですが圏論弱者なのでわからないです…。単なる全単射よりは条件が必要なことを主張している自覚があるのでとりあえず「いい感じ」としておきます。

ここでそのいい感じの全単射は明確に構成出来て、

1.に対応する全単射は

split:X^{Y_1\sqcup Y_2}\to X^{Y_1}\times X^{Y_2}\\ split(f)=(f|_{Y_1},f|_{Y_2})

2.に対応するのは

curry:X^{(Y_1\times Y_2)}\to(X^{Y_1})^{Y_2}\\curry(f)=g:a\mapsto (h:b\mapsto f(a,b))

となります。

さて、2のほうを見て、なぜ突然集合論の話をし始めたか、お判りいただけたでしょうか？ここのcurryによって、多変数関数（\iff多変数を「同時に」受け取る関数\iffなんらかの直積集合からの関数）が、同じ数の変数を「順次に」受け取っていく一変数（関数値）関数と同型になっているのです。これが一変数関数しか定義できない状況で多変数関数を表現する、Curry化と呼ばれる手法です。


さてここで前節の第四の略記を見てみましょう。実はこの略記はCurry化によって表現された疑似的な多変数関数を、多変数関数らしく書くための略記なのです。

実際前節で挙げた例を見ると、略記にする前の形は一変数を受け取って一変数関数を返す関数値関数ですし、略記の形は\lambda (x.y.z).xyzと隠れた括弧が入ると思えば多変数関数らしく見えませんか？

また構文上は一変数関数のみを扱い、Curry化によって多変数関数を表現する方法は、単に構文の定義を簡潔にできるというだけでなく、実効的な意味で、プリミティブに多変数関数を許す方法よりも優れている面もあります。

例えばプリミティブに多変数関数を許している方式で

f(x,y)=x+y

と定義したとします。この時特にx=1とした関数を扱いたい場合、基本的には関数を再定義するしかありません。

しかしCurry化による表現方針ではf\ 1と書いてそのような関数を表現する「部分適用」が可能なのです。これは「引数を『順次に』受け取っている」からに他なりません。

このようにCurry化というのは関数をプリミティブに扱う文脈では非常に優れた表現方針なのです。実際、非常に理論的なモデルであるラムダ計算だけにとどまらず、それをベースとした実用的な言語であるHaskellも、プリミティブな多変数関数を持たずCurry化による表現を行っていることからも、その有効性が知れるでしょう。

2.2 代入

さて突然ですが、何か変数的な概念が出てきたとき、最初に考えることは何でしょう？

そう「代入」ですね。ラムダ計算においても原子項は変数でしたから当然代入を考えたくなります。

ラムダ項Sをラムダ項Tの自由変数xに代入すること（この操作および結果として得られる項を記号でT[x\leftarrow S]と書きます）は直感的にT中の自由変数xをSに置き換えるだけで8割方良いのですが、二つだけ注意すべきことがあります（厳密な定義は僕の気が向いたら注釈に書きます。*6）。

第一の注意は代入によって束縛変数は置き換えられないということです。これはプログラム言語でいう変数のシャドーイングのような状況で問題になり、こう定義することで安全にシャドーイングされた状態になります。

第二の注意が「代入によるアブストラクタの新たな変数の捕捉」などと呼ばれる問題です。こちらを例を使って説明しましょう。

まずxyというラムダ項を考えると、これは原始項二つによる関数適用の形のラムダ項でx,yはともに自由変数です。もうひとつ\lambda x.xzというラムダ項を考えます。今度のxは束縛変数で関数の仮引数です。ここまでは良いでしょう。ではここで第二のラムダ項のzに第一のラムダ項を代入することを考えると結果はどうなるでしょうか？

\lambda x.x(xy)でしょうか？そうだとするとこんな違和感があります。\lambda x.x(xy)のxはどちらも全体を関数として見てその仮引数ですから、自由変数がいつの間にか束縛変数に化けているのです。すなわち代入によって\lambda（アブストラクタ）がもともと自由だったxを「捉え」て、束縛変数にしてしまっているのです。これは意味論上問題を引き起こします。

この問題の解決策は実は著者によって異なります。一致しているのは、直接代入すると新たに変数を「捕捉」してしまうλの仮引数名を、本質的にはすぐ後で説明するα変換によって「捕捉」しない仮引数名に入れ替えるという事なのですが、このケースでの代入自体の定義は人によって異なり

  1. そのようなケースでの代入の定義の中でα変換（やそれに対応する代入）を使ってしまい、再帰的定義とする人
  2. そのようなケースでは代入が「失敗する」、すなわち「結果がない」としておき、そのようなケースの発生自体をα変換を使って回避する人
  3. そのようなケースでも先に挙げたような違和感を押し殺して素直に機械的に置き換えることにしておき、そのようなケースの発生自体をα変換を使って回避する人

等がいます。この記事ではどれでもいいとしておきます。ただこの問題があることだけを認識しておいてくれればいいのです。

2.3 α変換

さて今度は急に哲学的な問いになりますが、「計算」とは何でしょうか？

様々な答えはあり得るでしょうが、一応現時点での僕の答えは


「ある対象をある意味で『同じ』であると言えるような、それでいてやはり何らかの意味で『より簡潔な』形へと変換する行為やその繰り返し」


という事になります。

例えば2+3=5という式を書いて「計算をした」と主張するとき、人は2+3と5がある意味で同じであるにもかかわらず5のほうが簡潔であると考える故にそうするわけです。

「ある意味で『同じ』であると言える」というのは数学でいえば「ある同値関係で同値」という事になるでしょうから、最初に与えられた『ある対象』と同値な同値類のうち、何らかの意味で『より簡潔な』代表元をとると言い換えることができそうです。

この見地に立つとラムダ計算には重要な二つの同値関係が定義されています。それが今節と次節で扱う「α同値」と「β同値」です*7。「α変換」や「β変換」という言い方をした場合はこれらの同値関係にある者同士での変換、言い換えれば代表元の取り換えを意味します。

さてではα同値の定義を見てみましょう。二つの項がα同値である（t\equiv_\alpha sと書くことにする）は以下のように定義されます。

\lambda x.T\equiv_\alpha \lambda y.T[x\leftarrow y]\text{(但しここで}y\text{は}T\text{に自由変数としては現れない)}\\T\equiv_\alpha S\land U\equiv_\alpha V \Rightarrow TU\equiv_\alpha SV\\T\equiv_\alpha S\Rightarrow\lambda x.T\equiv_\alpha\lambda x.S

論理式でややこしいので直感的に言ってしまえば、これは単に関数の仮引数名の付け替えです。「関数の仮引数名を付け替えても『意味』が同じ」というのは聞いたことがある方も多いでしょうし、納得もしやすいでしょう。

しかし名前の付け替えではどちらが簡単とは言えないと思った方もいらっしゃるでしょう。それはごもっともな指摘で、実はラムダ計算において上記の意味で「真に」計算をしていると言えるのは実は次の節で説明するβ変換のみだとも考えられます。すなわち「α変換」はあまり表舞台に出てこないのです。それでもα変換をここで紹介するのには二つの意味があります。

第一には、前節で匂わせた通りラムダ計算においての代入の定義はα変換と本質的に一種の相互依存関係を持っており、そしてβ変換では代入が核心的な役割を果たすためにα変換が必要なのです*8。ここでは前節でご紹介した「そのまま代入すると『新たな変数の捕捉』が起きるような代入」を回避できるように仮引数名を付け替えた形を、「より簡潔な形」と定義したと思っていただければよいかと思います。

第二には、やはりβ変換の定義と関係してしまうのですが、これ以降では特に計算の結果得られた項の、α同値な違いをほとんど無視します。そのため「α変換」はあまり表舞台に出てこなくても、「α同値（で割ること）」は本質的に重要な役割を果たすのです。

これら二つの事から、α同値はやはり詳しく述べる必要があると考えてここに置いた次第です。

2.4 β変換

さていよいよこの話がやってきました。β変換です！前節でも少し言ったようにβ変換はほとんどラムダ計算という計算モデルの「計算」部分を一手に担っているといっても過言ではないほど重要なものです。そのため実際にコーディングをするのが目標の我々にとっても勿論重要な部分です。しっかりと学んでいきましょう。

大げさに喧伝したにふさわしくβ変換の定義はα変換のように一発ではいきません。段階を踏まなくてはいけないのです。

まずラムダ項をラムダ項に変換する変換としてβ-1変換、記号ではラムダ項T,Sに対してT\to_{1\beta}Sというものを定義します。

(\lambda x.T)S\to_{1\beta}T[x\leftarrow S]\\T\to_{1\beta}S\Rightarrow TU\to_{1\beta} SU\\T\to_{1\beta}S\Rightarrow UT\to_{1\beta} US\\T\to_{1\beta}S\Rightarrow \lambda x.T\to_{1\beta} \lambda x.S

これだけみてもなんのこっちゃらなので、直感的意味を説明します。

β-1変換の直感的意味は、関数適用の「解決」にあります。

例えばλ抽象の時と同じ例ですが、日常的な文脈でf(x)=x^2,f(2)=2^2=4と書く場合の事を考えてみてください。このときf(2)というのはfに引数として2を与えるという「意味」を持っていて、それを実際に実行、解決したのが2^2です。

これと同様に関数適用というのは関数に値（ラムダ計算ではラムダ項）を与えることでしたから、それを解決するという事は仮引数に代入をすることで…そうなっていますね。このことからこの二つが「ある意味で同じ」と言えそうな気持もわかるでしょう。

さてこれでβ変換を定義できます。

ラムダ項Tがラムダ項Sにβ変換される（記号ではT\to S）とは、有限回のβ-1変換およびα変換の組み合わせでTがSに到達できるときに言う。

単にβ-1変換の推移閉包ではないことに注意してください（僕は一度大学の友人に説明しているときに間違いました。）。α変換を途中に挟んでいいことにしているのは、先に述べた通りβ-1変換で代入が起こるとき、新たな変数の捕捉問題が起きるのを回避できるようにするためです。そしてまた前節で計算（これはβ変換と言い換えてよいでしょう）の結果のα同値の違いは無視するといった理由もここにあります。すなわちβ変換の定義でα変換を任意に挟めることにより、最後にα変換をしたと考えれば、結局β変換の「仕方」次第では構文論的な等号が成り立っていたともいえるのでα同値の違いは気にしても仕方がないのです。
もっと形式的な定義もあるのですが、記述が本当に面倒くさいのでやりません。

また「β変換によって移る」という関係の同値閉包をβ同値と呼び、a=_\beta bのように書くことを付け加えておきます。

2.5 Church-Rosser性

先に言っておくと、ここでは証明は扱いません。というより僕もこの証明は理解も記憶もしておらず、何か参照しなくてはいけない状態です。

しかしそれでもこの性質が成り立つという事実だけは安心してコーディングをするうえで欠かせないので指摘しておきます。

ラムダ計算のβ変換は明らかに任意性があります。そもそもβ-1変換からして、4つのうち最初のルールが適用できる場所（β簡約基といいます）が複数あるかもしれないし、間に好きなだけα変換を挟んでもいいのだからかなりなんだってできそうに見えます。

しかし「ラムダ項Tが、異なるラムダ項SとUにβ変換されたとすると、SとUをさらに『うまく』β変換してやると同じラムダ項Vにできる」という事が知られています。

このような性質をChurch-Rosser性あるいは合流性と言い（微妙に異なった性質にこれらの用語を使い分ける流派もあるとか）、この性質があれば、特にもうβ-1変換できないようなラムダ項（β標準形、もしくは単に標準形と言います）にまで変換出来た場合には、α同値の分だけしか結果に差が出ないことがわかります。

この性質のおかげで我々はコーディングするとき、「少なくとも一つβ同値なβ標準形があるならば、それに変換してくれ。」とだけ、β変換をする人、または機械、または神、に注文しておけば、その誰かさんが自分の意図通りに変換してくれるかに悩む必要は、少なくともβ標準形を持つラムダ項に関しては、ないということになります。この後しばらくは出てくるラムダ項がほとんどがβ標準形を持ちますから、上の事実によって安心してコーディングができます。後にそうではない事態が出現しますが、それはその時にまた説明します。

3. ラムダ計算でコーディング

この章以降ではラムダ計算上に数学的概念（自然数や真理値、リストなど）を埋め込み、それによって実際にプログラム・計算が行えることを見ることによってラムダ計算が計算のモデル出ることを示すのが目的となります。

3.1 Church数項と加法・乗法

実は二章でラムダ計算の定義については全てお話ししてしまったのです。

こういわれてこう思った方もいるでしょう。「え？数学的概念は？」と。

ないんです。先に言った通りラムダ計算においては全ての対象が関数であり、従って自然数も実数もないと先に言った通りです。

しかし我々が計算と言われて想像するのは少なくとも自然数が登場するもののはずです。

ではどうするか、ある形の関数を自然数（のコード）だと「見做して」やるのです。

もったいぶらずに言いましょう（すでにもったいぶっている気もしますが）。

我々は以下のように「見做し」を「定義」します（知っている人向けに言えば集合論で0:=\emptyset,1:=\{\emptyset\},2:=\{\emptyset,\{\emptyset\}\},\cdots n+1:=n\cup\{n\},\cdotsと「定義」するのと同じです。）。

0:=\lambda S.Z.Z\\1:=\lambda S.Z.SZ\\2:=\lambda S.Z.S(SZ)\\n:=\lambda S.Z.S^nZ

すなわち関数と初期値を受け取って関数を初期値にn回反復合成した値を返すという高階関数（ラムダ項は全て高階関数なのですが）をnのコードとするのです。この方法でコードされた自然数の事をChurch数項と呼んだりします。

しかしながら自然数がコードされたからといって安心してはいられません。これはあくまでも「見做し」であって、本来は自然数でも何でもないのですから、我々の知っている自然数にできること、即ち計算、がこの「自然数」にできるかテストしてやらなくてはいけません。より具体的に言えば自然数を対象とする計算ができる関数、すなわちラムダ項、がラムダ計算の中でつくれるかを確かめるのです。そこでこの節ではまず「足す1」、「一般の加法」、「乗法」ができるかをテストしてやります。そしてこの章の終わりまでには四則演算が、さらにこの記事の最後までにはすべての自然数を対象としたプログラムが書けることをテストするのです。

ではまず「足す1」のテストから始めましょう。

これは種を明かしてしまった方が簡単なのでそうしてしまいます。「足す1」関数（後者関数、successorと呼ばれます）に対応するラムダ項はSuc=\lambda n.f.x.f(nfx)です。

実際に計算してみましょう。

(\lambda n.f.x.f(nfx) )(\lambda S.Z. S^nZ)\\\to_{1\beta} \lambda f.x. f((\lambda S.Z. S^nZ)fx)\\\to_{1\beta} \lambda f.x. f((\lambda Z. f^nZ)x)\\\to_{1\beta}\lambda f.x.f(f^nx)\\\to_\text{abbreviation}\lambda f.x.f^{n+1}x

（最後の変形はラムダ計算の体系内部での変換ではなく我々の略記に由来するものなので\to_\text{abbreviation}と書いた。）

となり、これは確かにn+1のコードである\lambda S.Z.S^{n+1}Zとα同値です。

では一般の加法はどうでしょう？

ここで自然数の「定義」を思い出してみましょう。自然数nとは「関数と初期値を受け取って初期値に関数をn回適用する高階関数」でした。そして加法というのは「足す1」の反復です。
つまり

Add=\lambda m.n.m\ Suc\ n

が加法関数になるのです。ここでSucは先の「足す1」関数で（先ほど名前を付けてあります）、あの関数をもう一度ここに書くのは、書く僕は面倒くさいだけ、読む皆さんは読みづらいだけで誰も得をしないので今後はこういう略記をよく使います。なおこの略記のせいで仮変数がかぶるみたいなことが若干心配になるかもしれませんが、そこは実在のプログラム言語でいう変数のシャドーイングをするようにラムダ抽象の定義を拡張したうえで、α変換でよろしくできるので大丈夫です。

では乗法はというとこれも同じ考え方です。乗法n\times mは0への「足すm」の反復適用です。そして「足すm」をつくるには？二章で学んだ部分適用が使えますね。即ち乗法は

Mul:=\lambda n.m.n\ (Add\ m)\ 0

となるのです。この方法を応用すれば指数関数、テトレーション…と作っていくことももちろん可能ですから演習問題代わりにやってみてください。

これでめでたく我々の自然数のコードは少なくとも加法と乗法が定義できる程度には自然数だという事がわかりました。

3.2 IsZero?述語とコードされたブーリアン、タプル

さて、我々が計算をしたいとき、扱いたいのは何も自然数だけではありません。

条件分岐やそれに伴う論理演算もまた計算に必要です。

そのためにはまずブーリアンの定義が必要なのですが次のようになります（これをここではコードされたブーリアンと呼ぶことにします）。

True:=\lambda F.S.F\\False:=\lambda F.S.S\equiv_\alpha 0

このブーリアンに対しても、先ほどの「自然数」と同様、我々が望ましいと思う性質を満たすかどうかの試験をせねばなりません。

我々がブーリアンに求めることと言えば、一にも二にもif式でしょう。

実はif式は大変簡潔な以下の表示を持ちます。

If:=\lambda\ bool.\ positive\text{-}case.\ negative\text{-}case.\ bool\ positive\text{-c}ase\ negative\text{-}case

実際に計算してみましょう。こんどはSucの時より少しだけ変形途中を飛ばすことにします（書く僕が面倒くさいので）。

If\ True\ P\ N\\\to_{\beta}(\lambda F.S.F)\ P\ N\\\to_{\beta}P

If\ False\ P\ N\\\to_{\beta}(\lambda F.S.S)\ P\ N\\\to_{\beta}N

（ここでP,Nはそれぞれラムダ項）

となり、確かにこれはif式です。

また、我々がブーリアンに求めるものには命題論理結合子もありますが、if文があれば命題論理結合子を作るのは容易ですから、それは省略することにします（\iff演習問題とします）。

我々がブーリアンに求めるものは、これらの他に何があるでしょう？そうです、算術の基本的な判定ですね、ゼロ判定、等号判定、大小判定ぐらいは欲しいところです。

ゼロ判定ができれば、あとで減法を作れば他の二つができますから（減法ができた後考えてみましょう。）、とりあえずゼロ判定を作りましょう。こうなります。

IsZero?:=\lambda n.n\ (\lambda x.False)\ True

これでなぜゼロ判定になるかわかるでしょうか？

まず、何度も言うようにこの世界ではnは「n回の反復適用を行う高階関数」ですから、もしnが0ならば、0回の反復適用、即ち初期値をそのまま返すことになり、初期値であるTrueを返します。

そして、反復適用するべき関数として渡している\lambda x.Falseは、引数によらずFalseを返す、いわゆるFalseへの定数関数ですから一度でも適用されればFalseになり、その後何度適用されてもずっとFalseを返すことになります。

これによってゼロ判定ができるのです。

さてこれでブーリアンについては（減法の後に回すということで棚上げした等号判定、大小判定を除いて）一通り説明したのですが、ここでお気づきの方はいるでしょうか？このブーリアン、ほとんどそのままタプルとも思えるのです。

その方法はこうです。

Cons:=Flip_2\ if\\\text{(where }Flip_i:=\lambda f.x.y_0.\cdots.y_{i-1}. f y_0\cdots y_{i-1}x\text{)}\\Car:=\lambda x. x\ True\\Cdr:=\lambda x. x\ False

僕はLispを書いていた時間が長いので、タプルのコンストラクタ、デストラクタの名前をLispのものにしていますが、意味論的に良い名前ではないのでお好きな名前で考えてください。またFlip_iの表記は自然数添え字iに対して、一般にこう定義するという意味です。これは多変数関数の第一引数を「後回し」にする、言い換えると引数を並べ替える高階関数です。Haskellの組み込み関数のflipはFlip_1に対応します。

このようにしてタプル型を得られることは、実際に計算してみてもわかりますが（演習問題とします。）、Trueの時とFalseの時の値をそれぞれ持っておくのがタプル型だと思えば自然なことだとも言えます。

（筆者からの注意: 次の段落以降急に難しくなったと感じる人がいるかもしれません。この記事はできるだけ大学の数学系や情報系なら1-2年次で習う程度の論理学や集合論の知識と、ほんの少しのコーディング経験があれば本筋を終えるように書くつもりだったのですが、ここから先はそもそも内容が難しいので、関数型プログラミングと手続き型プログラミングをどちらもある程度やったことがないと厳しいのかもしれません。）

そしてここで我々がタプル型を得たことは極めて重要です。というのも自然数が反復適用として定義されている現状、我々は事実上（自然数についての）forループ（もしくは知っている人向けに言えば原始再帰）を得ていることになるのですが、このforループ（原始再帰）はインデックスを使った処理が出来ないのです。しかしながらタプル型があれば我々は添え字と本命のアキュミュレータのタプルに関してループを回し、更新では添え字をSucしたものと本命の処理をしたアキュミュレータのタプルに更新するという方針によって、真のforループ（原始再帰）を得ることができるのです。

文章で書かれてもわかりにくいでしょうから、インデックスを使ったforループ（原始再帰）の簡単な例として階乗を計算するコードを書いてみましょう。こうなります。

Fact:=\lambda n.Cdr (n\ (\lambda x.(Cons\ (Suc(Car\ x) )\ (Mul\ (Car\ x)\ (Cdr\ x) ) ) )(Cons\ 1\ 1) )

これが確かに階乗計算になっていることは各自で確かめてください。方針は上に書いた通りです。このような方針で我々は一般にforループ（原始再帰）を得ることができるのです。

その他にも、タプルを得たことで、Lispのような方針でリストを扱うこともできますので、ここでタプルが手に入ったことは非常に表現力を引き上げているわけです*9。

3.3 減法

さてでは我々の主目的に戻って、Church数項が「自然数らしい」ことを確かめるために減法と除法をやっていきたいと思います。先にお断りしておくと、この記事でいう減法は\dot{-}と書かれることも多い演算で、第二引数が第一引数より大きいときも、マイナスにはならずに「0で止まる」（すなわちx\dot{-}y=\max(x-y,0)）減法です。

これから減法の定義をしたいのですが、減法は極めて難しく、定義を自分で考えだすことはおろか、正しい定義を見ても正しいと納得することも大変な感じです。この記事を書いている間に、ようやく筋の通った正当性の説明を見つけましたのでここでお話ししようと思います。とりあえずまず方針は以下の2ステップに分かれています。

  1. 「引く1」をする関数（前者関数、predecessorと言います）を作る。
  2. 1.をループさせる。

御覧の通り方針自体は加法を定義した時と同じなのですが、違うのは後者関数に比べて前者関数の構成が圧倒的に難しいことです。

とりあえずまず定義を見ましょう。

Pred:=\lambda n.[n\ \{\lambda f.If\ (IsZero?\ (f\ 1) )\ (\lambda m.m) (Compose\ Suc\ f)\} (\lambda l.0)]0\\\text{(where }compose:=\lambda f.g.x. f(gx)\text{)}

定義中の\{\},[]は、この後の説明のために強調の意味で()の代わりに使いました（つまりラムダ計算にとっては()として認識されていることにします。）。また、Composeは「（一変数の）関数合成」を意味しています。

さて、一見してこれが「引く1」だと納得できる人は恐らく、ほとんどというか、居ないと言っていいでしょう。即ちこの関数が「引く1」だという正当性の証明が必要です。

以降この関数に渡す引数をNとします。N=0のケースを考えてみましょう。このとき[]の中は反復適用の初期値になりますから、即ち\lambda l.0、つまりは0の定数関数になります。それに0を与えれば当然返り値は0です。

さて、ではN>0のケースはどうでしょう。これを考えるためには少しの逆算というか天下りというかを用いるのが楽です。すなわち[]内を計算した後、最終的にその結果に0を与えるとn-1になるようにしたいのですから、[]内は\lambda n.Suc^{N-1}n（と少なくともα同値）になるはずです。そう思って読むと…

一回目の\{\}内の適用では、If式は必ずTrue側に行きます。なぜならば初期値は0への定数関数だからです。True側には仮引数のfが出てきませんから、元の関数に関係なく[]内は\lambda m.m、即ち恒等関数になります。このことから翻ってPred\ 1=0がわかります。

そして二回目以降、N回目までの適用ではIf式は必ずFalse側に行きます。なぜならば数学的帰納法によってN-1回の反復適用の結果は\lambda n.Suc^{N-2}nになっているものとしてよいため、これに1を適用した結果は0にはなり得ないからです。そしてFalse側の処理は仮引数のfにSucを合成するものでしたから、結果は\lambda n.Suc^{N-1}nとなります。これは所望でした。

これによってあの突如出てきた関数が「引く1」だとわかったことになるのですが、納得いただけたでしょうか？

ちなみに余談ですが英語版wikipediaにはこれとほぼ同じ構成のPredが"Boolean"（記事中の言い回しでは"logic"）のところに乗っているのですが、日本語版はちょっとした工夫によってIf,IsZero?を使わずに同様の効果を得ているので、かえって難読コードと化しています。

ちょっとした自慢ですがComposeを一個の関数として切り出すのは僕のアイデアで、これで結構読みやすくなる気がしています。

さて、このとても大変な構成を終えてしまえば、本節の残りはウイニングランです。減法の定義は先に触れた通り加法と全く同じ

Sub:=\lambda n.m. m\ Pred\ n

で済みます。

また前節の「宿題」も片付けておきましょう。

\dot{-}の定義からn\leq mはx\dot{-}y=0と同値ですから、

Leq?:=\lambda n.m.Iszero?\ (n\ Sub\ m)

で、大小関係が定義できます。

さらに両向きの大小関係が成り立つことを等号とすれば等号判定、不等号が成り立ってかつ逆向きの不等号が成り立たないことを記述すれば狭義の不等号を手に入れることができるのです（ここで論理積と否定（下のコードではAnd,Notとして登場しています）が必要になります。これは演習問題としていましたが解けましたか？）。

Eq?:=\lambda n.m.And\ (Leq?\ n\ m)(Leq?\ n\ m)

Less?:=\lambda n.m.And\ (Leq?\ n\ m)(Not\ (Leq?\ n\ m))

3.4 有界探索と除法、残った課題

n未満の自然数で述語（:\iff返り値がTrueかFalseの関数）pを満たすもののうち最も小さいものを探索したい、というシチュエーションはよくあります。これは有界探索と呼ばれており、一般的な方法は次の関数を用います。

BoundedSearch:=\lambda p.n.n\ (\lambda m.If\ (p\ m)\ (Suc\ m)\ m)\ 0

これは前にも述べた通り、Church数項の自然数による反復適用が実質的にforループであることを考えれば理解しやすいかと思います。反復適用に使われている関数は、ある数m(\lt n)でp\ mが成り立たなければ引数を1大きくし、成り立てば引数をそのまま返すので、ループするたびにp\ mが成り立つようなmが見つかるまでは引数が増大していき、一度見つかったらそれ以降は変わらないわけです。もしも、そのようなn未満の自然数が発見できなければ、値はnまで増加することになりますから、もし返り値がn未満の自然数でなくnになっていたら「探索失敗」を意味するわけです。

この有界探索を知っていれば除法は極めて容易です。割る数が0でない、自然数による除法の商はかならず割られる数以下なので

Div:=\lambda n.m.If (IsZero?\ m)\ 0\ (BoundedSearch\ (\lambda l.(Less? (Sub\ n\ (Mul\ m\ l) ) m) n)

これでn-m\times lがmを下回る最小の自然数、即ち定義よりnをmで割った商が計算できます。（mが0の時通常の除法は定義されませんので仮に0を返すようにしてあります。またm=1だとn未満には商がないのですがその時はnを返すことになっていましたから、やはり問題ありません。）

商ができてしまえば余りはもっと簡単で割られる数から割る数と商をかけたものを引くだけです。

Rem:=\lambda n.m.Sub\ n\ (Mul\ m\ (Div\ n\ m) )

こうしてついに我々は四則演算全てを手に入れたのです。

ここまでの我々の成功とこの過程で得た大量の副産物から、「これだけあれば普通にプログラムできるじゃん」と思われる方も多いと思います。実際ここまでのコーディングテクニックを応用すれば、相当多くのものが手に入るのは間違いないのですが、一つだけ我々がまだ得ていないものがあります。それは再帰呼び出し、あるいはwhileループに対応するものです。

実はTuring完全性には一章で述べた定義のほかに非形式的な判定基準があり、

  1. If文に対応する構造
  2. while文、もしくは再帰呼び出しに対応する構造
  3. ごく基本的な算術演算（ここに何が必要かは体系によって微妙に変わります。）

が備わっていればTuring完全になるという基準が存在します（これはKleeneの公理化された再帰関数について少し知ると妥当であるとわかります。）。

このうち我々にはまだwhile式,、より一般に再帰呼び出しがないのです。

この再帰呼び出しを見つけるために次章に進みます。

4. 無制限再帰

4.1 不動点コンビネータと無制限再帰

我々の目的を達成するためには不動点コンビネータと呼ばれるラムダ項Rを手に入れれば十分です。これは全てのラムダ項fに対して、

Rf=_\beta f(Rf)(=_\beta f(f(Rf) )=_\beta\cdots)

を満たすRを言います。どうして不動点コンビネータというのかと言えばfを関数、Rを高階関数と見た時、これはx=_\beta fxであるようなx、つまり関数fの不動点をfから生成しているように見えるからです。

より重要かつ難しいのは、どうしてこのようなRがあれば再帰呼び出しが実装されたと言えるかという点です。

これは実装を見ながら説明しましょう。

上で我々は既にforループによる階乗を得ていますが、例の簡明さのために再び階乗を、今度は再帰呼び出しで作ることを目標にしましょう。

まず何も考えずに書けば

Fact1:=\lambda x.(If\ (Iszero?\ x)\ 1\ (Mul\ x\ (Fact1\ (Pred\ x) ) ) )

となりますが、ラムダ計算の定義にこのような「名前による再帰」は含まれていないのでこの定義はこのままではラムダ計算による関数定義になりません。

そこで一旦右辺のFact1をλ抽象したものを考えます。即ち

Fact1!:=\lambda Fact1!.(\lambda x.(If\ (Iszero?\ x)\ 1\ (Mul\ x\ (Fact1!\ (Pred\ x) ) ) ) )

とを考えます。

後はどうにかして「Fact1!の第一引数に自分自身を代入し、しかもその突っ込まれた第一引数としての自分自身の第一引数にも自分自身が代入されており…」という状況を作れれば目的達成となるのですが、これを達成するために先の不動点コンビネータを用いるのです。

つまりここでR\ Fact1!を考えます。すると

R\ Fact1!\\=Fact1!(R\ Fact1!)\\=Fact1!(Fact1!(R\ Fact1!) )\\=\cdots

となり、即ちFact1!の第一引数にFact1!が代入されているのですが、その第一引数にもFact1!が代入されており…となっており、所望の状況を得たことになります。

しかし…これで納得できる人はいるのでしょうか？ちょっと難しすぎますね。

もう少し簡単な例で考えてみましょう。今度はリストを（左から）潰す関数、普通のプログラム言語でいうとreduceやfold-light(foldl)と呼ばれるような関数を作ってみましょう。

まず先ほどと同じように普通に再帰で書くと

Reduce:=\lambda list.f.start.\ (If\ (Null?\ list)\ start\ (Reduce\ (Cdr\ lst)\ f\ (f\ start\ (Car\ acc) ) ) )

となります。これを先ほどと同じように処理すれば

Reduce!:=\lambda Reduce!.list.f.start.\ (If\ (Null?\ list)\ start\ (Reduce!\ (Cdr\ lst)\ f\ (f\ start\ (Car\ acc) ) ) )\\Reduce:=R\ Reduce!

となります。

ここでもう一度何が起きているのか考えてみましょう。

Reduceは受け取ったリストが空でなかった場合、ある処理（つまりこの後使う引数の計算）をした後、ある引数で自分自身を呼び出そうとします。

つまり比喩的に言えば、Reduceは引数の計算という仕事をした後、残りの仕事を誰か（といっても自分自身なのですが）に委任するようになっています。自分自身が現れる部分を仮引数に置き換えたReduce!では、代わりに引数に受け取った何かしらの関数を呼び出そうとする、比喩でいえば自分自身ではなく本当に他人に残りの仕事を委任しようとするわけです。

しかしR\ Reduce!を考えれば、不動点コンビネータの性質により、仮引数（仕事の委任先）は自分自身（の仮引数（委任先）にさらに自分自身が代入されて…なもの）になるわけです（知っている人向けに言えば継続渡し形式の継続として自分自身を、そのまた継続としてさらに自分自身を…呼び出したことになります。）。

僕が二つ目の例を挙げた理由は、第一の例では自分自身を呼び出した後にnを掛けるという処理が続いており（つまり末尾再帰になっておらず）、本質が見えにくいかと思ったからです。

もしあなたがこのような不動点コンビネータによる再帰に初めて触れるなら、この節の説明が全く理解できなかったとしてもむしろ当然のことです。僕もこれが直観的に納得できるようになるまでずいぶん時間がかかりました。しかしとりあえずそのようなラムダ式を得る方法だけは簡単に覚えることが出来ます。再帰を使ったラムダ式を書いたならば、再帰に使った自分の名前を一番外側でλ抽象して仮引数にし、最後にそれをRに適用すればそれで出来上がりです。

もし、継続という概念は知っているが、不動点コンビネータ周りがずっと腑に落ちていなかったという方がいらっしゃれば、この節の括弧内で触れたように不動点コンビネータは継続渡しに自分自身を与えてくれるものだと考えると少なくとも末尾再帰についてはすっきり理解できるはずです。末尾再帰でない場合には、継続が複雑化（自分自身と他の関数の合成が継続となる）しますが、その場合でも継続渡しに少なくとも渡す継続として自分自身が選択可能であるという状況を作り出すものだと考えると考えやすいと思います。

ではこの節の最後にこの節ではずっとRと書いてきた不動点コンビネータがラムダ項として実在することを示します。実際には無限に多くのこのような例があることが知られていますが、ここでは最も簡単なものを紹介します。

R:=\lambda f.(\lambda g.f(gg) )(\lambda g.f(gg) )

これにはCurryのYコンビネータという名前がついています。これが不動点コンビネータであることを確かめてみましょう。

RF\\\to_{\beta 1}(\lambda g.F(gg) )(\lambda g.F(gg) )\\\to_{\beta 1}F( (\lambda g.F(gg) )(\lambda g.F(gg) ) )\\\leftarrow_{\beta 1}F(RF)

これにより、めでたく我々は再帰的な定義をする方法を手に入れたのです。

4.2 無限ループへの対処、定義の明確化

ここまでで皆さんは「ラムダ計算でコーディング」するのに必要な技術を本質的には全て知ったことになります。後は通常のプログラミング言語でのコーディングの知識や経験と多少の思索があれば、本質的には通常のコンピュータができることを何だってラムダ計算の上ですることが出来ます。例えばラムダ計算の上でラムダ計算のインタープリタを書くことも原理的には可能です（それなりに大変でしょうけど）。

ではなぜこの記事が続いているかというと実は前節の不動点コンビネータはここまでにない新たな状況を生じさせているからです。

それは何かというと前節でCurryのYコンビネータが不動点コンビネータであることを示したとき、

RF\to_{\beta 1}(\lambda g.F(gg) )(\lambda g.F(gg) )\\\to_{\beta 1}F( (\lambda g.F(gg) )(\lambda g.F(gg) ) )\\\leftarrow_{\beta 1}F(RF)

としましたが、ここで二行目の式はまだβ1簡約出来ます。できる限りβ1簡約を続けようとすれば

RF\to_{\beta 1}(\lambda g.F(gg) )(\lambda g.F(gg) )\\\to_{\beta 1}F( (\lambda g.F(gg) )(\lambda g.F(gg) ) )\\\to_{\beta 1}F(F( (\lambda g.F(gg) )(\lambda g.F(gg) ) ) )\\\to_{\beta 1}F(F(F( (\lambda g.F(gg) )(\lambda g.F(gg) ) ) ) )\\\to_{\beta 1}\cdots

となり、Fが増えていくばかりで簡約列が止まらないことがわかります。これは実際にはCurryのYコンビネータだけでなく、不動点コンビネータに共通の性質になるのは不動点コンビネータの定義式に類似の無限列が出現していたことからわかると思います。

このことからこんなことがわかります。

実際には、例えばR\ Fact1!\ nは正規形を持ち、それがn!であるのは前節でみた通りですが、そのような「意図した答え」に簡約されるのは「うまい順序で簡約したとき」に限るのです。なぜならばR\ Fact1!の部分を簡約し続ける限り、先ほどと同じ無限ループに陥るからです。

そこで我々が最初にβ変換をしてくれる誰かさんとした約束「一つでも標準形を持つならば、それに簡約してくれ」というのが生きてくるのです。この約束の上では上記のような心配はいらず、我々の欲しい結果にラムダ項は簡約されます。ここには一つ問題があり、「『標準形があるならばそれになるような簡約』というのを簡約してくれる誰かさんはどうやって知るのか？」ということです。「誰かさん」が神様の場合ならばいいでしょうが、多くの我々は神と交信する手段を持たないので、β簡約を実際に行ってくれるのは大抵はコンピュータであり、コンピュータは今行っている方針で簡約が終わるのかどうか判断する手段を持ちません。しかし実は以下のようなことが知られています。

Def.5.1 最左最外戦略とはβ簡約の手順を定義するものであり、関数適用があればその左側に着目し、構文木上もっとも浅いβ簡約基から簡約するような手順である。

Fact.5.2 対象となるラムダ項に一つでも正規形が存在すれば、それに最左最外戦略で到達できる。

これらにより、実はコンピュータにも上記のような「依頼」をすることが出来ることがわかるのです。

Fact5.2の証明はここでは扱わないのでHenk P. Barendregt, ”The Lambda Calculus, its Syntax and Semantics''などをお読みください。

実際には多くのプログラム言語のインタープリタやコンパイラは最左最外戦略で簡約するわけではないので、そのような状況ではより複雑なことが起きます。実は不動点コンビネータの選び方によって意図したとおりに簡約されたりされなかったりするのです。しかし我々は現在理論的な興味でラムダ計算を扱っているので、このあたりの話題には深入りしません。ともかく、簡約してくれる誰かさんに一つでも正規形があればそれに簡約してもらうことにし、特に誰かさんがコンピュータの場合であってもこれが可能であるという点を指摘するだけにとどめます。

またここで「ラムダ計算でコーディング」したことで我々が実際に何を得たのかを明確にするため、ラムダ計算における関数や値についてをキチンと定義してみましょう。というのもこのようにβ標準形で表示できない関数が出現したことで、我々は少しラムダ計算の中での「関数」や「値」という概念について注意深くなる必要があるからです。我々は関数に値を適用して計算した結果の値についてはβ標準形であることを要求しているため、関数はβ標準形で書けないこともあるというのは若干片手落ちな気もしてしまうからです（実際前章までに定義した関数はβ標準形になっているか、何段階か簡約すればβ標準形になるようになっていました。もしよければ名前による略記をそれが表すラムダ項に置きなおして計算してみてください）。さらに言えば最初のほうで計算モデルにおける関数は「値がないこと(\uparrow)」も許していることについて述べましたが、まだラムダ計算において定義された関数の値がないとはどういうことかも定義していませんでした。お察しの通りこれがまさに標準形がないことなのですが、それについても定義しておく必要があるでしょう。

このように定義しましょう。

Def 5.3

  • ラムダ計算における値とは、β標準形の事である。
  • ラムダ計算における関数とは「ラムダ項」と「『意図した入力』となる標準形のラムダ項の集合」のペアの事である。
  • ラムダ計算における述語とはラムダ計算における関数であって、それが意図した入力を適用されて、かつ正規形に簡約されるならばその値がTrueかFalse（とα同値）になることである。
  • ラムダ計算における関数Fが入力Aで値を持たない（\uparrow）とは、FAが正規形を持たないことである。
  • ラムダ計算において関数Fが自然数値部分関数fを表現するとは、Fの意図した入力がチャーチ数項を含み、Fにチャーチ数項としてのnを与えた項Fnが正規形を持つこととnがfの定義域に属することが同値で、かつFnが正規形を持つ限りその正規形はf(n)をチャーチ数項として表現したものと（α同値の意味で）同じになることである。
  • ラムダ計算において関数Pが自然数値部分述語pを表現するとは、Pの意図した入力がチャーチ数項を含み、Pにチャーチ数項としてのnを与えた項Pnが正規形を持つこととnがpの定義域に属することが同値で、かつPnが正規形を持つ限りその正規形はp(n)をコードされたブーリアンとして表現したものと（α同値の意味で）同じになることである。
  • ラムダ計算において関数（述語）Fが全域であるとは、FにFのどの意図した入力を適用した結果も標準形を持つことである。

（「意図した入力」という言葉が新たに出てきましたが、これは我々が今まで作ってきた多くは自然数値関数を表現するラムダ項に、もしも自然数でないラムダ項を適用すれば、その結果は全く予測できない、という事態に対処するためです。これは本来は今回の記事では扱わない型付きラムダ計算と呼ばれる体系で対処するべきことなのですが、ここでは便宜上このように定めておきます。個々の関数に対して「意図した入力」となる集合を実際に記述しようと思うと、それはほとんど型付きラムダ計算を導入するのと同じことになるので、ここでは第五、第六の定義から自然数値関数をプログラムする際には意図した入力は自然数のスーパーセットである必要がある、という事だけを指摘しておきます。）

この定義によって、値と関数を区別されたことで我々は関数の表現がβ標準形で書けないことに後ろめたさを感じずに済み、また値がないというプログラミング的な状況を標準形がないことだとして数学的に取り扱うことが出来るようになったわけです。

長々とお付き合いありがとうございました。これにてようやく「ラムダ計算でコーディング」は全編終了です。最後に定義が出てくるという数学としては珍妙なスタイルになりましたが、ラムダ計算で「実際にコーディングをする」ことを重視した結果なのでどうかご容赦いただければと思います。

6. 謝辞など

Twitter:@hennin_Itn いつも議論相手になって頂いています。参考文献の中にあるラムダ計算インタープリタも彼の作。
Git Hub:github.com/tani 僕に継続を教えてくれたり、下の参考になるブログを教えてくれたりした方。
リアル同研究室の皆様 普段のゼミがこの記事を書くモチベーションになったり、細かいながら定義次第でバグりがちなところの相談に乗ってもらったり。

7. 参考文献など

Benjamin C. Pierce著: Types and Programming Languages
J. Roger Hindley著:Basic Simple Type Theory
Henk P. Barendregt著:The Lambda Calculus, its Syntax and Semantics

日Wikipedia:

ラムダ計算(https://ja.wikipedia.org/wiki/%E3%83%A9%E3%83%A0%E3%83%80%E8%A8%88%E7%AE%97#)

計算モデル(https://ja.wikipedia.org/wiki/%E8%A8%88%E7%AE%97%E3%83%A2%E3%83%87%E3%83%AB)

英Wikipedia:

Lambda calculus(https://en.wikipedia.org/wiki/Lambda_calculus)

Model of Computation(https://en.wikipedia.org/wiki/Model_of_computation)


@hennin 作ラムダ計算インタープリタ（リンク先→REAdME.md→WebREPLからブラウザ上でも使えます）https://github.com/utatatata/untyped-lambda-calculus

*1:これが普通の（集合論的な）意味での関数、述語の等しさでした

*2:この節で出てくるエミュレータの定義は実はまさにそうで、外延的に同じ関数が異なる定数に移されることを認めないといろいろとうまくいかないことが知られています。

*3:「自然な」といったのは特に1.1節で書いた計算モデルの（非形式的な）共通点のうち、2.や3.をわざと失わせ、人間や既存のコンピュータにできそうにないほど複雑な操作（e.g. プログラムの停止性の判定、真の乱数の生成、無限回ステップの繰り返し…etc）を加えた計算モデルを考えることもあるからです。オラクル付き計算モデルなどと呼ばれることもあるこれらは、ある意味当然ですが、この先で説明する一種の「限界」を突破することができます。

*4:多くのプログラム言語で無名関数を定義するときに使われる"lambda"や"\"というキーワードはここに端を発しています。

*5:完全に余談ですがはてなブログは"(("や"))"を脚注の記法だと思って読んでしまうので、僕はエスケープシーケンスを使ったり、間にスペースを入れるなどの対策をしなくてはならず、普通にLaTeXで同じものを書くのに比べてさらに五割増しぐらいで大変です

*6:形式的な定義の一つ（節の後半でいうところの1.の変数捕捉回避のアプローチ）は以下のようになる。 1.x[x\leftarrow T]=T\\2.y[x\leftarrow T]=y\ (\text{$x\neq y$の時。})\\3.(UV)[x\leftarrow T]=(U[x\leftarrow T])(V[x\leftarrow T])\\4.(\lambda y.U)[x\leftarrow T]=\lambda y.U[x\leftarrow T](\text{$x\neq y$かつ$x$は$T$の自由変数でない時。})\\5.(\lambda x.U)[x\leftarrow T]=U\\6.(\lambda y.U)[x\leftarrow T]=\lambda z.( (U[y\leftarrow z])[x\leftarrow T])\\(\text{$x\neq y$かつ$x$が$T$の自由変数である時。ここで$z$は$T$の自由変数でも$U$の自由変数でもないような変数から任意に取る。})

*7:実はもう一つ「η同値」と呼ばれる同値があるのですが、これがなくともラムダ計算の体系としてTuring完全になるためここでは扱いません

*8:といってもうまくやればα変換を回避する実装上の工夫も存在します。興味のある方はNameless Lambdaやde Bruijn indexでググってみてください

*9:この記事ではリスト処理について詳しくはやりませんが、例えば空リストをFalseで表し、Listについて、Listへの要素の追加を\lambda x.Cons\ x\ List、先頭要素の取り出しをCar\ List、先頭要素を取り出した残りのリストをCdr\ Lispとするなどして、以降はLisp言語でのコーディングテクニックに合流しますので、SICP（参考文献参照）などを参考にしてください。この時、Lispに標準的に備わっている機能のうち、リストの空判定のみ明らかでありませんが、Null?:=\lambda list.list\ (\lambda x.y.\lambda z. False)\ True)で与えらます（λが連続したときの略記を一部しか使っていない理由は、正当性を実際に計算して確かめてみればわかります。）。

ファジー論理の定義(意味論側)とか他の論理との比較とか

Aaronです。

アドカレ遅れてすいません。

自分の研究にちょっとだけファジー論理が出てきたのでせっかくなのでまとめたものを投稿します。

今回は意味論に絞って(MTLと呼ばれる体系などには証明論が対応して完全性定理が成り立ったりするようだが、こちらはまだ僕も調べられていないので今回はスルー。)主に古典論理や（Belnapのものよりは、LukasiewiczやGodelのものに近い）有限多値論理との比較という観点から見ます。

1.動機と歴史と導入

我々が日常的な文脈での議論を行うときや、統計的な議論を行うとき、古典論理（の意味論）で議論するときのように「真か偽のいずれか」を考えるというよりも、「真らしさの度合い」や「真である確率、信頼度（僕は統計に疎いのでこの辺の言葉遣いがおかしいかもしれない。おかしかったら教えてください。）」を考えていることの方が多いかもしれない（ただし確率を真偽値と捉えるものは確率論理と呼んでファジー論理とは区別されるようである。例えばNaive Baise手法などの文脈で論理式に似た構造を扱うことがあるが、それは真理値割り当てのみによって論理結合子の解釈が決まらないという性質を持っており、ここで解説する枠組みでは扱えない。）。

これは「古典論理の真理値や付値関数が二値的であるために表現力が欠如しているため」とも考えられる。

Lukasiewicz（本当はLの縦棒の部分に小さいスラッシュのような装飾が入る。）はこの考え方から、新たな真偽値0.5を追加した真偽値集合\{0,0.5,1\}を持つ論理を提案した（Lukasiewiczの三値論理）。しかし彼の構成法を基にすれば追加される真偽値は一つである必要はなく、一般の\it n個の真偽値を持った\it n値論理、そしてさらには[0,1]上の任意の値を真偽値として取れる無限値論理が提案された。これがファジー論理の（一つの）導入経緯である（歴史を詳しくは調べられていないので、もっと以前にファジー論理のインスタンスが現れていたりするかもしれないが、これも一つの経緯ではありそうだし、直感的に自然な経緯なので採用した。「歴史的にはそうじゃない」とかいうツッコミがあったらご連絡ください。）。

2.定義

ファジー論理の論理自体や論理式の定義は古典論理とほとんど変わらない。

ただ、少数の論理結合子で完全な基底を得ることができ、歴史的によく知られた論理結合子から適当に導入すれば問題は少なかった古典論理と異なり、ファジー論理では豊かな表現力を出すために多くの論理結合子を考えるのが普通であるし、よく知られた結合子に「対応する論理結合子」がどんな関数なのかも明らかではない（これについては後で触れる）から論理結合子の意味論的解釈を途中で変えたいと思うかもしれない。

そこで論理の定義に、使う論理結合子の選び方の自由度を残しておき、解釈も「論理結合子の解釈」と「命題変数の解釈」の二段階に分けると多くの状況に対応できる。

形式的には以下のようになるがほとんどの読者は自分で再構成できると思うのでずらずらと書いてしまう。

ファジー論理とは「命題変数」と呼ばれる記号の空でない集合\it Atomと、「論理結合子」と呼ばれる、記号と「Arity」と呼ばれる自然数の組の関数的な集合（すなわち同じ記号を前者とする組は唯一であるような集合）\it Connective\subset ConnectiveSymbol\times \mathbb{N}との2つ組\it{\rm (}Atom,Connective{\rm )}である。

またその上の論理式とは

  • \it Atom\subset Fml.
  • \forall ({\it c},{\it n}) \in {\it Connective}.(({\it c,n}),{\it f}\ )\in {\it Fml}.\ (\text{where}\ {\it f\ {\rm :}\ n\to Fml}\ )

 を満たす最小の\it Fml（の元）を言う。ただし集合論で使われるトリックで自然数\it nを「\it n未満の自然数全ての集合」とみる。

ファジー論理の論理結合子の解釈とは関数

\displaystyle{\it ConnectiveInterpretation}:{\it Connective}\to\bigcup_{\it n\in\omega}[0,1]^{[0,1]^{\it n}}

であって

{\it ConnectiveInterpretation}({\it c,n})\in [0,1]^{[0,1]^{\it n}} 

を満たすものを言い（割とよくあることだが「解釈」という用語は少し曖昧である。この関数自体を指すことと、特定の論理結合子に対応する関数値を指すことがある。）、これをファジー論理の定義に含めてファジー論理を三つ組とみる場合と、冒頭のように含めない場合がある。さらに言えば論理結合子の（空でない真）部分集合の解釈を論理の定義に含め、それ以外については含めないという事もあり得る。そこで論理の定義に解釈が含まれているような論理結合子について「解釈が固定されている」とかいうことにする。

命題変数の解釈あるいは付値とは関数

{\it Valuation}:{\it Atom}\to [0,1]

のことであり、論理結合子の解釈と付値が共に与えられれば論理式の解釈

{\it FmlValuation}:{\it Fml}\to [0,1]

が

{\it FmlValuation}({\it a})={\it Valuation}({\it a})\ (\text{where}\ {\it a\in Atom}).

{\it FmlValuation}(({\it c,n}),{\it f}\ )={\it ConnectiveInterpretation}({\it c,n})({\it FmlValuation\circ f}\ )\\(\text{where}\ {\it {\rm (}c,n{\rm )}\in Connective})

によって定まる。

3.古典論理との比較

由来（の一つ）を見ても明らかなように、ファジー論理は古典論理の拡張または亜種たらんとする設計思想がある。したがって論理結合子もまた古典論理が備えているものを備えていてほしいと思うのは自然なことである。ここでは矛盾、含意、否定、連言、選言に対応する論理結合子を備えている（そのほかの論理結合子を備えていてもよいし、「複数の連言や選言」を持ってもよいとする。また矛盾、含意、否定、連言、選言に対応する論理結合子の解釈は、少なくとも真偽値0,1については古典論理の対応する演算子（の解釈）と外延的に等価であることが要求されるものとしする。）ファジー論理をこの記事では「擬古典的」と呼ぶことにしよう。

これらのうち、矛盾の解釈については同意が得やすいだろう。

矛盾（\perp）とはArityが0で解釈が（引数を取らずに）0を返す関数になるような論理結合子である、としておそらく反対するものはほぼいないだろう。

 しかしそのほかの論理結合子に対しては（Arity以外）合意を得るのは難しい。

一見して妥当と思える理由のある定義が多くあるからである。

例えば日本語Wikipediaの「ファジィ集合（ファジー論理の上で展開された集合論だと思ってよい）」の項目の末尾には、ファジー論理に特有な「論理和」「論理積」のリストがある（なぜファジー論理のページでなく集合論のほうにあるのかは不明である）。

またt-normという概念は（この概念は日本語Wikipediaでは「ファジィ論理」の項目の「命題ファジィ論理」の箇所に「三角型ノルム」として紹介されている。さらに英語版では専用の項目が立ち、さらに「t-norm fuzzy logic」の為にも別の項目が立っている。）いくつかの性質、即ち

  1. 可換性
  2. 結合性
  3. 単調性
  4. 1の単位性

（これらの条件は代数学で議論されるものと同じである。）

を持つものという形で論理積（の解釈）を公理化したものであり、逆に言えばこれを満たす実数値関数ならば（それは膨大な数ある。）、論理積の解釈として妥当だという一種のテーゼと取ることもできる（（英語wikiを信頼するならば）t-norm fuzzy logicといった場合はt-normが連続であることも論理積の解釈の公理に要求するようである。一方で前述のリストに出てくる激烈積がそうであるように、直感的に自然な意味づけが可能なt-norm（論理積（の解釈））であって、連続でないものもあり得る。）。

ここまでは含意や否定に触れなかったが、含意や否定についても同様に膨大な妥当と思わしき定義を作ることができる。

そこで我々はこのような膨大に存在する各々の論理結合子の解釈の定義に着目するのではなく、弱く擬古典的な論理における論理結合子同士の関係性に着目すべきである。

ファジー論理が古典論理における重要な関係（定義可能性）、たとえば、

  • \perp \Leftrightarrow \lnot (A\to A)（Aは勝手な命題変数。矛盾の定義可能性）
  • \lnot A\Leftrightarrow A\to\perp（否定の定義可能性）
  • A\to B\Leftrightarrow \lnot A\lor B（含意の定義可能性）
  • A\land B\Leftrightarrow \lnot(\lnot A\lor \lnot B)（連言の定義可能性）
  • A\lor B\Leftrightarrow \lnot(\lnot A\land \lnot B)（選言の定義可能性）

（ただし記号\Leftrightarrowは全ての\it FmlValuationについて両辺の付値が等しくなることを主張するメタ記法である。特にメタという点は重要で体系内でこれに当たる論理結合子が定義できるとは限らない。）

などのうちのいずれかを満たすとき、この記事では左辺の論理結合子は右辺に出現する論理式に対して「整合的」であると言うことにする（もちろん古典論理上同値な定義式は他にもあるので定義式を指定して「整合的」というべきだが、煩わしいのでこの記事ではこの定義式に対して整合的な時は単に整合的と呼ぶことにする）。

しかし多くの論理結合子を整合的にするためには代償を払わなくてはならない。たとえば、論理積の解釈を最小値関数（Godel t-normというらしい）で、否定の解釈をf(x)=1-x（Lukasiewicz negationというらしい）で固定し、矛盾を持たず、ほかの論理結合子の解釈は論理和と整合的な体系（整合性からほかの論理結合子の定義はわかるはずなので演習問題代わりに定義してみよ。この体系をこの記事でだけK_\inftyと呼ぶことにする。どうしてこう呼びたいかは後でわかる。）を考えれば、これについて以下がわかる。

Prop3.1 K_\inftyは恒真式を持たない。ここで恒真式とは全ての\it FmlValuationについて付値が1になるような論理式の事である。

Proof)値が恒等的に0.5であるような\it Valuationを考える。この時対応する\it FmlValuationは恒等的に0.5である（論理式の構成に関する帰納法でわかる）。

Cor 3.2 K_\inftyで上の整合性によって定義された矛盾は、この章の前半で定義した性質を満たさない。特に値が使用する命題変数によって変わってしまい、Arityが0とみなせない。より強く、方法によらず前半で定義された性質を満たす矛盾は（既存の論理結合子の略記としては）K_\inftyでは定義できない。

Proof)主張の後半を示せば十分である。矛盾が定義可能だったとすると\lnot\perpは恒真のはずである。これはProp3.1に反する。

 

このような問題があるため、含意は一般的には整合性を定義とはせず、「論理積（の解釈）の残余(residuum)」と呼ばれる演算で定義するのが普通なようである。

これは論理積の解釈を\starとして、\max_C(A\star C\leq B)を含意の解釈とするものである。

 

以下では例としてGodel t-normからそのようにして得られた含意（陽に書けば

{\it ConnectiveInterpretation}(\to)({\it x,y})=\begin{cases}1\ ({\it x}\leq {\it y})\\{\it y}\ ({\it x}\gt {\it y})\end{cases}

です。）とそれに整合的な否定を持ち、論理和と論理積はK_\inftyのものを用いる体系を考える（いわゆるGodel-Dummettファジー論理）。

この含意に対して整合的な否定（Godel negationというらしい）は、

{\it ConnectiveInterpretation}(\lnot)({\it x})=\begin{cases}1\ ({\it x}= 0)\\ 0\ ({\it x}\gt 0)\end{cases}

であり、Lukasiewicz negationとは異なる。従って、論理積と論理和を整合的にせず、さらに含意が論理和と否定に整合的になることもない。古典論理との類似性との観点からは否定を二つ持っており、整合性ごとに異なる否定を用いているとみるべきかもしれない。

引き換えに矛盾の定義可能性（さらにおまけとして「恒真」の定義可能性）を持っているのである（実は矛盾を定義するだけならば、この含意は必要ではなくK_\inftyに「第二の否定」としてGodel negationを追加した論理を考えるだけでも良い。これに類似した論理がのちに現れる。）。

 

一方でたとえばLukasiewicz t-normもしくは限界積と呼ばれる論理積、即ち\max(A+B-1,0)、とLukasiewicz negationを持つ体系では、残余による含意と整合性による含意が一致し、矛盾も定義可能である（さらに、含意と整合的な否定はLukasiewicz negationなのでその意味でも整合的になる。この整合性からたとえば二重否定除去がconsequenceとなる）。しかし今度はA\land AがAと等しくならないという代償を払うことになる。

4.\it L-ファジー論理と部分ファジー論理

少なくとも1章で説明したモチベーションをなぞるのであれば、ファジー論理とは古典論理や有限多値論理の拡張として理解したいのであるのが、しかしファジー論理は普通の意味でのそれらの「拡張」ではない。

というのも古典論理の時そうであったように普通、論理の意味論というのは\it Valuationを動かす形で議論されるが、ファジー論理は\it Valuationのcodomainが[0,1]で固定されてしまっているため、古典論理をその中で解釈しようとしても(0,1)の値を取る付値をいわば押し売りされてしまうのである。

そこでファジー論理をより拡張することで、古典論理を特別なインスタンスとして実現できるような枠組みを作りたいと考えるのは自然である。

L-ファジー論理とよばれる枠組みはそれを可能とする。これはファジー論理で使われたAtomとConnectiveに加え、何らかの順序構造\it Lを加えた三個組\it{\rm (}Atom,Connective,L{\rm )}で、論理値を[0,1]ではなく、\it Lに取るものとして定義される（形式的な構成は一章でやったものを[0,1]だけを\it Lに置き換えればよいので省略する。）。これを用いれば例えば直観主義論理はHeyting Algebra-ファジー論理であると言える。

しかし、これは少々冒頭に掲げた我々の目的、「古典論理や（Belnapのものよりは、LukasiewiczやGodelのものに近い）有限多値論理との比較」には一般すぎるように思われる。

そこで\it Lとして[0,1]の部分順序集合を取るような\it L-ファジー論理を、この記事では「\it L-部分ファジー論理」と呼ぶことにする。

古典論理は\{0,1\}-部分ファジー論理だし、Lukasiewiczの\it n値論理も\{\frac{\it m}{{\it n}-1}:0\leq {\it m}\lt {\it n}\}-部分ファジー論理だからこれは我々の目的に見合う論理である。

また論理結合子の解釈を固定したファジー論理\it Aと[0,1]の部分集合\it Sについて、全ての\it f\in {\rm range(}ConnectiveInterpretation_A{\rm)}が\it {\rm image}_f{\rm(}S^{\ n}{\rm)}\subset Sを満たすとき、\it Aは自然に\it S-部分ファジー論理にもなる。これをファジー論理の制限とでも呼ぶことにする。

5.制限されたファジー論理と古典論理および有限多値論理との比較

定義から古典論理はどのような擬古典的なファジー論理の制限としても得ることができる。

では有限多値論理はどうだろうか？

ファジー論理の制限のうち、有限集合、とくに\{\frac{\it m}{{\it n}-1}:0\leq {\it m}\lt {\it n}\}（さらにn=2とすれば三点集合\{0,0.5,1\}）への制限を考えると多くの知られた三値論理を得ることができる。

例えば三章で導入したGodelファジー論理の三値への制限はGodel論理(の三値版)を生み出し、K_\inftyの制限はKleeneの強三値論理（K_3）となる（それぞれ計算してみよ）。

Lukasiewiczの\it n値論理を得るのはもう少し難しい。

Lukasiewiczの\it n値論理の含意に対応するファジー論理はLukasiewicz t-normによるものなのだが、連言と選言についてはGodel t-norm（の制限）を使っている。

つまりLukasiewiczの三値論理に対応するファジー論理（Lukasiewiczファジー論理といいます。）は二つの連言と選言を持っており（Lukasiewicz t-normによるものを強い連(選)言、Godel t-normによるものを弱い連(選)言と言う。）、有限値論理版では強い連言による連言と選言および弱い連言による含意は忘れられてしまっているのである

なおBochvarの三値論理はこの形では実現できない。これは選言の解釈の1の単位性も否定の解釈の単調減少性も成り立たないからである。

最後にこれらのような有名どころではないが、現在僕が考えている論理についても少し触れておこう（ネタばらしをすれば、ファジー論理を調べたのはこの論理をファジー論理の研究の文脈に位置づけたかったからであった）。

僕はK_3に新たなArityが1の論理結合子\mathbb{E}を加えた論理を考えている。

その解釈は固定されており、

{\it ConnectiveInterpretation}(\mathbb{E})({\it x})=\begin{cases}1\ ({\it x}=1\lor{\it x}=0)\\0\ ({\it x}=0.5)\end{cases}

である。

このモチベーションや直感はいくつもあるが、一つ挙げるならば、K_3における真理値0.5が直感的意味付けとしては「計算中」に対応しているにもかかわらず、「では計算は終わったか？」と問いかける役割を果たす論理結合子はK_3には無いため\mathbb{E}がその役割を果たすというものである（\mathbb{E}の直感的解釈は二通りあり、時相を導入して「『今』、計算は終わっているか？」と問うものだという解釈と、「計算はいずれ終わるか？」というTuring oracleのようなものだという解釈があり得る）。これは特にCSへの応用を考えると自然な対象であり、CSの文脈でK_3（に似た体系？）がデータベース処理（例えばSQL）などに使われることがある（らしい）が、その場合「マージされる直前の処理が終わっているか？」と問いかけることは自然だからである。

K_3にこの\mathbb{E}を追加したものをEK_3と呼ぼう。

実はEK_3は（つい先ほどLukasiewiczの三値論理を理解するときにそうしたように）K_3にLukasiewicz t-normと解釈される選言（以下では\dot{\land}で表記する。）を追加した体系（以下ではXK_3と書く。）と本質的に同じ（definitional extension）であることが以下からわかる。

まずXK_3において

\mathbb{E}x\Leftrightarrow x\dot{\lor} x\to x\dot{\land} x

と定義して解釈すれば、これはEX_3における\mathbb{E}の解釈と外延的に等価であるし、逆にEK_3において

x\dot{\land}y:\Leftrightarrow (\mathbb{E}x\land x\land y)\lor(\mathbb{E}y\land y\land x) 

 x\dot{\lor}y:\Leftrightarrow \mathbb{E}x\lor\mathbb{E}y\to x\lor y

と定義すればこれはLukasiewicz t-normとして振るまう。もともとK_3はLukasiewiczの三値論理と含意の解釈のみが違うのだったから、EX_3やXK_3は（論理結合子を減らす前の）Lukasiewiczファジー論理（の制限）において、含意の定義に使う論理積をLukasiewicz t-normからGodel t-normに変えて、しかも定義を残余ではなく整合性だと思った（ここでLukasiewicz t-normは含意を残余で定義しても整合性で定義しても同じになるという性質を思い出そう）ものだと言えるのである。このことからEK_3やXK_3はK_3やK_\inftyと違い、恒真式を持つこともわかる。これは（含意の定義としてそれを使っていないだけで）Lukasiewiczの論理の含意に当たる関数が定義できるからである。

さらに先に少しふれたとおり（今さっき「第二の」論理和論理積を追加したのと同じ考え方で）「第二の否定」としてGodel negationと解釈される否定（以下では\dot{\lnot}で表記する。）を追加するという考え方もある。この体系はGK_3と呼ぶことにする。

このとき

\mathbb{E}x\Leftrightarrow\dot{\lnot}x \lor\dot{\lnot}\lnot x

\dot{\lnot}x\Leftrightarrow \lnot x\land\mathbb{E}x

が先ほどと同様の意味で成り立つ。すなわちK_3のそれぞれモチベーションの異なった3つの拡張がある意味では一致するのである。

ここからは完全に余談になるが、一度このように形式化された意味論を考えるのをやめて、思想を考えることにしよう。

特に\mathbb{E}は本当にLukasiewicz t-normと等価だと思っていいのかという事についてである。

\mathbb{E}は計算が終わっている（もしくは終わる）のかどうか、言い換えれば古典的、決定的な値なのかを調べるという直感的意味を持っていた。それに対応する論理積があるとすればむしろ激烈和（定義は上述のWikipediaのリストを参照）であるべきではないか？

実は激烈積は三値に制限した時に限ってはLukasiewicz t-normと一致する。したがって三値という値の数が今の場合は足りず、我々は本質を見逃した可能性がある（このようなことは普通にあり得る。何しろこの章の冒頭で述べたように全ての擬古典的なファジー論理は二値的な（つまり古典論理への）制限を考えれば同じになってしまうのだから。三値論理は違いを見出すには古典論理に近すぎた可能性があるわけである。）。僕はこの後、もう一度K_\infty（もしくはそれの3より大きい\it nに対する\{\frac{\it m}{{\it n}-1}:0\leq {\it m}\lt {\it n}\}への制限）に戻ってこのあたりをもう少し試してみるつもりである。

6. 後書き、謝辞

アドベントカレンダー遅くなって申し訳ありませんでした。

今回はファジー論理の話でした。

僕にとっても慣れないファジー論理で実は途中まで大間違いをしており、Godelファジー論理を誤ってK_\inftyだと誤解しており、研究室の先輩から「おかしくないか？」と指摘されて含意の定義が残余であることに気づいた経緯があります。

先輩ありがとうございました。

今回内容について直接助力いただいたのはその先輩のみですが、よく話しては多くの示唆をくれる多くの友人にいつもながら感謝しています。

数学をやるのに必要なのは、ホワイトボードとネット環境と良い師や友人と、それに歩き回れる広さのある喫煙スペースだなあ（勿論本来はまずいのだが、僕はJAISTの駐車場周辺を徘徊しながら歩き煙草して考えをまとめている。）というところで、記事を終わらせていただきたいと思います。

いつも通り誤りの指摘等はtwitter(@sanjutsu_yu)までお願いします。

参考)

・Stanford Encyclopedia for Philosophyのfuzzy logicの項目

https://plato.stanford.edu/entries/logic-fuzzy/

・日本語版Wikipediaのファジィ論理及びファジィ集合及び3値論理及びゲーデル論理の項目

https://ja.wikipedia.org/wiki/%E3%83%95%E3%82%A1%E3%82%B8%E3%82%A3%E9%9B%86%E5%90%88

https://ja.wikipedia.org/wiki/%E3%83%95%E3%82%A1%E3%82%B8%E3%82%A3%E8%AB%96%E7%90%86

https://ja.wikipedia.org/wiki/3%E5%80%A4%E8%AB%96%E7%90%86

英語版WikipediaのFuzzy logic,T-norm,T-norm fuzzy logic,Fuzzy set,Three-valued logic,Four-valued logic,Intermediate logic,Lukasiewicz logic,Godel logicの項目

https://en.wikipedia.org/wiki/Fuzzy_logic

https://en.wikipedia.org/wiki/T-norm

https://en.wikipedia.org/wiki/T-norm_fuzzy_logics

https://en.wikipedia.org/wiki/Fuzzy_set

https://en.wikipedia.org/wiki/Three-valued_logic

https://en.wikipedia.org/wiki/Four-valued_logic

https://en.wikipedia.org/wiki/Intermediate_logic

https://en.wikipedia.org/wiki/%C5%81ukasiewicz_logic

https://en.wikipedia.org/wiki/G%C3%B6del_logic

継続に関する感想

どうもAaronです。

今回はちょっと継続について考えていて思ったことがあるので書きます。

証明どころか解説ですらないどころか感想なので決して真に受けぬよう。

1.束縛付き継続スタック付きマシン

束縛付き継続スタック付きマシンとはTuring完全なマシン\it M(マシンモデルはここではあまり重要ではない)と「引数を表す\it Mのデータ(値)(ラムダ計算ならラムダ項、帰納的に定義された関数やレジスタ機械なら自然数…)の可変長リストと継続(\it Mのプログラム、関数…etc)の組が積まれるスタック\it S」と「束縛(シンボルと\it Mのデータの組)のリスト\it B」の組({\it M},{\it S},{\it B})である。

\it Mが行う処理は「原始的な処理」と「処理の合成」に分けられる。

直感的には原始的な処理は組み込み関数、処理の合成はユーザー定義の関数である。

\it Mは\it Bの環境下で挙動し、\it Sに積まれた処理を上から順に実行する。原始的な処理ならばそれは直ちに実行され、逆に処理の合成ならばそれはより簡単な処理に分解され\it Sに積まれ、それぞれの処理の結果を表すために「衝突のないシンボル」が予約される。従って処理の合成はそれ単体として解決されるものではないが、再び同じ場所まで\it Sが進行したとき処理の合成が終了したとみなす。このため、ある原始的な処理の終了が処理の合成の終了でもあるという事が起きる。さらに言えばある原始的な処理の終了によって複数の処理の合成が同時に終了することもある。実在機械の実装上は\it Sに処理の合成を分解したことを表すマーカー(呼び出しマーカーとでも呼ぶことにしよう)を積むことでこれを実装するかもしれない。

原始的な処理であれ、処理の合成であれ実行を終わるとその返り値を「事前に予約された衝突のないシンボル」に束縛するように(こうしておかないと多変数関数の呼び出しで複数の関数コールが同時に発生したときとかに困る。)\it Bを更新し、\it Sをポップし新たな処理を行う。

(e.x.

(f (g x) (h y) (i z) 4)

なら

 

\it S

(g x)

(h y)

(i z)

(f temp1 temp2 temp3 4)

 

という感じにスタックに積まれて処理される。

)

 

ある処理がほかの処理の合成に分解されるか、それ以上分解できないものとして(一般には値を返して)スタックから取り除かれるかはそのモデルに依存する。

 

このモデルの下でいくつかのプログラミング言語の概念を説明してみよう。

 

2.動的寿命

「衝突のない予約されたシンボル」に束縛された値がもう呼び出されないとわかったならそれを\it Bから取り除いても問題ない。GCがあるような実用プログラミング言語においてはこれを管理して「もう呼び出されない(動的寿命を終えた)」値を\it Bから取り除く。

3.副作用

\it Mに\it Bを強制的に変更するような挙動があることをゆるすならば、そのような挙動を副作用と呼ぶ。(例：定義、代入…etc)

4.継続に関する副作用

\it Mに\it Sを強制的に変更するような挙動があることをゆるすならば、そのような挙動を継続に関する副作用と呼ぶ。(例:call/cc、条件分岐(後述))

5.継続による条件分岐

理論的には「ラムダ計算による『純粋関数型的な』if」や「再帰的に定義された関数による『純粋算術的な』if」が可能であるにも関わらず、ほとんどのプログラム言語では利便や簡単性のためそのようなifではなく、継続のダイナミックな変更によるifを実装している。そのため理論と異なり関数型言語で副作用やcall/ccを用いないコードであってもifの内側を先に評価してよいことにはならないのである。

 6.末尾再帰最適化

末尾再帰最適化とは「処理の合成」がスタック上で分解されたときにスタックの容量を節約するため、ある処理の合成Pの解決中、Pを構成する処理のうち構文上「最後に処理される」処理P’を呼び出したときP'の呼び出しマーカーと引き換えにPの呼び出しマーカーをオミットしてしまうことである。これによりP’がPの本来の継続から呼び出されたのと同等になる。

AARASS-REGI名称設定・仕様更新

今回はずいぶん前から作ってはアドバイスを貰ったり、紹介したりしていたレジスタマシン

 

takumim97.hatenablog.com

 

に大幅アップデートを入れましたのでまとめておきます。(PDFはTwitterだと共有が面倒くさいので、もうブログにしてしまえホトトギスとこうなりました。)

また今回の仕様からこの仕様および仕様の実装を”AARASS-REGI"と呼称することにし、過去のものも遡ってそう呼びます。

とりあえず現物がないと読んでても何も面白くないのでオンラインIDEで実装したURLがこちら

→https://repl.it/@takumim97/7th-register-machine#main.scm

(コードが目に晒せるサイトとして使ってますが1000行を超えるコードを書くとこのサイトまともに動かないのであとでなんかいい方法を考えます。githubってソフトの共有には向いてるけどこういう実装を合わせてみてもらいたいコードの共有ってどうなんでしょうね…。というか大まかにはブラウザ上で動くJSのインタープリターのはずなのに、なんで1000行やそこらでこんなに重いんでしょう…?アプリとブラウザタブの開きすぎで僕のローカル環境が重いだけって説あります?)

1章.AARASS-REGIについて

1.1 名称・経緯

このAARASS-REGIの仕様や実装を「Aaronさんのレジスタマシン」と呼んでくださる方がいてうれしいのだが、実は一つ悩みがあった。

AARASS-REGIの最大の特徴であると思われる、「ジャンプを(それ専用の命令を用意するのでなく)自然に考えるとpartial functionになるdecr命令のフォローとして用意することによって命令数が減っている」という特徴は、実は僕の学部時代に計算理論の講義を担当していただいた新井敏康先生の講義及び著書で見ることのできるレジスタマシンからいただいたアイデアである(ただし新井先生のレジスタマシンには無条件ジャンプのGOTO命令は存在していた)。また前回までの入出力方法やメモリの初期状態についての制約もまた新井先生のレジスタマシンと同一である(ただし後述するようにこの部分は今回大幅に変更されている)。このようなことからむしろ僕はこれを「新井先生のレジスタマシン」と呼んでいたのである。

しかし新井先生のオリジナルの方のレジスタマシンは「save命令が存在しない。」「halt命令が存在せずプログラムファイルのEOFで停止する。」、「AARASS-REGIでいうincr,decrの引数の「値の表現」がなく、常に1とみなされる。」、「ポインタやラベルなどといった高級な表現はなくすべて自然数で処理される。」、「そもそも機械上の実装を伴ったものではなく仮想上のモデルである。」など、現在のAARASS-REGIとはかなり異なったものである(しかしながら実は僕が開発を始めた当初はAARASS-REGIのようなものを定義するつもりはなく、新井先生のオリジナルのレジスタマシンの実装を目指していた。表現力が貧弱すぎてプログラマの能力と実行時間を考えると事実上まともなプログラムを書けない事の解決策としてAARASS-REGIの初期版が生まれたのである。)。また新井先生本人に確認してみたところ、decr(新井先生のオリジナル版ではDECREMENT)のこの仕様は先生ご自身のアイデアではないらしく、これらのことからAARASS-REGIを「新井先生のレジスタマシン」と呼ぶのはかえって失礼であろうとも思える。そこでこの"AARASS-REGI"の名称を作成した。このレジスタマシンに影響を与えた三つの要素、すなわち実装者である僕自身(Aaron)、キーアイデアを与えてくれた新井先生、そして仕様を拡張する際参考にしたアセンブリ言語からちょうど三字ずつとって組み合わせたものである。

1.2 パラダイム・思想

AARASS-REGIは以下の特徴がある。

1.レジスタマシンとして挙動するチューリング完全なヴァーチャルマシンである。
2.極端に小さな命令セットと、極めて明瞭な操作的意味論を持つ。
3.各AARASS-REGIの実装は実行時に確保できるレジスタの最大個数や一つのレジスタに格納できる自然数の大きさの限界、許容されるプログラムファイルの長さを陽に制限・宣言する必要はなく、実行環境が許す限りとしてよい(がそうすることをAARASS-REGIの仕様として要求するわけではない)。
4.2と3から実装が極めて容易である。

AARASS-REGIはBrainfuckやその亜種と同様に、この命令セットでプログラムを行おうとする者にとってではなく、この処理系を実装する者にとって容易であることを目指すのが特徴と言える。

1.3 命令ファイルの書式とパーサーについて

本記事はAARASS-REGIの命令ファイルの書式とそのパーシングについて、全く何も規定・要求しない(が提案や推奨や許可はするかもしれない)。

各AARASS-REGIの実装は独自の仕様の命令ファイルとそのパーサーを持ってよいし、パーサーを持たず、ヴァーチャルマシンを構築するプログラム上のデータとして命令を管理する実装があってもよい(僕の手元の実装はそうである)。

AARASS-REGIはあくまでもマシンモデルと命令セットとその挙動の仕様である。

1.4 レイヤー構造

AARASS-REGIを動作させる命令表現は、仮想機械を実際に動作させる「コア命令表現」と、コア言語にいくつかの拡張表現を追加したものであり、ごく小さなコンパイラーによってコア言語に簡約される「拡張命令表現」と、さらに高級な表現仕様を含んだ「マクロ表現」に分類される。この記事ではコア言語に要求される仕様について述べる。拡張命令表現およびマクロ表現については別記事を出す。

「AARASS-REGIの実装」とはコア命令表現によって挙動する仮想機械及び拡張命令表現をコア命令表現に、マクロ表現を拡張命令表現に簡約する二つのコンパイラーの組の事を指す。ただし各実装は必要に応じてマクロ表現のコンパイラー、場合によってはさらに拡張命令表現のコンパイラーをも省略してもよい。

2章.基本語彙

2.1 プログラム

AARASS-REGIが処理する(コア命令表現による)プログラムは「命令」の任意の長さの(0-basedに)自然数で添字づけられた列である。プログラムの終わりは必ずしも明確に定義される必要はなく、無限に空命令(後述)が続くように見なしてもよい。

2.2 命令

命令は以下のいずれかの命令ジェネレータ

「incrジェネレータ」

「decrジェネレータ」

「haltジェネレータ」

「emptyジェネレータ」

「putnジェネレータ」

「putcジェネレータ」

にそれぞれ規定される数の引数の表現を続けたものである。各命令ジェネレータについては3章で述べる。

2.3 レジスタ

レジスタはAARASS-REGIの記憶領域であり、整数で添え字づけられている。

全てのレジスタには自然数が格納されている。

またレジスタのうち負の添字(番地)を持つものにはプログラム実行のどの段階でも常に0が格納されており、命令によって値を書き換えられても直ちに0に戻る(ただし書き換えようとする試みがエラーするわけではない)。

実装は-1より小さい番地のレジスタをサポートしなくてもよい。

3章. 命令表現

この章では命令がどのように表現されるかに焦点を当て、各命令の効果は大まかに述べるにとどめる。各命令が詳しくどのような効果を持つかは4章で操作的意味論の一部として与える。

3.1 incr命令

incrジェネレータに「レジスタの表現」と「値の表現」を与えたものがincr命令である。

実装は「値の表現」がない形式のincr命令を許してもよい。その場合「値の表現」として即値の1を受け取ったように見なすことを要求する。

incr命令は大まかには与えられたレジスタに格納された値を増やす命令である。

3.2 decr命令

decrジェネレータに「レジスタの表現」と「継続の表現」と「値の表現」を与えたものがdecr命令である。実装は「値の表現」がない形式のdecr命令を許してもよい。その場合「値の表現」として即値の1を受け取ったように見なすことを要求する。

decr命令は大まかには与えられたレジスタに格納された値を減らす命令であるが、自然数には下限0があるためこの命令は失敗することがあり、その場合にジャンプが引き起こされる。

3.3 save命令

saveジェネレータに「レジスタの表現」と「値の表現」を与えたものがsave命令である。

save命令は大まかには与えられたレジスタに格納された値を強制的に変更する命令である。

3.3 putn命令

putnジェネレータは「値の表現」を受け取りputn命令を作る。

putn命令は大まかには値を出力する命令である。

3.4 putc命令

putcジェネレータは「値の表現」を受け取りputc命令を作る。

putc命令は大まかには文字を出力する命令である。

3.5 halt命令

haltジェネレータは追加の表現を必要とせず、単独でhalt命令を作る。

3.6 空命令

emptyジェネレータは追加の表現を必要とせず、単独で空命令を作る。実装はemptyジェネレータ用に記号を用意せず、空白を持ってこれに変えてもよいし、それが推奨される。

空命令は大まかには「何もしない事」を表す命令である。

3.7 値の表現

各AARASS-REGI実装は値の表現として少なくとも以下の3種類をサポートしなくてはならない。

1.即値表現

自然数の表現を書き込まれ、そのまま値として用いる表現。

2.直接参照表現

整数の表現を書き込まれ、「それを番地に持つレジスタに格納されている自然数」を値として用いる表現。

3.間接参照表現

整数の表現を書き込まれ、「『それを番地に持つレジスタに格納されている自然数』を番地に持つレジスタ」に格納されている自然数を値として用いる表現。

3.8 レジスタの表現

各AARASS-REGI実装はレジスタの表現として少なくとも以下の2種類をサポートしなくてはならない。

1.インデックス

整数の表現を書き込まれ、「それを番地に持つレジスタ」をレジスタとして用いる表現。

2.ポインタ

整数の表現を書き込まれ、「『それを番地に持つレジスタに格納された自然数』を番地に持つレジスタ」をレジスタとして用いる表現。

3.9 継続の表現

継続の表現は値の表現と同等の表現能力のものを要求する。

4章. AARASS-REGIの操作的意味論の概要

4.1 プログラムカウンタ

AARASS-REGIの操作的意味論にはプログラムカウンタ(以下PC)と呼ばれる自然数が重要な役割を果たす。

PCは直感的に言えば「次に実行するべき命令の添字」である。

AARASS-REGIのコアマシンがなんらかのプログラムの実行を始めたときはいつでも、PCは0である。

動作中のAARASS-REGIコアマシンは命令実行中でない場合、PCに等しい添字が割り当てられた命令を探して実行しはじめるが、その直前にPCを1だけ増やす。

そしてその命令の実行が終わると、またPCに等しい添字の命令の実行を行おうとする。

命令のうちdecr命令(後述)だけがプログラムカウンタを強制的に変更する可能性がある。

 

以降では命令について述べる。

 

4.2 incr命令

incr命令の実行は、「受け取ったレジスタ」に格納された値を、「受け取った値」だけ増加させる。

4.3 save命令

save命令の実行は、「受け取ったレジスタ」に、「受け取った値」を格納する。

4.4 decr命令

decr命令の実行には「成功」と「失敗」が存在する。

decr命令の「受け取った値」が「受け取ったレジスタ」に格納されている値以下ならばdecr命令は成功し、「受け取ったレジスタ」を「受け取った値」だけ減少させる。

逆に「受け取った値」が「受け取ったレジスタ」に格納されている値より大きけれならば、decr命令は失敗となる。

decr命令は失敗するとレジスタは一切書き換えず、PCを「受け取った継続」に変更する。

4.5 空命令

空命令の実行はレジスタもPCも変更しない。

4.6 halt命令

halt命令も空命令同様レジスタもPCも変更しない。

halt命令が空命令と違うのは、halt命令が実行されたとき、AARASS-REGIコアマシンは動作を終了することである。

4.7 putn命令・putc命令

putn命令及びputc命令は内部状態に関しては完全に空命令と同一である。

しかるにputn命令及びputc命令の実行は「受け取った値」を外部に出力する(「出力」は本記事では定義されない。各実装が対応するデータないし標準出力を含むファイルを割り当てること)。

putn命令は「受け取った値」を自然数として、人間が視覚的に数だと認識できる形式で出力するものである。この書き方はいささか解釈の余地があるが2進数、8進数、10進数、16進数のいずれかが標準的であろう。

putc命令は「受け取った値」を何らかの文字コードを通して文字として出力する。使用する文字コードをこの仕様が規定することはしない。

4.7 初期化

AARASS-REGIコアマシンは、プログラムの実行開始に際して全てのレジスタとPCを0に初期化することを保証する。

 

拡張命令表現仕様→

 

takumim97.hatenablog.com

 マクロ表現仕様→

 

takumim97.hatenablog.com

 

参考)

新井敏康著,数学基礎論 = Mathematical logic,岩波書店, 2011.5

(実際に直接参考にしたのは先生が講義で扱ったものですが、ほとんど同様のものがこちらに出ています)

 

AARASS-REGIマクロ表現仕様

本記事はAARASS-REGIのマクロ表現の仕様について述べる。

1章. 概要

1.1 概要

AARASS-REGIマクロ表現は、AARASS-REGIコアマシンで挙動するある程度実効的なプログラムを書くための助けとするための拡張表現である。

1.2 非単純拡大性

マクロ表現と拡張命令表現の関係は、拡張命令表現とコア命令表現の関係とはきわめて異なっている。

ある拡張命令表現、それどころかあるコア命令表現はマクロ表現として非妥当である。

そのためマクロ表現は拡張命令表現の単純な拡大ではない。

1.3 マクロ表現の仕様策定方針

マクロ表現は各AARASS-REGI実装が自由に拡張してかまわない。ここで要求する機能は最低限の要求としての意味しかない。

また要求する機能の効果もごく大まかに指定するにとどめる。実際の効果は実装に任せる。

2章. 追加・変更される概念

2.1 行

マクロ表現では行の概念が拡張される。BNFで書けば以下の通りである。

<ラベル無し行>:=<命令>|<宣言文>|<ブロックジェネレータ>

<行>:=<ラベル無し行>|<ラベル形式><ラベル無し行>

拡張命令表現の時と同様、実装は複数のラベルがある行を許すよう拡張してもよい。

2.2 シンボル

シンボルは直感的に言えば文字列の事である。

マクロ表現ではユーザーが自分の理解の助けとなる名称をレジスタやブロックにつけることが可能になるため、それらの名前として用いられる。

2.3 宣言文

宣言文は静的に解析され、それ以降のプログラムで有効になるある種のマクロを定義するものである。

宣言文は命令ではなく、静的に解決される。

ブロックジェネレータが作るブロックを超えて宣言文の効果が伝播することはない。

2.4 ブロックジェネレータ、ブロック

ブロックジェネレータにはさらに「オープンブロックジェネレータ」と「クローズブロックジェネレータ」が存在する。

対応する「オープンブロックジェネレータ」と「クローズブロックジェネレータ」に囲まれたプログラムの領域を「ブロック」と呼び、ブロックを超えて宣言文の効果は伝播しないという性質を持つ。

直感的にはブロックとは「ひとまとまりの手続き」の事である。

ブロックには「手続き名」が与えられる。

ブロックの中でさらにブロックを作ろうとした場合の効果は未規定である。実装はこれを高級言語におけるローカル関数のように解釈することにしてもよいが、それを要求はしない。

3章. マクロ表現の仕様

3.1 コア命令表現及び拡張命令表現では要求されたがマクロ表現ではサポートを免除される仕様、およびプログラマへの注意事項

以下のような点でマクロ表現の仕様はコア命令表現や拡張命令表現のそれと異なる。

1.継続の表現としての即値の不許可

マクロ表現は「継続の表現」に即値を使うことを許可しなくてよい。

これはマクロ表現を拡張命令表現にコンパイルする際には行数がずれる為である。

また同じ理由で、プログラマは継続をレジスタに積む場合などでも、マクロ表現の行数を数えて行うのはバグの可能性があることを知るべきである。特殊な場合を除き継続を表す数が欲しい場合は、いつでも必ずラベルを用いて行うことが求められる。

2.レジスタおよび継続の0以外への初期化の許容

マクロ命令表現のコンパイラーはプログラマーにとって不可視な方法でレジスタや継続の「見た目上の初期値を0以外」にするような形式にコードをコンパイルすることが許されている。

プログラマーは必要に応じて明示的に初期化をする必要があるかもしれない。

3.内部処理用のレジスタ・ラベルの存在

マクロ表現をコンパイルして得られる表現はプログラマが明示したレジスタの挙動だけでなく、マクロ表現に要求される挙動を達成するための内部処理にもレジスタを用い、その値を変更するであろう。ラベルも同様である。

実装は内部処理に用いるレジスタとプログラマが安全に用いることができるレジスタを区別できる方法を提供するべきである(例えばプログラマに奇数の番地のレジスタを使うことを要求するなど)。しかしこのような工夫のいずれかを仕様として要求するわけではない。実装は、コンパイラーが作ったのでない命令が内部処理に用いるレジスタを破壊することをエラーとしてもよい。が、これも要求はしない。

同様にラベルについてもプログラマーが安全に使えるラベル表現を指示するべきである。

逆にプログラマは内部処理に用いるレジスタを破壊した場合、あるいはそのようなラベル表現と同一のラベル表現を用いた場合、この記事の、あるいは実装の保証する仕様通りの挙動が得られるとは限らない。これを避けるのはプログラマの責任である。

3.2 hold宣言

hold <シンボル>

という形式は宣言文でありhold宣言と呼ばれる。

hold宣言はプログラムまたはブロックの先頭、あるいはほかのhold宣言の直後でのみ妥当である。

hold宣言は受け取ったシンボルに未使用のレジスタを対応させ(これをレジスタをシンボルにholdするという)、それ以降のプログラムでレジスタ番地として整数を指定する代わりにそのシンボルを使うことを許可するマクロを生成する。

同じブロック内で、もしくはプログラム先頭で複数回同じシンボルにレジスタがholdされることの効果は未規定である。実装はエラーを通知しても、単に無視してもよいし、そのたびに新たにレジスタを割り付けてもよい。

実装はシンボルを使ったレジスタ、値、継続の表現の為に番地を直接使ったものとは異なった文法を用意してもよい。

実装は初期状態ですでにレジスタをholdしているシンボルを用意してもよい。またそのような形でholdされているレジスタを0以外に初期化することにしてもよい(逆にシンボルにholdされていないレジスタを0以外に初期化することは避けるべきである。が、厳密に禁止はしない。)。

例としてコア命令表現の仕様記事の冒頭に貼ったRepl.itで読める僕の実装は初期状態で0番地をreturn(これを関数の返り値を渡すのに使っている)、4番地をstackpointer(内部で関数スタックを組むために使っている)、8番地をtemp1、12番地をtemp2というシンボルに束縛しており、stackpointerは0でなく2に初期化される。

また実装はプログラマがholdされているレジスタを気づかずに使うことを防ぐため、holdされる可能性があるレジスタとないレジスタを区別できる工夫をするべきである(例えばholdは4の倍数番地のレジスタしか確保しないとするなど)。しかし、そのような工夫のいずれかを仕様として要求するわけではない。

またhold宣言が確保したレジスタが0に初期化されることは要求されない(がそういう実装があっても良い)。そのレジスタはもし以前に他の処理に使われていたならばその時の値がクリアされずに残っているかも知れない。

3.3 begin_defun,end_defun

begin_defun <シンボル(関数名)> <シンボル(引数名)>

<行>*

end_defun <シンボル(関数名)>

という形式でブロックを生成できる。このブロックにはbegin_defunの後ろに続くシンボル(関数名)が「手続き名」として割り当てられる。

このとき

begin_defun <シンボル(関数名)> <シンボル(引数名)>

はオープンブロックジェネレータ、

end_defun <シンボル(関数名)>

はクローズブロックジェネレータである。

「引数名」にあたるシンボルは後述するcall命令で値を書き込まれることを除いては、begin_defunの直後にレジスタをholdしたのと同じ状態になる。

3.4 begin_main,end_main

begin_main

<行>*

end_main

という形式でブロックを生成できる。このブロックにはシンボル"main"が「手続き名」として割り当てられる。

このとき

begin_defun

はオープンブロックジェネレータ、

end_defun

はクローズブロックジェネレータである。

マクロ表現をコンパイルして得られるコア表現をコアマシンに与えた場合、コアマシンは(プログラムファイルの先頭からでなく)"main"手続きの頭部から実行を開始する(かのようにジャンプで飛び込む)ようにコンパイルされる。

3.5 call命令

call <手続き名> <値の表現>*

の形式で、それより上方で定義されたか前方宣言された<手続き名>を割り当てられたブロックを実行することができる。

当該ブロックが「引数名」を持っていた場合、<値の表現>がそのシンボルにsaveされたうえで実行が始まる。

callは再帰的に呼び出されるかもしれない。即ちあるブロック内で自分自身を呼び出したり、前方宣言を利用して二つ以上の手続きが相互にお互いを呼び出し合うかもしれない。

あるブロック内でcallされたブロックは、呼び出し側のブロック内でholdされたレジスタを参照することも書き換えることもないことが保証されている。これは再帰的なcallが行われた場合も変わらない。すなわち再帰的なcallが発生した場合、hold宣言やbegin_defunの引数はシンボルにそのたびに新たなレジスタを割り付ける。

callの解決後には呼び出し前に割り付けられていたレジスタに割り付けが戻される。

3.6 前方宣言

 front_declare <関数名> <引数名>*

の形式は宣言文であり、前方宣言と呼ばれる。

前述したようにcall命令はそれ以降に定義された関数を呼び出せないため、そのままでは相互再帰的な呼び出し等はできない。

そこで前方宣言を呼び出したい位置より前に記述することで、「まだ定義されていない関数」を呼び出せる。

前方宣言した関数を実際に定義するときには以下の一点を除いて通常通りbegin_defun、end_defunを使えばよい。―即ち引数をもう一度宣言する必要はない。

ブロックジェネレータと同様、前方宣言もブロックの中で行われた場合の効果は未規定である。

 

AARASS-REGI拡張命令表現仕様

この記事ではAARASS-REGIの拡張命令表現の仕様を述べる。

1章. 概要

1.1 概要

AARASS-REGI拡張命令表現は、プログラマーにフレンドリーでないAARASS-REGIのコア命令表現を多少扱いやすくするための拡張である。

1.2 単純拡大性

AARASS-REGI拡張命令表現は、コア命令表現の単純な拡張になっていなければならない。即ちすべてのコア命令表現は拡張命令表現でもなくてはならない。

2章. 追加される概念

AARASS-REGI拡張命令表現を理解するためには、コア命令表現にはなかった概念が一部必要になる。

2.1 行

拡張命令表現では新たに「行」という概念が導入される。

行はBNFでは以下のように定義される。

<行>:=<命令>|<ラベル表現><命令>

直実装は複数のラベル表現を一つの行につけることを許してもよい。即ち

<行>:=<命令>|<ラベル表現><行>

などとなるように拡張してもよい。

なお、コア命令表現についての仕様の記事で述べた通り、この仕様は命令ファイルの書式やパーサーの仕様には言及しないため、実際に「行」をファイル上の「行」として定義することは義務ではない。同様にラベル表現と命令の間に区切り文字を用いるかどうか、用いるとしたら何を用いるかなども実装が定めてよい。

コア命令表現の仕様で、プログラムを命令の列としていたところ拡張命令表現としていたところ、拡張命令表現ではプログラムは行の列となる。命令も行の一種だからこれは単純拡大性に違反しないことに注意せよ。

2.2 ラベル

ラベルはコア命令表現でプログラムを書く際、「継続の表現」を書くためにプログラムの行数をいちいち数えねばならないという問題を解消するため、行にタグをつけるものである。

概念としてのラベルは「ラベル表現」と「ラベル値」という2つからなる。

ラベル表現とは行につけたタグの事である。

ラベル値とは「値の表現」や「継続の表現」として「タグをつけた行番号」を呼び出すことである。

実装はラベル表現として付けるタグの形式を自由に定めてよいし、「ラベル値」の表現としてタグそのものを用いることにしてもよいし、適当な接頭詞、接尾辞をつけたり外したりしたものを用いることにしてもよい。

3章.追加される表現

「値の表現」および「継続の表現」の両方に以下を追加する。

3.1 ラベル値

2.2で解説した通りである。

3.2 プログラムカウンタ値

値及び継続の表現にプログラムカウンタ(PC)の値を用いることが許される。仕様上命令実行中のPCは常に「命令のあった行番号+1」だから、この表現は静的にコンパイルできることに注意せよ。