$`x = f(x)`$ $`x \ne f(x)`$ これの解釈： $`\forall x\in X.\, x = f(x)`$ $`\exists x\in X.\, x = f(x)`$ $`\forall x\in X.\, x \ne f(x)`$ $`\exists x\in X.\, x \ne f(x)`$ 関数レベルでの等式： $`\mathrm{id}_X = f`$ $`\mathrm{id}_X \ne f`$

気力がなくなる理由： 何のためにやるのか分からない。動機不足、不毛感、虚無感。 何をやったらいいか分からない。困惑感、不安感、無力感。 難しすぎる。どうせ無理。徒労感、劣等感。 目標と前提： ターゲット 前提（過程、仮説）、あるいは資源〈リソー…

トピックワードとは、記述本体内に散在して出現するワードで、トピックを表すキーワード。以下、実際に予定しているトピックワード。 基本データ型 基本データ値 複合データ型 複合データ値 自然数による非負有理数の構成 自由な帰納的構成 自由な相互再帰的…

カントール 1845 -- 1918 ヒルベルト 1862 -- 1943 ラッセル 1872 -- 1970 ハスケル・カリー 1900 -- 1982 ノイマン 1903 -- 1957 チャーチ 1903 -- 1995 ゲーデル 1906 -- 1978 ゲンツェン 1909 -- 1945 チューリング 1912 -- 1954

Lisp由来であることを強調する必要はない。MiniLisp - (新) 檜山正幸のキマイラ飼育記 メモ編 で書いた以外の構成素： var宣言、または初期化構文 let式 if文、case文、while文 ブロックスコープ構造 論理言語のインタープリター実装 $`\newcommand{\MPL}{\m…

データ型 Nat Bool String Nil Basic := Nat | Bool | String | Nil Tree(X) List(X) 基本関数 Nat, Bool, String の色々 Tree: left, right, pair, isBasic List: fst, rest, cons, nth, isNil プログラム式の評価：$`\quad (p, \rho) \overset{E}{\mapsto}…

ラムダ記法＋適用：$`\quad (\lambda x\in X. P(x))(a) \equiv (P(x) \mid x = a)`$証明可能性：$`\quad \vdash_S (P(x) \mid x = a)`$エミュレーション：$`\quad \vdash_T \sigma(\ulcorner p \urcorner, a) \iff \vdash_S p(a)`$自己エミュレーション：$`\…

課題と参考文献： インスティチューションがうまく使えない - 檜山正幸のキマイラ飼育記 (はてなBlog) 2005年7月の疑問・課題 はじめての圏論 その第5歩：変換キューの圏 - 檜山正幸のキマイラ飼育記 (はてなBlog) はじめての圏論 第6歩：有限変換キューと半…

数学の時代区分 エジプト／バビロニア／中国の時代 事実と手法の集積 ギリシャ、ユークリッドは紀元前300年前後アレクサンドリアの人、 公理と証明の発明 19世紀 古典述語論理と集合論による厳密化・体系化、ヒルベルト ？ コンピュータで検証可能な記述 問…

いずれの描画法でも、平面を順方向エリアと逆方向エリアに区切っている。この区切り線を中心線と呼ぶことにする。代表的な3つの描画法を述べる。もちろん、他の選択肢もある。描画の約束によりファントム交差／ファントムカーブは生じる。相互変換には鏡映変…

アリーナ1 {旅行 → {1日目, 2日目, 3日目}} $`y^3`$ アリーナ2 {和 → {焼き魚, 煮魚, 刺し身}, 洋 → {グリルチキン}, 中華 → {エビチリ, 麻婆豆腐}} $`y^3 + y + y^2`$ アリーナ3 {和 → {羊羹, わらび餅}, 洋 → {ショートケーキ, モンブラン, ババロア}} $`y…

トレース付きモノイド圏の新しい定義 圏論的レンズ 4： テレオロジー圏 トレース付き圏の公理を次のように名付ける。 バニシング バンドリング （通常はバニシング 2） タイトニング スライディング ヤンキング スーパーポージング テレオロジー圏のトートロ…

確かムーアは論理式の集合の上の閉包作用素として演繹系を定義したと思う。アクツェルの推論系〈inference system〉の定義は以下のよう： 判断〈judgement〉の集合 U 演繹ルール〈deduction rule〉は A⊆U と c∈U の組 (A, c) 、これを A/c とも書く。 A を演…

フラットコンステレーション＝ストリング図テンプレート⊇ワイヤリング図 ソリッドディスク＝ストリング図⊇無ノード・ワイヤリング図＝スパイダー図 外サークル＝ストリング図のキャンバス境界 内サークル達＝ストリング図テンプレートのスロット境界達 中間…

右の欄はローヴェアの代数セオリー。 アリーナ コンステレーション 代数指標 カローラ テンプレート オペレーション アリーナ テンプレートキット 指標 ツリー コンステレーション 項 フォレスト コンステレーションキット 割り当て〈代入〉系 リーフ スロッ…

コンテナをアリーナ＝カローラ・フォレストで図示するとして： ツリーをグラフと見るとき、通常グラフ解釈かオープングラフ解釈か？ リーフをどう描くか？ ドット、アロー、ワイヤー ルートをどう描くか？ ドット、アロー、ワイヤー ツリーとルートを別物と…

困っている。 何がプレーンレンズ〈バニラレンズ〉か分からない。 元祖レンズの有法則／無法則は、まーハッキリしている。 単相レンズ〈monomorphic lens〉と双相レンズ〈ニ相レンズ | bimorphic lens〉の区別はあるが、一般的とも言えない。ヘッジーズ〈Hea…

そうそう、セルに型が付くのだった。セルに型フィールドと値フィールドがある。特定番地のセルのフィールドに値が入っていることを$`\quad \text{A2.Val} = 7\\ \quad \text{A2.Typ} = {\bf N} %`$まとめて$`\quad \text{A2} = (7 : {\bf Nat})`$次の機能が…

ヒエー、僕は使ったことない。 表計算ソフト〈スプレッドシート〉が便利なのは、入力に対する自動計算／自動再計算をやってくれるから。 高機能かつDomainSpecificな電卓〈カリキュレーター〉として使える。 セル番地は A1, C30 のように英字と数字の並び、…

顔負け 貫禄負け 気圧される 圧倒される 威圧される 威嚇される 怖気づく 萎縮する 恐怖を感じる 親しみを持てない 劣勢に立たされる 例えば：$`{\displaystyle \int_{x = a}^b \frac{df}{dx}(x)\, dx = \Big[ f(x) \Big]_{x = a}^b}`$

コンテナ〈ファミリー〉の演算と特別な射： {{ディリクレ}?{テンソル}?}!積 $`\otimes`$ ： コンテナ＆レンズ演算〈(0 | 1)-オペレーター〉、遷移系の演算とも考えられる。 ジョイン $`\triangleleft, \triangleright`$ ： 遷移系の演算、遷移系だけ考えると…

構文論： 基本概念 別名 ラベル 名前, 変数, 不定元, 定数, 識別子 シング n-射, もの, 実体, 具体物 割り当て 束縛, 代入, 関連付け〈association〉 リテラル 定数, 名前, 記号 コネクティブ 演算{子}?記号 コンビネーション 項, 式, 図式 ※ 論理のリテラル…

CoqでもLeanでもPropを使うが、Prepの正体は何でもよくて、デカルト閉半環圏（の対象集合）であればよい。自然数上に定義された述語 p は p: Nat → Prop だが、その実体が次のいずれでも、さらに他の何かでもいい。$`\quad p:{\bf N} \to {\bf B} \text{ in …

構文は： law 2-ラベル :: 閉じた論理式または variable 変数の型宣言 law 2-ラベル :: 自由変数を含む論理式法則の圏論的実体〈シング〉は2-射なので、法則名は2-ラベルとする。事例： signature LawlessMonoid within Set { sort U operation e: 1 → U ope…

名前〈記号〉とモノを区別できない。a と [​[a]​] （スコットブラケット）で区別する。 命題と主張を区別できない。P と |- P で区別する。 要素と集合を区別できない。a ∈ A で区別する。 内包と外延を区別できない。A = {x∈A | P(x)} で区別する。 所属と…

section 分数の定義と掛け算 { declare 0-mor F in Set define F := Int×(Int＼{0}) declare 0-mor 1 in F // オーバーロード define 1 := (1, 1) declare 1-mor m : F×F → F in Set reserve a, b, c ∈F reserve x, y ∈Int define m := λ(a, b).( (a_1×b_1, …

話し手の態度（意図の復元可能性）： 話し手基準： 自分（話し手）なら、この言い方で分かる（復元可能）。 聞き手基準： 聞き手は、この言い方で分かる（復元可能）だろう。 主要な責任： 話し手責任： コミュニケーションを成立させる責任は話し手にある。…

(n, k)→(m, l)-コンストラクタ F とは： C はn-圏、|C|_k は C のk-射の集合 D はm-圏、|D|_l は D のl-射の集合 F: |C|_k ⊇→ |D|_l が、CからDへの(n, k)→(m, l)-コンストラクタ 部分写像でないときはフルコンストラクタ 例： (0, 0)→(0, 0)-コンストラクタ…

コンステレーションの図示にいおて、1次元キャンバスの場合も2次元に描く習慣があるのか？ -- これは混乱のもとだな、良くない。 1次元穴あきキャンバス： 区間に穴が開いている。穴は幅0でも有限幅でもいい。穴の境界にプロファイル情報が載るが、それは A …

terminology _ vocabulary コンステレーション { サークル ポート マーカー 向き付きサークル〈oriented circle〉 順序付きサークル = 向き付きマーカー付きサークル 方向付きサークル〈directed circle〉 方向付き順序付きサークル〈directed ordered circl…