気付いた
半グラフは開放辺を持つ無向グラフである。半グラフに対するアンカリングとは： Aアンカリング： 各頂点に接続する辺の集合に全順序を入れる。Aは All ports から。 Bアンカリング： 各頂点に接続する辺の集合を二分割して、2つのパートにそれぞれ全順序を入…
自然数集合から可換モノイドへのインスタンスメーカーが3つあって、 足し算 掛け算 最大値（小さくないほう） 最小公倍数 それとは別に、ベキ等可換モノイド（演算記号 ◇）をジョイン（演算記号 ∨）半束にするインスタンスメーカーがあるとする。インスタン…
指標Σに対して、モデルの集合は |Model[Σ]| となる。適当な集合 K からの写像 K → |Model[Σ]| をインスタンスメーカー〈クリエイター | コンストラクタ | ビルダー〉と呼ぶ。なんらかの忘却射影 U:|Model[Σ]| → K があり、インスタンスメーカーがセクション…
コンテキストと指標は、構文的には区別できないのだが、次の違いがある。 指標はインスティチューション的な意味での指標である。 指標のあいだの射は指標射で、モデル圏のあいだのリダクト関手を定義する。 コンテキストは、固定した指標に対する構文的圏の…
宣言のみからなるテレスコープ〈依存レコード | 指標〉を純コンテキストと呼ぶことにする。宣言と割り当てが混じったコンテキストを混合コンテキストと呼ぶ。純コンテキスト〈指標〉のあいだの手続きは多型判断〈poly-typejudgement〉と言ってもよい。次が予…
型 ←→ 命題 ←→ 対象 関数（要素含む） ←→ 定理（証拠含む） ←→ 射 関数コンビネータ ←→ 定理コネクティブ？（言及も命名もされない） ←→ オペレーター／コンビネータ リーズニング・コマンド 対応物がないゲーム・コマンド 圏論的に整理するなら もの〈シン…
次を区別しなくてはならない。 命題 証明〈証拠〉 判断〈主張〉シーケント 質問〈問題 | 問い合わせ〉シーケント フォワードリーズニング（推論ルール含む） バックワードリーズニング（バックワード推論ルール含む） 定理は、証拠〈証明〉を引数として証拠…
あれ、型付きプロセスの概念が急にわかってしまった。プロセスのプロファイルを書くには、時間が入った型が必要。線形時間ならたとえば正規表現が型として使える。分岐時間ならツリー形状をベースにした型だ。型の定義にオートマトンが使えるだろう。
本編の https://m-hiyama.hatenablog.com/entry/20100416/1271386224 で、reference<WebSite>型とかを出したけど、第二型引数を認める reference<T, A> ： 参照先の型はT、トリガーオブジェクト〈アンカー〉の型はAである参照型 すると： reference<integer, address> はメモリーオブジェクト</integer,></t,></website>…
直接的な関係を意識せずに考えていた次のようなトピック、 git JavaScriptのモジュール方式（CJS, ESM） NPMパッケージ 概念設計とコース設計 ストリング図とオープングラフ などが、同一の問題なのだと気付いた。有向グラフの取り扱いと利用法の問題だった…
まさに気付いたことだが； アカウントデータベース - (新) 檜山正幸のキマイラ飼育記 メモ編 で、アカウントは、二部グラフの有向辺として定式化できると書いたが、gitの構造もグラフ構造で定式化できるだろう。git自体のグラフ的解釈は、本編 もうGitは怖く…
bitbucket 2022 (2) - (新) 檜山正幸のキマイラ飼育記 メモ編 から気付いたこと、考えたこと。内容： アプリパスワード gitのクレデンシャルヘルパー 錯綜の要因 追記 アプリパスワードbitbucketは「アプリパスワード〈App password〉」という用語を使ってい…
アカウントデータベース - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。登場する存在物〈エンティティ〉は、行動主体と行動環境だが、行動環境が行動主体の参加〈ログイン〉への許可するという意味で「認証する側」、行動主体＝ユーザー は「認証される側…
SSH関連の概念的まとめ - (新) 檜山正幸のキマイラ飼育記 メモ編 を書いていて気づいたのだけど； アカウントを記述する二部グラフは、グラフDBだと思えるから、アカウントデータベースとはグラフDBということだな。パスワード管理ソフトの LastPass では、 …
靴はオンラインでは書いにくい、と思っていたが、気に入った靴を決め打ちにして、同じ型番のものを買い続ければいいのか。「いつも同じ靴」現象は起きるが、楽ちんさが勝る。
コンステレーションの図示にいおて、1次元キャンバスの場合も2次元に描く習慣があるのか？ -- これは混乱のもとだな、良くない。 1次元穴あきキャンバス： 区間に穴が開いている。穴は幅0でも有限幅でもいい。穴の境界にプロファイル情報が載るが、それは A …
index.js, index.ts とかでメインエントリーポイントを指定する習慣があるが、これはやめたい。 ファイル名だけでは何をするものか想像ができない。ディレクトリ名／プロジェクト名の情報が別に必要。 コピーして上書きする危険がある。 パッケージ／ディレ…
「‥‥とは何か？」という疑問・質問。例えば「型とは何か？」 合意目的の質問： 何かを便宜的に約束しよう、という提案 追求目的の質問： 一意的なホントの意味を探ろう、という提案 追求目的のの質問は、追求すべき実態が存在しないとナンセンスになる。しば…
多様体の定義を見ていて思ったこと。 多様体やその点が実体としてまずある、から出発する流儀 測定器と測定値がまずある、から出発する流儀 それぞれ、実体主義、測定主義と呼ぶことにする。現代のメジャーな多様体の定義は、実体主義的だが、昔は測定主義的…
$`\newcommand{\mrm}[1]{ \mathrm{#1} }% \require{color} % 緑色 \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\ClassOf}{\Keyword{ClassOf } }% \newcommand{\Things}{\Keyword{ Things} } %`$関係圏を2-圏のインスタンスとみ…
次の図のSのようは関手を、Fに沿ったエキストラセクション〈extra section along F〉と呼ぶことにする。エキストラセクションの全体を とする。引き戻しファイバー付き圏との関係はファイバーバンドルの場合はに対して、エキストラセクションの空間は色々な…
ファイバーバンドルとファイバー付き圏の類似性は思っていたよりずっと精密で本質的なようだ。$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\hyp}{ \text{-} } %`$ ファイバーバンドル ←→ ファイバー付き圏 底空間 ←→ 底圏 インデックス付き空間 ←→ …
位相空間の離散位相と同様に、任意の圏に自明グロタンディーク位相が入る（https://ncatlab.org/nlab/show/trivial+topology）。自明グロタンディーク位相が入った圏を離散サイトと呼ぶ。すると、前層と層の区別をする必要がない。あらゆる前層は層とみなせ…
デカルト閉復圏とラムダ計算 - (新) 檜山正幸のキマイラ飼育記 メモ編、ラムダ図 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。とても良い描画法を思いついた。青で書いているのは黒がなかったせい。ラムダハウスは関手ボックス／関手ストライプ／オペレ…
連言ボックス、選言ボックス、全称ボックス、存在ボックス - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。モヤモヤを晴らすためにすること。 ラムダ項の圏論的位置付けをハッキリさせる。 単なる圏ではなくて復圏〈オペラッド〉を使う。 デカルト閉復圏＝…
考えながらダラダラと書く。まず普通のシーケント計算： Γ, A ⇒ B ---------- 含意導入 Γ ⇒ A→B Γ, x:A ⇒ P(x) ----------------- 全称導入 Γ ⇒ ∀x:A.P(x)こう見ると確かに似てる。PがAとの依存性がないとは、P(x) = B が常に成立。よって、∀x:A.P(x) = ∀x:A…
選言ボックスと二面ノード - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。絵は裏写りがすごくて、ゴミが入っていたりする。図の右下はゴミ（別な図の一部）。左から右、上から下の順で説明。 ∀elim ： ∀i∈I.A ⇒ A(a) （⇒はシーケント矢印）の証明。ケーブ…
いいこと思いついた。たいぶいいこと思いついた。NK風証明図のストリング図による描画で、けっこう困るのが選言〈論理OR〉の処理。これの描画法を思いついた。思いついた時系列に沿って説明する。分配法則 A∧(B∨C) ⇒ A∧B ∨ A∧C （シーケント矢印は二重矢印）…
almost surely equal w.r.t. P を P-a.s.e と略記し、=P-a.s. と書く。 almost empty set = almost impossible event almost total 日本語では： Pに関してほとんど等しい（surelyの「確実に」は要らない） ほとんど空、ほとんど起こり得ない、ほとんどあり…
