記事とコメントのインポート完了。 インポートページ ログイン - はてな

記法： コ/モナド ： モナドまたはコモナド 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リーズニングが分からない」とあったのですが、まー、分かりにくいでしょう。「なんでワイヤーが曲がるのだろう？」と考えても、そりゃー分かりませんぜ。天…