大小関係、最小限と足し算との協調性 - (保存用) 檜山正幸のキマイラ飼育記 メモ編 を再掲。 証明要求： Γ |-? ∃a.∀x.a≦x BEGIN ∀-BOX var u 0 + u = u --[●∃導入 t:←左辺のu] ∃t.0 + t = u 0 ≦ u --[●∀導入 x:←u] ∀x.(0 ≦ x) END ∀x.(0 ≦ x) --[●∃導入 a:←0…

section 分数の定義と掛け算 { declare 0-mor F in Set define F := Int×(Int＼{0}) declare 0-mor 1 in F // オーバーロード define 1 := (1, 1) declare 1-mor m : F×F → F in Set reserve a, b, c ∈F reserve x, y ∈Int define m := λ(a, b).( (a_1×b_1, …

データベースへの操作で： 用法その1 update ： レコードの値を変更する modification ： update, create, delete 用法その2 update ： modification, create, delete modification ： レコードの値を変更する ちなみに、modification は 2-transfor だし。

MacOS向けインストール手順 Windows向けインストール手順 が分岐の具体例。記述単位〈モジュール〉の入り口条件として、 事実・自体が成立するか 知っているか、分かっているか 何かを実行したか、その結果、ある状態になっているか 練習問題を解いたか など…

リファレントの名前が http: から https: に変わっても同一性をもつので、同義語として処理すべきだ。が、やってない。

イニシャルなので似た名前の人の論文もリストされる。フルネームにしたところで、同姓同名ならやはり不正確。アイデンティティをアイデンティティファイできてない。academia.eduからも「お前、この論文書いたか？」とメールが来る。

国会図書館： https://id.ndl.go.jp/information/about/ から： シェークスピア シェイクスピア シェークスピヤ シェイクスピア, ウィリアム 沙士比阿 これらの表記のゆれを次の標準にマップする。 Shakespeare, William, 1564-1616 そういや、「ダイヤモン…

https://www.w3.org/TR/json-ld/ 笑ってしまったのが、そもそも、この文書内で使われている用語 term, context なんかが甚だしく曖昧。プレフィックス jld （JSON-LD）とか使って： jld:term jld:context とかしないと。ボキャブラリー（タームの集合）にボ…

[クラス=学級] [クラス=組] [クラス=授業] [クラス@日常] [(クラス=階級)@日常] [クラス@教育] [クラス@オブジェクト指向言語] [クラス@OOP] [クラス@関数型言語] [クラス=型クラス] [クラス@集合論] [クラス@数学] [クラス=真のクラス] [クラス=真のクラス=…

目次： 1 ‥‥ 1--3 2 ‥‥ 2--3 2.1 ‥‥ 3--3 2.2 ‥‥ 3--3 3 ‥‥ 4--6 3.1 ‥‥ 4--6 3.2 ‥‥ 6--6 索引： A ‥‥ 3 B ‥‥ 4, 5 C ‥‥ 6 D ‥‥ 4, 5, 6 E ‥‥ 3

Tenjinの0-指標はインターフェイス記述に使えるからIDLでもある。次が例題になる。 最小抽象ファイルシステム仕様をセミフォーマルに書いてみる - 檜山正幸のキマイラ飼育記 (はてなBlog)

if if if

以上より：もう少し書き換えると：成分は0か1に限る。固定したaに対して、1になれるβは高々ひとつだけ。まとめると： 成分は1か0だけ。 固定したaに対して、1になれるβは高々ひとつだけ。 シャープ射は部分関数。

variables (P Q:Prop) theorem sample (hp : P) (hq : Q) : P ∧ Q ∧ P := begin apply and.intro, -- 5 assumption, -- 4 apply and.intro, -- 3 assumption, -- 2 assumption -- 1 endtry it! ☆ ☆ ---------- 1 ---------- 2 P, Q → P P, Q → Q ☆ ---------…

core.lean 内の定義： @[inline] def band : bool → bool → bool | ff _ := ff | tt ff := ff | tt tt := tt notation x && y := band x y[inline] というアトリビュートがある。その場で展開されるのかな？アンダスコアは無名変数〈匿名変数〉で、パターン…

section funcomp variables {X Y Z:Type} def comp (f:X → Y) (g:Y → Z) :X → Z := λ x:X, g (f x) end funcomp #check comp infix `;` := comp constants A B C D:Type constants (f:A → B) (g:B → C) (h:C → D) #check comp #check comp f g #check f;g;h …

「用語ペアの関係性」の続き。 ⊆： 包含的 ⊆→ ： 規準的埋め込み可能 ⊥： 排他的 ∪： 総称 環、可換環、非可換環 用法 1： 環 ＝ 可換環 ⊆ 非可換環 用法 2： 可換環 ⊆ 非可換環 ＝環 用法 3： 可換環 ⊥ 非可換環、環 ＝ 可換環∪非可換環 数、単項式、多項式…

形容詞を 原子＝基本＝単純 として使おうと思っても： 原子論理式 ＝ 基本論理式 ＝ 単純論理式 ： OK 原子定理 ＝ 基本定理 ＝ 単純定理 ： 定理という名詞の意味から、基本定理、単純定理は別な連想が働く。 同義語扱いを増やすと、区別したいときに困る。…

基底変換、なにそれ？ - 檜山正幸のキマイラ飼育記 (はてなBlog) 「空間」と呼ぶが、空間ではないし（位相はないし）、群作用の特殊例。 随伴系はなぜ難しいか - 檜山正幸のキマイラ飼育記 (はてなBlog) 「ペア」と呼ぶがペアだけでは意味がない。

同義語・類義語： 基本、組み込み、ビルトイン、単純、アトミック、原子{的}?、プリミティブ、原始{的}?、既約、分解不能、素、生成｛的｝? 同義語・類義語 英語： basic, builtin, simple, atomic, primitive, reduced, irreducible, indecomposable, prime…

負号 単項演算子（足し算の逆〈反対〉を取る、反数演算の記号） 二項演算子（反数との和） 負号としてのマイナス記号はなくてもいい。が、負数はリテラル表記できなくなる。 二項演算子記号もなくてもいいが、煩雑になる。

関係性は： 同義〈同一〉である。 排他的である。 包含的である。 所属的である。 同型である。 埋入的である。 その他。 言語の基本： 国、地域、（人の）集団、文脈、状況、場面などで意味と用法が変わる。例： (単項式, 多項式) (数, 単項式) (数, 式) (…

sumii先生情報： > 「2x」や「x^2」は「多項式」ではない、 知りませんでした。確かに謎ですね。

Pは人の集まりで、“無作為な”標本抽出の確率分布μが載っている。3つの確率変数を、 そのときの年齢 a:P→N 身長 h:P→R 男女の別 g:P→{男, 女} として、同時確率変数 <a, h>, <a, g>, <h, g>, <a, h, g> などを考える。同時確率分布（無作為抽出測度の前送り）、部分周辺化＝条件周辺化、</a,></h,></a,></a,>…

現在作業中のメモ。形容詞「ドブ板」 - 檜山正幸のキマイラ飼育記 (はてなBlog) -- ドブ板計算 (苦笑)。対象がAが定義する、右からのA-掛け算関手 (-)□A と A-累乗関手 [A, -] が定義する随伴系の単位と余単位を定義する。そのために、ラムダ計算をテーラー…

H82 = 82文字ひらがな集合 H48 = 48文字ひらがな集合 H82 = 82文字反ひらがな集合 K48 = 48文字カタカナ集合 部分圏： Shiri[H48] は、Shiri[H82] の部分圏 H82の任意の部分集合X をとると、充満部分圏ができる。 長さ２以下の文字列だけを射とする圏が部分…

[n] = {1, ..., n} が作る集合・写像の圏 アミダ図の圏と置換（代入ではない）の圏 1,0を持つ半環係数の行列圏 ラベル付き boxes-and-wires 図の圏 ルシアン・アーディ図〈Lucian Hardy〉 一般論 インデックス付き圏としてのブール行列圏 弱いトポスとしての…

単なる集合からグラフを作る方法。 一端アロー化： Aに⊥を加えて、⊥→a （a∈A） をアロー＝有向辺 として足す。Aとアローは1:1に対応。 ニ端アロー化： Aに⊥, T を加えて、⊥→a→T （a∈A） をアロー＝有向辺 として足す。Aとアローは1:1に対応。 ループ化： ⊥を…

親子関係で入れ子になった指標＝ジニアロジーの書き方はまだ試行錯誤だけど、ともかくも、いくつかの論理的概念の定義を試みる。 3-signature { sort LoicalCat 2-signature { /* Cは論理的圏の構造を持った圏 Cでは、対象定数_Bや指数ベキが意味を持つ。 */…

後で追加修正するかも。指標の一覧： 名前 提供記号 ひとこと Magma * 乗法記号使ったマグマ UnitalMagma *, 1 単位的マグマ MonoidAste *, 1 モノイド MonoidPlus +, 0 モノイド Group *, 1, ~ 群 AbGroupPlus +, 0, - アーベル群 Ring +, 0, -, *, 1 可換…