…ストしたい場合は、「モノイド閉圏の事例：」で検索すればいいでしょう。 シリーズ記事を検索 記事の推敲・リライト、再編成などは（当初は多少やるつもりでいたが）やる気はありません。明らかな間違い（誤字・脱字含む）の訂正以外は、もう変更はないでしょう。やった計算／やってない計算のリストは次にあります。 モノイド閉圏の事例： 必要な計算 「*」付きは計算をやらなくても理論的に出ます。△は、ほんとはやるべきだが省略した計算です。概念的な話は： ラムダ計算の自然性とお絵描き モノイド閉圏…

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

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

ここまで計算してきて感じたこと： 図（ストリング図）のワイヤーにラベルがないのは分かりにくい。横着せずにワイヤーにラベル（対象の名前）を書いたほうがいい。悪い例は↓ 写像ブロックとデータブロックを区別して書く必要はないかも。「写像ブロック←→データブロック」の入れ替えをよくするので、括弧の書き換えがめんどくさい。どちらも角括弧でいいと思う。 写像ブロックとデータブロックを統合するなら、セマンティクスも統合したほうがいいだろう。ブロックベースのラムダ計算を構成することになる。 …

前の記事の続き。後でひとつの記事にまとめるかも。 真っすぐなスライディング Φ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') ) ALSO λx→x'∈X.( [ λ01a∈A.( q(f(x→x',…

前の記事の続き。後でひとつの記事にまとめるかも。 カーブに沿ったスライディング Φ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(a')) ∈Y) OR λ(x, a'→a'')∈X□A'.( f(x, p(a'→a'')…

参考：ラムダ計算の自然性とお絵描き - 檜山正幸のキマイラ飼育記 (はてなBlog) 続きの記事2つあり。内容： 記法と設定と法則 タイトニング カーブに沿ったスライディング 真っすぐなスライディング 定義の確認 カリー化 Φ 射のボックス積 f□g hom(p, Y), hom(A, q) 計算 タイトニング 記法と設定と法則 を ΦX,A,Y に、 を □ に変える以外は元記事と同じ記号を使う。idA などは、バンプアップ記号'^'を使って A^ などと書く。 f:X□A…

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

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

具体的な結果を示すには具体的な計算が必要で、往々にして計算はドブ板作業になります。ドブ板作業を少しでも軽減するために、ツール（計算デバイス）を整備・改善します。内容： ブロック式構文 値の型の表記 高階グラフ射の表現 ブロック式構文視認性・可読性・理解容易性を改善するために、ラムダ記法にブロック式という構文を導入する。とはいえ、囲み記号として角括弧 '[', ']' を新規に追加するだけ。角括弧は、λ0, λ1, λ01 で始まるラムダ式と、ALSO, OR 接続詞の組み合わ…

とりあえず、記号の使い方を決めます。が、使っているうちに変更される可能性があります。決めた記法により、いくつかの定義もします。用語のバリエーションの書き方は「用語のバリエーション記述のための正規表現」を参照。内容： 基本的な記法 記号の乱用 文字の使い方の目安 グラフ射を部分に分ける ラムダ記法 ボックス積 射のボックス積 変形 ホムグラフ エバル〈評価射〉 カリー化〈随伴転置〉 基本的な記法記法の決め方の方針： 誤解をしにくい。 視認性が良い。 手早く書ける。 上の項目ほど…

単に箇条書きで列挙するだけ。「*」が付いている項目は、理論上は不要。だけど、実際の計算を示すのが望ましい。済んだ項目には順次「◯」を付ける。「△」は、ほんとはやるべきだが省略した計算。 (SG, □, 1, α, λ, ρ) がモノイド圏であること □の定義 ◯ □の双関手性 ◯ α, λ, ρ の定義 △ α, λ, ρ の同型性 △ マックレーンの五角形 △ マックレーンの三角形 △ hom(-, -) の定義 ◯ hom(-, -) が双関手であること * カリー化の定…

[追記 date="2019-12-07"] 追記を、ここ（記事冒頭）と記事のおしりにします。が、既存部分の編集はしません。タイトルも変えません。☓は実際ダメなヤツだと思うので。しかし、☓の直後に○が付くと、☓のダメさは打ち消されます。☓○ = ○ 。さらに、最初から○な状況であるなら、☓の効果も○の効果もなくなってしまい、何もしないプレーンな状態が回復します。（末尾の追記部分に続く。）[/追記]内容： 一般的な定義 推論の書き方 基本的な性質 定理と注意 追加の記法と基本的…

…記]最終回の記事： モノイド閉圏の事例： オシマイ - (2nd) 檜山正幸のキマイラ飼育記[/追記]）ドラフト状態で公開するので、後からの変更が激しくなるでしょう。単一の記事内での変更に留まらず、記事の構成が大幅に変化するかも知れません -- それは、記述・投稿の時間順序が論理的順序にはならないと思うからです。内容： この事例について 用語と記法 露骨な表示 この事例についてモノイド閉圏〈monoidal closed category | 閉モノイド圏 | closed …