指標（"インデキシング・ベース圏”の対象）と命題（{インデキシング垂直圏 | ファイブレーションのファイバーである圏}の対象）のペアを仕様と呼ぶ。仕様はグロタンディーク／エルブラン圏＝ハイパーベース圏の対象であると同時に、ハイパーインスティチュー…

重要なのはグロタンディーク／エルブラン圏である。 MLの概念 グロタンディーク／エルブラン圏 別な言い方 シグニチャー 仕様 セオリー ストラクチャ 絶対セオリー インスタンス ファンクタ 相対セオリー トランスフォーマー シグニチャに属するストラクチャ…

素材： 名前の集合 Name アンビエントドクトリン アンビエント圏C： アンビエントドクトリンから1つ選ぶ 論理ドクトリンL 以上から、指標圏と指標射が作れて、指標圏を定義できる。この指標圏をベース圏として、論理ドクトリンLに値をとるインデックス付き圏…

存在しなくなったターゲットを検出したい。バックグラウンド・バッチ処理。 存在しなくなったターゲットの代替を定義したい。 ブックマーク本体（body部）を別なリソースに書きたい。 ボディとターゲット以外に、関連リソースへのリンクを含めたい。 httpとh…

AtomエディタかVSCodeエディタを使おうかと思っている。現在作業中のEmacs（バッファを抱えている）のメモリー使用量（メガ以下は切り捨て）が 1プロセス 77M Atomを起動直後 5プロセス 2, 37, 123, 164, 184 VSCodeを起動直後 7プロセス 2, 12, 14, 22, 24,…

ストラクチャ＝{構造体 | クラス | 型クラス | レコード | 指標 | オブジェクト} トランスフォーマ＝{ファンクタ（SML） | 型クラス・インスタンス | セオリー} プロファイリング ： ストラクチャのメンバーの一部 バインディング ： ストラクチャのメンバー…

用語法、表記法 オペレーター | オペレータ | 演算子 | 作用素 | コンビネータ | コンビネーター コンストラクタ | コンストラクター | 構成子 | 構築子 | 生成子 例 トレースオペレーター 不動点オペレーター CADGの微分オペレーター／微分コンビネータ デ…

Erlangにパーズトランスフォームってのがあったけど、あんな感じだろうな。プログラミング言語であれば、そのプログラミング言語でパーズトランスフォームを書けたらいいが、専用構文のほうが可搬性はあるかもしれない。いずれにしても、入力構文の適当なタ…

「型」と「型つけ」の概念が曖昧。型の代わりにプロファイルを導入して、型つけ〈タイピング〉の代わりにプロファイリングを使う。型は対象のことだとして、型付けは、基礎射のプロファイリングの意味に限定して使う。つまり、f:->A in C の形のプロファイリ…

検索やソートに利用できる項目ソート／グルーピング ブックマークの生成時刻 タイトル文字列のソート順、あまり意味ねー URLのあるレベル（ドメイン名など）でグルーピングする。 人気順（ユーザー数が多い順） 検索／制限 タグによる検索 コメント内にある…

http://b.hatena.ne.jp/help/entry/port#export に従う。 ユーザー画面から設定画面に 「データ管理」タブに移動します エクスポートより、Atomフォーマットを選んで、右クリックでダウンロード。 何も変更しないと、ダウンロードのファイル名はdump.htmとな…

当然にインスティチューション 当然に述語論理＝ハイパードクトリン 限量子随伴性 ＝ ΣΔΠ随伴性 否定があるなら、否定双対性。スター自律圏かな？ 継続との関連は？ 契約は仕様と関連するから、メイヤー先生のDbCとは関連する。 仕様モジュール、セオリー・…

スペクトラム〈spectrum〉の複数形がスペクトラ〈spectra〉。スペクトルはスペクトラと同義だろう。forvoでは、 https://ja.forvo.com/search/spectra/ 「ペッ！」を強調するスペクトラと聞こえる。スペクト「ル」とは聞こえないがaが消えるとspectrで「ル」…

name object 呼び名 圏論 変数名 型 型宣言 指標対象成分 関数名 項 関数 指標射成分 ラベル 命題 表明 論理対象 定理名 証明 定理 論理射 名前の宣言 name 宣言 名前のソート ソート式 変数名 var x:X 型 型項 関数名 function f:(x:X, y:Y)->Z プロファイ…

Sを指標圏、Lを論理ドクトリンとするハイパードクトリンH:S→Lがあるとする。Σ∈|S| に対してH[Σ]は指標Σ上の論理圏であり、その論理圏は論理ドクトリンLに所属する。ハイパードクトリンHをインデックス付き圏とみなして、そのグロタンディーク平坦化をTheo(H)…

計算解釈 論理解釈 項 証明 項ブロック 証明ブロック ユニット型 真 エンプティ型 偽 型 命題 型構成子 論理結合子 依存型構成子 限量子 定数 公理 関数 定理 関数の定義項 定理の証明 関数のヘッダ 定理のヘッダ 定数・関数名 公理・定理ラベル 関数コンビ…

ドクトリンは、CCCのような、Cat上の具象圏だとする。ハイパードクトリンは拡張されたドクトリンくらいの意味だが、 ベース圏（論域の圏）の上のインデックス付き圏であり、余域はCCCのようなドクトリンになる。 ベース圏の射に対して、ΣΔΠ随伴性がある。Σは…

ハイパードクトリン インスティチューション ベース対象 型コンテキスト 指標 ベース射 コンテキスト拡張／置換 指標射 ファイバー 命題の圏 モデルの圏 誘導関手 引き戻し リダクト関手 随伴関手 限量子 - 妥当性 - 充足関係 こうして見ると、限量子随伴性…

カリー／ハワード対応を信じるなら、関数の記述と定理の証明はまったく同じはず。だったら同じ書き方ができるはず。 // f:X×Y→Z function f given x:X, y:Y ensures Z begin ... end // t:A∧B→C theorem t given a:A, b:B ensures C begin ... end関数定義に…

管理・配布のメカニズム パッケージ バージョン（パッケージに付く） スクリプト（物理的にはファイル、拡張子は.tenjinscript） モジュール（スクリプトに制限を付けたもの、拡張子は.tenjin） リポジトリ インターネット上でパッケージを保存している場所 …

定理記述 - 檜山正幸のキマイラ飼育記 メモ編の続き。少し変える。 theorem 定理の名前 import モジュール1, モジュール2 for 宣言1, 宣言2 given 命題1, 命題2 ensures 命題 begin 証明 end endproofという語は避けた。 圏論 論理 始対象 False 終対象 True…

名前空間の構造化に関連する概念 名前空間の親子関係 シャドーイング 入れ子名前空間（ブロックスコーピング） 上掛け（overlay）名前空間 大域名前空間 名前付き名前空間 無名名前空間 名前空間もオブジェクトと考えてツリー構造をなす。ルートノードの名前…

個別のツールやらその使い方やらでは問題があったりするが、全体としてみるとWebフロントエンドというか、むしろNode.js中心のコミュニティはなかなか凄いものがある。人口が多いとエネルギーの総量も大きいから（中国が凄いのと同じかも）。まず、感心して…

ここでのタグはブログエントリーとかブックマークエントリーとかに付く文字列のこと。タグ付け（＝タギング）する対象であるモノをアイテムと呼び、アイテムの全体をアイテム空間と呼ぶ。アイテム空間はひとつだけ想定する。タグ空間は複数あってもよい。 単…

コマンドは、先頭が動詞原型または動詞過去分詞形、それに続いてキーワード目的語名詞が続いてもいい。apply, make conjunction, found inconsistency など。「命題 by 根拠名詞 引数並び」でも証明が書けるとする。以下、根拠名詞とコマンド動詞の対応表。 …

命題、証明、規則をそれぞれ0-射、1-射、2-射の意味で使う。 公理 公理証明 ax_A : * -> A * ----[ax A] AAx⊆|C| なので、Axは命題の集合として与えられるが、それはデカルト閉圏の特殊事情で、一般には、 a : X -> A X ---[a] Aつまり、Ax⊆Mor(C)。Axはどん…

A1, ..., Anを仮定（assume）してBを結論（conclude, entail, result, produce, show）する証明があるとき、その証明内で使っている暗黙の知識がある。これを証明の文脈とか環境と呼ぶ。で、文脈とは正確には何か？ が大問題。それと、トンネル論法（コンパ…

Webフロントエンドでの話 - 檜山正幸のキマイラ飼育記 メモ編 の続き。browserify, babele, webpackとか。 babelはトランスパイラである、と。で、browserifyはトランスパイラとは違うのか？ browserifyは、依存性を分析してブラウザー向けに変換するのかな…

Webフロントエンドとは縁がないのでよく知らんが、ビルドツールは 最近のビルドツールって何なの？ - 檜山正幸のキマイラ飼育記 で取り上げたことがある。2017年前半に、bowerというツールも終焉したらしい（よく知らんが、ご愁傷様）。 https://qiita.com/M…

ざっと調べたが、雑でイイカゲンで未完成である。一般的な概念 モジュールとパッケージ：モジュールを集めてパッケージ パッケージマネージャ グローバルインストールとローカルインストール プロジェクト： 作業をするための環境 パッケージのメタ情報 パッ…