曖昧表現は： 名前・記号の借用 例： G = (G, *, 1) 省略 例： G = (G, *) 名前・記号の多義的使用〈オーバーロード〉 曖昧表現の解決は、データベース検索。検索条件はパターンマッチ問題〈ユニフィケーション問題〉となる。パターンマッチ問題を解いて曖昧…

次の計算系がある。 計算対象物 CC圏 CC複圏 CC多圏 （広義）射 ◯ ◯ ◯ コンビネータ △ ◯ ◯ アレンジメント △ ◯ ◯ CCは Cartesian Closed ◯：うまく定式化できる。 △：ある程度は定式化できる。 演算： 射に対して： 結合、直積、カリー化、評価 コンビネータ…

lambda ： ラムダ抽象 assume backlog ： バックログラムダ抽象 postulate / demand 要請、ラムダ抽象だがバックログだとマークする。ラムダ変数はバックログ変数＝スタブ＝ダミー。 prepare ： 引数の準備 next ： 区切り記号 and_also ： 区切り記号 end …

関数があるとき、引数型と戻り型の仕様が型プロファイル、単にプロファイルとも呼ぶ。プロファイル概念は集合圏の射以外でも考えられる。引数変数を含む項を使って関数を定義するときの $`\cdots \mapsto \cdots`$ は戻り値指定〈return value disignation〉…

視点移動とフットワーク： 階層的宇宙のなかで自分がどこのいるのか？ 区別する／区別しない（同一視する／しない）、どちらの立場か？ 例： 引数なし関数名と定数名 名前が定数名〈固有名〉か変数名〈不定名〉か？ スコープに依存（事項）。 名前のスコープ…

$`\Gamma \mapsto \psi : T`$ が判断のとき、コンテキストのラベル〈名前〉をすべて取り除いたものを $`\widehat{\Gamma}`$ とする。プロファイルは：$`\quad \widehat{\Gamma}\to T`$$`f := \big\langle \Gamma \mapsto \psi : T\big\rangle`$ が定義のとき…

圏論 型理論 論理 メタ論理 指数 [_, _] [_→_], → ⇒, → (⇒) 項の定義 |→ |→, |- |-, |→ (|-) プロファイル → →, ~~> →, ~~> (→) ホムセット {_→_} {_→_}, {_~~>_} {_→_}, {_~~>_} {_(→)_}

関数・定理の定義・記述 Γ |- ψ : A 型推論問題の質問 Γ |-? ψ : ? 項推論問題の質問 Γ |-? ? : A プロファイル宣言 Γ |- _ : A （アンダースコアは不定の意味） 単なる省略 Γ |- ψ : _ （不定だが、型推論で確定可能） ホムセット {f | f: Γ |- _ : A} 毎回…

判断・主張と質問・問題の区別ができること。 命題と事実と証拠と証明の区別が出来ること。 証明とリーズニングの区別が出来ること。 ローカル前提とグローバル・コンテストの区別が出来ること。 公理や前提と先送りの区別ができること。 コンテスト環境とバ…

ステージデザインとシナリオスクリプトで指定すること。 ストーリー〈コース〉の開始ステージ（入り口）と終了（出口）の指定。 各ステージのコンテキスト（予備知識）とスキル（コマンドセット） ステージクリア条件 クリアした後の進行先の選択肢、条件付…

論理的体系のマクロな構造とその学習は、リーズニングゲームで行う。リーズニングゲームは、背景知識／背景スキル〈コマンドセット〉を提供するグリモワ〈仏: grimoire | 魔導書〉と、ゲーム・ストーリーからなる。ゲームストーリーはパッケージとして流通単…

まだユルユルな議論なのだが、コンテナの次元UPした概念である2-コンテナとインスティチューションを組み合わせてセオリー論を洗練させられる気がする。$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} }`$ コンテナ インスティ…

ステージと知識シーケントは同じもの。ステージは内部にシーケントをホストする。 ステージのコンテキストはステージ矩形の上部にだけ描いて、内部には貫入しない。 ステージのコンテキスト部のレイアウトは知識シーケントと同じ。 ステージは、コンテキスト…

基本的にステージクリア型ゲーム。ビジュアルノベル（選択式アドベンチャーゲーム）の要素も入る。 ステージはツリー状に配置される。親ステージと子ステージ〈サブステージ〉がある。 ステージツリーは、状態遷移により動的に変化する。 ステージにコンテキ…

これは、recomendation = enabling specification 。ソフトウェア開発で培われた技法を、文書の執筆・編集・編成・出版にも適用する。結果として、Web上に体系化された文献群〈literature〉を実現する。 関与者の役割 関与者〈参加者 | participant〉の役割…

リリースのディビジョン構造 ひとつのディビジョンは次のものからなる。 メタデータとエキストラデータ（エキストラデータは style, script など） テキストブロックまたはテキストスパン（blobオブジェクトの一部分） ディビジョンはどれかのblobオブジェク…

正確・適切なドキュメントを提供したい。 コンテンツの価値が（課金も含めて）正当に評価されるようにしたい。 複数人での共同執筆を可能にしたい。 関与者とその役割をハッキリさせたい。 誰がいつ何をしたかをトレーサブルにしたい。 参照と引用が自由・柔…

モットー／方針 可能な限り、既存の技術、ツール、方法論を使う〈Use existing technology, tools and methodlogy〉。 徐々に構造化〈gradual structuring〉 非強制的（強制する／必須のルールを少なくする〉non-restrictive and encompassing パブリッシャ…

参照可能性を確保するのが重要。それには次の行為が必要。 ラベリング： 外部から参照される項目〈アイテム〉に名前を付ける。 タギング： 外部から参照されるタグを付ける。タグは分類タグと話題タグ。 参照： 公開されている項目を参照する 参照マッピング…

モットー writing is programming （writing as programming） documents should be formally verified ブリットとは： BLit = Web Literature Web上で利用できる、関連する文書達のアーカイブネットワーク マスブリットとは： MathBLit = Mathematics Web L…

数学の時代区分 エジプト／バビロニア／中国の時代 事実と手法の集積 ギリシャ、ユークリッドは紀元前300年前後アレクサンドリアの人、 公理と証明の発明 19世紀 古典述語論理と集合論による厳密化・体系化、ヒルベルト ？ コンピュータで検証可能な記述 問…

参考： 多相関数と依存型をちゃんと理解しよう 次をどう解釈すべきか？ length: ∀α.list(α) → Int次の例を見ると、 first: ∀α.list(α) → maybe(α)括弧の付け方は次のようになる。 length: ∀α.(list(α) → Int) first: ∀α.(list(α) → maybe(α))意味は、 length…

対象物： 型 関数 値〈データ | ポイント〉 特別な関数 汎関数〈メタ関数〉 命題（真偽値、述語、論理式） 導出 保証 特別な導出 リーズニング〈メタ導出〉 カリー／ハワード／ランベック対応 型 命題 関数 導出 値 保証 汎関数 リーズニング 項： 型項（多…

https://arxiv.org/abs/2102.03044 から。 証明が行うこと 読者の心に形成されるもの guarantee trust explain insight, understanding

構文は： law 2-ラベル :: 閉じた論理式または variable 変数の型宣言 law 2-ラベル :: 自由変数を含む論理式法則の圏論的実体〈シング〉は2-射なので、法則名は2-ラベルとする。事例： signature LawlessMonoid within Set { sort U operation e: 1 → U ope…

信頼できる談話環境〈trustable discourse environment〉とは、そのなかでの発話行為、または記載（何かが書いてある）がそのまま事実と解釈してよい環境。一番外側の記述は、信頼できる談話環境のなかにあると考える。そうでないと、「‥‥はほんとうか？」の…

導出とシーケントを混同する理由 - (新) 檜山正幸のキマイラ飼育記 メモ編 に関連して。信頼できる目録があるとする。目録に登録されていることが、存在を保証するならば、 登録は存在命題に匹敵する。 演繹システムのシステム指標／ライブラリ指標は、信頼…

既存導出を組み合わせて新しい導出作ることにより証明を行う。このとき、実際の導出が何であるかは問題にならない。なので、シーケント〈導出のプロファイル〉を書くだけで導出を書いたことになる。これより、導出とシーケントが混同、あるいは同一視される…

大小関係、最小限と足し算との協調性 - (保存用) 檜山正幸のキマイラ飼育記 メモ編 を再掲。 証明要求： Γ |-? ∃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…

導出： false-elim ＝ initial : ⊥ → P true-intro ＝ final : P → T forall-elim ＝ instantiate ＝ projection : ∀x∈X.P(x) → P(a) exists-intro ＝ uninstantiate = injection ： P(a) → ∃x∈X.P(x) リーズニング： Forall-Intro-Right :: (x∈X. φ(x):A→P(…