Lean
過去記事： タクティク解説、等式の種類も タクティクのためのゲンツェン法則 「Leanタクティク」は、実際のLeanのタクティクを話題にする。参考URL： https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2022/Part_C/Part_C.html ケビン…
ステージデザインとシナリオスクリプトで指定すること。 ストーリー〈コース〉の開始ステージ（入り口）と終了（出口）の指定。 各ステージのコンテキスト（予備知識）とスキル（コマンドセット） ステージクリア条件 クリアした後の進行先の選択肢、条件付…
論理的体系のマクロな構造とその学習は、リーズニングゲームで行う。リーズニングゲームは、背景知識／背景スキル〈コマンドセット〉を提供するグリモワ〈仏: grimoire | 魔導書〉と、ゲーム・ストーリーからなる。ゲームストーリーはパッケージとして流通単…
まだユルユルな議論なのだが、コンテナの次元UPした概念である2-コンテナとインスティチューションを組み合わせてセオリー論を洗練させられる気がする。$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} }`$ コンテナ インスティ…
この論文、参考になる。 https://kwarc.info/people/frabe/Research/KRW_isabelle_19.pdf Making Isabelle Content Accessible in Knowledge Representation Formats Michael Kohlhase, Florian Rabe, Makarius Wenzel 日付はハッキリしないが、2020以降なの…
新しく導入する構文は： 変更可能代入文 副作用付きif文〈手続き的if文〉 キーワードと構文： let mut := 代入の右辺式は純 if-then-else if-then unless-do 翻訳： mutキーワードは、変数が変更可能であることを宣言する。let mut 変数 ← ... は、変更可能…
少しずつ説明。 構文範疇に、式と文〈ステートメント〉がある。 文には式文（式はそのまま文）と副作用let文がある。 do構文は式（do式）、純let式も式 let文といったときは副作用let文で、let式は純let式。 翻訳： do式の翻訳は、そのボディブロックを翻訳…
前提： 条件{節}? conditional clause 事実： 主張 assertive sentence 判断： 証拠付き主張 ／ 証拠 with Evidence 質問： 疑問文 interrogative sentence / Question コンテキスト、項、戻り型〈return type〉がある。 コンテキスト 項 戻り型 記号 知識 …
https://dl.acm.org/doi/pdf/10.1145/3547640 より：
総称型も「型」と言ってる。Type u → Type v は宇宙非エンド〈universe non-endo〉な型関数だが、これが単項〈1パラメータ〉の総称型。関手やモナドの台構造はこの種の「型」。広義の“型”上に構造が載るので型クラスになる。 「総称型＝型関数」という“型”上…
https://www.slideshare.net/onoremiz/mmorpg-14352457 より： レベルの要素とは： アイテムの配置 地形や動線の設定 敵の配置／AIの設定 ギミックの配置 クリア条件の設定 レベルデザインとは： ゲーム内の環境や経験をデザインすること。 レベルエディタ〈…
まず、Leanコミュニティでも用語の個人差がある。object, term, value, element なんかは要注意。型クラスのパラメータは、相対指標の部分指標の指定なので、ファイバー付き圏のベース圏を指定する。C が1パラメータの型クラスとして、固定したξに対して (C …
クラスBindは、">>=" または bind を持っている構造のクラス。 クラスPureは、pure を持っている構造のクラス。 クラスFunctorは、map を持っている構造のクラス。mapしてから適用するのを <$> で表す？？ 型クラスのベース〈パラメータ〉は型関数＝総称型だ…
戻り値にステータスを返したいなら IO UInt32 とする。戻り値不要なら Unit でもよい。 def main(args : List String) : IO Unit := do let len := List.length args IO.println s!"length of args is {len}" for i in [0:len] do IO.println (List.get! arg…
s!を前置するとテンプレート文字列になる。他にもナントカビックリがあるのか？ s!"Hello, {hello}!"改行は普通に入れられる。エスケープの必要はない。
Listはなぜかモナドから外されて単なる関手扱い。 白が“クラス”で青が“インスタンス”ということだろう。 矢印はクラス間の extends と、インスタンス-クラス間の member-of モナドの末尾は M というネーミングルールだが、守られてはいない。 Pure と Bind …
戻り値にステータスを返したいなら IO UInt32 とする。戻り値不要なら Unit でもよい。 def main(args : List String) : IO Unit := do let len := List.length args IO.println s!"length of args is {len}" for i in [0:len] do IO.println (List.get! arg…
s!を前置するとテンプレート文字列になる。他にもナントカビックリがあるのか？ s!"Hello, {hello}!"改行は普通に入れられる。エスケープの必要はない。
ステージと知識シーケントは同じもの。ステージは内部にシーケントをホストする。 ステージのコンテキストはステージ矩形の上部にだけ描いて、内部には貫入しない。 ステージのコンテキスト部のレイアウトは知識シーケントと同じ。 ステージは、コンテキスト…
基本的にステージクリア型ゲーム。ビジュアルノベル（選択式アドベンチャーゲーム）の要素も入る。 ステージはツリー状に配置される。親ステージと子ステージ〈サブステージ〉がある。 ステージツリーは、状態遷移により動的に変化する。 ステージにコンテキ…
Ident 公理 Cut オペラッド結合 Weak 水増し Cont 冗長性縮約 contraは矛盾 Perm 交換 CtxAndIntroL CtxAndIntroR CtxtOrIntro CtXImpIntro （LJ変形） CtxNotIntro CtxUnivIntro CtxExIntro TrgAndIntro TrgOrIntroL TrgOrIntroR TrgImpIntro TrgNotIntro T…
等式の種類： definitional equality ： Leanカーネルが判定する項の同一性。システムレベルで「同じ」とみなす。 propositional equality ： 等値性を意味する命題（真か偽の文）。証明がないと保証されない。システムレベルで事前に成立している同一性では…
型付きJSON（むかし、XIONとかXJSON呼んでいたヤツ）をマクロで実装する。 ベキ等可換モノイドからジョイン半束を作る。 乗法ベキ等可換環のスペクトル理論（昔のブログ記事にある） 距離連続写像は位相連続写像である。 定義・証明だけでなくて組織化を注意…
型と計算 命題と証明 型演算／構成子 命題結合子 依存型構成子 限量子 型ファミリー (命題ファミリー) インデックス域 論域 インデックス 個体 インデックス変数 限量束縛変数 関数 保証 戻り型 結論命題 ターゲット型 ターゲット命題（質問の） 引数リスト …
Coqの宇宙は {Set, Prop} → Type → Type → ... Leanの宇宙は Prop → Type → Type → ...Typeには番号が付く。別にどっちでもいい。圏論的には次の圏を準備する。$`\newcommand{\mrm}[1]{\mathrm{#1}} `$ $`{\bf Ded}`$ $`{\bf Set}`$ $`{\bf SET}`$ $`{\bf CA…
入力法は、コマンド "lean4: Show all abbribiations" で表示される。 文字 名前 番号 入力法 用途 “λ” Greek Small Letter Lamda U+03BB \lam ラムダ抽象 “↦” Rightwards Arrow from Bar U+21A6 \map ラムダ抽象の区切り “·” Middle Dot U+00B7 \. 無名ラム…
def main (args : List String) : IO UInt32 := doimport Mathlib.Tactic.LibrarySearch #check library_search%パーセント記号は相変わらず意味不明。名前短縮とは、修飾名を短くすること。ひとつは、open でカレント名前空間に別名前空間の名前をぶちまけ…
def main (args : List String) : IO UInt32 := doimport Mathlib.Tactic.LibrarySearch #check library_search%パーセント記号は相変わらず意味不明。
http://www.omdoc.org/pubs/omdoc1.2.pdf の印刷ページ21（p.37）から：Definition 3.2.5 (Monoid) A monoid is a semigroup $`S = (G, \circ)`$ with an element $`e\in G`$, such that $`e ◦ x = x`$ for all $`x ∈ G`$. $`e`$ is called a left unit of $…
モジュール（Leanモジュールと外部・他言語モジュール） 名前空間 セクション キーワード （module は無い、欲しかったが） import namespace section open ： pretectedなら修飾必要、privateは見えない。export は修飾なしになる。 scoped ： 名前空間内に…
