混合コンテキストが、次のレベルで提供される。 ライブラリ パッケージ モジュール 名前空間 セクション 関数・定理（のボディブロック） 入れ子ブロック（by, doなど） これらの組織化機構〈organizing mechanism / feature〉は独立ではないし、一様でもな…

証明図〈横棒図〉やストリング図を扱うこと、解釈すること。 順行リーズニング 柔軟な参照（固有名、固有ラベル以外の参照方法） 直示 位置による参照 曖昧参照 リーズニングの中断保留（未完成のままに保存） 順行リーズニングと逆行リーズニングを混ぜたリ…

命題の真偽判定： 白黒つける、決着をつける。どうやって？ 証明項の正当性検証： 構文を決めれば機械的に決定出来るか、または無限走行 証明項の生成工程〈リーズニングプロセス〉の正当性検証： 構文を決めれば機械的に決定出来るか、または無限走行 証明…

問題は、絵図で自明なことをどうやってテキストエンコードするか？ 論理絵図＝横棒図〈バー図〉 圏論絵図＝ストリング図 テキスト 論理絵図 圏論絵図 命題 命題 ワイヤー・ラベル 証拠ラベル バー・ラベル ノード・ラベル 証明項 横棒図 ストリング図 公理 …

次が基本概念： 色々なレベルのコンテキスト ステージ（リーズニングの状態） フォーカス（リーズニング中に注目している判断または問題） ターゲット（判断または問題の項と型） コンテキストには： ライブラリ（知識ベース）のコンテキスト ステージのコン…

一般 抽象的 Lean 具体的 ライブラリコンテキスト プレリュードとインストールしたパッケージ達 ワーキングコンテキスト モジュール／名前空間／セクションのコンテキスト 質問コンテキスト 未証明定理の前提 判断コンテキスト 既証明定理の前提

コンテキストの階層は、外から内に向かって： ライブラリコンテキスト＝知識ベース ワーキングコンテキスト＝ステージコンテキスト 判断コンテキスト または 問題コンテキスト コンテキスト＝混合コンテキストには次のものが格納される。情報の重複がある。…

次の3つを混同しない！ 定理のボディ（関数定義のボディ相当） 証明項 リーズニング リーズニング： バックワード フォワード 背景知識ベース 背景知識ベース リーズニング・ステージ リーズニング・ステージ ステージ・コンテキスト ステージ・コンテキスト…

problem Γ ok? （コンテキスト Γ は正しいか？） judgement Γ ok （コンテキスト Γ は正しい） problem Γ |- t ok? （項 t は、コンテキスト Γ で解釈できるか？） judgementm Γ |- t ok （項 t は、コンテキスト Γ で解釈できる） problem Γ |- ?t : A （型…

命題は型である。← そんなわけないだろ。 命題は型の一種である。 [間違い] 命題はデータ型の一種である。 命題とデータ型は違う。が、命題は型の一種である。 命題は広義の型の一種である。 命題は広義の型の一種であり、データ型も広義の型の一種である。 …

矢印の奪い合い問題 含意を表す 指数型〈関数型 | アロー型〉を表す 射のプロファイルの区切り記号 シーケントの区切り記号（前提と結論） 暫定的解決 含意と指数はカリー／ハワード対応により同一視して → を使う。 射のプロファイルの区切り記号にターンス…

proof ... end {theorem | lemma} 名前 : 前提リスト |- 結論 proof ... end {fact | rule} 名前 : 前提リスト |- 結論 we have ラベル : 命題 from 証明項 we have ラベル : 命題 （前提または直前の結果から） we have 命題 {from 証明項}? （ラベルは thi…

Type Prop プロファイル シーケント 型判断プロファイル 命題判断シーケント 型問題プロファイル 命題問題シーケント 計算合成〈synthesis〉 証明合成 計算合成コマンド 証明合成コマンド 順方向計算合成コマンド 順方向証明合成コマンド 逆方向計算合成コマ…

Type Prop 型 命題 計算 証明 関数 定理 定数 前提なし定理 組み込み関数・定数 公理 プロファイル シーケント フルかりー化プロファイル 片側シーケント 既存関数のプロファイル宣言 事実（定理の名前とシーケント） サブルーチン（一例） ルール 型の要素 …

R-En/Comp R-En/Proof computation proof let := have from lambda assume call use〈using〉 providing return suffices because where := try〈attemp〉 改行 return of showed from 同義語： obtain, show, clarify, describe, indicate, exhibit, prove,…

項と型の型付け〈typing〉チェック ＝ 証明と命題の演繹〈deduction〉チェック 型付けの宣言〈型宣言 | 型判断〉 ＝ 演繹の宣言〈命題判断〉 ＝ 無名定理 型付けの正しさ〈correctness〉＝ 演繹〈deduction〉の正しさ 項の型 ＝ 証明の結論命題〈ターゲット…

混合コンテキストは、次を混ぜたもの。 型宣言文 値割り当て文 型宣言文だけのコンテキスト（実体は依存レコード＝テレスコープ）は指標〈signature〉。型宣言されたすべての名前に値割り当てしたコンテキストは環境〈environment〉と呼ぶ。混合コンテキスト…

define（Scheme）, def（Lean）, 無し function（JavaScript）, func（Go言語、Swift）, fun（Standard ML）, fn（Rust, Zig）, proc（Nim）, sub（Perl） 無し（Ruby, Python, Lean） defun（Lisp） defstruct（Lisp） ここでは、def fun foo のようにする…

axiom, constant, parameter, hypothesis などは同義語であり、どれを選ぶかは好みの問題。 axiom exclusive_middle {P :Prop} : P∧￢P → False : Prop constant exclusive_middle {P :Prop} : P∧￢P → False : Prop parameter exclusive_middle {P :Prop} :…

e はルール（証明の名前＝定理の名前〉、利用側からはルール。Prover's English ＝ P-En OBTAIN ::= prove | show | present | reach | obtain RESULT ::= conclusion | target | result assume文 ::= {we}? assume x : X have文 ::= {we}? have x : X {from…

λ(x:Int, y:Int).(x*x + y :Int) を次にように書く。 assume x: Int, y: Int providing z: Int, return z + y of Int where z: Int := x*xもっと証明っぽく： we assume x: Int and y: Int it suffices to prove z: Int because the result comes from z + y…

推論システムの公理化の有名なものはアクツェル〈Aczel | アクゼル〉のもので、 Aczel, Peter (1977). “An Introduction to Inductive Definitions”. In: Handbook of Mathematical Logic. Ed. by Jon Barwise. Vol. 90. Studies in Logic and the Foundatio…

コンテナ〈ファミリー〉の演算と特別な射： {{ディリクレ}?{テンソル}?}!積 $`\otimes`$ ： コンテナ＆レンズ演算〈(0 | 1)-オペレーター〉、遷移系の演算とも考えられる。 ジョイン $`\triangleleft, \triangleright`$ ： 遷移系の演算、遷移系だけ考えると…

公理系を演繹的に拡大するメカニズムの定式化に： 閉包システム〈closure system〉 単純伴意システム〈simple entailment sysmte〉 バンチ伴意システム〈bunched entailment sysmte〉 双対バンチ伴意システム〈dual bunched entailment sysmte〉 伴意関係を …

色付き／色無しは無意味で誤解をまねくリスクがあるので使わない。 対称／(非対称) ： 対称作用を持つか？ 対称構造の忘却で非対称になる。 モノイド／(非モノイド) ： モノイド積を持つか？ モノイド積の忘却で非モノイドになる。 ワイド／ナロー ： 多結合…

次のようなメタ記号を使う。$`\newcommand{\TS}{\mathrel{\,|\!-} } \newcommand{\TTS}{\mathrel{\,||\!-} } \newcommand{\TTTS}{\mathrel{\,|||\!-} } \newcommand{\Imp}{\Rightarrow } \newcommand{\Iff}{\Leftrightarrow } \newcommand{\In}{\text{ in } …

長谷川真人さんの "Classical Linear Logic of Implications"https://www.kurims.kyoto-u.ac.jp/~hassei/papers/clli.pdf ：加法的〈非線形〉コンテキストと乗法的〈線形〉コンテキストを持つ型判断〈typing judgement〉$`\quad \Gamma ;\Delta \vdash M:\si…

"Shapely monads and analytic functors" by Richard Garner, Tom Hirschowitz https://arxiv.org/abs/1512.05980 これが多圏類似構造のテキストとして非常によい。多圏類似構造の分類を絵算〈グラフィカル計算〉との関係で論じている。多射の図がどうなるか…

論域が大きい場合〈large domain of discourse〉を考える。 複アロー構成と多アロー構成、そのときのパラメータとしてのコレクションモナド コレクションモナドの一種としてのバンチモナド 型コンテキストと指標は同一概念であること。 命題コンテキストはフ…

構文論： 基本概念 別名 ラベル 名前, 変数, 不定元, 定数, 識別子 シング n-射, もの, 実体, 具体物 割り当て 束縛, 代入, 関連付け〈association〉 リテラル 定数, 名前, 記号 コネクティブ 演算{子}?記号 コンビネーション 項, 式, 図式 ※ 論理のリテラル…