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

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

「CTRL+ALT+P」で Powershell だったのだが、この設定は： [Win]+[Q] から Powershell を探す。 [ファイルの場所を開く] でディレクトリを見る。 "Windows Powershell" がリンクになっているので、プロパティを見る。 プロパティのショートカットキー項目に…

久しぶりで色々忘れている。 MSYS2のルート / は C:\msys64\ MSYS2の /c/ は C:\ したがって、/c/msys64/ は / /ucrt64/, /mingw64/, /clang64/ と、それらの32ビット版があるが、当初はダミーで空っぽ clang32.exe, clangarm64.exe, mingw64.exe, ucrt64.ex…

src/Init/Notation.lean からの情報。構文範疇precは項の優先度を表す値（の表現）のことで： 項の優先度： max = 1024, arg = 1023, lead = 1022, min = 10 パイプ記号 は優先度は min = 10 =, ∈ が50 足し算は65、 規表現風接尾辞の *,+,? は arg = 1023 S…

演算子優先度〈prec〉は適切かどうかわからない。 infix:70 "←" => Nat.pow #eval 5 ← 2 -- 25 def sqPow (n:Nat) : Nat := n ← (n * n) #eval sqPow 2 -- 16

Idris 2で次のコードを書けるようだ。 def typeDesc (ty : Type) : String := match ty with | Int => "integer" | String => "string" | List α => "list of " ++ typeDesc α | _ => "something else"Leanでは無理だ。パターンマッチ match/withが帰納的集…

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…

':=' を使わなくなったようだ。structure/where 、マクロかも知れない。 structure WordCount where wordCount : Nat lineCount : Nat charCount : Nat inWord : Bool宣言文の並びなので、構造体もコンテキストの一種、特に指標の一種と考える。インスタンス…

variable b:Bool はダメで、variable (b:Bool) 。そもそも「変数」は通常の意味の変数ではない。共通に予約された暗黙束縛変数のこと。