このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」(http://d.hatena.ne.jp/m-hiyama-memo/)のデータを移行・保存したものであり、今後(2019年1月以降)更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

2018-12-01から1ヶ月間の記事一覧

定義と仕様

次のようなシーケントスタイルの定義は、 For C in Cat, D in 0Cat For FO : C.Obj → D.Obj in Set For FM(A, B in C.Obj) : C(A, B) → D(FO(A), FO(B)) in Set Define F : C → D in Cat // F is-a-functor :⇔ F = (FO, FM) SuchTaht ... End仕様としてまと…

リテラチャー

リテラチャーは、セオリーのk-レイヤーの構成素 - 檜山正幸のキマイラ飼育記 メモ編で初めて出てくる概念。基本的な関係は、 Lk = k-Lit(Σk+1) Σk in Lk ここで、 Lkは、k次元レイヤーにいるリテラチャー Σk+1は、(k + 1)次元レイヤーにいる特定された指標 k…

高次射の定義の形式化

随伴に関する注意事項 - 檜山正幸のキマイラ飼育記で書いた、「構造か命題か」の問題があるので、構造としての随伴対は、adj(L -| R) と書いて、L -| R は命題として使うことにする。ほんとは絵で描くのが良いのだが、なんとかアスキーで定義を書いてみる。…

アイレンベルク/ムーア持ち上げとクライスリ余持ち上げ

dRAdjL, dLAdjR を随伴系の二重圏だとする。その構成素〈constituents〉は、 0-射は圏(または厳密2-圏の対象) 垂直1-射は随伴系を左関手方向で考えたもの。 水平1-射は関手(または厳密2-圏の射) 2-射は、右または左の四脚2-射 右四脚2-射、左四脚2-射と…

モナドの圏が17種類

モナドの圏を σMndγ(K) の形で書く。σは圏のソート、γは圏の修飾子とする。まず、修飾子は形容詞を組み合わせて作る。 形容詞記号 意味 L 左 R 右 Alg 1-射が代数的 EM アイレンベルク/ムーア、1射が右斜め加群 Kl クライスリ、1射が左斜め加群 S 単純、2-…

Kock-Zöberleinの発音

コック/ツーバライン https://ja.forvo.com/search/Z%C3%B6berlein/

Gurski の発音

ガースキイ https://www.youtube.com/watch?v=h3M5AMkZ1u4

関手ナントカの本文記事リンク

「関手オートマトン」で検索: http://d.hatena.ne.jp/m-hiyama/searchdiary?word=%B4%D8%BC%EA%A5%AA%A1%BC%A5%C8%A5%DE%A5%C8%A5%F3 「関手データ」で検索: http://d.hatena.ne.jp/m-hiyama/searchdiary?word=%B4%D8%BC%EA%A5%C7%A1%BC%A5%BF

問題集10の目的と解答と追加説明 (A19R10)

※この記事は「記事19 解答10」問題集10とは、次の記事(の問題部分)のことです: スパイダーパズル (A17P10) 解答だけでなく、「どうしてこのような練習をするか?」や、関連する事項の説明もします。内容: スパイダーパズルと演繹システム 書き方の注意 …

スパイダーの構成不可能性定理を変更 (A18)

当初(2018-12-18)、「スパイダーパズル (A17P10)」において、「次の定理を証明せよ」という問題を出しました。 構成不可能性定理: プロファイルの形が Γ → Δ で、リストΓ内に出現するBの個数が、リストΔ内に出現するBの個数より少ないとき、このプロファ…

スパイダーパズル (A17P10)

※この記事は「記事17 問題集10」この記事の問題をやれば、形式化された証明や演繹システムに対して、(詳細はともかくとして)かなりの程度のイメージが持てると思います。問題の解答例は、早めに(たぶん次回)出す予定です。[追記]解答はこちら → 問題集10…

絵図の描き方と省略法 (A16)

※この記事は「記事16」次の問題はやってみましたか? ノード・ワイヤー図と横棒記法の例と練習 (A2P1) 解答(の一例)は次の記事にあります。 問題集1の目的と解答と追加説明 重要! (A13R1) 引き続く次の記事も類似の問題です。 整数式の操作 (A3P2) 整数式…

問題集8の解答と解説: 当たり前であることを証明する (A15R8-1)

※この記事は「記事15 解答8-1」問題集8とは、次の記事(の問題部分)のことです: シーケントとスコット・ブラケット (A10P8) 「シーケントとスコット・ブラケット (A10P8) // 組み込み推論を表すシーケント」の解答例+解説。 シーケント (x, y∈R), x2 = -3…

問題集6の目的と解答と追加説明 その2 (A14R6-2)

※この記事は「記事14 解答6-2」問題集6とは、次の記事(の問題部分)のことです: 命題と、そのコンテキスト/真理集合 (A8P6) 「その1」は、次の記事です。 問題集6の目的と解答と追加説明 (A14R6-1) 内容: 書き方の注意 限量子を含む閉論理 コンテキスト…

問題集6の目的と解答と追加説明 (A14R6-1)

※この記事は「記事14 解答6-1」問題集6とは、次の記事(の問題部分)のことです: 命題と、そのコンテキスト/真理集合 (A8P6) 解答だけでなく、「どうしてこのような練習をするか?」や、関連する事項の説明もします。誤解されがちなメタ論理やメタ論理記号…

問題集1の目的と解答と追加説明 重要! (A13R1)

※この記事は「記事13 解答1」「だ・である調」から「です・ます調」に変更します。問題集1とは、次の記事(の問題部分)のことです: ノード・ワイヤー図と横棒記法の例と練習 (A2P1) 解答だけでなく、「どうしてこのような練習をするか?」や、関連する事項…

ともかくシーケントなんだから、頼むよ、皆んな (A12)

※この記事は「記事12」シーケントは論理の中核的な概念であり、演繹システムを構成するにしろ、意味論を考察するにしろ、シーケントを基本的対象物とみなすことなる(そうするのが、現状では最良の選択肢だと思われる)。「シーケントとは何であるか?」とい…

シーケントに親しもう (A11P9)

※この記事は「記事11 問題集9」記号的表現に対して「自然言語(日本語や英語)による読み下しが出来ないと馴染めない」という事情も当然だから、シーケントの読み下し練習をする。そして、「“シーケントの正しさ”を正しく判断する/判断できる」とはどういう…

シーケントとスコット・ブラケット (A10P8)

※この記事は「記事10 問題集8」シーケントはゲンツェンにより導入された概念であり、(数学の一分野としての)論理が扱う主要な対象物(のひとつ)である。論理式が論理の主役なのではない。 論理式は、論理式のリストを構成する素材に過ぎない。 論理式のリ…