これでオシマイにします。シリーズ記事をすべてリストしたい場合は、「モノイド閉圏の事例：」で検索すればいいでしょう。 シリーズ記事を検索 記事の推敲・リライト、再編成などは（当初は多少やるつもりでいたが）やる気はありません。明らかな間違い（誤…

ボックス積 (-□-) を Box:SG×SG→SG とも書く。ボックス積が双関手性を持つとは、直積圏からの関手であることだから： Box( (f, f');(g, g') ) = Box( (f, f') );Box( (g, g') ) （結合の保存） Box( (A, B)^ ) = Box( (A, B) )^ （単位の保存） 中置演算子形…

(ΦX,A,Y(f)□A^);ev = f ΦX,A,Y(f) = Φ(f) = F と置いて、(ΦX,A,Y(f)□A^) = F□A^ を計算する。 F□A^ : X□A→hom(A, Y)□A = [ λ0(x, a)∈A□A.( (F(x), a) ∈hom(A, Y)□A ) ALSO λ1(x→x', a)∈A□A.( (F(x→x'), a) ∈hom(A, Y)□A ) OR λ1(x, a→a')∈A□A.( (F(x), a→a')…

反カリー化を定義して、カリー化の逆写像であることを計算で直接的に示してみる。念のために、カリー化の定義を再掲： ΦA,B,C : Hom(A□B, C)→Hom(A, hom(B, C)) := λf∈Hom(A□B, C).( [ λ0a∈A.( [λ0b∈B.( f(a, b) ∈C) ALSO λ1b→b'∈B.( f(a, b→b') ∈C) ] ∈hom(…

ここまで計算してきて感じたこと： 図（ストリング図）のワイヤーにラベルがないのは分かりにくい。横着せずにワイヤーにラベル（対象の名前）を書いたほうがいい。悪い例は↓ 写像ブロックとデータブロックを区別して書く必要はないかも。「写像ブロック←→デ…

前の記事の続き。後でひとつの記事にまとめるかも。 真っすぐなスライディング ΦX,A,Y'( f;q ) = ΦX,A,Y(f);hom(A, q) : X→hom(A,Y') 左辺： Φ( f;q ) : X→hom(A,Y') = [ λ0x∈X.( [ λ0a∈A.( q(f(x, a)) ∈Y') ALSO λ1a→a'∈A.( q(f(x, a→a')) ∈Y') ] ∈Hom(X, Y…

前の記事の続き。後でひとつの記事にまとめるかも。 カーブに沿ったスライディング ΦX,A',Y( (X^□p);f ) = ΦX,A,Y(f);hom(p, Y) : X→hom(A', Y) 左辺のΦの内側： (X^□p);f : X□A'→Y = [ λ(x, a')∈X□A'.( f(x, p(a')) ∈Y) ALSO λ(x→x', a')∈X□A'.( f(x→x', p(…

参考：ラムダ計算の自然性とお絵描き - 檜山正幸のキマイラ飼育記 (はてなBlog) 続きの記事2つあり。内容： 記法と設定と法則 タイトニング カーブに沿ったスライディング 真っすぐなスライディング 定義の確認 カリー化 Φ 射のボックス積 f□g hom(p, Y), ho…

表題の記法・概念を説明します。まだ、計算の準備。内容： 写像ブロック データブロック 適用 適用とイータ同値 代入計算 写像ブロックブロック記法を導入しましたが、一般的に f:A→X, g:B→Y, h:C→Y in Set に関して [f ALSO g] は写像の直和になり、[g OR h…

homが反変・共変の双関手であることは、直接示す必要はありません（間接的に言えます）が、計算のための具体的な表示は必要になります。内容： グラフ射と変形の結合 ホムグラフとグラフ射 グラフ射と変形の結合f:A→B がグラフ射、β:w⇒w':B (0→1) C が変形だ…

具体的な結果を示すには具体的な計算が必要で、往々にして計算はドブ板作業になります。ドブ板作業を少しでも軽減するために、ツール（計算デバイス）を整備・改善します。内容： ブロック式構文 値の型の表記 高階グラフ射の表現 ブロック式構文視認性・可…

とりあえず、記号の使い方を決めます。が、使っているうちに変更される可能性があります。決めた記法により、いくつかの定義もします。用語のバリエーションの書き方は「用語のバリエーション記述のための正規表現」を参照。内容： 基本的な記法 記号の乱用 …

単に箇条書きで列挙するだけ。「*」が付いている項目は、理論上は不要。だけど、実際の計算を示すのが望ましい。済んだ項目には順次「◯」を付ける。「△」は、ほんとはやるべきだが省略した計算。 (SG, □, 1, α, λ, ρ) がモノイド圏であること □の定義 ◯ □の…

[追記 date="2019-12-07"] 追記を、ここ（記事冒頭）と記事のおしりにします。が、既存部分の編集はしません。タイトルも変えません。☓は実際ダメなヤツだと思うので。しかし、☓の直後に○が付くと、☓のダメさは打ち消されます。☓○ = ○ 。さらに、最初から○な…

「モノイド閉圏の事例」はシリーズ記事になる予定です（何回になるかは不明）。定義と命題は書きますが、記述はかなりラフなものとなり、解説は最小限、または省略される（解説なし）かも知れません。（[追記]最終回の記事： モノイド閉圏の事例： オシマイ …