$`\newcommand{\Within}{\sqsubseteq} \newcommand{\conc}{\mathop{\#} } \newcommand{\dmid}{\mathrel{\|} } \newcommand{\mrm}[1]{\mathrm{#1} } %`$$`\mrm{Ext}(\Sigma)`$ は拡張指標（派生指標）の全体。すると、$`\quad \Gamma \in \mrm{Ext}(\Sigma) \…

$`\newcommand{\Within}{\sqsubseteq} \newcommand{\conc}{\mathop{\#} } \newcommand{\dmid}{\mathrel{\|} } \newcommand{\mrm}[1]{\mathrm{#1} } %`$ 証明の定式化が欠けている。→ πインスティチューション 非論理的指標部分と論理条件が分離されている。…

指標テレスコープがあるとする。$`\newcommand{\Within}{\sqsubseteq} \newcommand{\conc}{\mathop{\#} } \newcommand{\dmid}{\mathrel{\|} } %`$$`\quad \Sigma_1 \Within \Sigma_2 \Within \cdots \Within \Sigma_n`$それ自身が指標でなくても、なんらかの…

$`\newcommand{\mrm}[1]{ \mathrm{#1} }`$ 0-指標の場合は関数の定義 1-指標の場合は関手の定義 型理論： 証拠〈witness〉付き型判断（コンテキスト＝名前付き指標） 論理： 証明 プログラミング：ソフト実装、アダプター 手続きの域は指標だが、ソース・コ…

長さ1の指標テレスコープ$`\newcommand{\Within}{\sqsubseteq}`$ $`(\emptyset \Within S)`$ 指標の標準分解： 宣言の個数と同じ長さの指標テレスコープ 無法則パートと全体で長さ2の指標テレスコープ 任意の長さの自明テレスコープ 指標テレスコープの最初…

以前にも書いたが、包含的圏〈inclusive category〉は、 Composing Hidden Information Modules over Inclusive Institutions (2004) Joseph Goguen, Grigore Rosu 25p https://fsl.cs.illinois.edu/publications/goguen-rosu-2004-dahl.pdf 包含系は： Grot…

次の記事の内容を今の言葉で書き直す。 n-セオリーとインスティチューション - (保存用) 檜山正幸のキマイラ飼育記 メモ編 セオリーとインスティチューション - (新) 檜山正幸のキマイラ飼育記 メモ編

指標と仕様 - 檜山正幸のキマイラ飼育記 (はてなBlog) パート分けと多パート指標〈multipart signature〉は、テレスコープで解釈できる。法則パートを定義できれば、有法則指標と無法則指標の概念も定義できる。$`(S \sqsubseteq T)`$ のとき、$`S`$ が無法…

$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\Within}{ \sqsubseteq } `$ $`\cat{Sign}`$ 指標の圏 $`\cat{Alg}`$ 代数の圏 $`\mathbb{F}:\cat{Sign} \dashv \cat{Alg} : \mathbb{U}`$ 自由忘却随伴系 $`J:\ca…

本編でいつか書くかも知れない。

https://www.win.tue.nl/automath/archive/pdf/aut103.pdf Telescopic mappings in typed lambda calculus by N.G. de Bruijn ド・ブラウンのテレスコープ https://leanprover.github.io/reference/declarations.html#contexts-and-telescopes Leanのテレス…

相対指標と利用法 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\Within}{ \sqsubseteq } `$指標の圏は $`\cat{Sign}`$ と書く。指標はローマン体大文字。指標…

基本的道具は： Composing Hidden Information Modules over Inclusive Institutions (2004) Joseph Goguen, Grigore Rosu 25p https://fsl.cs.illinois.edu/publications/goguen-rosu-2004-dahl.pdf 特に、"3 Inclusive Institutions" 。$`\newcommand{\cat…

靴やジーパンをネット通販で買うことを目指して： リーバイスのジーンズ - (新) 檜山正幸のキマイラ飼育記 メモ編 そうか、メモしておけばよい - (新) 檜山正幸のキマイラ飼育記 メモ編 無印良品〈MUJI〉ジーンズ： w31 (78.5cm) 股下 82cm 股下を 71.5cm に…

$`\require{color}% \newcommand{\Keyword}[1]{ \textcolor{green}{ \bf #1} }% \newcommand{\When}{\Keyword{when\:\:} }% \newcommand{\And}{ \Keyword{\:\: and \:\:} }% \newcommand{\Then}{ \Keyword{then\: } }% \newcommand{\Holds}{ \Keyword{holds\…

XyJaxを使った例 $`\xymatrix@R-1.8pc@C-2pc{ {} &*{A:Type} & &*{a:A \vdash F(a):Type} & \\ {}\ar@{-}[rrrr] & & & & \\ {} & &* {\prod_{a:A}F(a) : Type} & }`$ \xymatrix@R-1.8pc@C-2pc{ {} &*{A:Type} & &*{a:A \vdash F(a):Type} & \\ {}\ar@{-}[rrr…

「圏論 vs 順序論」の対応表が意外に抜けているので再作成。 順序 圏論 順序集合 圏 自己単調関数 自己関手 閉包作用素 モナド 自己単調関数のプレ不動点〈減少点〉 自己関手の代数 自己単調関数のポスト不動点〈増大点〉 自己関手の余代数 自己単調関数の最…

カントール 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)`$自己エミュレーション：$`\…

https://youtu.be/JEOKvG1zcbY?t=464

よくある二項対立的分類： クライアント vs サーバー 生産者 vs 消費者 送信側〈sender〉 vs 受信側〈receiver〉 順行〈順方向〉 vs 逆行〈逆方向〉 内部 vs 外部 変わった分類： エージェント vs 環境 データ vs 反データ 電子 vs 陽電子 電子と陽電子が出…

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

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

出現するたびに悪口を言っている。https://m-hiyama.hatenablog.com/entry/2020/09/07/165418 蒸し返し： アドホック多相 vs パラメトリック多相 '∀'は、もともとは記号論理の全称限量子〈universal quantifier〉の記号です。僕は、ここに'∀'を使うのは好き…

https://m-hiyama-memo.hatenablog.jp/entry/20171209/1512807104 からコピー 用語法、表記法 オペレーター | オペレータ | 演算子 | 作用素 | コンビネータ | コンビネーター コンストラクタ | コンストラクター | 構成子 | 構築子 | 生成子 例 トレースオ…

$`\newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\In}{\text{ in } } \newcommand{\B}[1]{ \{\!| #1 |\!\} } \newcommand{\A}[2]{ \langle\!| #1 \mid #2 |\!\rangle } `$$`\text{Basic} :::\\ \forall A \in |\cat{D}|.\\ \forall M \in |\cat{M}|.\\ \…

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

参考： 多相関数と依存型をちゃんと理解しよう 次をどう解釈すべきか？ length: ∀α.list(α) → Int次の例を見ると、 first: ∀α.list(α) → maybe(α)括弧の付け方は次のようになる。 length: ∀α.(list(α) → Int) first: ∀α.(list(α) → maybe(α))意味は、 length…