思い付いたことを順不同にダダーっと箇条書きにする。後で整理する。まだごった煮。先に意味領域： 集合の集合がある。小さい具象圏の対象集合 ＝ Type ＝ |Sem| 0, 1 はType内にある。0, 1∈Type 型がAの個体〈individual〉とは、1からのAへの射のこと。 関…

{絵|図|絵図}は、{figure | picture | diagram | drawing | painting | illustration | visual object} などがあるが、図＝diagram とする。ムービーのフレームのあいだのトランジションの制作には、図コンビネータ〈diagram combinator〉のコマンドを使う。…

オリジナルのゲンツェンLKでは、 公理は一種類（1パターン） 推論規則は左右それぞれ10種で合計20種 Cutが一種 合計で21種の推論規則 LK改では、 id:A ↔ A !:A → T π[1]:A, B → A π[2]:A, B → B Δ:A ↔ A, A α:A, B, C ↔ A, B, C （注記参照） λ:T, A ↔ A ρ:A…

ホントに酷い、腐っているとしか言いようがない。整理を試みれば試みるほどに酷さを痛感する。 「証明」は無理だ。使用しない。 「推論」を使う。ただし、「推論」と「リーズニング」はまったく別。 「定理」は使える。[追記]いや、使えないわ。[/追記] 絵図…

語源、由来、謂れ、いわく、物語、逸話 とかを要求されると困るのだが、人々はそれを求めるので、書いておく。 記号 由来 ! たぶん唯一性から ∃! と同じ由来 π projectionのp ι injectionのi Δ diagonalのd、それと形状の類似 λ leftのl ρ rightのr（rh） α …

以下の文章（引用ではない）内の「証明」「主張」は専門用語ではない。非形式的に使用している言葉。主張は assertion, declaration, claim, statement, judgement, thesis など。 証明とは、主張の正しさを保証するものである。その主張に至る過程も含めて…

展開＝マクロ展開＝expand で、いいと思う。展開の逆だが、 contraction, collapsing がある。contraction〈縮約〉はthinning〈水増し〉と対にもなる。水増しは複製〈duplication〉でもある。複製の逆は併合〈merge〉、unionではない。対になるべき語がうま…

証明ストリング図のノードラベルが、メタ変数でラベルしているのか、システム内のラベルでラベルしているのが分からないという問題があった。ラベルのテキストで区別するのは現実的ではないが、ノード形状で区別ならなんとかなる。まず、ノード種別を インラ…

絵を中心に考えるしかないだろう。で、絵のノードだが、誤解を招きそうな気がしてきた。ノード → スパイダーと改名したほうがいいかも知れない。グラフ理論の頂点とは違って、むしろ近傍部分グラフみたいなものだから。スパイダーは脚を持つ。脚の付け根をピ…

メタ変数、メタ論理、メタ数学 とかの奇妙な言葉。メタ変数は実質的に困難をもたらす。 変数集合V上を走る変数 x, y 。で、V = {x, y, ... } だったりする。 状況としては、 日本語と共通の単語が多くあり、意味が同じだったり違っていたりという外国語があ…

フントニモウ、ムカムカムカムカ、ムッキー！！ 矢鱈に同義語があったりする（例：論理AND、論理積、連言、合接、コンジャンクション）のに、肝心なモノ・コトに言葉がなかったり、曖昧過ぎて使いものにならなかったり。むっかー！ 定理 証明 公理と推論 定…

比喩： 具体素子 基本リーズニング 証明図（スチル） ムービー 料理 食材 基本調理法 料理のスナップショット 料理動画 回路工作 素子とワイヤー 基本組み立て法 回路のスナップショット 工作動画 ピクチャーパズル ピース 基本組み立て法 ピクチャーのスナ…

fA→B これではバラエティが足りないのでもっと描き足すつもり。それと、題材は f:A, B→C にする。

関連しそうな自分のエントリー。ウヘー、我ながらいっぱいあるなー。ざっと読んでいこう。読んだら、感想を一言ずつ書いていこう。 述語論理とインデックス付き圏と限量随伴性 20170824 テンソル積の作り方 20160829 中学レベル代入計算からカリー／ハワード…

無名変数 ハイフンまたはアンダースコア〈アンダーバー | アンダーライン〉 セクション記法 関数のプロファイル（多変数・多値のカンマ区切りもあり） maps-to記法 |→ 関数適用〈引数渡し | 関数呼び出し〉の中置記法 関数が右からの関数適用 ラムダ記法 コ…

リーズナー〈reasoner〉は、{定理|証明}コンビネータのこと。 ; （二項） （二項） （二項） ◇ （任意項） □ （任意項） Λ （単項） p, qが{定理|証明}で、Pが{定理|証明}のインデックス族とするときの適用結果は： p;q pq pq ◇P □P Λp ただし、は'∧'に輪（…

意味結び付きを切り替える儀式として 記憶を助けるヒントとして ← コジツケでもいい

論理AND、合接、論理積、連言、コンジャンクション 論理OR、離接、論理和、選言、ディスジャンクション 論理NOT、否定、{ニ | ネ}ゲーション 含意、条件{法}?、インプリケーション 多義語： 矛盾： 矛盾命題＝偽命題＝偽的命題〈falsy prop.〉、演繹システム…

言語・習慣・文化のせいで、せっかくの原則がうまく使えない例がカリー／ハワード対応。なんとかしてキレイに整理する。演繹システムでは不明瞭で、プログラミング・システムでは明瞭な概念： システム組み込み vs ユーザー定義 ライブラリによるシステムの…

http://d.hatena.ne.jp/m-hiyama-memo/20181102/1541141733の最後の余談を敷衍する。domain of discourse の訳語に論域を使う。すると、命題関数の域は論域となる。「論域＝命題関数の域」で事情が少しハッキリする。シーケントにおける自由変数の指定は、論…

記法バイアスと記法独立な把握： 順序随伴を例として - 檜山正幸のキマイラ飼育記では、 標準的テキスト記法の強烈なバイアスに支配されている、あるいは記法の獄舎に投獄されているからです。 自ら「記法の獄舎」に閉じこもりたい傾向（思考、指向、嗜好）…

一言でいうと節約原理。 ページ節約： 紙面とインクを使わない。リソース・コストの節約。 絵図排除： 絵図（イラスト・ピクチャー）を避けて活字組版で処理したい。人件費と時間の節約。 コピー排除： 手書きのとき、コピー（転記）を避けたい。手間の節約…

※この記事は「記事5 問題集4」ノード・ワイヤー図〈ストリング図〉の解説は： ノード・ワイヤー図〈ストリング図〉 これより前に行うべき練習は： ノード・ワイヤー図と横棒記法の例と練習 整数式の操作 整数式の構文解析木 今回は、式の操作を表す横棒記法…

※この記事は「記事4 問題集3」ノード・ワイヤー図〈ストリング図〉の解説は： ノード・ワイヤー図〈ストリング図〉 これより前に行うべき練習は： ノード・ワイヤー図と横棒記法の例と練習 整数式の操作 今回も、「整数式の操作」で定義した整数式を扱う。諸…

※この記事は「記事3 問題集2」ノード・ワイヤー図〈ストリング図〉の解説は： ノード・ワイヤー図〈ストリング図〉 これより前に行うべき練習は： ノード・ワイヤー図と横棒記法の例と練習 この練習では、整数とその足し算／掛け算について考える。足し算／…

※この記事は「記事2 問題集1」ノード・ワイヤー図〈ストリング図〉の解説は： ノード・ワイヤー図〈ストリング図〉 中学校で習った二元連立一次方程式を例にする。内容は難しくないが、作業（トレーニング）はそれなりに手間がかかる。手間を減らす工夫は各…

※この記事は「記事1」ノード・ワイヤー図はいたるところで使う、極めて重要なツールである。内容： ノード・ワイヤー図とは 描画方向 結合と併置 テキスト記法 グルーピング〈ブラケティング〉と描き換え 横棒記法 ノードの形状 図の引用元 ノード・ワイヤー…

次の3つは区別されるべき。 計算指示としての式 例：算術式 計算結果としの値 例：自然数値＝算術値 計算する行為 計算をオペレーションと言い直すと： オペレーション指示としての式 オペレーション結果としの値 オペレーションする行為 値はオペレーション…

実際にこんな会話はないけど（あくまで例え話）。 某氏「プログラムが止まるかどうかは決まっているんですよね？」 檜山「決まってます。止まるか止まらないかのどちらかです。」 某氏「でも、判断はできないのですよね。」 檜山「はい、判断はできません。…

∀x.(…) 任意のxについて、… 任意のxに対して、… 任意のxに関して、… どんなxであっても、… xが何であっても、… すべてのxに対して、… あらゆるxに渡って、… 勝手にxを取ってきて、… xを好きに選ぶと、… ∃x.(…) 適当なxを取れば、… あるxがあって、… xをうま…