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

ボックス積 (-□-) を 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"] 追記を、ここ（記事冒頭）と記事のおしりにします。が、既存部分の編集はしません。タイトルも変えません。☓は実際ダメなヤツだと思うので。しかし、☓の直後に○が付くと、☓のダメさは打ち消されます。☓○ = ○ 。さらに、最初から○な…

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

※ まだ解答作成は未完で、現時点では問題1だけ。「基本スキルの確認と練習 (G2 A6P3, C A7P3)」の練習問題への解答です。内容： 問題 1 問題 1この練習問題には6問あるが、（もとの書き方含めて）6×72 = 432 種の書き方を列挙するという“バカバカしくも手間…

※ この練習問題は、前期、および今期の2つのセミナー（論理と圏論）に共通なので、一度やったことがあればやる必要はない。予備知識は特に要求しない。どの時点でやってもかまわないが、早めにやればそれだけ効果的。ただし、この練習問題を全部やる必要はな…

全域決定性関数に対する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)}…

※この記事は「記事5」この記事は、第一期セミナーで受けた質問に対して書かれた過去記事を元にリライトしたものです。一般的な内容は別記事「論理式の集合とは何か？」に書いてあり、セミナー受講を前提にした内容は本記事で書きます。限量子の意味と使い方…

※この記事は「記事4 解答1」 ※今回は「です・ます調」。問題集1とは、次の記事（の問題部分）のことです： 命題と、そのコンテキスト／真理集合 (G2 A1P1) 解答だけでなく、「どうしてこのような練習をするか？」や、関連する事項の説明もします。誤解されが…

「集合圏における可換図式による法則の記述 (C A3P2)」の練習問題への解答です。内容： 問題 1 問題 2 問題 3 問題 4 演算 m の結合律（もっと正確に） 演算 m の左単位律 演算 m の右単位律 演算 m のベキ等律 演算 m の左逆元 演算 m の右逆元 関係 r の反…

「第1回 宿題＋追加説明 (C A2P1)」の練習問題への解答です。が、問題が 実例がほんとにナントカであることを証明（自分で確信が持てるまで確認）せよ。 なので、正解は特にありません。よく分からない、納得がいかないことがあれば、檜山にコンタクトしてく…

大事なことなのでもう一度。内容： 固有名と一般名 1 は 1 だけではなく、単位元一般をも指す 文脈ごとに解釈を変える 役割に注目する 固有名と一般名第2回メイン資料p.1「予定」より： 「言語としての数学」との付き合い方と使い方（のスキル）を習得する。…

問題文はピンク文字で書いてある。 「p.3」などのページ参照は、第2回メイン資料（紙）のページ番号。 後から次の追記・修正を行った。 第2回メイン資料（紙）への参照を追加。 ラムダ記法の解説を追加。 集合圏の重要な射の定義を追加。 マックレーンの五角…

※この記事は「記事3 問題集2」内容： 人間とシステム 三種の表現の区別 日本語表現、メタ記号表現、記号表現（練習問題あり） 練習問題： 日本語表現 → メタ記号表現、記号表現 練習問題： 記号表現 → メタ記号表現 人間とシステム演繹システム〈deduction s…

以下のナントカの例に対して、実例がほんとにナントカであることを証明（自分で確信が持てるまで確認）せよ。素材である集合と関数は与えられているので、法則を満たすことを証明すればよい。※ 練習問題の解答は「解答（特にないけど）： 第1回 宿題＋追加説…

配布印刷物の誤りとその訂正。ご指摘、ご協力ありがとうございます。 ページ番号 場所 誤 正 1 全般的な注意の次の行 言った（はず）だが 言った（はずだ）が 1 なかほど 約語 訳語 1 なかほど transformatioin transformation 4 最初の箇条書き4番 min (2箇…

※この記事は「記事2」なんか社会問題を論じようとしているわけじゃないですよ。論理〈数理論理 | 形式論理〉での話。僕（檜山）の経験・観測によると、言葉や記号へのこだわり・固執や、現実には存在しない整合性を期待していることが、学習を阻害しているこ…

※この記事は「記事1 問題集1」与えられた論理式〈形式化された命題〉に対して、そのスコット・ブラケットを実際に計算する練習。スコット・ブラケット（の値）と真理集合は同じもの。予備知識として、中学・高校で習った、方程式・不等式と図形の関係が必要…