palette CCC { parameter wire X, Y, Z node left-eval[X, Y] : (X, X⇒Y) → (Y) node decomp-prod[X, Y] : (X×Y) → (X, Y) node swap[X, Y] : (X, Y) → (Y, X) action LeftCurry[X, Y, Z] :: ((X, Y) → (Z)) ~~→ ((Y) → (X⇒Y)) // ...省略... parameter node…

描画モデルは、描画エージェント（一人、ペインター、画師、絵師）、キャンバス（入れ子可能）、パレット（複数可能）からなる。 唯一のカレントキャンバスを持つ。 唯一のカレントフォーカスポイントを持つ。それは、カレントキャンバス上の点。 カレントフ…

型・関数 命題・導出 0-射 型 0-射 命題 0-オペレータ 積 0-オペレータ 連言 0-オペレータ 指数 0-オペレータ 含意 0-射 指数型 0-射 含意命題 1-射 関数 1-射 導出 1-射 データ 1-射 保証〈ワランティー〉 1-射 入射〈余射影〉 1-射 証拠 1-射 射影〈成分〉…

少し追記。 型コンテキストを型判断と呼ぶ用語法は採用しない。 型シーケント $`\Gamma \vdash M:\sigma`$ を型判断〈typing judgement〉と呼ぶのは許容しよう。 型判断の意味はセマンティック・デカルト閉圏の射になる。特に集合圏では単なる写像。型コンテ…

まず、次は同義語扱いしたほうがいい。 変数の型宣言 型コンテキスト 0-指標 ポイント1-射だけの1-指標 構造体定義 レコード定義 テーブルスキーマ 例えば、 variable x, y : Real, c : Color type-context {x:Real, y:Real, c:Color} 0-signature _ { 0-mor…

型の圏（複圏、多圏もある）と命題の圏（複圏、多圏もある）との関係。カリー／ハワード／ランベック対応（むしろ、カリー／ハワード／ランベック・フレームワーク）があるので似てる。抽象化すれば同じになる。が、型コンテキストの圏の対象の上に命題の圏…

MEDL（Mathematical Entity Description Lang.）とDIDL（Drawing Instruction and Description Lang.）について。DIDLはある程度は汎用の絵図記述言語。だが、直接的な目的は証明記述。「証明」は曖昧語なので、テクニカルタームとしては導出〈derivation〉…

MP導出の図を向きを変える。 スタックとリストの関係と等式の証明 計算図 リーズニング図 紙芝居方式リーズニング図リーズニング図の同値変形 分岐合流紙芝居方式リーズニング図 線形証明とグラフ証明図とツリー証明図連言リストと宣言リスト、α, β は論域。…

演繹システム - (新) 檜山正幸のキマイラ飼育記 メモ編 演繹システム (2) - (新) 檜山正幸のキマイラ飼育記 メモ編 演繹システム (3) - (新) 檜山正幸のキマイラ飼育記 メモ編 $`\newcommand{\derive}{ \vdash }% \newcommand{\deduce}{ \mathop{\|\!-} }% \…

Title: A Taste of Categorical Logic — Tutorial Notes Authors: Lars Birkedal (birkedal@cs.au.dk), Aleš Bizjak (abizjak@cs.au.dk) Date: July 10, 2017 URL: https://cs.au.dk/~birke/papers/categorical-logic-tutorial-notes.pdf これは良いチュート…

https://cs.au.dk/~birke/papers/categorical-logic-tutorial-notes.pdf の P.3 の11個の規則 IDENTITY WEAKENING CONTRACTION EXCHANGE MULTI-COMPOSITION （もとは無名） PAIRING PROJ-1 PROJ-2 ABS APP UNIT（むしろTERMINALだろうが） 使う文は以下。確…

面積問題への対策（あるいは無策） (A21) - (保存用) 檜山正幸のキマイラ飼育記 メモ編 2019-01-08 意味不明な言葉達 - (保存用) 檜山正幸のキマイラ飼育記 メモ編 2018-11-15 お絵描き証明の例 - (保存用) 檜山正幸のキマイラ飼育記 メモ編 2016-02-24 $`\v…

CoqでもLeanでもPropを使うが、Prepの正体は何でもよくて、デカルト閉半環圏（の対象集合）であればよい。自然数上に定義された述語 p は p: Nat → Prop だが、その実体が次のいずれでも、さらに他の何かでもいい。$`\quad p:{\bf N} \to {\bf B} \text{ in …

ストリング図の描画指令〈instruction〉と記述〈description〉のための言語 Drawing Instruction Description Language 目的は違うが名前が似ているもの： https://www.ijcai.org/Proceedings/03/Papers/069.pdf LADDER (LAnguage to Describe Drawing, disp…

構文は： law 2-ラベル :: 閉じた論理式または variable 変数の型宣言 law 2-ラベル :: 自由変数を含む論理式法則の圏論的実体〈シング〉は2-射なので、法則名は2-ラベルとする。事例： signature LawlessMonoid within Set { sort U operation e: 1 → U ope…

信頼できる談話環境〈trustable discourse environment〉とは、そのなかでの発話行為、または記載（何かが書いてある）がそのまま事実と解釈してよい環境。一番外側の記述は、信頼できる談話環境のなかにあると考える。そうでないと、「‥‥はほんとうか？」の…

導出とシーケントを混同する理由 - (新) 檜山正幸のキマイラ飼育記 メモ編 に関連して。信頼できる目録があるとする。目録に登録されていることが、存在を保証するならば、 登録は存在命題に匹敵する。 演繹システムのシステム指標／ライブラリ指標は、信頼…

既存導出を組み合わせて新しい導出作ることにより証明を行う。このとき、実際の導出が何であるかは問題にならない。なので、シーケント〈導出のプロファイル〉を書くだけで導出を書いたことになる。これより、導出とシーケントが混同、あるいは同一視される…

演繹システム上で解釈可能な記述〈description〉をスタンドアロンな記述と言う。 何も提供・公開してない記述をノートパッドと呼ぶ。 スタンドアロンなノートパッドがTypeScrptのスクリプトに対応する。 演繹システムでは、スタンドアロンではないノートパッ…

$`\newcommand{\derive}{ \vdash }% \newcommand{\deduce}{ \mathop{\|\!-} }% \newcommand{\afford}{ \mathrel{\|} }% \newcommand{\Sign}[1]{ \mathscr{#1} } \newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\In}{ \text{ in } } \newcommand{\ImpL}{ …

順不同。 選言ボックスと二面ノード - (新) 檜山正幸のキマイラ飼育記 メモ編 選言ボックスと二面ノード デカルト閉復圏とラムダ計算 - (新) 檜山正幸のキマイラ飼育記 メモ編 ラムダ図 これはいいぞ！ ラムダハウス - (新) 檜山正幸のキマイラ飼育記 メモ編…

TypeScriptと比較する。 TypeScript Tenjin MEDL 備考 スクリプト ノートパッド 使い捨て モジュール アーティクル .medl.md ファイル パッケージ パッケージ 同じNPM構造 名前空間 デビジョン division インターフェイス 指標 signature 総称クラス 構成手…

declare は実はどこに書いてもいい。.d.tsファイルじゃなくてもいい。が、アンビエント宣言だけ切り離してまとめておいたほうがいいので、.d.tsファイルがある。.d.ts ファイルに関する特別な扱いの規約・メカニズムも整備されている。 declare var -- 変数…

従来： システム組み込み ユーザー定義 ワイヤー 公理 仮説、仮言、仮定 ケーブル 公理系 仮説、仮言、仮定 ノード 公理、推論規則 定理 オペレータ 推論規則 ？ 同値性 ？ ？ 今後： システム組み込み ユーザー定義 ワイヤー 命題 命題 ケーブル 構造化命題…

真偽値 述語（述語関数、述語記号） 論理式 閉じた論理式 命題論理、述語論理を区別する形容詞 命題を論理文とも呼ぶ。

(1) (2) なんか面白い、作者 Fuzzyma〈Ulrich-Matthias Schäfer〉の発想が面白い。 WantToDo指向 「何をするか／したいか」に注目する発想をWantToDo指向とでも呼べば、FuzzymaはWantToDo指向で、次のToDo〈Doing〉を設定している。 creating オブジェクトを…

https://svgjs.dev/docs/3.0/events/ を読んで。文書を読むと次のように読める。null = {null}。 signature Element { sort self operation click: (self, ClickHandler) → self operation click: (self, null) → self }同じような方式で、dblclick, mousedo…

暫定！ $`\newcommand{\derive}{ \vdash }% \newcommand{\deduce}{ \mathop{\|\!-} }% \newcommand{\afford}{ \mathrel{\|} }% \newcommand{\Sign}[1]{ \mathscr{#1} } \newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\In}{ \text{ in } } \newcommand{\…

演繹可能性メタ命題 - (新) 檜山正幸のキマイラ飼育記 メモ編 で参照した過去記事達（新しい順）： 互換な演繹システムとシーケント、そして矢印記号 - 檜山正幸のキマイラ飼育記 (はてなBlog) 演繹定理 論理／メタ論理の記法をどうするか 2: 悟りへの道 - …

基本概念： 描画 テキスト記述 キャンバス ステージ ワイヤー 論理式 ケーブル 構造化論理式 ノード 導出 グループボックス プレーンブロック リーズニングボックス リーズニングブロック コンステレーション図 導出記述 言い方： 描画 テキスト記述 描く 導…