2020-07-22

NFAを実装するSchemeコード

どうもAaronです。

またSchemeでおもちゃ作ってたので紹介記事を書きます。

NFA(非決定型有限状態オートマトン)を生成するプログラムです。

モノはこちら(Repl.it)→https://repl.it/@takumim97/automata#main.scm

予備知識(Schemeの外部表現)

主題とは関係ありませんがこれがわかってないと自分でオートマトンをデザインできないのでほんの少しだけ触れます(なおSchemeについての解説ではないので今回関係がある部分のみです。)

Schemeではプログラム中に’(クオート)に続けて「外部表現」と呼ばれる表現を書くことでScheme内部のデータ構造を人間にとって視覚的な表示で入力することができます(これはSchemeの意味論にとって正確な物言いとは言えないかもしれないが)。

そのなかでも今回使う引数の形式に対応する外部表現は以下のようになります。

(<object1> <object2> <object3> …)(object1,object2,object3,...は他の外部表現)

object1,object2,object3,...からなる「リスト」の外部表現です。

(<object1> . <object2>)(object1,object2は他の外部表現)

object1とobject2のペアの外部表現です。

"string"

「string」という文字列の外部表現です。

#\γ(γはSchemeが認識可能な一文字)

「γ」という文字の外部表現です。

あとはRepl.itの下のほうにある僕のサンプル見ながら慣れてください。

create-automata手続き

(抽象構文)

(create-automata State-Set Initial-States Transition Accept-States)

(説明)

日本語版wikipediaの「非決定性有限オートマトン」の記事で導入された定義を参照することにします。

ここでcreate-automata関数は以下のようなオートマトンをエミュレートする手続きを生成します。

以下特に定義なく用いた記号や用語はwikipediaの当該記事で使われているものを指します。

(以下create-automata関数の入力仕様及び実現されるオートマトンの仕様)

$\Sigma$ (入力文字集合):Schemeが読み取れる文字のうち、" $\$$ "を除くすべて。勿論必要に応じてその適当なsubsetだと勝手に考えることは自由である。

$\rm S$ (状態集合):第一引数で与える「文字列のリスト」を状態集合として用いる。

$\rm S_0$ (初期状態集合):第二引数で与える。また唯一wikipediaの定義と今回の実装がわずかにずれているところ。この実装は複数の初期状態があることを許しているため、初期状態をリストの形式で受け取る。

$\rm T$ (遷移関数):第三引数で与える。「「「「読み込む文字」と「現在の状態」のペア」と「遷移先の文字」のペア」のリスト」という形式で受け取る。

$\rm A$ (受理状態):第四引数で与える。形式は $\rm S$ や $\rm S_0$ と同じである。

なお空文字列の記号として $\epsilon$ はIDEへの入力が面倒くさいため、代わりに $\$$ を用いた。

(以上)

前述の通り出力は手続きである。仮にtest-automataと呼ぶことにする。

test-automataは文字列一つを引数に取り、標準出力に「「上記のオートマトン」に「引数の文字列」を読ませた場合の操作的意味論」をエミュレートする。

2020-07-20

自己紹介(論理学友の会発表用)

今回の記事は論理学友の会での発表の時の自己紹介シート替わりです。

特に普段僕の記事を読んでくださってる方は、僕の生態を知りたい奇特な方以外はスルーしていただいて結構です。

名前:Aaron/アーロン/あーろん/sanjutsu_yu

年齢:23歳

好きな物:Ardbeg(ウイスキー)、もつ煮込み、アナログゲーム、Scheme(プログラミング言語)、レジスターマシン、直観主義論理

持病:アトピー性皮膚炎

所属:北陸先端科学技術大学院大学(JAIST)-先進科学技術研究科-情報科学専攻M2

→現在精神的不調に起因して持病を悪化させ、おまけに例の疫病のせいもあって実質的な休学状態。

専門:数理論理学(特に直観主義論理/計算論)

最近の興味:古典二値論理よりも弱い論理やその意味論。またそれを用いてCSや哲学において出現する、ある意味で「日常的な」問題を解釈すること。

→あまりテクニカルな数学内部の問題よりも、意味論やそれの日常的な出現を問題にすることが多い気がする。

2020-07-13

暗黙の型変換を嫌わないで!(暗黙の型変換がなぜ嫌われるのか、暗黙の型変換で数学的同一視を自然に表現する、暗黙の型変換もどきを自作する、暗黙の型変換で遊ぼう(BNFを表す型))

どうもAaronです。
皆さん、「暗黙の型変換」ってお嫌いじゃないですか？
まあ僕も基本嫌いなんですが…
今回は実は暗黙の型変換も
うまく使えば結構有用なんだよ、って話です。
なおいつも通り僕はあんまり主流なプログラミング言語を知らないので雰囲気が伝わるように疑似コードメインで書きます。悪しからず。

1.そもそも暗黙の型変換とは？なぜ嫌われるのか?

暗黙の型変換について知らない人も多いと思いますのでいくつか例を見ていきましょう。

例えば

int a = 2;
float b = 3.0;
printf(a<b);

と書くと少なくない言語では、aとbは型が違う変数であるにもかかわらず、そして<は同じ型の変数を取ると規定されているにもかかわらず(勿論この辺の規定自体が違う言語もあります。例えば動的型付き言語のSchemeでは、そもそもintやfloatという型がなく「整数」や「実数」という言葉を数学的なそれに近い意味で使うため、2と3.0を<で比較することに何の問題もありません。しかし取り合えずそういうツッコミは置いといてある程度多くありそうなプログラミング言語の仕様について考えることにします。)trueを出力します。
これは<に渡されたint型のaが、「勝手に」float型に変換された上で処理が行われる、という仕様になっているからです。
このようにユーザーが明示的に命令していないにもかかわらず、後の処理(特に比較系の処理に多い)に必要になるように型を合わせてしまう仕様の事を「暗黙の型変換」と言います。
これを聞くと「整数を対応する浮動小数点数に変えるぐらいで、いちいち型変換子をタイピングするのも大変だしいい機能なんじゃない？」と思う人もいるかもしれません。
いや実際そういう側面はありますし、だからこそ多くの言語の仕様に残ったんだと思いますが、このような仕様があまりに多いと大変なことになります。
特定の言語をdisる意図はありませんが、僕の知ってる範囲でもいくつかこれに型エラーでもfalseでもなく、なんとtrueを出力する言語があります。

string a="4";
int b=4;
printf(a==b);

まあ確かに入出力回りなどでこういう処理が欲しいことはありますが、そもそも型というのはユーザーが間違って意図しない処理を書いたら、それにすぐ気づけるというのが利点の一つなのにこれでは本末転倒です。
まあそういうわけで暗黙の型変換は古い時代のプログラミング言語の負の遺産と見做されることも多いのです。

2.暗黙の型変換で数学的同一視を自然に表現する

しかしながら実は暗黙の型変換には入力の手間を減らす以外にも有効で、しかも自然な使い道があります。
それは数学ではありふれている「同一視」という概念を自然に実装することです。
例えば次のような場合に暗黙の型変換が欲しいと感じるのは、むしろ自然なことに思われます。

a.数学的な同型(乃至埋め込み)がcanonicalに固定でき、同一視するべきオブジェクト

・・・例えば「 $\it GF_2$ とBooleanが別々の型として実装されているので、このお互いを自由に読み替えたい」とか「環 $\it R$ の型をその多項式環 $\it R{\rm [}X{\rm ]}$ の型の部分型と見たい」という要求は極めて自然です。これを達成する一つの手段として暗黙の型変換があります。

b.構文上異なる型に属するが、数学的な要求により同じであるとみなしたいオブジェクト(「型をまたぐ等号・型レベルの等号」の表現)

・・・これは次章で例を出します。

実際非常に数学的な言語であるCoqには暗黙の型変換をユーザー定義する機能があるそうで(僕はCoqは詳しくないので人から聞いた話になってしまいますが)、恐らくは「入力の手間を省く」というよりは(それも理由ではあるのかもしれませんが)、上に述べたような数学的な同一視の表現に使うことが想定されているものと思われます。このような暗黙の型変換で同一視された型をcoercion typeという(?)っぽいです。すいません、ここはあまり調べられていないのでツッコミあったらお願いします。
言うなれば「ものは使いよう」ということでしょうか？

3.暗黙の型変換もどきを自作する

さて、ここでは自作の型の間に、あるいは言語が用意している型であっても暗黙の型変換がないときに型変換もどきを自作する方法を説明します(先述のCoqのように言語機能で自作できる場合は勿論それでよいのですが)。
まずは例をお見せしましょう。例はかなりHaskellっぽく書いてますが、Haskellに詳しくなかったため関数名は適当です。また例2の後半では依存型か依存型もどきが必要になり、Haskellの型レベル計算を強化するライブラリーがあるらしい(https://github.com/goldfirere/singletons/blob/master/README.md)んですが、そもそもHaskellエアプに理解できるはずもなく、心があっさり折れたので「まあHaskellに似た依存型がある疑似コードってことでいいや」と妥協しました。許してください。
例1

data TraditionalBadSilentTypeConversion = TBSTC1 String | TBSTC2 Int

(equal) :: TraditionalBadSilentTypeConversion->TraditionalBadSilentTypeConversion->Boolean
(equal) TBSTC1 a TBSTC1 b = (a == b)

(equal) TBSTC2 a TBSTC2 b = (a == b)

(equal) TBSTC1 a TBSTC2 b = (a == (intToString b))

(equal) TBSTC2 a TBSTC1 b  = ((intToString a) == b)

例2

data Append x y = Append x y

(equal) :: Append x y->Append z w->Boolean
(equal) (Append a (Append b c)) (Append d (Append e f))
= ((Append (Append a b) c) == (Append (Append d e) f))

(equal) (Append a (Append b c)) (Append d e) = ((Append (Append a b) c) == (Append d e))

(equal) (Append a b) (Append c (Append d e)) = ((Append a b) == (Append (Append b c) e))

(equal) (Append a b) (Append c d)
=if ((sameType a c) && (sameType b d))
 then (a==c && b==d) 
 else False

例1は先ほど批判したいくつかの言語に搭載されている過剰な暗黙の型変換を(あくまで例として)再現したものです。
例2は「「型レベルの文字列」のようなものを作るために、文字列というのは結合則を満たすものなのでAppend (Append A B) CとAppend A (Append B C)という二つの異なる型を同一視(するためにそれらに属するオブジェクトAppend (Append a b) cとAppend a (Append b c)を同一視)したい。」というシチュエーションです。これは前に挙げた「b.構文上異なる型に属するが、数学的な要求により同じであるとみなしたいオブジェクト」の例です。
例1と例2は見た目が結構違いますが、エッセンスは同じであり、

1.暗黙の型変換により変換したい変換前・変換後両方の型を含む型を、直和型・和集合型(直和型と和集合型の違いには注意せよ)(例1)あるいは型変数で量化された型(例2)を用いて作る(ここで作った型をこの記事では便宜上「型変換ラッパー」と呼ぶことにする)。

2.1で作った型の述語や演算をユーザー定義し、場合分けを利用して「型変換させたい値を直接型変換後の値に書き換えた後改めて述語や演算を適用する」ようにする。

というアイデアで「暗黙の型変換もどき」を自作しています。あげた例は両方とも等号を定義する例でしたが、勿論そのほかの述語や演算でも必要に応じて同様に定義することができます。なおここでは「equal(その他必要な述語・演算)を(オーバーライドor型ごとにユーザー定義)できる」という体で書きましたが、それができない言語ならmodifiedEqualとか適当な名前で実装すればいいでしょう。
実用上は1のステップで直和型を用いるか和集合型を用いるかの選択は重要です。
直和型を用いた場合の特徴はユーザーが型変換ラッパーのデータコンストラクタを用いてラッピングを行わない限りは変換が発生しない、「言うほど暗黙でもない変換」だという事です。これには利点と欠点があります。
まず利点は「言うほど暗黙でもない変換」なので暗黙の型変換をしてほしくないときに誤爆する可能性がないことです。一章で指摘した暗黙の型変換の問題点であるバグのリスクが下がるわけです。
逆に欠点は結局いちいちラッピングをするため、一章で説明したような「入力の省略」としての使い方にはそこまで有効ではないという事です。そもそも例を見てわかるように変換の定義も結構面倒くさくなりますし(それでも当たり前みたいな型変換を何重にもかけなきゃいけないような処理をする場合には多少使えるかもしれませんが)。
総じて一章で解説したような素朴な「入力の省略」としての利点・欠点は薄れており、二章で解説したような「自然な同一視」の実装としての側面が強いものです。
逆に和集合型を使えば本当に暗黙の型変換そのものになり、便利な反面バグのリスクは非常に高いと言えるでしょう。
もっとも直和型と和集合型のどちらかしかない言語も多いと思うので選択肢がない場合もあるでしょうが…

4.型変換(によって実装された型同型)による異なる型の同一視

3章の例2についてもう少し考えてみましょう。これは(equal)に関する限り、Append A (Append B C)型とAppend (Append A B) C型とを区別しなくてよい、という事を意味します。
すなわち変換は値レベルで行われていますが、実は型レベルまで同一視が可能なのです。このような状況を「型同型」などと呼んだりし、
$\rm Append\ A\ (Append\ B\ C)\leadsto Append\ (Append\ A\ B)\ C$
などと書きます。「代数的データ型たちの空間は、原始型を定数とし、型コンストラクタによって生成される項代数だと見做せる」という有名な話がありますが、型同型が実装されることで、型の空間を項代数に限らない、一般的な代数と見做しえることになります。
たとえば今回の定義でいえば、型コンストラクタAppendが結合性を満たすかのように見做せる、ということになります。

5.3章例2のさらなる応用(BNFを表す型)

ここでは3章の例2で導入したAppendを利用して遊んでみましょう。
まずここではsubtypingとnon-discriminated-union-typeがある言語を仮定します。
そして例2では勝手な型変数を取っていたAppendを以下のように制約します。
$\rm (forall\ x:x\subset String||x=Append\ a\ b)\Rightarrow(forall\ y:y\subset String||y=Append\ c\ d)\\\Rightarrow Append\ x\ y=Append\ x\ y$
(実はこの方のAppendならば上で僕が苦労した挙句ごまかした依存型もどきがいる部分はいらず、単にStringとしての==で比較できるので型の制約とかに見慣れているならこちらのほうがわかりやすい例になる。)
そしてこのAppendに対して以下のappendCollapse関数を定義します。
$\rm appendCollapse::(Append\ a\ b||String)\rightarrow String\\appendCollapse\ x\ |\ x::String\ =x\\appendCollapse\ Append\ x\ y=concat\ (appendCollapse\ x)\ (appendCollapse\ y)$
ただしダブルバーティカルバーを和集合型とします。この時、appendCollapse関数は例2で定義されたAppend型の等号に対してwell-definedです。なぜならば文字列の結合concatは結合律を満たすからです。言い方を変えるとappendCollapseは例2で定義されたAppend型上の同値類を一意な文字列として解釈します。(なおappendCollapseをStringとAppend型の間の暗黙の型変換にするのはやめたほうが無難です。同じ文字列に対応するAppend型の要素は複数あるため、暗黙の型変換をすると情報が減るという事故の元要素だからです。)
さてここで以下のような性質を持つ型のクラスBを考えてみましょう。

1.任意のStringの有限部分型はBに属する。

2.「Bに属する型にAppendを有限回適用する操作(ただし０回の適用、すなわち何もしないことも許される)で得られる型」有限個の和集合型として得られる型はBに属する。この時Bに属する型同士であれば相互参照があってもよい。特に自己参照があってもよい。

実はBに属する型をappendCollapseで解釈すると、任意のBNFが表現できます。終端記号はStringの有限部分型をすべて含むから表現できますし(なので実際には1の条件は「任意の『１文字文字列を唯一の成分とするシングルトン型』はBに属する。」とかにしても大丈夫です。)、非終端記号はこのようにして作られる型だとみなすわけです。BNFの表記法って結構謎だと思ってたんですが型システムだと思うと妥当ですね(!?)。

6.あとがき

いかがだったでしょうか？
暗黙の型変換という言葉には悪いイメージしかないかもしれませんが、以上のようなコードの数学的自然さを高める使い方もあります。
再評価路線一つお願いします。

こぼれ話をすると、今回のテーマは実は5章の部分で、『論理学友の会』で「BNFの解説公演が聞きたい」という要望があり、「型システムかなにかに帰着させたらわかりやすいんじゃね？」というノリで考え始めたんですが、「異なる型を同一視する方法論」とかnon-discriminated-union-typeとか自分にとってすら初耳の概念が出てきて様々な人に助けられてようやくまとめることができたのですが、引き換えに初心者向けには程遠い内容になった、という経緯があります。
それでは今回も助けていただいた方に感謝を込めて締めたいと思います。

また7/26の「論理学友の会」にてこの記事をテーマにした発表をしたのですが、その後に「型ではなく項代数レベルで考えてはどうか？」という指摘がありました。
僕としては、このテーマについて
・実は型変換によって型の同型 $\rm Append\ A\ (Append\ B\ C)\leadsto Append\ (Append\ A\ B)\ C$ を表現していることにより、同型を同一視したもとに型の空間が項代数ではなく、非自明な等号(実際には同型だが)をもつ空間になること。
・BNFの再帰的な記法を表現するためには代数的データ型に近いコンセプトが有効だと考えたこと。
が面白いと感じたポイントだったことを付記しておきます。

今回のスペシャルサンクス(twitterネームです):
@emptst 様(「異なる型を同一視する」方法論として「暗黙の型変換」というsuggestionを頂きました。つまりこの方がいなかったら今回の記事はコンセプトが出てきてません。またCoqにユーザー定義の暗黙の型変換があることも教えていただきました。また前述の「論理学友の会」においても発表を助けてくれたり、その後いろいろな意見をくださったりと本当に頭が上がりません。)
@hennin_Itn 様(Haskell素人の僕が疑似コード書くのにいくつか質問させていただきました。)
@Lugendre 様(前述の心が折れて放り投げたライブラリーの情報提供を頂きました。一応あれ使えれば疑似コードじゃなくてもHaskellで例2と同じことができるみたいです。)
@Kory 様(BNF実装のために始めた企画で、僕がnon-discriminated-union-typeの存在を知らなかったため実装に詰まり、暗黙の型変換だけの記事にしようと半分以上諦めていたところに、subtypingを利用したnon-discriminated-union-typeがいくつかの言語(Scalaの新世代の試作品であるScala3、みんな大好きTypeScriptなど)に存在することを教えていただき、一気に光明が見えました。この記事が当初の予定通りの形で完成したのは彼のおかげです。)
その他suggestionを頂いた方々
and YOU!

P.S.今回の記事は今まででトップクラスに内容に自信がないです。大間違いがあったら教えてください。

2020-06-22

天邪鬼がオートマトンの導入をするとこうなる(自由生成された圏としてのオートマトン)

※このページはmathjaxの使い過ぎで表示が重くスマホでの閲覧に適しません。パソコンでも通信環境やスペックによっては数秒から数十秒放置してからスクロールを始めたほうがストレスがないかと思います。

どうも、Aaronです。

今回はとても天邪鬼にオートマトンの導入をしていこうと思います。

※この記事において「小さい」という言葉は「クラスに対して定義された概念が実際には集合で与えられている。」という意味でのみ用います。有限や可算であることを「小さい」と表現することはありません。

＊やや細かい集合論の知識を要求する箇所が一部ありますが、それ以外については若干の例外を除いてself-containedに書くつもりです。

1章準備(代数)

Def1.1 前代数系

前代数系 $\it {\rm (}X,\times,error{\rm )}$ とはクラス $\it X$ であって、必ずしも全域的でない二項演算 $\times$ を持つものである。概念上はそれだけなのだが、「全域的でない」という状況を現代数学の記法では書きにくいため、ここでは $\it error\not\in X$ をとり、 $\it \times{\rm :}X\times X\to X\cup \{error\}$ として定式化することにする。

前代数系 $X$ が「小さい」とか「有限である」というのは台クラス $\it X$ がそうであることである。

また紛れの恐れがないならば台クラスのみで前代数系を指定することがある。

Def1.2 局所半群

局所半群 $\it {\rm (}X,\circ,error{\rm )}$ とは前代数系であって、その演算が（必ずしも全域的でないが）等式の両辺が定義される限りにおいて結合的な、すなわち

$\it\forall\alpha,\beta,\gamma\in X.{\rm [}\alpha\circ\beta\neq error\land\beta\circ\gamma\neq error\rightarrow{\rm (}\alpha\circ\beta{\rm )}\circ\gamma=\alpha\circ{\rm (}\beta\circ\gamma{\rm )]}$

を満たすものである。ここで前件は後件の等式の両辺が定義されるために必要であるが、後件の等式が「両辺の値がともに $\it error$ 」を持って成立することも定義上は許容されることに注意せよ。

局所半群の演算 $\circ$ のことを以降では結合積と呼ぶ。

局所半群が「小さい」とか「有限である」というのは前代数系としてそうであることである。

また紛れの恐れがないならば台クラスのみで局所半群を指定することがある。

＊名称について・・・このような非常に弱い代数構造（全域的でないものは代数構造とすら呼ばないのかも知れない）の名前は「半(semi-)」とか「擬(quasi-)」とか「亜(-oid)」とかを適当に順につけたような呼び名ばかりであり、文献同士で衝突していることも珍しくない。最初この概念にはsemi-groupoidの訳として「半亜群」という言葉を当てていたのだが、groupoidという言葉自身に「結合的ですらなくてよいが全域的な二項演算を持つ体系」と「全域的でなくてよいが、単位元(ただしここでの単位律は「値を持つ限り」という意味で成立する)の存在(一意性を含まない)とその単位元に関する可逆性を満たし、しかも結合的な二項演算を持つ体系」という少なくとも二つの用法があることを思い出し、また後にもう一度触れるが「半」という接頭詞は「単位元・単位射を持たない」という意味で揃えて使いたかったため、今回一般的でない造語を用いることにした。Wikipediaによると全域的でない演算を「局所的」と呼ぶことがあるらしいため、このフレーズを用いて表現することにした。これはこれで「局所環」などと被ってしまうが、今回環や体は出てこないので許していただきたい。

Def1.3 局所モノイド

局所モノイド $\it {\rm (}X,\circ,error,ids{\rm )}$ とは、局所半群であって空でない集合 $\it ids\subseteq X$ が与えられており、

$\it\forall a.a\in ids\Leftrightarrow{\rm (}\forall b.{\rm [}a\circ b=b\lor a\circ b=error{\rm ]}\land\forall c.{\rm [}c\circ a=a\lor c\circ a=error{\rm ])}$

（単位律と呼ばれる）

を満たすものである。

局所モノイドが「小さい」とか「有限である」というのは局所半群としてそうであることである。

また紛れの恐れがないならば台クラスのみで局所モノイドを指定することがある。

Def 1.4 代数系

代数系 $\it {\rm (}X,\ \cdot\ {\rm )}$ とはクラス $\it X$ であって、全域的な二項演算 $\ \cdot\$ を備えたものである。

代数系 $X$ が「小さい」とか「有限である」というのは台クラス $\it X$ がそうであることである。

また紛れの恐れがないならば台クラスのみで代数系を指定することがある。代数系の演算 $\ \cdot\$ は単に積と呼ばれることが多い。

＊筆者の偏見かもしれないし、あるいは逆に筆者の不勉強でちゃんとした理由があるのかもしれないが、なぜか非全域的な演算には $\it\times$ や $\circ$ 、全域的な演算には $\ \cdot\$ が用いられる印象があるため今回の記事ではそうすることにする。全域的になると演算の記号が塗りつぶされる、という事になる。

Def1.6 半群

半群 $\it {\rm (}X,\ \cdot\ {\rm )}$ とは代数系であって、二項演算 $\ \cdot\$ が結合的なものである。全域的なのでここでの結合律は

$\it\forall\alpha ,\beta ,\gamma\in X.{\rm (}\alpha\cdot\beta{\rm )}\circ\gamma=\alpha\circ{\rm (}\beta\cdot\gamma{\rm )}$

という慣れ親しんだ形に戻る。

これは局所半群 $\it X$ であって

$\it\forall a,b\in X.a\circ b\neq error$

たるものであるといっても同じである。

半群 $X$ が「小さい」とか「有限である」というのは代数系としてそうであることである。

また紛れの恐れがないならば台クラスのみで半群を指定することがある。

Def1.7 モノイド

モノイド $\it {\rm (}M,\ \cdot\ ,id{\rm )}$ とは半群であって、単位元と呼ばれる元 $\it id\in X$ が与えられており、

$\it\forall a\in M. a\cdot id=id\cdot a=a$

を満たすものである。これは局所モノイドであって

$\it\forall a,b\in X.a\circ b\neq error$

たるものだといっても同じである。

ここで「局所モノイドでは複数の単位元の存在を許していたが同じなのか？」と思った読者は賢明である。もっと賢明な読者は同じである理由を知っていたかもしれない。今あるモノイド $\it M$ の $\it id$ と異なるかもしれない元 $\it id\ '$ も単位律を満たしたとしよう。このとき単位元の性質と仮定から

$\it id\ '=id\cdot id\ '=id$

となる。従って、モノイドの単位元たりえる元は唯一なのである。（ここで値を持たない( $\it error$ )という選択肢がなくなったことが有効に働いていることがわかるだろう。)

モノイド $X$ が「小さい」とか「有限である」というのは半群としてそうであることである。

また紛れの恐れがないならば台クラスのみでモノイドを指定することがある。

Def1.8 群

群 $\it {\rm (}G,\ \cdot\ ,id,{}^{\rm -1} {\rm )}$ はモノイドであって、さらに対応 $\it \ {}^{\rm -1}{\rm :}G\to G$ を持ち

$\it \forall a\in G.a^{\rm -1}\cdot a=a\cdot a^{\rm -1}=id$

(これは可逆律と呼ばれ、 $\it a^{\rm -1}$ を $\it a$ の逆元と呼ぶ。)

を満たすものである。

ちなみにモノイドの単位元の条件同様、群の逆元の条件をみたすものも(各 $\it a\in G$ ごとに)一意である。これは以下のようにしてわかる。ある $\it a$ に対して $\it a^{\rm -1}$ と同じとは限らないが可逆律と同じ等式を満たす $\it a^{\rm -1}_1$ があったと仮定すると、仮定と可逆律から下の等式が成り立つ。

$\it a^{\rm -1}_1=a^{\rm -1}_1\cdot id=a^{\rm -1}_1\cdot a\cdot a^{\rm -1}=id\cdot a^{\rm -1}=a^{\rm -1}$

群 $X$ が「小さい」とか「有限である」というのはモノイドとしてそうであることである。

また紛れの恐れがないならば台クラスのみで群を指定することがある。

＊群より強力な構造(可換群、環など)は今回出てこないので導入しない(群だって怪しいものだったのだが、ここまでやって導入しないのもおかしいかと思い導入した)。各自、一般的な代数学の教科書を参照のこと。

Def1.9 準同型

2つの前代数系 $\it X,Y$ の間の準同型 $\it f{\rm :}X\rightarrow Y$ とは以下を満たすような台クラスの間の対応である。

$\it\forall a,b\in X.{\rm [}a\times b\neq error\rightarrow f{\rm (}a\times b{\rm )}=f{\rm (}a{\rm )}\times f{\rm (}b{\rm )}{\rm ]}$

(これを「演算を保つ」と表現することが多い)

そのほか1章で定義した各構造についても同様に準同型が定義される。

ただし局所モノイド $\it {\rm (}X,\circ,error,ids_X{\rm )},{\rm (}Y,\circ,error,ids_Y{\rm )}$ およびモノイド $\it {\rm (}X,\ \cdot\ ,id_X{\rm )},{\rm (}Y,\ \cdot\ ,id_Y{\rm )}$ (あるいはさらにこれらの上位に位置する構造)に対する準同型 $\it f{\rm :}X\rightarrow Y$ は $\it ids,id$ についての追加の条件

$\it f(ids_X)\subseteq ids_Y\\f(id_X)=id_Y$

をも満たさねばならない。

ところで群の ${}^{\rm -1}$ に対しても準同型に追加の条件

$\it f{\rm (}a^{\rm -1}{\rm )}=f{\rm (}a{\rm )}^{\rm -1}$

を課すことが多いがこれは実は冗長である。すでに課されている条件から $\it a\cdot b=id_X$ ならば準同型 $\it f{\rm :}X\rightarrow Y$ に対して

$\it f{\rm (}a{\rm )}\cdot f{\rm (}b{\rm )}=id_Y$

が成り立つが逆元の一意性より $\it f{\rm (}a{\rm )}$ は $\it f{\rm (}b{\rm )}$ の、 $\it f{\rm (}b{\rm )}$ は $\it f{\rm (}a{\rm )}$ の逆元になるからである。

＊この節では異なる前代数系同士の演算の記号に同じものを用いてしまったが、とてもメジャーな記号の濫用なので誤解を生まないと信じたい。

2章準備(箙・圏・関手)

Def2.1 箙(えびら)

箙 $\it {\rm (}Q,A,Hom{\rm )}$ とは対象クラスと呼ばれるクラス $\it P$ と射クラスと呼ばれるクラス $\it A$ とホム対応と呼ばれる対応

$\it Hom{\rm :}Q\times Q\to {\mathcal P}{\rm (}A{\rm )}$

( $\rm{\mathcal P}(X)$ は冪集合(または冪クラス)を意味する。ただしクラスにおける冪とはその部分集合(部分クラスではなく)のなすクラスであることに注意せよ。これは(少なくともNBG集合論の下では)クラスを元に持つ集合やクラスは許されないからである。)

の組であり、かつ $\it Hom$ が $\it A$ の分割を与える(すなわち二条件

$\it \forall\alpha,\beta,\gamma,\delta\in Q.{\rm [}Hom(\alpha,\beta)\cap Hom(\gamma,\delta)\neq \varnothing\rightarrow {\rm (}\alpha=\gamma\land\beta=\delta{\rm )}{\rm ]}\\\displaystyle \bigcup_{\alpha,\beta\in Q}Hom{\rm (}\alpha,\beta{\rm )}=A$

を満たす)であるようなものである。

箙が「小さい」とか「有限である」というのは $\it Q$ と $\it A$ が共にそうであることである。

また紛れの恐れがないならば対象クラスのみで箙を指定することがある。

なお以降では対象クラスの元の事を対象、射クラスの元の事を射と呼ぶ。またホム対応の値域の元の事をホムと呼ぶことがある。

＊ここで導入された箙（またこの後導入される半圏や圏も）を「局所小な箙」と呼び、真のクラスであるような $\it Hom{\rm (}\alpha,\beta{\rm )}$ を許した定義をすることもある。しかしそのような定義は僕が知る範囲ではあまり恩恵が多くないし、そのくせ記述上の煩わしさか、少なくともNBG集合論では扱いきれない不厳密さかの少なくとも一方を代償に払うことになるためここでは局所小なものに限って箙（半圏、圏）と呼ぶことにする。

Def2.2 半圏

半圏 $\it {\rm (}S,A,Hom,\circ,error{\rm )}$ とは箙であり、かつその射クラスが結合積 $\circ$ を備えた局所半群であって、しかも $\it a,b\in A$ に対して

$\it a\circ b\neq error\Leftrightarrow \exists \alpha,\beta,\gamma\in S.{\rm [}a\in Hom{\rm (}\alpha,\beta{\rm )}\land b\in Hom{\rm (}\beta,\gamma{\rm )}{\rm ]}$

を満たしているとき（この論理式の後半の条件を「型が合う」などと表現することがある。）に言う。

半圏が「小さい」とか「有限である」というのは箙としてそうであることである。

また紛れの恐れがないならば対象クラスのみで半圏を指定することがある。

＊この「半圏」という用語が一般的である自信は全くないし、そもそも応用例もあまりなさそうなので特別な用語を割り当てない事のほうが多いのかもしれないが、ステップバイステップで条件を増やしていく導入のほうが統一感があってわかりやすかろうと思ったのと、群から単位元の存在性の仮定を外したものが半群なので、圏から単位射の存在性の仮定を外したものであるこれを半圏と呼んでも用語に違和感が少ないと感じたためこの名で導入した。

Def2.3 圏

圏 $\it {\rm (}C,A,Hom,\circ,error,ids,id{\rm )}$ とは半圏であり、射クラスが局所モノイドにもなっており、さらに全単射な対応 $\it id{\rm :}C\to ids$ が $\it id{\rm (}\alpha{\rm )}\in Hom{\rm (}\alpha,\alpha{\rm )}$ を満たすようなものである。ここでは $\it id$ について $\it id{\rm (}\alpha{\rm )}$ と一般的な写像の記法に従って記したが、多くの圏論の文脈では $\it id_\alpha$ と書かれる(そしてこの方がわざわざローマン体に戻して括弧を打つよりタイピングが楽である)ため、以降ではこちらを使うことにする。また圏では $\it ids$ の元を単位射、もしくは恒等射と呼ぶことが多い。

圏が「小さい」とか「有限である」というのは半圏としてそうであることである。

また紛れの恐れがないならば対象クラスのみで圏を指定することがある。

Fig2.4 ここまで定義されたもののまとめ

f:id:takumim97:20200623204321j:plain — まとめの図

Ex 2.5 一点圏

対象クラスがシングルトン(一点集合)であるような圏を考えると、どの二つの射も型が合うことから定義より合成積の全域性が回復し、射クラスが(小さい)モノイドになる。このような圏を一点圏という。このことから小さいモノイドを一点圏と同一視することがある。この記事ではこれ以上解説しないが、同様にモノイドより上位の構造は特殊な公理や追加の構造を備えた一点圏と思うことができる。

Def2.6 関手

2つの圏 $\it {\rm (}C,A,Hom,\circ,error,ids_C,id{\rm )},{\rm (}D,B,Hom,\circ,error,ids_D,id{\rm )}$ の間の関手 $\it F$ とは、圏の射クラスの間の準同型 $\it C\to D$ の事である。圏(実際には前圏)の条件から、 $\it C$ で型が合う射は $\it D$ でも型が合わなくてはならないため、対象同士の対応をも自然に誘導され、それが関数的になることに注意せよ。

Def2.7 反対圏と基本反変関手と反変関手

圏 $\it {\rm (}C,A,Hom,\circ,error,ids,id{\rm )}$ に対してその「反対圏と基本反変関手の組」とは圏 $\it C^{op}={\rm (}C,A^{op},Hom^{op},\circ,error,ids,id{\rm )}$ と全単射な対応 $\it opp{\rm :}A\to A^{op}$ の組であり、

$\it\forall \alpha,\beta\in C,a\in A.{\rm[}a\in Hom{\rm (}\alpha,\beta{\rm )}\rightarrow opp{\rm (}a{\rm )}\in Hom^{op}{\rm (}\beta,\alpha{\rm )}{\rm]}$

を満たすようなものである。

また2つの圏 $\it C,D$ の間のある対応が $\it C$ の基本反変関手 $\it opp$ と $\it C$ の反対圏 $\it C^{op}$ から $\it D$ への関手 $\it F$ との合成で得られるとき、そのような対応を一般に反変関手という。

Ex2.8 圏の直和、直積

2つの圏 $\it {\rm (}C_1,A_1,Hom_C,\circ,error,ids,id{\rm )},{\rm (}C_2,A_2,Hom_D,\circ,error,ids,id{\rm )}$ が与えられたとき、新しい圏を作る方法がいくつか存在する。

そのようなものの中で最も簡単なものの2つを紹介する。

2つの圏 $\it C,D$ の直和圏 $\it C_1\sqcup C_2={\rm (}C_1\sqcup C_2,A_1\sqcup A_2,Hom_{C_1}\sqcup Hom_{C_2},\circ,error,ids,id{\rm )}$ は単に対象クラスと射クラスをそれぞれ $\it C,D$ のそれの和クラスとし、ホム対応 $\it Hom_{C_1}\sqcup Hom_{C_2}{\rm (}\alpha,\beta{\rm )}$ を

$\it Hom_{C_1}\sqcup Hom_{C_2}{\rm (}\alpha,\beta{\rm )}=\begin{cases}Hom_{C_1}{\rm (}\alpha,\beta{\rm )}\ \ {\rm (if\ }\alpha,\beta\in C_1{\rm )}\\Hom_{C_2}{\rm (}\alpha,\beta{\rm )}\ \ {\rm (if\ }\alpha,\beta\in C_2{\rm )}\\\varnothing\ \ {\rm (otherwize)}\end{cases}$

で定め、結合積の演算は $\it C,D$ のものをそのまま使ったものであり、要するに2つの圏を単に並べただけであるようなものである。

また2つの圏 $\it C_1,C_2$ の直積圏 $\it C_1\times C_2={\rm (}C_1\times C_2,A_1\times A_2,Hom_{C_1} \times Hom_{C_2},\circ,error,ids,id{\rm )}$ は対象クラスと射クラスを $\it C,D$ のそれらの直積クラスとし、ホム対応 $\it Hom_{C_1}\times Hom_{C_2}{\rm (}{\rm (}\alpha,\beta{\rm )},{\rm (}\gamma,\delta{\rm )}{\rm )}$ は

$\it Hom_{C_1}\times Hom_{C_2}{\rm (}{\rm (}\alpha,\beta{\rm )},{\rm (}\gamma,\delta{\rm )}{\rm )}=Hom_{C_1}{\rm (}\alpha,\gamma{\rm )}\times Hom_{C_2}{\rm (}\beta,\delta{\rm )}$

で定め、結合積は順序対の成分ごとに結合積を取ったもので定めたものである。

この時 $\it C_1$ (resp. $\it C_2$ )から直和圏 $\it C_1\sqcup C_2$ へ、また直積圏 $\it C_1\times C_2$ から $\it C_1$ (resp. $\it C_2$ )へ以下のような非常に自然な関手が取れる。

< $\it C_1$ (resp. $\it C_2$ )から直和圏 $\it C_1\sqcup C_2$ への関手(包含関手)>

射クラスの包含写像(本記事では多くのコレクションにクラスを用いることを許してきたため、集合であるとの感覚を抱かせるかもしれない「写像」という言葉を避け、「対応」という言葉を好んで用いていたが「包含対応」という語彙は違和感が大きかったため、ここでのみ写像という言葉を使う。これは射クラスが集合であることを仮定しているわけではない。)によって誘導される関手が存在する。これを包含関手と呼ぶ。

<直積圏 $\it C_1\times C_2$ から $\it C_1$ (resp. $\it C_2$ )への関手(射影関手)>

$\it C_1\times C_2$ の各射(定義より順序対である)を、その第1成分(resp.第2成分)に出現する $\it C_1$ (resp. $\it C_2$ )の射に対応させる(第2成分(resp.第1成分)は無視する。)関手が存在する。これを射影関手と呼ぶ。

remark:これらの関手は非常に自然であるが、これらの関手が $\it C_1,C_2$ から直和圏 $\it C_1\sqcup C_2$ へ、また直積圏 $\it C_1\times C_2$ から $\it C_1,C_2$ への唯一の関手というわけではない。実際どんな2つの圏の間にも定関手(この記事では定義しない。きわめて簡単な概念なのでWikipediaなり他のだれかのブログなりで確認できるであろう)を取ることができ、 $\it C_1,C_2$ が単位射のみを持つ一点圏でない限り包含関手や射影関手は定関手ではない。

Ex2.9 箙によって自由に生成される圏

任意の箙 $\it {\rm (}Q,A,Hom{\rm )}$ は以下の方法によって、同じ対象クラス $\it Q$ を持ち、 $\it A$ を部分クラスに持つような射クラスを持つ圏 $\it\langle Q\rangle={\rm (}Q,\langle A\rangle,\langle Hom\rangle,\circ,error,ids,id{\rm )}$ に拡張することができる。これを「箙による圏の自由な生成」とよび、得られた圏 $\it\langle Q\rangle$ を、「箙 $\it Q$ によって自由生成された圏」と言う。

<構成>

(結合積は $\it a\ {\rm\hat{\circ}}\ b$ から誘導され、いずれの $\it Hom_n{\rm (}\alpha,\beta{\rm )}$ にも $\it a\ {\rm\hat{\circ}}\ b$ が含まれない $\it a,b\in\langle A\rangle$ に対して結合積は値無し( $\it error$ )と定義される。)

remark:上記の $\it Hom_n{\rm (}\alpha,\beta{\rm )}$ の構成の過程で導入された $\rm\hat{\circ}$ は形式的な積であり非自明な等号を持たない(それゆえ結合積の記号として導入した $\it \circ$ ではなくハットをつけて区別した記号を用いた)。ゆえに $\it \langle \widetilde{Hom} \rangle{\rm (}\alpha,\beta{\rm )}$ は演算に関する公理を満たさず、圏どころか半圏ですらない。 $\it \langle \widetilde{Hom} \rangle{\rm (}\alpha,\beta{\rm )}$ を結合律と単位律を満たす同値関係で割ることによって、はじめて演算の規則が成立した $\langle Hom\rangle{\rm (}\alpha,\beta{\rm )}$ を得るのである。また圏であるためには箙でなくてはならないため、最後の行の和集合が実際には非交和であることも確かめる必要がある。しかし構成法から明らかに等号が成り立つのは同じ $\it\langle Hom\rangle{\rm (}\alpha,\beta{\rm )}$ に属する元同士に限るため(厳密な証明を求めるなら、項の構成に関する帰納法により自明な等号が発生するのは同じホムの内部でだけであることを示し、その後同値関係で割る操作で異なる二つの $\langle\widetilde{Hom}\rangle{\rm (}\alpha,\beta{\rm )}$ に属する元が等しくはならない(なぜならば結合順で属するホムは変わらないためである。この事実もまた項の構成に関する帰納法で得られる)ことを利用すれば容易に得られる。)、この点は問題ない。

Explain2.10 箙からの圏の自由生成の直感的意味

定義から箙は多重辺を許し、しかも多重辺はそれぞれに区別があり、ループも許される有向グラフであると見做せる。

この見方において、その箙から自由生成された圏の射 $\it Hom{\rm (}\alpha,\beta{\rm )}$ は $\it \alpha$ から $\it \beta$ に至るパスの集合だという事ができる。

Ex2.11 文字列空間

対象クラスがシングルトンであるような箙 $\it {\rm (}{\bf 1},A,Hom{\rm )}$ によって、一点圏 ${\rm (}{\bf 1},\langle A\rangle,\langle Hom\rangle,\circ,error,ids,id{\rm )}$ を自由生成することを考える。このときの射クラス $\it\langle A\rangle$ として得られるモノイドを「文字集合 $\it A$ 上の文字列空間」などと呼ぶことがあり、特別に記号 $\it A^*$ で書かれることがある。文字列空間の元は文字列と呼ばれる。構成を見ればなんとなく理解できるように、文字列空間はモノイドとしてある意味で「最も一般の」ものである。

3章状態遷移系・オートマトン

Def3.1 添字づけられた箙

添字づけられた箙 $\it {\rm (}Q,A,Hom,I,ass{\rm )}$ とは箙と添字クラス $\it I$ と添え字対応対応 $\it ass{\rm :}A\to I$ の組である。

remark:一般に「添字づける」といった場合、対応の向きは逆であることもある。特にここでは一つの添字が複数の射に割り当てられて良い（が、逆に複数の添字を割り当てられた同一の射や、一つの添字も持たない射は許されない）ことに注意せよ。

また特に各 $\it\alpha\in Q$ に対して $\it ass$ の $\displaystyle\it\bigcup_{\beta\in Q}{\rm (}\alpha,\beta{\rm )}$ への制限が全単射になるとき、箙 $Q$ は「決定論的に添え字づけられている」ということにする（この用語もまた全く一般的なものではない。後の説明にこの条件に名前があると便利だったので割り当てたに過ぎない。)

Def3.2 モノイドで添字づけられた圏

モノイドで添字づけられた圏 $\it {\rm (}C,A,Hom,\circ,error,ids,id,M,\ \cdot\ ,ass{\rm )}$ とは圏であり、添字づけられた箙でもあり、かつその添字クラス $\it M$ が積 $\ \cdot\$ を持つモノイドであり、しかもその添字対応 $\it ass$ が局所モノイドの準同型であるときに言う。

Ex3.3 添字づけられた箙によって自由に生成されるモノイドで添字づけられた圏

Def2.9で行った箙からの圏の自由生成と同様にして、添字づけられた箙 $\it {\rm (}Q,A,Hom,I,ass{\rm )}$ からモノイドで添字づけられた圏 $\it {\rm (}Q,\langle A\rangle,\langle Hom\rangle,\circ,error,ids,id,\langle\ I\ \rangle,\ \cdot\ ,\langle ass\rangle{\rm )}$ を自由生成することができる。詳しく書けば

$\displaystyle \it Hom_0{\rm (}\alpha,\beta{\rm )}=\begin{cases} Hom{\rm (}\alpha,\beta{\rm )}\ \ {\rm(if}\ \alpha\neq\beta{\rm )}\\Hom{\rm (}\alpha,\beta{\rm )}\cup\{ id_\alpha\}\ \ {\rm (if}\ \alpha=\beta{\rm )}\end{cases}\\I_0=I\cup{\rm \{}id{\rm\}}\\\displaystyle Hom_{n+1}{\rm (}\alpha,\beta{\rm )}=Hom_n{\rm (}\alpha,\beta{\rm )}\cup\bigcup_{\gamma\in Q}\bigcup_{a\in Hom_n{\rm (}\alpha,\gamma{\rm )}}\bigcup_{b\in Hom_n{\rm (}\gamma,\beta{\rm )}}\{a\ {\rm\hat{\circ}}\ b\}\\\displaystyle I_{n+1}=I_n\cup\bigcup_{\mathcal{A},\mathcal{B}\in I_n}\{\mathcal{A}\ {\rm\hat{\cdot}}\ \mathcal{B}\}\\\displaystyle\langle \widetilde{Hom}\rangle{\rm (}\alpha,\beta{\rm )}=\bigcup_n Hom_n{\rm (}\alpha,\beta{\rm )}\\\displaystyle\langle\ \tilde{I}\ \rangle=\bigcup_n I_n\\\langle Hom\rangle{\rm (}\alpha,\beta{\rm )}=\langle \widetilde{Hom} \rangle{\rm (}\alpha,\beta{\rm )}/\sim_{\rm associativity\ and\ unit}\\\langle\ I\ \rangle=\langle\ \tilde{I}\ \rangle/\sim_{\rm associativity\ and\ unit}\\\langle ass\rangle{\rm(}id_\alpha{\rm)}=id\\\langle ass\rangle {\rm(}a{\rm)}=ass{\rm(}a{\rm)}\ \ {\rm (if}\ a\in A{\rm)}\\\langle ass\rangle{\rm (}a\ {\rm\hat{\circ}}\ b{\rm )} = \langle ass\rangle{\rm (}a{\rm )}{\rm\hat{\cdot}} \langle ass\rangle{\rm (}b{\rm )}$

(ここで導入された $\ \rm\hat{\cdot}\$ も、また $\ \rm\hat{\circ}\$ 同様形式的な演算であり同値関係で割ることで演算規則を回復していることに注意せよ。)

である。添字に関する部分が追加された分だけ見た目は煩わしくなったが、よく見ればほとんど変更がないことがわかるだろう。またこの構成で得られる添字モノイド $\it \langle\ I\ \rangle$ が実は文字列になることも、 $\it\langle\ I\ \rangle$ の構成が $\it I$ を箙の射クラスと思えば、 $\it\langle Hom\rangle$ の構成と全く同じであることからわかるだろう。

このような構成で得られるモノイドで添え字づけられた圏を「ラベル付き状態遷移系」と呼ぶことがある。

Def3.4 オートマトン

添字づけられた箙 $\it {\rm (}Q,A,Hom,I,ass{\rm )}$ によって自由生成された文字列空間で添字づけられた圏 $\it {\rm (}Q,\langle A\rangle,\langle Hom\rangle,\circ,error,ids,id,\langle\ I\ \rangle,\ \cdot\ ,\langle ass\rangle{\rm )}$ であって、初期状態とよばれる空でないクラス $\it init\subseteq Q$ 及び、受理状態と呼ばれる空でもよいクラス $\it acc\subseteq Q$ が与えられたものをオートマトンという。

オートマトンに対してその添字となる文字列空間の文字列 $\mathcal{A}$ であって、

$\it\exists\alpha\in init,\exists\beta\in acc,\exists a\in Hom{\rm(}\alpha,\beta{\rm)}.{\rm[}\langle ass\rangle{\rm(}a{\rm)}=\mathcal{A}{\rm]}$

を満たすものを受理文字列と言い、受理文字列全ての集合を受理言語という。

またオートマトンを生成する箙の添字が決定論的であり、しかも初期状態がシングルトンであるときオートマトンは決定型であると言い、そうでないとき非決定型であるという。

また少なくない文脈ではオートマトンという語は対象クラスが有限な場合に限って用いる。

Def3.5 オートマトンの直和・直積、反対オートマトン

オートマトン $\it C,D$ の直和は圏としての直和に、初期状態及び受理状態も単純に $\it C,D$ のそれの和クラスとして与えたものである。

しかしオートマトン $\it C,D$ の直積は圏としての直積ではない。状態クラスおよび初期状態及び受理状態も単純に $\it C,D$ のそれの積クラスであるが、射は積クラスの以下のような部分クラスになる。

$\it {\rm(}f,g{\rm)}\in Hom{\rm(}{\rm(}\alpha,\beta{\rm)},{\rm(}\gamma,\delta{\rm)}{\rm)}\iff ass_C{\rm(}f{\rm)}=ass_D{\rm(}g{\rm)}$

$\it where\ f\in Hom{\rm(}\alpha,\beta{\rm)}{\rm)},\ g\in Hom{\rm(}\gamma,\delta{\rm)}$

オートマトン $\it C$ の反対オートマトンは圏としての反対圏であり、初期状態及び受理状態は不変のものである。

Problem3.6 ★★

Def3.5で定義された三概念がそれぞれオートマトンであることを確かめよ。

Problem3.7 ★★★

Def3.5で定義された三概念は、特定の形式を持つ受理言語を持つオートマトンを作る方法論として有用である。どのような受理言語を作ることができるか、説明してみよ。

Problem3.8 ★★★★(not yet clearly solved by writer)

オートマトンの間に準同型を定義してみよ。直感的な定義は可能であるしそれはとりあえず整合的であるが初期状態と受理状態をどうするかは非自明である。回答は一通りとは限らない。

Problem3.9 ★★★★★(further research target of writer)

3.8で定義される同型は恐らくオートマトンの受理言語を理解するには細かすぎる。何らかの圏論的枠組みを用いてより緩い同型、ないしホモトピー的な概念を定義できないか？

Problem3.10 ★★★★★(further research target of writer)

豊穣圏のようなより高級な圏論的枠組みを用いてプッシュダウンオートマトンをはじめとするオートマトンの様々な変種を今回行ったような方法で記述せよ。

あとがき

いかがでしたでしょうか？とても天邪鬼な方法でオートマトンを導入してみました。一応定義は一貫させたつもりですが、この記事でオートマトンに入門するのは勧めません。むしろ一般的な定義と見比べてみるとよいでしょう。今回これをやったのにはいくつか意味があり、勿論一番は天邪鬼心を満たすことだったのですが数学的な理由もいくつかあります。

第一に、なんであれ「ある概念」をほかの概念や分野の言葉に言い換えることは、しておくとなにかいいことがある可能性があるという一般的な事実です。こうしておけばProblemであげたような圏論的枠組みが使える、少なくともその可能性があります。

第二に、一般的な定義に登場する「遷移関数」という概念がやや人工的に感じる(少なくとも僕にとっては)のに対し、この定義は一読してもらえばわかる通り「構造を生やしていったらいつの間にかできた」という感じのものであり、ある意味ではより自然であることです。

第三に、少し第一と被りますが圏論の言葉を用いて記述すると、オートマトン同士の積や和、準同型、ホモトピー同値などを考えるモチベーションや指針がわかりやすいと思われたことです。勿論一般的な定義ではこういうことを考えることができないわけではありませんが、やはりそれ自体が圏であることにすると少なくとも心情的には見通しがよいです。

さて内容についての話はこの程度にして少し今回の執筆前・執筆中の周辺談についてお話ししたいと思います。

今回の記事を書こうと思ったきっかけはいくつかあり、ひとつは自分が手慰みに作ったこんなトイコードhttps://repl.it/@takumim97/automata#main.scmでした(一応一般の非決定型オートマトンを定義できる。現在バグ取り中)。

別の一つは知り合いが組織した「論理学友の会」という団体の初の発表会があったことです。少し体調が不安定で発表できるかはわからないのですが、次回でもよいので一応発表資料に使えるようなブログを書いておこうと思ったわけです。

論理学友の会slack→https://w1591611733-7t9107570.slack.com/join/shared_invite/zt-exqosl9f-0UoPMiU4lcORnzGeu6qLbA#/

また今回の記事ではかなり基礎的な定義から行ったこともあり、僕が間違ったところもたくさんあったり、僕がふさわしい用語を知らない概念もありました。

それらについてアドバイスをいただいたtwitterの友人(@AlweLogic様、@amntksr様、@R_O_R_I_J_O様)に最大限の感謝をこめて。

※指摘・質問はtwitter:@sanjutsu_yu宛にしてもらえると気付くスピード・確率とも上がります(確実とは言ってない)。

2020-06-16

MTGアリーナでプラチナになった話

どうもAaronです。

今回は数学ともプログラムとも論理学とも哲学とも関係ない純然たる趣味の話です。

実は僕は今でこそこんな数学オタクやっていますが、学部生のころは数学よりボードゲームに使った時間のほうが何倍も長いという生活をしてました。

知ってる人も多いと思いますが現在体調不良で実家療養中、数学やるモチベもない状態なので、学部生のころの気持ちに戻って暇つぶしにMTGアリーナを導入してここ数日遊んでいたんですが、割とあっさりプラチナランクになれたので（「ダメそうなら課金するかー」とか思ってたら、する前に到達した）、プラチナが遠い、っていう初心者さんのためにも、使ったデッキの紹介と低ランク帯の環境分析を残しときます。

f:id:takumim97:20200616163606p:plain — 証拠画像

まずとりあえず僕がプラチナ行ったデッキ、ドーン！

ナヤパンプアップ

メインデッキ 60

クリーチャー 16
《癒し手の鷹》4
《幸運な野良猫》4
《剣術の名手》4
《生命力の天使》4

スペル 21
《ショック》3
《巨大化》3
《希望の光》1
《争闘+壮大》4
《希望の夜明け》1
《平和な心》4
《解呪》1
《樫変化》4

土地 23
《平地》6
《山》2
《森》5
《花咲く砂地》4
《風に削られた岩山》3
《岩だらけの高原》2
《踏み鳴らされる地》1

サイドボード 0

以上となっています。まずこのデッキの解説からしましょうか。

Q1.このデッキはどんなゲームプランを取るの？

A1.最高に理想論を語れば

1ターン目　タップイン処理　

2ターン目　《剣術の名手》着地

3ターン目　《名手》に《樫変化》をエンチャント。殴って8点。

4ターン目　《名手》に《巨大化》、《争闘+壮大》を唱えて殴る。トランプル付き22点でワンショットキルが成立。

という4ターンキルプランを軸にしたデッキ。もちろん現実的にはここまでうまく回らないことが大半だが、フライヤーや絆魂生物にこれらのパンプアップ呪文を打ってダメージレースを大幅にひっくり返すこともできる。

Q2.なんでこのデッキを選んだの？

A2.低ランク帯は白単orオルゾフ（白黒）カラーのライフゲインアグロに溢れていて、のんびりなゲームプランを取るとリソース差で圧殺されたり、巨大なスタッツになった《アジャニの群れ仲間》や《血に飢えた曲芸師》が処理できなくなって負けたりするのでそれより早いゲームプランを持ったデッキを探していてこれになった。またあまりそういうのは良くないのかもしれないが、低ランク帯では「二段攻撃」のルールを理解していない人が多く、それにフォーカスするだけで大量のプレミ勝ちが拾えた。

Q3.マッチ相性は？

A3.大まかに言って「アグロデッキに有利で、白系および黒系コントロールデッキに不利」と思えばよい。

クリーチャーを絞り、単体強化を連打するデッキである以上、白や黒の確定除去を当てられて勝てる道理はない。

一方でライフゲインアグロを含む大半のアグロデッキよりは、（回れば）こっちのほうがキルが速く、またアグロデッキはスタッツがでかくなったこちらのクリーチャーを処理するのに困ってくれることが多いため、有利がつく。

また除去を火力やマイナス修正に依存するコントロールデッキにも、パンプアップ戦略で五分程度を取ることができる。

ただしこれは低ランク帯での話であり、「赤単《エンバレスの宝剣》アグロ」などはほぼほぼこちらの上位互換だし、「変容」のように除去手段豊富なアグロに対してはガン不利。これらのデッキは低ランクでの生息数はたかが知れているため割り切り。逆に言うと高ランクでこのデッキで勝つのはほぼ不可能だと思うし、僕もプレチナランク以降では使う気ない。

ただブン回った時のキルターンが速いためどんなデッキにもワンチャン持ってるのが強み。特にゴールド以下は勝率40パーセントでも長期的にはポイントが増えるため、「ワンチャン」が重要。

Q4.《アジャニの群れ仲間》は入らないの？

A4.《群れ仲間》は確かにゲインランドをマナベースとし、絆魂生物8枚体制を取るこのデッキとは相性がよく見える。しかしこのデッキにおいてライフゲインプランはあくまでサブプランであり、本質的には「パンプアップ呪文およびP/T修正と相性のいいクリーチャーを詰め込んだデッキ」と説明することができる。その点回避能力も絆魂も先制攻撃も持たない群れ仲間はこのデッキのカード採用基準に適わない。強いて言えばP/Tが大きくなるためトランプルがつく《争闘+壮大》とは相性がいいが、その何十倍も相性がいい《名手》が同じマナ域でメインプランなのだからわざわざ入れる理由がない。

Q5.その割に《生命力の天使》は4積みなんだ？

A5.やはり飛行があるのが大きい。これがあるだけでパンプ呪文の撃ち先としての適性が跳ね上がってる。それに《群れ仲間》と違って「ライフゲインした回数」ではなく「現在値」を参照するのが、絆魂をパンプアップして使うことが多いこのデッキとは相性いい。

Q6.《希望の夜明け》の2枚目はなし？

A6.全然あり。単純に生成したくなかっただけ。

Q7.《怒り狂うレッドキャップ》や《速太刀の擁護者》はなし？

A7.むしろ入れたい。単純にパックから出なかった。ただこの辺入れるならもうちょっとマナベース考えないとね。

Q8.《成長の季節》や《節くれ背のサイ》はなし？

A8.両方なし。《成長の季節》はテンポロスがひどいし、《節くれ背のサイ》は最初入れてたけど4マナ到達も緑ダブル捻出もきついので事故要因にしかならなかった。

Q9.《希望の光》《解呪》はなんのため？

A9.テーロスの神や亜神、《石とぐろの海蛇》、《希望の夜明け》、《幸運のクローバー》、《戦慄衆の侵略》、《魔女のかまど》などいくらでもやばいカードが思いついたうえ、低ランク帯で最も見かける除去が《平和な心》であるため1枚ずつ採用。

軽くてほかの使い方もできる《希望の光》だけでいいかとも思ったが、スタンダードのトップメタの「猫かまど」や「アドベンチャー」はエンチャントではなくアーティファクトがキーカードであるため《解呪》と1枚ずつにした。

但し結果的には低ランク帯にそれらのデッキはあまりいないし、居たら居たで小手先の対策でどうこうなるものでもなかったため、腐らない《希望の心》だけでよかったとは思う。

Q10.このQ&Aいつまで続けるの？

A10.そろそろ終わろう。

というわけでナヤパンプアップでプラチナまで駆け上がったわけだが、ざっと環境分析をしてみた。

まず圧倒的に印象に残っているのがすでに何度か触れた白系のライフゲインアグロだ。

カラーチャレンジの構築済みデッキのうち白だけ露骨に完成度が高いため、それを少し改造したりそのまま潜っている人がブロンズでは圧倒的に多かった。

少しずつランクが上がってくると、昔でいう「ステロイド」のような赤緑の中から大型のクリーチャーを扱うデッキや、オルゾフやマルドゥ（白黒赤）カラーのPIG能力にフォーカスしたミッドレンジデッキにも当たるようになった（後者は「猫かまど」が事故ってたのかもしれない。）。

多くのプレイヤーがカード資産が足りず、必然的に低速な環境では「ステロイド」の《炎の大口、ドラクセス》の制圧力が厳しく、僕自身「マッチして相手が回ったら諦める」という方法をとった。

シルバー後半かゴールドあたりから「変容」もかなり増えた。前述の通り不利なのであまり当たりたくなかった。

逆にトップメタでも「アドベンチャー」や「赤単」には、プラチナに到達するまでほぼ当たらなかった。

おまけ

他に使った、もしくは考慮したデッキ集

1.「ディミーア（青黒）フライヤー」

最初に使ったデッキ。クリーチャーを飛行で固めてドレイン呪文で《血に飢えた曲芸師》を強化するクロックパーミッションデッキ。フリー対戦に持って行ったが、フリー対戦にはライフゲインアグロがあふれており、確定除去が《殺害》（しかも初期カードプールには二枚のみ）しかないこのデッキでは巨大化した相手の《群れ仲間》や《曲芸師》がどうしようもなかったため諦め。

2.「エスパー（白黒青）フライヤー」

1から追加の除去として《平和な心》を求めて白をタッチした形。

だいぶましになったが一戦に時間がかかりすぎて疲れるうえに、線が細すぎたため微妙…。

友人に「多少重いカードいれないと常にマナフラッドするよ」とアドバイスされて（僕はふだんはエターナル環境の記事読んでるため、マナ域の感覚がスタンダードとズレてしまっている）《暴風のドレイク》を入れたり、「せっかく白タッチしたなら《癒し手の鷹》どう？」とアドバイスされて入れたらかなり強かったり、ある程度リストを練ったけど、とにかく疲れるのでブロンズ抜けたところでお役御免。正直「青以外使いたくない」みたいな人じゃなきゃ使わなくていいと思う。

「『とにかくライフゲインアグロだらけ』っていう環境にあってなかった」説はあるので今度引っ張り出して使うかも？

3.「セレズニア（緑白）オーラ」

紹介した「ナヤパンプアップ」の原型。ほとんど構造は同じだけど《争闘+壮大》を取ってないせいでブロッカーがいるだけで勝てなくてストレスがたまったので「ナヤパンプアップ」に移行。

4.「オルゾフ《夢の巣のルールス》アグロ」

《ルールス》を相棒に据えたウィニーデッキ。あまりにも《ルールス》のパワーが高すぎて、使い始めた途端に自分のプレイが雑になってモチベーションが溶け始めた、というしょうもない理由で封印。あと《ルールス》の本領はパワーマイナス修正オーラが揃ってからだと思ってるのでそれまで楽しみに取っておこうかなと。

5.「ジャンド（黒赤緑）パンプアップ」

ここから実際には使ってないデッキ。

「ナヤパンプアップ」回してて確定除去1枚で負けるのに腹が立ち、「『ナヤパンプアップ』の構造は変えずに、《名手》を《怒り狂うレッドキャップ》に変えて白を落とし、黒をタッチして《強迫》を入れる。」というアイデアが浮かんだ。

結構いいアイデアだとは思ったのだが《レッドキャップ》を生成するのがもったいなくてやめた。

6.「ティムール（青赤緑）パンプアップ」

《強迫》を《否認》に読み替えて4とほとんど同じ。

青には優良な回避能力持ちがいて、第二希望以降のパンプ呪文の撃ち先に困らないためこっちのほうが本命感あったかもしれない。

7.「白単orオルゾフライフゲイン」

正直これが一番丸いと思う。構築済みデッキを少し改造するだけでいいから生成しなきゃいけないカードも少ないし。

僕は単純なアグロデッキが正直嫌いだし（「じゃあ『ナヤパンプアップ』はどうなんだよ？」と言われるかもしれないが、僕の中ではこれは古えの「ヘイトレッド」や少し前モダンを騒がせた「SCZ（スーパークレイジーズー）」と同じようなコンボデッキという判定だ）、同じデッキのミラーマッチも正直嫌いなので使わなかったが、そういうこだわりがないなら使えばいいと思う。

ではまた今度。

2020-04-25

自作カードゲーム用ライブラリ簡易仕様書兼技術的な説明書

どうも!Aaronです。

また気分転換に(僕の中では)がっつりコーディングをして技術負債を作ったので使い方を書いていきます。

コードはここにあります。→https://repl.it/@takumim97/Card-Game

なおこのコードの実装は一部(RnRSでなく)SRFIで議論されている規格に依存しています。特に本質的なものとしてはランダム関数(random-integer)を仮定していますが、これはRnRSの規格に含まれていません。ちょっと調べたところだとSRFI27をサポートしていれば大丈夫っぽいです。

またSchemeは動的型付き言語ですが、「型注釈はドキュメント」なのでコンパイラじゃなく人間に向けた型注釈(注意すべきことに、即ちそれに違反したからと言って直ちにエラーが出るとは限らない)をつけておきます。

1.create-deck関数:usInt{a}->( ()->(Union [0...a] |deck_is_empty!\) )

自然数aを引数に受け取り、０からa-1までの「カード」でできた「デッキ」を生成します。

返り値はクロージャー(関数)です。これをこの記事では便宜上drawと呼びます。

drawは「引数を受け取らずに「生成したデッキから1枚引いた結果」を返す」という挙動をします。このとき一度出たカードはデッキに戻さないものとします。

drawを呼び出したとき、「すでにデッキが空になっていた」場合、すなわち既にa回以上drawを呼んでいた場合、にはdeck_is_empty!というシンボルが返されます。

なお複数のdrawを作った場合でもそれらは互いに相関はないですし、「デッキの残りカード」は外から参照されたり書き換えられたりすることはありません。

これは「デッキの状態」を表現する変数がcreate-deckするたびに独立して確保され、その時作成されたdrawのみから参照されるという環境を作るからです。

今回のライブラリーは本質的にはこのcreate-deckとdrawを「うまく使う」ことで動いています。

2.card-decode:

(Union Int | deck_is_empty!)->(Union (Product (Union ♠ | ♡ | ♢ | ♣ |) | [1...13]) | Joker | deck_is_empty!)

整数aを1つ受け取り対応する「トランプ」を返すか、deck_is_empty!を受け取りdeck_is_empty!を返します。

0≦a<52ならばジョーカー以外の52枚のいずれかに、この範囲以外のaに対してはジョーカーに変換します。

0≦a<52の値に対しては4で割った余りでスートが、4で割った商(+1)で数が決まります。

3.create-trump-deck

:usInt->( ()->(Union (Product (Union ♠ | ♡ | ♢ | ♣ |) | [1...13]) | Joker | deck_is_empty!) )

自然数aを受け取り、ジョーカーがa枚だけ入ったトランプのデッキを作ります。

そのほかの注意事項や使用法はcreate-deckと同じです。

内部的にはcreate-deckで作ったdrawから値を引き出してからcard-decodeをかけているだけです。

(余談ですが「トランプ」というのは和製英語で原義は「切り札」という意味なのは有名ですが「なら英語であの『52枚のカード+ジョーカー』という特定のカードセットは何て呼ぶんじゃい?」というのがわからな過ぎたのでこの関数名になってます。)

4.create-TCG-deck:

(List (Product Obj | usInt))->Obj

「デッキリスト(入っているカードと枚数内訳)」を受け取り、そのデッキを作る。

そのほかの注意事項や使い方はcreate-deckと同様。

内部的には実はcreate-trump-deckとある意味大して変わらず、card-decodeに当たる部分をデッキリストから実行時に生成しているだけだったりします。

5.draw-n-times:((()->Obj)×usInt)->IO()

1,3,4などで生成された引数を取らない関数と自然数aを受け取り、関数をa回試行してその結果を標準出力に投げます。

6.play-hand:usInt->IO()

create-trump-deckとdraw-n-timesを利用したテキサス・ホールデム形式のポーカー占い/ハンドシミュレーターです。

希望のジョーカーの枚数を選択すると標準入出力で一人ポーカーが始まります。

最初にハンドが配られ、nextと打つとコールが成立してフロップ→ターン→リバーと続きます。

ハンドが弱かったらfoldでおりましょう。

※非技術者の方に向けて

上のplay-handは

(play-hand [希望するジョーカーの枚数])

と打って実行するだけで非技術者の方でも遊べます。

また

(define [デッキ名] '([デッキリスト]))

(draw-n-times [デッキ名] [あなたが好きなTCGの初手の枚数])

#デッキリストは[([カード名] . 枚数) ([カード名] . 枚数) ...]という形式です(角括弧は外す)。

と打つとデッキの初手チェッカーとして使えます。

2019-09-10

自作レジスタマシン簡易仕様書

今回は前から作ってちょこちょことアドバイスもらったり、紹介したりしていたレジスタマシンがとりあえず納得いく形になりましたのでその仕様をまとめておこうかと思います。(PDFはTwitterだと共有が面倒くさいので、もうブログにしてしまえホトトギスとこうなりました。)

とりあえず現物がないと読んでても何も面白くないのでオンラインIDEで実装したURLがこちら
→Repl.it - 4th register-machine

先に言っておくとパーサー作るのさぼって実装言語であるLispの特定のデータ型のパターンを「プログラム」とか「行」とか言ってます。(オンラインIDEで作ってる以上、実装状況に大きく依存するファイル処理に大きく依存するパーサー書いても空しい、というのと、僕はプログラマーではなくロジシャンなので理論上動くことがわかったらもういいでしょ、となったのが大きな理由です。)
そのためここではレジスタマシンそのものの仕様と、それがLispの中でどう表現されているかの両方を説明します。

0 概要・仕様

今回作成したのは以下で説明するようなプログラムと任意個の引数（自然数、現在はリストとして表現されている）を受け取り、仮想レジスタマシンをエミュレートする関数、register-machine-kerです。コマンドによって命令の内部表現や、実行中の各段階のプログラムカウンタやレジスタの様子を出力することもできます。
仮想レジスタマシンには整数(自然数でなく)で添え字(番地)づけられた自然数が格納できる無限個のレジスタ(メモリー)があり、プログラムの実行開始に際して与えられた引数(仮にn個とする)が1番レジスタからn番レジスタまでに格納され、それ以外のレジスタには0が格納されます。
レジスタマシンは与えられたプログラムを0番目の命令から原則的に番号順に1つづつ実行していき、halt(停止)命令に至った時かつその時に限り、その時点での0番レジスタの値を返して止まります。

第一引数→レジスタマシンのプログラムを後述するようにリストで受け取る。
第二引数→レジスタマシンの実行時の引数を任意の長さのリストとして受け取る。リストの先頭が第一引数となる。
第三引数→内部表現出力フラッグ。#tになっていると、エミュレートを行う前にレジスタマシンのプログラムを多少モディファイした内部表現を標準出力に出力する。作成者である僕のデバッグ用なので基本的には#fを渡しておいてください。
第四引数→プログラムカウンタ逐次出力フラッグ。#tになっているとエミュレート中のプログラムカウンタを標準出力に出力する。
第五引数→レジスタ逐次出力フラッグ。#tになっているとエミュレート中のレジスタ(ただし非負かつ一度でも0でない値になったことがある番地まで)をベクタ形式で標準出力に出力する。

出力→halt命令が実行された時点での0番レジスタの値。

1 基本語彙

「文字」という語彙に関しては読者は十分な直観を持つことができるとします。さしあたっては「アルファベット+数字+いくばくかの記号」程度の認識でも大きな問題は生じません。

Def1.1 プログラム

レジスタマシンのプログラムは「行」からなる0から始まる自然数で添え字づけられた列です。現在は「行」のリストとして表現されています。なおプログラムの「終わり」は明確に定義されておらず、あたかも無限に空行が続いているかのように意味論上扱います。

Def1.2 行

行はシンボルがいくつか区切り文字で区切られて並んだものです。現在はシンボルのリストとして表現されています。

Def1.3 シンボル

シンボルは区切り文字以外の文字からなる文字列です。現在は(Lispの)シンボルとして表現されています。

2.命令

命令とは特定の形をした行です。

Def2.1 命令

命令(command)は以下のいずれかの形をした行です。
$\{\lt label \gt\lt\ labelless{\text -}command\gt\}\\\{\lt labelless{\text -}command\gt\}$
ここで $\lt label \gt$ (ラベル)は「:」で終わる文字列であり、 $\lt labelless{\text -}command\gt$ は以下のいずれかです。
$\{{\rm incr}\lt index\gt (\lt value\gt )\}\\ \{{\rm decr}\lt index \gt\lt jump\gt (\lt value \gt)\}\\\{{\rm save}\lt index\gt\lt value\gt\}\\\{{\rm halt}\}\\\{\}$
$()$ で囲まれているのはその部分が省略可能であること、ローマン体で $\lt\gt$ に囲まれずに書かれている部分はその部分が（ほかの部分のような抽象構文でなく）そのままシンボルであることを意味します。
また見てもらった通り、どの命令にもちょうど一個の $\lt labelless{\text -}command\gt$ が含まれるので、この部分をラベルレスコマンド部分などと呼びます。
$\lt index\gt$ は操作するレジスタのレジスタ番号を、 $\lt jump\gt$ は後述する制御構造において発生する実行する命令番号の強制的な変更(ジャンプ)における移動先の行番号を、 $\lt value\gt$ は操作に際して使用する引数を意味しますが、後述するようにこれらに(数学の教科書に出てくるようなレジスタマシンに比べると)かなり柔軟な表現を許している(ことによって先のリンク先で僕が実際にやって見せたように、何とか手動かつ実行時間も常識的な範囲内で、「階乗」などそれなりに高級な関数を実装することができる)のが今回の仮想機械の特徴です。
しかし、理論上はここに自然数( $\lt index\gt$ には整数)しか書けないとしてもモデルはTuring完全なことが示せますので、ここでは一旦、単に自然数(整数)だと思っていただくことにして次の章でさっさと操作的意味論をやってしまうことにします。またincrとdecrにおいて $\lt value\gt$ を省略した場合、1を引数に取ったかのように振舞います。実際には数学の教科書に出てくるようなレジスタマシンは大抵引数が1に限定されていますし、saveは命令そのものがないことすらあり、それでもなおTuring完全です。その意味では先ほど少し話したような柔軟な表現がなくとも、すでに僕たちはかなり恵まれた境遇にいるとも言えます。

3.操作的意味論

(そんなに形式的にやる気は)ないです。

Def3.1 プログラムカウンタ

プログラムカウンタは自然数でプログラムの行数と対応しており、実行中逐次的に変化する。
実行開始時は0である。

Def3.2 命令サイクル

レジスタマシンは原則として、以下の命令サイクルを単位として挙動する。

プログラムカウンタに対応した行の命令を読み込む。
プログラムカウンタを1進める。
読み込んだ命令を実行する。
1に戻る。

ただし例外として強制的にプログラムカウンタが変更される「ジャンプ」と、実行した時点でプログラムの実行全体が終了する命令の「halt」がある。
注意すべきは、(本物のアセンブリ言語がそうであるように)ある命令の実行中プログラムカウンタはすでに1つ先の命令の行に進んでいることです。

Def3.3 incr命令

ラベルレスコマンド部分がincrで始まる命令はincr命令です。
incr命令は $\lt index\gt$ 番レジスタに格納されている値を $\lt value\gt$ だけ増加させます。

Def3.4 save命令

ラベルレスコマンド部分がsaveで始まる命令はsave命令です。
save命令は $\lt index\gt$ 番レジスタに $\lt value\gt$ を格納します。

Def3.5 decr命令

ラベルレスコマンド部分がdecrで始まる命令はdecr命令です。
他の命令と異なり、decr命令には成功と失敗があります。
$\lt index\gt$ 番レジスタに格納されている値が $\lt value\gt$ 以上ならばdecr命令は成功し、 $\lt index\gt$ 番レジスタに格納されている値を $\lt value\gt$ だけ減らします。
もし、 $\lt index\gt$ 番レジスタに格納されている値が $\lt value\gt$ 以下ならばdecr命令は失敗しジャンプが発生します。
このときプログラムカウンタが $\lt jump\gt$ に強制的に書き換わります。

Def3.6 halt命令

ラベルレスコマンド部分がhaltのみからなる命令はhalt命令です。
halt命令が実行されたときプログラム全体の実行が終了し、その時点での0番レジスタの値がプログラム全体の返り値(結果)になります。

Def3.7 空命令

ラベルレスコマンド部分が空白からなる命令は空命令です。
空命令の実行は何も実行しないことと同じです。

Def3.8 負番地レジスタ

負の番地を持つレジスタは命令によって値を書き換えられても瞬時に0に戻る、と約束します。

4.拡張表現(アドレッシングモード)

Def4.1 $\lt index\gt$ の拡張表現

$\lt index\gt$ として以下の表現を書くことができる。
1.直接参照{記法:[整数](e.g. 2)}
記述された値を番地にもつレジスタを表す。
2.間接参照{記法:p[整数](e.g. p3)}
「pに続く整数を番地にもつレジスタに格納されている値」を番地に持つレジスタを表す。

Def4.2 $\lt value\gt$ の拡張表現

$\lt value\gt$ として以下の表現を書くことができる。
1.即値{記法:[整数](e.g. 2)}
記述された値をそのまま使う。
2.レジスタ値{記法:v[整数](e.g.v2)}
「vに続く整数を番地にもつレジスタに格納されている値」を使う。
3.ポインタ値(間接参照レジスタ値){記法:p[整数](e.g.p2)}
「『pに続く整数を番地にもつレジスタに格納されている値』を番地に持つレジスタに格納されている値」を使う。
4.プログラムカウンタ{記法:pc}
「現在のプログラムカウンタの値」を使う。

Def4.3 $\lt jump\gt$ の拡張表現

$\lt jump\gt$ として以下の表現を書くことができる。
1.即値{記法:[整数](e.g. 2)}
記述された値をそのまま使う。
2.レジスタ値{記法:v[整数](e.g.v2)}
「vに続く整数を番地にもつレジスタに格納されている値」を使う。
3.プログラムカウンタ{記法:pc}
「現在のプログラムカウンタの値」を使う。
4.ラベル名{記法:上記以外の実装言語Lisp上でシンボルとして認識できる文字列}
上記に当てはまらない表現はラベル名とみなされる。「[ラベル名]:」の形の文字列を「[ラベル名]に対応するラベル」と呼び、ラベル名が $\lt jump\gt$ として与えられた場合、対応するラベルで始まる命令が書かれた行へのジャンプとみなされる。

なお $\lt jump\gt$ としてポインタ値を書く構文は現在サポートしていない。
気まぐれで追加するかもしれないが、割といらないと思っている。

ここまでで規約は一通り説明したことになる。

5 典型的なプログラミング手法

いくつかの典型的なプログラミング手法を紹介する。
1. ラベル及び空命令を利用したコメントアウト
 コメントアウトの機能は実装されていないが、(ジャンプには使用しない)ラベルを(場合によっては空命令を作って)張ることによってある程度行うことができる。空白(区切り文字)が入るとラベルとみなされなくなるため、_や-を使うこと。
2. iszero分岐
iszero分岐が必要なら以下のようにする

decr [判定したいレジスタ] then
incr [判定したいレジスタ]
else: {非ゼロの場合の処理}
...
then:{ゼロの場合の処理}

3. 無条件のジャンプ
無条件のジャンプをしたいなら負番地レジスタに対してdecr命令を使えばよい。

4.関数(サブルーチン)コール
以下で関数コールができる。
save [メモ用のレジスタ] pc
incr [メモ用のレジスタ] 2
decr -1 [関数名]
…
[関数名]:{関数の処理}
…
decr -1 v[メモ用のレジスタ]

それでは皆様楽しい計算モデルライフを！

(9/12追記:
やや可読性の高い後継言語として
Repl.it - 5th-register-machine
を作成しました。
仕様は大筋で似ていますが、 $\lt jump\gt$ を$で囲む記法となったこと及びニーモニックに割と大きな変更が入っています。
$\lt index\gt$ の直接参照が「[整数]」から「i[整数]」に、
$\lt value\gt$ 及び $\lt jump\gt$ のレジスタ値が「v[整数]」から「rv[整数]」に、
$\lt value\gt$ のポインタ値が「p[整数]」から「pv[整数]」に
それぞれ変更されています。
また内部表現へのコンパイルと実行を分離したため、register-machine-kerに食わせる前にmodify-commandsで内部表現(ソースコード見るとわかりますが、ジャンプの拡張表現が潰されるだけなので人によっては直接手で書けるかもしれません)化できます。