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

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

2018

シーケントの役割、使い所

形式/非形式とレイヤー構成 - 檜山正幸のキマイラ飼育記 メモ編にシーケントが出てこないが、シーケントは構文形式なので、幾つかの使い途がある。 基本推論図は、ひとつのシーケントで表現可能で、基本推論図とそのシーケントは同一視してもよい。 一般の…

形式/非形式とレイヤー構成

大分類 非形式 形式化データ 備考 計算 対象式 対象式(項) もともと形式化されている 論理 命題 論理式 文字列または構文解析木 論理 推論 推論図 仮定と結論がある 論理 リーズニング リーズニング図 ツリー状ノード・ワイヤー図 すべての形式化データは…

ため息しか出ない

ずーーっと、用語法の整理、使える用語/使えない用語の選別をしている。酷い状況であることはもちろん承知はしていたが、作業してみると、その酷さをまざまざと実感する。命題を表す変数を「命題変数」と呼びたいが、「命題変数」は命題論理 -- コンテキス…

なるほどダメだ:シーケント記法

推論のストリング図をテキストで表したものがシーケントだと解釈すると、通常のシーケント記法はダメなことがわかる。シーケント矢印が 推論のスパイダーを表す矢印 ケーブリングを表す矢印 の区別ができないと、ストリング図を書き写すことができない。次の…

レベルごとの演算子

演繹システムのパート分類(モジュラー/レイヤード設計・実装のため): 分野固有パート 論理パート(分野によらない共通パート) 分野固有パートは: 個体レベル 型レベル 論理パート 命題レベル 推論レベル システムが単ソート〈single{- | }sort{ed}?〉…

メタレベルと対象レベル

メタ(形容詞)=我々が生きている現実世界の … 対象(形容詞)=我々が調査と考察の対象(目的物)とする数学的モデル(対象演繹システム)内の … 例: メタ記号 vs. 対象記号 メタ変数 vs. 対象変数 メタ命題 vs. 対象命題 メタ定理 vs. 対象定理 メタ側がモヤ…

証明と呼ばれるかも知れないモノ

推論を次のように規定する。 推論には必ずプロファイルがある。 プロファイルは仮定命題リストと結論命題リストからなる。 推論はラベル付きのときもあれば、ラベル無しのときもある。 推論は組み込みのときもあれば、ユーザー定義のときもある。 組み込み推…

ダメな言葉と矢印のまとめ

名詞 動詞能動態 形容詞-済み 形容詞-可能 証明 × × ○ 推論は- ○ 推論は-、命題は- 推論 ○ △ 仮定が結論を- × × リーズニング ○ ○ 上式が下式を- ○ 推論は- ○ 推論は- 言い方の候補: Γ infers Δ Γ concludes Δ Γ derives Δ Γ entailes Δ ξ reasons η ξ conc…

アニメムービー用語

マルチスクリーンムービー ムービーフィルム フレーム(のコンテンツ) 絵コンテ〈ストーリーボード〉 {絵コンテの{コマ | シート} | {ストーリー}?シート} シーン {アクション}?コマンド スクリプト(ActionScriptは固有名詞) スクリプトのユーザー定義関…

各種のオペレーターの呼び名

なんかもう、ひたすら単語の選択と(必要なら)造語をしている。いいかげんウンザリはしている。全般的に、用語法において、関数と関数を表す式と関数値の区別が付いてない/付けてないことが分かる。これは普遍的(どこでも見いだせる)な現象だ。関数まわ…

構文領域と意味領域

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

中間まとめ:アニメ用語との対比

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

LK改の説明:ハイパードクトリン的な解釈

オリジナルのゲンツェン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 にする。

便利な書き方とコンテキスト風書き方

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

カリー/ハワード論理の6つのリーズナーの記法

リーズナー〈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 の訳語に論域を使う。すると、命題関数の域は論域となる。「論域=命題関数の域」で事情が少しハッキリする。シーケントにおける自由変数の指定は、論…

土着性、翻訳不可能性と同義語・多義語による障害

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