ステイ／メレディス(↓)から辿って、主にローヴェル・セオリー関係の文献。 Logic as a distributive law Mike Stay, Lucius Gregory Meredith 17p https://arxiv.org/abs/1610.02247 ステイ／メレディス(↑)が参照しているもの。まずはハイランド／パワー： T…

コンピュータッドは図形的な対象。シリンダを作ることは意味がある。シリンダはホモトピーと関連する。写像錘とか錐体、簡易懸垂とか、色々と図形的な構成が出来る気がする。コボルディズム圏も作れるのではないか。単に、コンピュータッドの射を考えるので…

defintion and example - 檜山正幸のキマイラ飼育記 メモ編 同義語・多義語の例 - 檜山正幸のキマイラ飼育記 メモ編 指標とモデルと意味論 - 檜山正幸のキマイラ飼育記 メモ編 代数的定義形式とアンビエント構造 - 檜山正幸のキマイラ飼育記 メモ編 決める側…

coherence {axiom | equation | relation | identity | constraint | law} {一貫性 | 整合性}{公理 | 等式 | 関係 | 恒等式 | 制約 | 法則}

要らないものを多そうだが、、、JPEG画像だけを探してみると： ~\.emacs.d\image-dired\ の下に大量の画像、すべて一時的。 .emacs.d -> Dot.emacs.d というシンボリックリンクがある。このためにimage-diredのキャッシュ画像が二重に検索される。 ~\ に若干…

{definition (form)? | specification | signature | (type)? class | interface | concept} {example | model | (type)? instance | structure | implementation | class | algebra}

表記のゆれも考慮すると、用語表記は爆発する、という話。 https://ncatlab.org/nlab/show/Lawvere+theory 考えられる表記は、まず、 {代数的 | ローヴェル}{理論 | セオリー} 「ローヴェルの代数的セオリー」もある。「的」の有無もあるから、 {代数(的)? |…

匿名性、非差別性 - 檜山正幸のキマイラ飼育記 メモ編の続き。環境依拠主義（って言葉が適切な気はしないが）は、要素還元主義とは違う（たぶん対極的）。なぜなら、対象（圏論の意味での対象でもあり、一般的な語彙としての対象でもある）を解体（分解、腑…

要素還元主義と環境依拠主義 - 檜山正幸のキマイラ飼育記 メモ編の続き。nLab記事 https://ncatlab.org/nlab/show/principle+of+equivalence の同値性原理〈principle ofequivalence〉は、 リスコフの置換原則 「インターフェイスに対してプログラミングせよ…

仏教 大乗仏教中観派と一般モデル理論 - 檜山正幸のキマイラ飼育記 スノーグローブ スノーグローブ現象 再び - 檜山正幸のキマイラ飼育記 マイクロコスモ原理 マイクロコスモ原理の恐怖 - 檜山正幸のキマイラ飼育記 入れ子 入れ子の世界が大好きだけど怖い -…

愚痴： さまざまな「ならば」達 - 檜山正幸のキマイラ飼育記 文字や記号はいつだって足りないのだ - 檜山正幸のキマイラ飼育記 論理記号のいろいろ - 檜山正幸のキマイラ飼育記 型推論に関わる論理の概念と用語 その1 - 檜山正幸のキマイラ飼育記 絵算（スト…

ステイ／メリディスの次の論文、とても良い。 Title: Logic as a distributive law Author: Mike Stay, Lucius Gregory Meredith URL: https://arxiv.org/abs/1610.02247 僕がふだん考えていることだから、問題意識が一致して分かりやすい。本論じゃないとこ…

困った時の米田頼み、ご利益ツールズ - 檜山正幸のキマイラ飼育記 で述べたこと： 自然演繹とシーケント計算の関係は、僕が長年興味を持っているテーマのひとつです。ある程度は理解しているつもりなんですが、なんかスッキリしない。説明しろと言われれば出…

代数的定義形式とアンビエント構造 - 檜山正幸のキマイラ飼育記 メモ編 の続きで、ローヴェル・セオリーを可能とするフレームワークについて。ローヴェル・セオリーローヴェル・セオリーの導入・説明では、有限集合の圏FinSetの骨格として、基数（それ自身集…

昨日 代数的定義形式とアンビエント構造 - 檜山正幸のキマイラ飼育記 メモ編、次の用語を導入した。当たり前で自己説明的な言葉だと思う。 (n-)?代数(的)?定義(形式)? (n-)?定義(形式)? 同義語が： (n-)?指標 (n-)?仕様 (n-)?セオリー (n-)?型クラス (n-)?イ…

内容： 代数的定義形式 代数的定義形式の同義語群 アンビエント 定義形式のアンカリング 単位対象と格上げ 値k-射と定義形式の格上げ モデルとモデルの圏 TBD：ローヴェル・フレームワーク TBD：族と抽象と脱抽象 代数的定義形式n-圏と関連する圏論的実体〈c…

0≦k≦n に対して、(n, k)-シングルトン圏と呼べるn-圏がある。 (n, 0)-シングルトン圏は、ただ1つの対象〈0-射〉を持ち、すべての射が恒等射（自明射）であるn-圏。 (n, k)-シングルトン圏は、ただ1つの非自明なk-射を持ち、それ以外のすべての射が恒等射（自…

トランスフォーマーを考えると、定義体の内部で使う名前の供給源として、 名前は環境から供給される（名前は環境内のモノを参照する） 名前は引数から供給される（名前は引数内のモノを参照する） 名前はパラメータから供給される（名前はパラメータ内のモノ…

7zip AutoHotkey : Powershell用にBetterPSKey.exeを作った。これはスタンドアロンだから移動可能か？ CarotDAV : 必要になったら。 CatDataIDE : とりあえずいらん。 J言語 ： とりあえずいらん LastPass Thunderbird OMake Mercurial Ritouch Pilot Skype …

n-圏Cがあるとして、この対象が何であるによって扱いが変わると思う。 |C|∈0-Cat であるとき、Cの深さは0。このとき、対象類＝0-モーシングは集合。 |C|∈1-Cat であるとき、Cの深さは1。このとき、対象類＝0-モーシングは圏。圏を対象とするn-圏。 |C|∈2-Cat…

"Monoidal Topology, A Categorical Approach to Order, Metric and Topology" 508ページのPDF http://sweet.ua.pt/dirk/artigos/HST14_Monoidal_topology_A_categorical_approach_to_order_metric_and_topology.pdf モノイド概念がトポロジーにも使える、と…

本編で書いた米田モナドだが、 http://d.hatena.ne.jp/m-hiyama/20180110/1515553121 次の論文にほとんど書いてある。 https://arxiv.org/abs/1612.03678 上記本文では、単に前層モナドと言っている。台が前層関手だから。前層モナド＝米田モナドは、PSh:Cat…

Standard MLではモロに関手（functor）と呼んでいるのだが、やり過ぎだと思うので： トランスフォーマー： 現状、これを使っている。問題は、自然変換のトランスフォーメーションと似ていること。 リダクト： インスティチューションではリダクト関手（reduc…

本編の追記に書いたが、 http://d.hatena.ne.jp/m-hiyama/20180117/1516157225 網羅性のチェックにnever変数への代入というトリッキーな方法がある。この方法は、次のページにあった。 https://basarat.gitbooks.io/typescript/docs/types/discriminated-uni…

割とVSCode使ってるが、emacsの場合： c-indent-level, c-basic-offsetは効かない。 tab-widthは効く。がそもそもタブは使いたくない。 indent-tabs-modeをnilにすると、タブは使わなくなる。 c-tab-always-indentという変数もある。たぶん効かないが、これ…

だいぶ昔、スクラッチバッファに書いてあった重要なメモがなくなって困ったことがあって、スクラッチバッファを保存するスクリプトを入れていたんだが、いつのまにかその設定とかELispファイルとかなくなっていた。ごく最近、同じくスクラッチバッファを失っ…

第一級オブジェクトとしてのトランスフォーマーを考えると： トランスフォーマーに名前を付けられる。名前無しでも扱える。 概念的には、トランスフォーマーが等しいかどうかを判定できる。現実的には無理なこともある（つうか、たいていは無理だけど）。 ト…

今まで、指標はコンピュータッドの同義語としてきたが、どうも違う。その違いは指標は名前（ラベル）があること。単なるグラフとラベル付きグラフの違い。2つの指標をとると、まったく無関係とは限らない。ラベリングによって、必然的にスパン構造＝貼り合わ…

宣言（名前のプロファイリング）と定義（束縛、名前のアタッチング）をゴッチャに混ぜて書いた形式をミクスチャと呼ぶことにする。 mixture Succ := { type X; X := int; value e: X; function succ : X->X }これはミクスチャの例。同じ名前に対して、「宣言…

シャドーイングの問題 - 檜山正幸のキマイラ飼育記 メモ編の続き。入れ子 Σ | Δ があるとき、シャドーイングがあろうとなかろうと、Σ←Σ'→(Σ' + Δ) ができる。この事実から、一段階の入れ子はスパンで表現できることがわかる。一般のスパンではなくて、両脚が…