このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

モノイド閉圏でウエス（上江州）計算

プログラム意味論 圏一般論 計算

本編に次のエントリーを書いた。

で、上江州＜うえす＞流ラムダ計算ならモノイド閉圏でも定式化できるだろうと思ったので、やってみた。どうやらうまくいく。概略とポイント（注意点）だけを書く。上江州抽象（後述）から自然に型付きオペラッド（後述）が出てくる。

以下で、C=(C, ×, I, [-, -])は選択され固定されたモノイド閉圏とする。

変数集合

Vを変数集合とする。type:V→|C| が前もって定義されていて、Vには全順序（辞書順と考えるとよい）が入っている。この全順序のおかげで、議論がだいぶ簡略化される。V*は変数列の全体、V→*は、整列している（互いに異なる）変数列の全体。「整列した変数タプル」と言えば、V→*の要素のこと。

PowFin(V)は有限ベキ集合、X∈PowFin(V)に対して、X→∈V→*は、Xの要素を整列して並べたものである。一般の重複出現のない列x∈V*でも、x→で整列を示すことがある。

また、type(x) = A であることを、x::A と表記する。

変数による圏の拡張

C[V]は、モノイド閉圏Cに、x∈Vごとの変域[x]と同型射x:[x]→type(x) を添加して作った最小のモノイド閉圏。これを僕は上江州拡張とか上江州アタッチメントと呼んでいたが、Cを係数圏、Vを変数集合とする多項式圏と呼ぶこともあるようだ。

C[V]のだいたいの雰囲気； 変数xごとに、対象[x]をCに付け加え、[x]をxの変域と呼ぶ。x::A だとして、[x]とは：

  1. [x]とAは同一ではないが、同型である。
  2. [x]とAは同型なので、[x]→A という同型射が存在する。そのような同型射が1つだけ特定されている。
  3. 特定された同型射 [x]→A を変数xの“意味”だとする。
  4. xとyが異なる変数なら、[x]と[y]は異なる対象である。

おおざっぱに言えば、C[V]の対象は、|C|に、{[x] | x∈V}を付け加えて、さらに{x:[x]→type(x) | x∈V}という同型射達も加え、その他必要な諸々も加えて整理して再び閉圏になるように仕上げたもの。

C[V]の作り方は技術的にめんどうなところなので、詳細は省略。

構文論

Cを固定しているので、ソート（型記号）とは|C|のことだとする。定数記号とは単にCの射のことだとする。定数fに対して、type(f) = cod(f)。

項（式）、自由変数集合、項の型を次のように定義する。

  1. 変数xは項。FV(x) = {x}、type(x)は前もって定義されている。
  2. E, Fを項として、FV(E)∩FV(F)が空のときに限って、ペア(E, F)は項である。FV[(E, F)] = FV(E)∪FV(F)。type[(E, F)] = type(E)×type(F)。
  3. (), (E), (E, F, G)などの任意の長さのタプルも項である。変数条件などはペアと同様。
  4. Eが項、type(E) = cod(f) のとき、f・E は項である。FV(f・E) = FV(E)、type(f・E) = type(f)。f・EをfEと略記してもよい。
  5. Eが項、X⊆FV(E)のとき、λX→.E は項である。FV(λX→.E) = FV(E)＼X。type(λX→.E) = type(E)
  6. E, Fが項、type(E) = [A, B], type(F) = A、FV(E)∩FV(F)が空のときに限って、E△F は項である。記号△を使っているが、これは適用である。FV(E△F)=FV(E)∪FV(F)、type(E△F) = B。

項を作るときの変数や型に関する条件は重要である。ラムダ変数を整列するルールも人為的で実用上は困るが、議論の単純化の効果は大きい。

項Eが、FV(E)=X、type(E)=A であることを、E:X⇒A と書く。例えば、E:{x, a, t}⇒A。集合Xを必ず整列させる約束で、波括弧をはずしても書いてもよい； E:a, t, x ⇒A。

意味論

Eの意味は【E】のように書くべきだろうが、同じ記号で書いてしまう（ヒドイ！）。変数集合X={x1, ..., xn}に対して、その変域は、[X]=[X→]=[x1]×...×[xn]（ただし、x1, ..., xnは整列しているとして）と定義される。Eの意味は常に、[FV(E)]→type(E)というC[V]の射。

  1. 変数xの意味は、x:[x]→type(x) である。
  2. ペア(E, F)の意味は、E×Fである。
  3. (), (E), (E, F, G)などのタプルは意味は、idI, E, E×F×G など。
  4. f・E の意味は、E;f である。
  5. λX→.E の意味は、モノイド閉圏のカリー化（随伴の自然変換）を適用したものである。
  6. 適用E△Fの意味は、(E×F);ev である。

上江州抽象

Xを変数集合として、(x1, ..., xn)をXを適当に並べた列（整列して無くてよい）とする。並びを置換する射と各xiの逆射を組み合わせると、type(xi)×...×type(xn)から[X]への同型ができる。これを(x1, ..., xn)#:type(xi)×...×type(xn) → [X] と書く。

E:X⇒A が項、その意味を同じ記号E:[X]→Aで書いて、(x1, ..., xn)#;E を <x1, ..., xn | E>と書く。正確には、<x1, ..., xn | E> は新しい構文で、その意味は今言ったとおり。

項Eから、構文的に<x1, ..., xn | E>を作る操作を上江州抽象と呼ぶ。その意味は上で述べたが、Cの射と解釈するより、Cから作った複圏の上で解釈するほうが自然。複圏の射は型付きオペラッドと呼んでもいいだろう（マズイからしら？）。

計算

β変換、α変換、η変換は、意味論と整合する。変換による合同を≡と書くと。E≡Fならば、【E】= 【F】 in C ってこと。逆向きは難しそうだな。でも、たぶん成立する。

上江州抽象とラムダ項には次の関係がある。簡単のために変数は1つだとする。構文と意味をゴッチャにして書くけど：

  • <y | F>・<x | E> = <x | (λy.F)△E>
  • <x | E>×<y | F> = <x, y | (E, F)>

β変換を考慮すると、

  • <y | F>・<x | E> = <x | F[E/y]>

上江州抽象を最初から構文論に入れておくと、オペラッドが混じった計算になる。これで計算力が上がるわけではないが、ラムダ項だけだと、[X]→A （A∈|C）の形の射（上江州さんの用語ではv→射）しか表現できないが、上江州抽象を使ったオペラッドなら、A→Bの形の射も自由に表せる。例えば、f:A→B として、変数x::Aを使って、<x | f(x)> と書けばfそのものになる。

<x | E> は、インフォーマル・ラムダに近くて、<y | F>・<x | E> = <x | F[E/y]> は、インフォーマル・ラムダの計算でもβ変換が使えることを示す。上江州抽象とオペラッド形式は、通常のラムダとは微妙に異なる“インフォーマル・ラムダのフォーマライズ”になっている。

注意

E(x)の意味が、E・(x) = E・x なのかE△xの意味か混乱することがあるから注意。例えば、高階関数fのf(a)(x)の解釈はf(a)△x = (f・a)△x である。

上江州計算では、変数との適用が、E・x と E△x で区別される。また、ラムダ抽象λx.E と上江州抽象 <x | E> も区別される。Eがxしか変数を含まないときは、λx.E : I→[A, B]、<x | E> : A→B の違いがある。<x | E>をfとするなら、λx.E はfのネーム（ゲーデル・コード）を与えると言ってよい。