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

前の記事の続き。後でひとつの記事にまとめるかも。 真っすぐなスライディング Φ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"] 追記を、ここ（記事冒頭）と記事のおしりにします。が、既存部分の編集はしません。タイトルも変えません。☓は実際ダメなヤツだと思うので。しかし、☓の直後に○が付くと、☓のダメさは打ち消されます。☓○ = ○ 。さらに、最初から○な…

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

全域決定性関数に対するRecコンビネータのプロファイルは： g∈Total(X, Y) h∈Total(N×Y×X, Y) --------------------------------------- RecX,Y f∈Total(N×X, Y) ここで： gは、初期値関数 g:X→Y hは、再帰ステップを推進させる関数 h:N×Y×X→Y fは、定義され…

集合演算（主に直和） 集合演算は： 直積： A×B 直和： A + B 直和は、直感的には「AとBが交わらないように置いたもの」だが、集合論内で扱う場合は次のように定義する。 A + B := ({1}×A)∪({2}×B) = {(n, x)∈{1, 2}×(A∪B) | (n = 1 ∧ x∈A) ∨ (n = 2 ∧ x∈B)}…