課題
型付きJSON（むかし、XIONとかXJSON呼んでいたヤツ）をマクロで実装する。 ベキ等可換モノイドからジョイン半束を作る。 乗法ベキ等可換環のスペクトル理論（昔のブログ記事にある） 距離連続写像は位相連続写像である。 定義・証明だけでなくて組織化を注意…
次のようなキーワードの名前スコープと使い方について考える。 def, theorem let in, let return providing return where section module package 名前とスコープに関する概念： イミュータブル名〈プログラム定数〉とミュータブル名〈プログラム変数〉 公理…
宣言のみからなるテレスコープ〈依存レコード | 指標〉を純コンテキストと呼ぶことにする。宣言と割り当てが混じったコンテキストを混合コンテキストと呼ぶ。純コンテキスト〈指標〉のあいだの手続きは多型判断〈poly-typejudgement〉と言ってもよい。次が予…
structure PreOrder where U : Type le : U → U → Prop le_refl : ∀(x : U), le x x le_trans : ∀(x y z: U), (le x y ∧ le y z) → le x z inductive ab where | a | b def ab_le (x : ab) (y : ab) : Prop := match (x, y) with | (.a, _) => True | (.b, .…
オリジナル vs 生成 本体 vs 周辺物〈ペリフェラル〉 オリジナル 生成 本体 ◯ ☓ 周辺物 △ ◯ ☓は存在してはいけない。△はあり得る。周辺物では、オリジナルと生成物を組み合わせる必要があるかも知れない。用語集がその例。これは課題。
用語集〈glossaly〉の半自動生成 用語索引の自動生成 参考文献リストの半自動生成 目次＝ナビゲーションの自動生成（パッドからの情報で） 記号索引の自動生成 チャレンジング 図や表のリストの自動作成 これは目次と同じか 脚注一覧とかも。 タグ検索、メタ…
バンチと圏論を使えばいいのに - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。一般論だが； 集合、部分集合、要素の区別はけっこう難しい。要素と単元集合、ボトム要素と空集合などがある。同様にクラス／型とインスタンスの区別も難しい。クラス／型はス…
曖昧、明瞭化したい。 作業 作業工程 過程、プロセス ワークフロー タスク アーティファクト〈成果物〉 デリバラブル〈成果物〉 プロダクト〈製品〉 プロダクション〈作成 | 製造〉 ビルド デプロイ デリバー イシュー チケット
ユーザー（読者）目線で。 自動タームリンク、記事ごとに辞書を変える。 https://think-like-a-git.net/ のようなキーボード操作、U で UP も欲しい。 https://graphql.org/learn/queries/ のように見出しの一部をクリックするとURLのフラグメントIDが変わる…
unistのツリー構造とJSON-LDを統合できないだろうか。
参照可能性を確保するのが重要。それには次の行為が必要。 ラベリング： 外部から参照される項目〈アイテム〉に名前を付ける。 タギング： 外部から参照されるタグを付ける。タグは分類タグと話題タグ。 参照： 公開されている項目を参照する 参照マッピング…
bitbucket 2022 (2) - (新) 檜山正幸のキマイラ飼育記 メモ編 から気付いたこと、考えたこと。内容： アプリパスワード gitのクレデンシャルヘルパー 錯綜の要因 追記 アプリパスワードbitbucketは「アプリパスワード〈App password〉」という用語を使ってい…
次の記事の内容を今の言葉で書き直す。 n-セオリーとインスティチューション - (保存用) 檜山正幸のキマイラ飼育記 メモ編 セオリーとインスティチューション - (新) 檜山正幸のキマイラ飼育記 メモ編
課題と参考文献： インスティチューションがうまく使えない - 檜山正幸のキマイラ飼育記 (はてなBlog) 2005年7月の疑問・課題 はじめての圏論 その第5歩：変換キューの圏 - 檜山正幸のキマイラ飼育記 (はてなBlog) はじめての圏論 第6歩：有限変換キューと半…
参考： 多相関数と依存型をちゃんと理解しよう 次をどう解釈すべきか？ length: ∀α.list(α) → Int次の例を見ると、 first: ∀α.list(α) → maybe(α)括弧の付け方は次のようになる。 length: ∀α.(list(α) → Int) first: ∀α.(list(α) → maybe(α))意味は、 length…
Title: A Taste of Categorical Logic — Tutorial Notes Authors: Lars Birkedal (birkedal@cs.au.dk), Aleš Bizjak (abizjak@cs.au.dk) Date: July 10, 2017 URL: https://cs.au.dk/~birke/papers/categorical-logic-tutorial-notes.pdf これは良いチュート…
大事なことは、スキーマとインスタンスの扱い。スキーマ間の射の特別な場合がインスタンス。スキーマは、ラベルに対して型〈ソート〉を割り当てる。あるいは、型式〈ソート式 | 0-コンビネーション〉を割り当てる。つまり、スキーマは0-指標。スキーマのあい…
TypeScript の型定義ファイルと仲良くなろう - Hatena Developer Blog は良い解説だが、entity, container がイマイチ不明瞭。まず、entity とは、型付きの名前（値はない）、または名前と値のペアのどちらか。名前があることを強調したいなら named entity …
TypeScriptの名前構造を基準に考える。宣言空間とは、パーティションされた名前コンテナのパーティションのことで、通常は「名前空間」だが、名前空間が内部モジュールの意味なので宣言空間としている。宣言空間は、名前の集合というよりは、順番があるので…
TypeScriptの名前構造を基準に考える。宣言空間とは、パーティションされた名前コンテナのパーティションのことで、通常は「名前空間」だが、名前空間が内部モジュールの意味なので宣言空間としている。宣言空間は、名前の集合というよりは、順番があるので…
ストレージの日本語は「格納器」にするかな。格納器には次がある。 ファイルシステム ： ファイル名／パス名がキー 各種データベース ： IDフィールドの値がキー プログラミング言語が管理するメモリー空間 ： ハッシュマップ／ディクショナリのキーがキー …
RDFトリプルを (S, P, O) と書く。トリプルを宣言文とみた場合にトリプル文と呼ぶ。単一のリソース S だけを書いた文はシングル文。トリプル文の意味はRDFのとおりとして、シングル文は、その固有リソース〈エンティティ〉が存在することを主張する。 トリプ…
神崎さんの https://kanzaki.com/docs/sw/rdf-model.html を読みながら： RDFによって「関係の連鎖を辿ることができる」とあるが、これはリソース間の関係であって、リソースと値の関係（＝属性）ではない、と解釈したほうがよさそう。 混乱してしまうのは、…
最近のことは全然知らんかったが： ツールなどは共用〈sharing〉スタイルから隔離〈isolation〉スタイルに変わった。ディスク領域が気になる爺さんには抵抗がある。 ツールセットの相性がバージョンアップにより壊れてしまうなど、複数プロジェクトでの意図…
単純タギングとキー／バリュー・メタデータの関係性。キーの同義性や、キーのURI展開（RDF的なやつ）。
レンダリング関係： 数式が使える。 ストリング図が描ける。 ペースティング図が描ける。 graphvizグラフが描ける。 構造関係： gerbyのような参照が出来る。 命題・証明の依存関係が出力可能。 指標が書ける。バンドルではなくて散在記述〈scattered descri…
可換モナドとラックス・モノイド・モナド（動機も少し） - 檜山正幸のキマイラ飼育記 (はてなBlog) 指標の圏の上の構文モナドのクライスリ圏を考えるのが基本。だが、圏とその反対圏を同時に考えて、ストリング図を使うと混乱しがち。ストリング図の併置は直…
SSL証明書の更新手順。 ファイルのバックアップ。これは、ローカル側のバックアップの問題も含む。 ログの管理。 画像のリンク変更 [追記 date="2021-09-13"]画像のリンク修正は 画像ファイルの置き場所 - (新) 檜山正幸のキマイラ飼育記 メモ編 で述べたこ…
次の列挙型に特殊フォルダ名が含まれる。 Environment.SpecialFolder 列挙型 (System) | Microsoft Docs だが、Downloads/, Camera Roll/, Saved Games/ などは見つからない。Downloadsの場所が知りたいことはある。どうもこれらは別扱いで、"shell:***" で…
[追記]概より緩〈relaxed〉がいいかも[/追記]Xは標準ボレル空間として、 Π(X) ： X上の有限測度〈有界測度〉の全体、ベクトル錐〈半体上の半ベクトル空間〉 Π=1(X) ： X上の確率測度の全体、凸代数〈凸空間〉 Π≦1(X) ： X上の劣確率測度の全体、凸代数〈凸空…
