Wikipediaに ニコラース・ホーヴァート・ド・ブラウン という項目があるので、「ド・ブラウン」にする。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1} } %`$Automathの論文 "Telescopic mappings in typed lambda calculus" by N.…

まとめは「一貫性のまとめ」にある。「一貫性公理」は曖昧でヤバいから使用禁止とする。次を使う。 一貫性の基本射〈elementary morphism〉 基本射が同型なら基本同型射〈elementary isomorphism〉 一貫性条件： 基本射の組み合わせに対する等式の組 一貫性…

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

coherence nLab 一貫性の用語 続・一貫性の用語法 Wikipedia にある程度従うことにして： {一貫性の}?基本射〈elementary morphisms〉： 注目する生成射。 一貫性〈coherence〉： "various compositions of elementary morphisms are equal." であること。圏…

「依存アクテゴリーが面白い」という記事を書きました。実際僕は「面白い」と思っています。プロセスやシステムの記述と計算に使えそうだ、というところが心惹かれる理由でしょうかね。依存アクテゴリーはけっこう複雑な構造なので、定義を書き下すだけでも…

k-オペレータはk-射に作用するオペレータ、関手は (0 | 1)-オペレータ。 絵図要素 圏論 射の次元 ワイヤー 対象 Cの0-射 ノード 射 Cの1-射 ボックス 1-オペレータ Cの射ではない 細いストライプ 0-オペレータ Cの射ではない ストライプ 関手 Cの射ではない …

関連記事： SSH関連 - (新) 檜山正幸のキマイラ飼育記 メモ編 SSH関連 (2) - (新) 檜山正幸のキマイラ飼育記 メモ編 SSH関連 (3) known_hosts - (新) 檜山正幸のキマイラ飼育記 メモ編 この記事 ~/.ssh/known_hosts は、クライアントして接続する先のサーバ…

関連記事： SSH関連 - (新) 檜山正幸のキマイラ飼育記 メモ編 SSH関連 (2) - (新) 檜山正幸のキマイラ飼育記 メモ編 この記事 SSH関連 (3) known_hosts - (新) 檜山正幸のキマイラ飼育記 メモ編 C:\WINDOWS\System32\OpenSSH\ssh.exe と C:\WINDOWS\System32…

関連記事： SSH関連 - (新) 檜山正幸のキマイラ飼育記 メモ編 この記事 SSH関連 (2) - (新) 檜山正幸のキマイラ飼育記 メモ編 SSH関連 (3) known_hosts - (新) 檜山正幸のキマイラ飼育記 メモ編 困っていること で述べたように、~/.ssh/ が二箇所ある。さら…

内容： 設定ファイル（JSON） 目的 基本 秘密鍵ファイル名のコマンドライン指定 設定ファイルに秘密鍵ファイル名を指定 困っていること 設定ファイル（JSON） wt の設定ファイルの場所がややこしい！ $env:LocalAppData\Packages\Microsoft.WindowsTerminal_…

公理系を演繹的に拡大するメカニズムの定式化に： 閉包システム〈closure system〉 単純伴意システム〈simple entailment sysmte〉 バンチ伴意システム〈bunched entailment sysmte〉 双対バンチ伴意システム〈dual bunched entailment sysmte〉 伴意関係を …

クライアントにて： Windows Termina wt を起動。 ConoHa への接続のタブを開く。 ログインする。 接続情報は非常に分かりにくい場所にある。PowerShell構文で： $env:LocalAppData\Packages\Microsoft.WindowsTerminal_8wekyb3d8bbwe\LocalState\settings.j…

色付き／色無しは無意味で誤解をまねくリスクがあるので使わない。 対称／(非対称) ： 対称作用を持つか？ 対称構造の忘却で非対称になる。 モノイド／(非モノイド) ： モノイド積を持つか？ モノイド積の忘却で非モノイドになる。 ワイド／ナロー ： 多結合…

次のようなメタ記号を使う。$`\newcommand{\TS}{\mathrel{\,|\!-} } \newcommand{\TTS}{\mathrel{\,||\!-} } \newcommand{\TTTS}{\mathrel{\,|||\!-} } \newcommand{\Imp}{\Rightarrow } \newcommand{\Iff}{\Leftrightarrow } \newcommand{\In}{\text{ in } …

長谷川真人さんの "Classical Linear Logic of Implications"https://www.kurims.kyoto-u.ac.jp/~hassei/papers/clli.pdf ：加法的〈非線形〉コンテキストと乗法的〈線形〉コンテキストを持つ型判断〈typing judgement〉$`\quad \Gamma ;\Delta \vdash M:\si…

"Shapely monads and analytic functors" by Richard Garner, Tom Hirschowitz https://arxiv.org/abs/1512.05980 これが多圏類似構造のテキストとして非常によい。多圏類似構造の分類を絵算〈グラフィカル計算〉との関係で論じている。多射の図がどうなるか…

論域が大きい場合〈large domain of discourse〉を考える。 複アロー構成と多アロー構成、そのときのパラメータとしてのコレクションモナド コレクションモナドの一種としてのバンチモナド 型コンテキストと指標は同一概念であること。 命題コンテキストはフ…

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

リテラルは、シングの束縛〈割り当て | 結びつき〉を持つ名前〈ラベル〉 宣言文は名前〈ラベル〉へのプロファイルの割り当て ソフト定義文は名前〈ラベル〉へのコンビネーション〈項〉の割り当て、マクロ・ラベルを生成する。 ハード定義文は名前〈ラベル〉…

名前とラベルは同義語。束縛と割り当ては同義語。広義のタイピングとプロファイリングは同義。束縛にはハード束縛とソフト束縛がある（後述）。 束縛される前のラベルは変数 ハード束縛された後のラベルはリテラル 束縛の種類： ハード束縛： 名前〈変数〉に…

記述すべきモノを対象物〈objectum | オブジェクタム〉と呼ぶ。対象物の種別は意味範疇、文法内の品詞は構文範疇。次の意味範疇に属する対象物を扱う。 関数： 圏 $`\mathcal{TF}`$ の1-射、f∈Map(X, Y) 値・個体・データ ： 圏 $`\mathcal{TF}`$ のポインテ…

バンチ計算システムの構成素： 項 バンチ 書き換え規則 書き換えアクション 書き換え系列〈sequence〉 説明： 項は構文的コンビネーション ツリー構造 リーフは型付き変数または型付きリテラル、型は圏の対象 リーフ以外のノードはコネクティブ 文法範疇があ…

演繹システムの議論で、知識ベースの管理やダイナミズムの考慮が決定的に欠けていたと思う。知識ベースを $`\mathscr{K}, \mathscr{L}`$ などで表し、常に考慮する。知識ベースは、ハイパードクトリンやインスティチューションの生成系だと考える。生成され…

広義の項書き換え系について考えている。書き換えと置換〈substitution〉は区別しなくていいだろう。とりあえず、3種類の書き換え＝置換がある。 関数項置換： 変数／リテラルをリーフとし、関数記号をノードとする構文木において、部分木（リーフノードも、…

NPMでインストールできて簡単、と思ったら PowerShell から実行できない。.bin という拡張子のファイルを実行しようとして、データ扱いされる。cmd.exe では実行できる。Webで調べた解決策は： 環境変数 PATHEXT に .BIN を追加する。 自作のコマンドレット …

「命題」の曖昧性 真偽値 述語 論理式 （個体変数に関して）閉じた論理式 ところが、「論理式」が曖昧。 テンプレート述語項構文木（リーフが穴、ノードが述語コネクティブ） テンプレート述語項構文木＋述語コンテキスト 評価値である述語 型理論のときも、…

メタリーズニングの種類： ApplyReasoning : reas, deriv ≡> deriv ComposeReasoning : reas, reas ≡> reas ProductReasoning : reas, reas ≡> reas リーズニング 導出のマージ： MergeConj : conj → conj, con → conj ⇒ conj → conj MergeDisj : conj → dis…

$`\newcommand{\LLambda}{\mathrm{L}\Lambda} \newcommand{\Llambda}{\mathrm{L}\lambda} \newcommand{\RLambda}{\mathrm{R}\Lambda} \newcommand{\Rlambda}{\mathrm{R}\lambda} \newcommand{\Dia}{\diamondsuit} \newcommand{\mrm}[1]{\mathrm{#1} } \newco…

ド・モルガン双対 ド・モルガン双対をリスト〈バンチ〉に対して定義する。双対化演算は、 *(A1, ..., An) = (￢A1| ...| ￢An) *(,) = (|) *(A1| ...| An) = (￢A1, ..., ￢An) *(|) = (,) ** = id と定義する。推論規則は ￢ 左 (Γ → Δ| Φ) ⇒ (*Φ, Γ → Δ) …

シーケント計算をリーズニング構成の計算と考える。できるだけ少ないリーズニングで計算をしたい。リーズニングを少なくするには、プリミティブな導出を揃える。 ∧-モノイド構造 ∨-モノイド構造 ![A] Θ[A] Δ[A] ∇[A] π1[A, B] ι1[A, B] π2[A, B] ι2[A, B] X[…