2022-07-20から1日間の記事一覧
演繹システム - (新) 檜山正幸のキマイラ飼育記 メモ編 演繹システム (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}{ …
