という事情で、Catyの意味論を少しずつ書いていきます（あんまりタラタラはしてられないけどね）。こういう話は作り側に関わることで、使う人には何の関係もありません -- 次の記事を参照のこと：
この記事では、Catyスクリプト・インタプリタの仕様を、表示的意味論風に記述します。表示的と言っちゃいましたが、インタプリタを表す関数の定義をかなり具体的に与えるので、操作的意味論に近いです*1。式のdenotationを圏のなかに取る話（圏的意味論）は別な機会にします。
内容：
パラメータとプロファイル
Catyのコマンド（ネイティブコマンド）やスクリプトはパラメータを受け取れます。「パラメータ」は「引数」と同義ですが、オプションでない引数（プレーン引数、位置引数、名前なし引数などとも呼ばれます）を単に「引数」と呼ぶことが多いので、「オプション（名前付き引数） + 位置引数」の意味で「パラメータ」を使います。
パラメータのデータ構造paramは次のスキーマで定義できます。
type anyScalar = (null|boolean|number|string); // integerはnumberに含まれる
type options = object {*: anyScalar};
type plainArgs = array [anyScalar*];
type param = tuple [options, plainArgs];
param型のサブタイプ（詳細化した型、制限された型）をパラメータパターンまたは引数パターンと呼びます。例えば、次はパラメータパターンです。
tuple [
object {"force": boolean?, "config": string?},
array [integer, boolean?, string*]
]
コマンドとスクリプトはパラメータパターン（「パラメータなし」もパターンのひとつ）ごとに、入出力の型を持ちます。この入出力の型に関する仕様をプロファイルと呼びます。tuple [integer, integer] -> string はプロファイルの例で、tuple [integer, integer] が入力の型、stringが出力の型であることを意味します。違ったパラメータパターン*2には違ったプロファイルを割り当ててよいので、コマンド名はオーバーロード可能です*3。
式、閉じた式、開いた式
Catyスクリプトは式言語なので、Catyスクリプトのコードはすなわち式（expression）です。式（Catyスクリプトコードと同義）の全体をExprとします。E∈Expr は、Eが式であることを意味します。
一般に、式はパラメータ参照を含みます。現状では、パラメータ参照はパーセント記号（「%」）からはじまります。具体的なパラメータ値が与えられれば、その値によりパラメータ参照は具体化されます。まったくパラメータ参照を含まない式を閉じた式と呼びます。閉じてない式が開いた式です。
pがパラメータ（具体的な値のセット）のとき、ExpandParam(E, p) は、式E内のパラメータ参照を、pの対応する値で置き換えた式を意味します。Eが閉じた式なら、任意のpに対して ExpandParam(E, p) = E となります*4。ExpandParamは失敗することがあり、そのときは ExpandParam(E, p) = ⊥ としておきます（⊥は失敗を表す特殊な値）。パラメータの全体をParamとすると：
- ExpandParam: Expr×Param → Expr+{⊥}
ExpandParamがやることは、ほとんどマクロ展開ですが、実用上の理由から、簡単なパラメータ加工を入れる予定です。パラメータ加工とは例えば、文字列をパス名と解釈してベース名部分を取り出すような操作です。
閉じた式の全体をCExprと書くことにします。すると、次が成立します。
- Eが閉じた式 ⇔ E∈CExpr ⇔ 任意のpに対して、ExpandParam(E, p) = E
3項のEval
Catyでは、パラメータと入力（input）は区別されます。入力とは、パイプラインの入り口で式に渡されるデータです。式の評価結果（実行結果）は戻り値とは呼ばずに出力（output）と呼びます。評価には、「入力データ、式、パラメータ」を必要とするので、次の3項関数で評価（evaluation）を表現します。
- Eval(x, E, p) （xが入力データ、Eが式、pがパラメータ）
入力データはJSONデータです。JSONデータの全体をJsonとすれば：
となります。評価関数Evalの戻り値が、式Eの出力です。評価が失敗すれば、⊥が返るとします。
Catyでは、副作用（状態遷移）と例外も扱います。これらは、モナド／余モナド／両モナドにより定式化しますが、しばらくは、入力から出力を生成する過程だけに注目することにします。クライスリ圏を使えば、副作用と例外も入出力と同様に扱えるハズです*5
2項のEval
第2引数が閉じた式で、第3引数を持たないEvalも考えます。
3項のEvalと2項のEvalの関係は単純で、次のとおり。（⊥に関して、Eval(x, ⊥) = ⊥ と追加定義しておきます。）
- Eval(x, E, p) = Eval(x, ExpandParam(E, p))
つまり、2項のEvalとExpandParamがあれば、3項のEvalは定義できます。ExpandParamの仕様はEvalから切り離せる*6ので、以下では主に2項のEvalを考えます。
コンソール（キーボード）から式Eを渡した場合は、常に Eval(null, E) と評価されます。WebからHTTP GET で式Eを渡した場合は、やはり Eval(null, E) です。このときクエリパラメータは、オプションパラメータに変換されて、式Eに繰り込まれます。HTTP POST の場合は、POSTデータ（のJSON変換結果）をxとして、Eval(x, E) と評価されます。
1項のEval
xをJSONデータとすると、xはCatyスクリプトの定数リテラルでもあるので、パイプ結合 x | E は構文的に正しい式となります。この事実を利用すると：
- Eval(x, E) = Eval('x | E')
と書けます。つまり、2項のEvalも不要で、1項のEvalでも間に合います。コンソールシェルのコマンドプロンプトは、1項のEvalの対話的フロントエンドと考えるのが自然です。プロンプトに対して式Eが投入され、Eval(E) がコンソールディスプレイにプリティプリントされます。Eval(E)が⊥である場合は、なんらかのエラーメッセージが表示されます。Eval(E) で無限走行が起きないようにする*7ことは、Catyスクリプトの大きな設計・実装目標です
インタプリタの巡回構造
E, F∈Expr から、パイプ結合を作る構文的操作を Pipe:Expr×Expr → Expr とします。Pipe関数を使って、3項、2項、1項のEvalの関係を記述しておきます。
- Eval(x, E, p) = Eval(x, ExpandParam(E, p)) = Eval(Pipe(x, ExpandParam(E, p)))
パラメータはJSONデータとみなせるので、Param⊆Json です。すべてのJSONデータは、Catyスクリプトの定数リテラルなので、Json⊆CExpr。これらをつなげると、次のような、包含チェーンができます。
- Param ⊆ Json ⊆ CExpr ⊆ Expr
一方、文字列データの全体をStringとすると、次の包含関係もあります。
- String ⊆ Json ⊆ Expr
Catyスクリプトの式は、テキストとみなせるので、Expr ⊆ String と言えなくもありません。すると、次の巡回的包含関係になります。
このことから、JSONデータの領域を普遍領域、文字列の領域をコード領域とした巡回構造を作れます。リフレクションとかレイフィケーションと呼ばれる操作が可能となり、スノーグローブ現象が引き起こされます。
Catyのスノーグローブ現象と山猫スクリプト
巡回的包含関係 String ⊆ Json ⊆ Expr ⊆ String は、厳密に言えばインチキです。Exprを、例えば構文解析後のツリー（AST; Abstract syntax Tree）の集合だと思えば、Expr ⊆ String がウソなのは明らかでしょう。しかし、Exprはテキストへとマーシャリングできるので、Marshal: Expr → String を使って、ExprをStirngに埋め込む写像が構成可能です。
一方、スクリプトコードのテキスト表現をパーズしてASTを作る操作を Parse: String → Expr+{⊥} とすると、ParseとMarshalはだいたい逆になります。正確に言うと、ParseはMarshalに対するレトラクションです。あるいは別言すると、(Marshal, Parse)がEPペアになっています。EPペアは、ゲーデル化とか停止性とかの自己言及現象には必ず登場します。
この状況でとりあえず、CatyインタプリタEvalを内部化したシロモノを作っておきます。Eval(x, E) においてEは式ですが、Eval(x, E) = Eval'(x, Marshal(E)) となるEval'を考えると、
となります。(x, s)∈Json×String に対して、JSONレベルのタプル [x, s]（2項配列）を作れば、[x, s]∈Json となりますから、Eval'(x, s) = Eval''([x, s]) として、
を定義できます。このEval''に相当する関数をホスト実装言語（Caty/PythonではPython）で作ってCatyコマンドとみなしたものを eval（名前が小文字）としましょう。次が成立します。
- Eval(x, E) = Eval('[x, Marshal(E)] | eval')
あるいは、
- Eval(x, E) = Eval(x, '[pass, Marshal(E)] | eval')
つまり、我々生きている人間が、インタプリタを観察対象物として、Eval(x, E) = y という事実を認識できるのと同じように、Caty世界に住む妖精さん達は、([x, e] | eval) = y を認識できるわけです（e = Marshal(E)、E = Parse(e) としています）。そのCaty世界は、インタプリタEval（とコマンド達）により支えられて現象しています。このことは、我々が外の世界で行う観察や作業の一部を、Caty世界内部の妖精さん達に頼める可能性を示唆します。Catyの自己テスト用スクリプト（WildCats）は、この発想と原理に基づいて設計されます*8。
構文解析の結果であるASTは、Caty世界の外にあるので、ParseやMarshalはCaty世界の住人・妖精さんには見えません。しかし、ASTを内部化することもできます。例えば、foo --opt | bar hello という式を次のようにJSONエンコードしたとしましょう。（Catyではアットマーク・タグが使えますが、JSON仕様から逸脱はしません。）
@pipeline [
@commandCall ["foo", {"opt":true}, []],
@commandCall ["bar", {}, ["hello"]]
]
同様にして（他のお好きなやり方で）ASTをCatyの内部世界で定義できます。そうすれば、ParseやMarshalも内部化できるので、外部世界の現象をもっと精密に内部世界で再現できます。外の世界とまったく区別できない内部世界を構築することもできますが、Catyは完璧なスノーグローブにこだわってはいません。ミニチュアの世界は、ホンモノよりラフでもかまいません。
Evalを定義する
話が横道にそれました。Evalの定義を書き下すことにします。2項Evalを考えます。⊥がEval引数に入ったら⊥を返すことにして、2項Evalは次の形だとします。
Catyの式は帰納的（再帰的）に定義されます。定数リテラル（JSONデータ）とコマンド呼び出しを基本として、次の構成方法で式を組み立てます。以下で、α、βは名前文字列で、プロパティ名とタグ名として使われます。
| 番号 | 構成方法 | 式の形 | 圏論的な解釈 |
|---|---|---|---|
| 1 | パイプ | E | F | 射の結合 |
| 2 | 配列 | [E, F] | デカルトペア（名前なし） |
| 3 | オブジェクト | {α:E, β:F} | デカルトペア（名前あり） |
| 4 | 分岐 | when {α=>E, β=>F} | 余デカルトペア |
| 5 | 繰り返し | each {E} | 圏論的クリーネスター |
配列の項目、オブジェクトのプロパティ、分岐の選択肢（ケース）は任意の数に増やせます。が、話を単純にするために n = 2 の例を示すだけにします。
- Eval(x, E) = E
となります。定数は評価しても変わりません（プリティプリントで変わるのは見た目だけですよ :-)）。xは評価には関与せず、捨てられます。
Eがネイティブコマンド呼び出しのときは、ネイティブ言語により実装されたメソッドや関数を呼び出すことになりますが、これを Native(x, E) と書けば、
- Eval(x, E) = Native(x, E)
です。
構成された式の評価は以下のとおり。tag(x)とval(x)は、タグ付きデータのタグと値（タグを取り除いた部分）を意味します。
- Eval(x, E | F) = Eval(Eval(x, E), F)
- Eval(x, [E, F]) = [Eval(x, E), Eval(x, F)]
- Eval(x, {α:E, β:F}) = {α:Eval(x, E), β:Eval(x, F)}
- Eval(x, when {α=>E, β=>F}) = (tag(x) = α なら Eval(val(x), E)、tag(x) = β なら Eval(val(x), F)、その他は ⊥)
- Eval(x, each {E}) = (xは配列で長さがnなら、[Eval(x[0], E), ..., Eval(x[n-1], E)]、xが配列でないときは ⊥)
配列やオブジェクトの構成の際に、項目／プロパティのどれか1つでも⊥なら、全体の値も⊥だとします。
Catyでは、任意のデータにタグを付けられます。タグは、タギング演算子「@」によって実装されています。タギングの評価は次のようになります。taggedはタギングを実行する関数です。
- Eval(x, @α E) = tagged(α, Eval(x, E))
現状のCatyスクリプトの言語仕様は、これで全てです。つまり、表示的意味論の記述はこれで終わりです*10。
通常のプログラミング言語では、表示的意味論を与えるのはとても大変な作業ですが、Catyスクリプトは極端に単純なので、意味論も簡単です。「ハッキリとした意味論を持っていて、意味論に対する正当性が検証可能なソフトウェアを作りたいな」と思っても、通常は複雑すぎて大変すぎて到底無理な相談です。が、Catyならそれが出来るだろうと僕は期待しています。そうします、たぶん。
*1:そもそも、表示的／操作的／公理的のような分類が意味あるかどうかは怪しいです。
*2:「違ったパラメータパターン」の意味を定義するには、パラメータのシグニチャセットの概念が必要です。
*3:オーバーロードの処理振り分けは、コマンド実装内で手で書かなくてはなりません。オーバーロードをあまりお勧めはしないので、振り分けの自動化はしません。
*4:ExpandParamは、pのチェックを一切しないと仮定しています。Eをコンパイルするなら、コンパイル時に型宣言を生成して、pがEに対して整合的であるかどうかをチェックすることもできます。
*5:うまくいくかどうかの確認が完全には済んでいません。通常のクライスリ圏ではなくて、余モナドや両モナドまで扱えるようにした拡張圏を使います。→ http://d.hatena.ne.jp/m-hiyama/20090715/1247634707
*6:実は、ExpandParamの仕様をちゃんと考えてません。けっこう難しい。
*7:ただし、テスト用Catyスクリプト＝WildCats は、意図的またはミスにより無限走行します。
*8:まだ、WildCatsの設計は済んでませんけど。
*10:実用上の理由から入れたアドホック規則、例えばvoid規則などがありますが、それは少数だし、理論的には無視可能です。
