記事とコメントのインポート完了。 インポートページ ログイン - はてな
記法： コ/モナド ： モナドまたはコモナド A∨ : 上付きのチェックマーク（のつもり）は、文字修飾子。使い途はボールドなどと同じ。Aに対する演算子ではない。コモナドを表す文字・語への文字修飾に使う。 ベックの分配系は4種類あって、 モナド・モナド分…
形式／非形式とレイヤー構成 - 檜山正幸のキマイラ飼育記 メモ編にシーケントが出てこないが、シーケントは構文形式なので、幾つかの使い途がある。 基本推論図は、ひとつのシーケントで表現可能で、基本推論図とそのシーケントは同一視してもよい。 一般の…
大分類 非形式 形式化データ 備考 計算 対象式 対象式（項） もともと形式化されている 論理 命題 論理式 文字列または構文解析木 論理 推論 推論図 仮定と結論がある 論理 リーズニング リーズニング図 ツリー状ノード・ワイヤー図 すべての形式化データは…
「一貫性」という言葉が曖昧だから整理する。まず、律子〈rator〉は法則を与える2-射（あるいはもっと高次の射）のこと。律子が満たす等式を制約等式〈constraint equation〉または等式的制約〈equational constraint〉または単に制約〈constraint〉と呼ぶ。…
随伴に関する注意事項 - 檜山正幸のキマイラ飼育記に関連して：次の例は、http://www.math.uchicago.edu/~may/VIGRE/VIGRE2011/REUPapers/Berger.pdf から。ここ（以下のコピーのところ）で初めて記号'-|'が出てきている。随伴系の方向はペアの右の関手に合…
※この記事は「記事23 問題集11の解答」問題集11とは、次の記事（の問題部分）のことです： 小学生でも分かる論理計算 (A22P11) 上記記事への追記で次の文言を入れました。 「全部乗せで、完全にグラフィカルなリーズニング図」を描くのはムチャクチャ大変だ…
※この記事は「記事22 問題集11」伝達側が、省略なしに描いた絵を提示する労（と面積）を厭わず、学習者も絵を描く練習をするなら、専門家にも難解と言われるゲンツェン流の論理計算も、内容的には小学生レベルだと思います。このこと（「絵を使えば簡単だぞ…
昨日、Lambda基本リーズニング（「含意導入規則」と呼ばれることが多い）に関して、ワイヤーベンディング描画法を説明しました。描画法を考えた当事者の意図・目的を理解しないと、「変な絵」「ワケワカメな図」になってしまいます。描画法／記号法／表記法…
Lambdaリーズニングとは、'｜'の形のワイヤーを'∩'の形にひん曲げる操作です。アンケートに「Lambdaリーズニングが分からない」とあったのですが、まー、分かりにくいでしょう。「なんでワイヤーが曲がるのだろう？」と考えても、そりゃー分かりませんぜ。天…
次のようなシーケントスタイルの定義は、 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-射と…
モナドの圏を σMndγ(K) の形で書く。σは圏のソート、γは圏の修飾子とする。まず、修飾子は形容詞を組み合わせて作る。 形容詞記号 意味 L 左 R 右 Alg 1-射が代数的 EM アイレンベルク／ムーア、1射が右斜め加群 Kl クライスリ、1射が左斜め加群 S 単純、2-…
コック／ツーバライン https://ja.forvo.com/search/Z%C3%B6berlein/
ガースキイ 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
※この記事は「記事19 解答10」問題集10とは、次の記事（の問題部分）のことです： スパイダーパズル (A17P10) 解答だけでなく、「どうしてこのような練習をするか？」や、関連する事項の説明もします。内容： スパイダーパズルと演繹システム 書き方の注意 …
当初（2018-12-18）、「スパイダーパズル (A17P10)」において、「次の定理を証明せよ」という問題を出しました。 構成不可能性定理： プロファイルの形が Γ → Δ で、リストΓ内に出現するBの個数が、リストΔ内に出現するBの個数より少ないとき、このプロファ…
※この記事は「記事17 問題集10」この記事の問題をやれば、形式化された証明や演繹システムに対して、（詳細はともかくとして）かなりの程度のイメージが持てると思います。問題の解答例は、早めに（たぶん次回）出す予定です。[追記]解答はこちら → 問題集10…
※この記事は「記事16」次の問題はやってみましたか？ ノード・ワイヤー図と横棒記法の例と練習 (A2P1) 解答（の一例）は次の記事にあります。 問題集1の目的と解答と追加説明 重要！ (A13R1) 引き続く次の記事も類似の問題です。 整数式の操作 (A3P2) 整数式…
※この記事は「記事15 解答8-1」問題集8とは、次の記事（の問題部分）のことです： シーケントとスコット・ブラケット (A10P8) 「シーケントとスコット・ブラケット (A10P8) // 組み込み推論を表すシーケント」の解答例＋解説。 シーケント (x, y∈R), x2 = -3…
※この記事は「記事14 解答6-2」問題集6とは、次の記事（の問題部分）のことです： 命題と、そのコンテキスト／真理集合 (A8P6) 「その1」は、次の記事です。 問題集6の目的と解答と追加説明 (A14R6-1) 内容： 書き方の注意 限量子を含む閉論理 コンテキスト…
※この記事は「記事14 解答6-1」問題集6とは、次の記事（の問題部分）のことです： 命題と、そのコンテキスト／真理集合 (A8P6) 解答だけでなく、「どうしてこのような練習をするか？」や、関連する事項の説明もします。誤解されがちなメタ論理やメタ論理記号…
※この記事は「記事13 解答1」「だ・である調」から「です・ます調」に変更します。問題集1とは、次の記事（の問題部分）のことです： ノード・ワイヤー図と横棒記法の例と練習 (A2P1) 解答だけでなく、「どうしてこのような練習をするか？」や、関連する事項…
※この記事は「記事12」シーケントは論理の中核的な概念であり、演繹システムを構成するにしろ、意味論を考察するにしろ、シーケントを基本的対象物とみなすことなる（そうするのが、現状では最良の選択肢だと思われる）。「シーケントとは何であるか？」とい…
※この記事は「記事11 問題集9」記号的表現に対して「自然言語（日本語や英語）による読み下しが出来ないと馴染めない」という事情も当然だから、シーケントの読み下し練習をする。そして、「“シーケントの正しさ”を正しく判断する／判断できる」とはどういう…
※この記事は「記事10 問題集8」シーケントはゲンツェンにより導入された概念であり、（数学の一分野としての）論理が扱う主要な対象物（のひとつ）である。論理式が論理の主役なのではない。 論理式は、論理式のリストを構成する素材に過ぎない。 論理式のリ…
※この記事は「記事9 問題集7」単一の論理式〈形式化された命題〉だけではなくて、論理式のリストを徹底的に使い倒した最初の人はおそらくゲンツェンだろう。プログラミングで言えば、単一タプル引数（パックされた多引数）、単一タプル戻り値（パックされた…
