Lean
自然数の具体的リテラルを (nat_lit 3) とか書くが、事情は不明。追記： /-- The `nat_lit n` macro constructs "raw numeric literals". This corresponds to the `Expr.lit (.natVal n)` constructor in the `Expr` data type. Normally, when you write a…
罪も多い。次を混乱させてしまった。 指標とモデル圏 パラメータ付き指標とファイバー付きモデル圏 忘却射影に対するセクション（so-called インスタンス） ひとつのモデル モデル圏／ファイバー付きモデル圏のあいだの関手（構成手続き） 特に、ファイバー…
({foo := "hello"} : Bar) の代わりに、{foo := "hello" : Bar} が使える。 namespace Temp structure Bar where foo : String := "hello" baz : String := foo ++ "world" #check {foo := "hi" : Bar} #check { : Bar} #eval { : Bar}.baz instance : ToStr…
自然数集合から可換モノイドへのインスタンスメーカーが3つあって、 足し算 掛け算 最大値（小さくないほう） 最小公倍数 それとは別に、ベキ等可換モノイド（演算記号 ◇）をジョイン（演算記号 ∨）半束にするインスタンスメーカーがあるとする。インスタン…
指標Σに対して、モデルの集合は |Model[Σ]| となる。適当な集合 K からの写像 K → |Model[Σ]| をインスタンスメーカー〈クリエイター | コンストラクタ | ビルダー〉と呼ぶ。なんらかの忘却射影 U:|Model[Σ]| → K があり、インスタンスメーカーがセクション…
theorem ext {a b : Set α} (h : ∀ (x : α), x ∈ a ↔ x ∈ b) : a = b := funext (fun x ↦ propext (h x))事実 半形式的：$`\text{Fact ext}\\ \text{For } a, b : \mathrm{Set}\: \alpha \\ \text{When } \forall (x : α),\, x \in a \iff x \in b \\ \text{…
まだ未整理だが、とりあえず備忘メモ。まず、対称性がある操作達。 無制限タプル構成 無制限コタプル構成（無制限タプル構成の双対） 有限タプル構成（無制限から制限） 有限コプル構成（有限タプル構成の双対） 依存カリー化 カリー化（依存カリー化の非依…
Leanでは 対応する閉じ括弧をハイライトするとか、"go to bracket"コマンド（[ctrl+shift+\]）がうまく動かない。なにしろ、begin/endの括弧を使わない方針だから。
次のようなキーワードの名前スコープと使い方について考える。 def, theorem let in, let return providing return where section module package 名前とスコープに関する概念： イミュータブル名〈プログラム定数〉とミュータブル名〈プログラム変数〉 公理…
$`f`$ のフルカリー化を $`f^\wedge`$ として次が意味的には同じであること。 $`f(a_1, \cdots, a_n)`$ $`f^\wedge(a_1) \cdots (a_n)`$ $`(\cdots(f^\wedge\triangleleft a_1) \cdots )\triangleleft a_n`$ $`f^\wedge\: a_1\: \cdots\: a_n`$ これをストリ…
https://www.cs.vu.nl/~jbe248/lv2017/10x4.pdf より：the {type checking | proof verification} problem Γ |-? t:A the {typability | type {synthesis | inference}} problem Γ |- t:? the {{type | proposition} inhabitation | proposition provability…
コンテキストと指標は、構文的には区別できないのだが、次の違いがある。 指標はインスティチューション的な意味での指標である。 指標のあいだの射は指標射で、モデル圏のあいだのリダクト関手を定義する。 コンテキストは、固定した指標に対する構文的圏の…
$`\require{color} % 緑色 \newcommand{\In}{ \text{ in }} \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\For}{\Keyword{For } } % 使用 \newcommand{\Let}{\Keyword{Let } }% 使用 \newco…
判断シーケント＝関数定義があるとする。$`\quad a : (\Gamma \vdash t : \beta)`$これを次のようにパックする。$`\quad (a : [\Gamma \to \beta], a := t^\wedge)`$ここで、$`t^\wedge`$ は項のフルカリー化。パックした定義は、環境コンテキストに追加でき…
$`\require{color} % 緑色 \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\Providing}{\Keyword{Providing } }% \newcommand{\When}{\Keyword{When } }% \newcommand{\And}{\Keyword{And } }% \newcommand{\Holds}{\Keyword{Holds…
単に「コンテキスト」は混合コンテキスト 純コンテキスト＝宣言コンテキスト 混合コンテキスト＝宣言と定義のリスト 定義は、宣言（x:A）と割り当て（x:=t）のペア シーケントは三種類： 判断シーケント、事実シーケント、質問シーケント 判断シーケントは、…
ムービーはデータ構造 ムービーはフレームとトランジションからなる。 フレームはステージの構造的な集まり。 ステージはツリー構造を持つ。カレントステージが一意に決まる。 ステージは、シーケントとサブステージの集まり。 シーケントは判断シーケントか…
宣言のみからなるテレスコープ〈依存レコード | 指標〉を純コンテキストと呼ぶことにする。宣言と割り当てが混じったコンテキストを混合コンテキストと呼ぶ。純コンテキスト〈指標〉のあいだの手続きは多型判断〈poly-typejudgement〉と言ってもよい。次が予…
名前〈ラベル〉と型項のペアを型宣言、あるいは単に宣言と呼ぶ。型項は判断のパック形式〈packed form〉のことがある。したがった、判断も宣言にエンコード〈パッキング〉できる。宣言＝型宣言を束縛子ということもある。名前を型に束縛するから。しかし、名…
帰納的型の値コンストラクタ記号 帰納的型の型名は、パラメータを持つと型コンストラクタ 構造体型は、単一の値コンストラクタを持つ帰納的型だが、フィールド名をコンストラクタとも言う。 オブジェクト指向のコンストラクタは、単元集合またはパラメータ集…
依存アロー型とパイ型は同じもの。アロー型＝指数型は依存アロー型の特別なもの。Lean 4 で依存アロー型の書き方が (x:α) → β （βは型項）となったが、Agdaでは以前からこの形だったようだ。 Π(x:α), β ≡ ∀(x:α), β ≡ (x:α)→β カリー化／アンカリー化は同じ…
postulate 公準 prerequisite 要請 assumption 仮定 antecedent 前件 premise 前提〈プロミス〉 hypothesis 仮説 context 文脈 environment 環境
型の導入規則とは、型の生成規則で、型だけではなくて要素の構成規則も含む。 型を型構成子で生成する。 要素を要素〈値〉構成子で生成する。要素生成子は関数である。 型の除去規則とは、型の消費規則で、関数による要素の構成規則（「構成」で間違ってない…
テキスト ピクチャー ラベル（名前) ワイヤー頂点 型（命題含む） 色付きワイヤー 項 ストリング図 宣言 入力端頂点とワイヤー コンテキスト ワイヤーパレット シーケント ノード 公理シーケント 展開不可能ノード 割り当て 展開可能ノード ステージ パレッ…
※ 2023-01-17に書いたけど投稿忘れ。関数型言語で、デカルト閉圏の射としての関数を表すことはできない。表わされるのは、関数型〈指数型〉の要素。要素をポインター関数とみなしても、表わされるのはポインター関数に限る。2つのポインター関数に対して、ev…
※ 2023-01-17に書いたけど投稿忘れ。演算子の優先度 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続きLeanの場合、まだ調整は必要かも知れない： PrefixSuffixPrecidence 1024 = max ArgumentPrecidence 1023 = arg CompositionPrecedence 90 ($`\circ`$) Exp…
散文化は prosify。 映像作品を、通常の文章に直して伝えること。 映像作品を鑑賞することは誰でも出来るが、ノベライズ／散文化は難しい。
「状況」、「シーン」なども用語候補だが、「ステージ」を使う。コマンドは、ステージ上の判断／質問を操作する。またステージ自体もコマンドで操作する。同じ名前に対して、フォワードコマンド doXxx とバックワードコマンド undoXxx がある。全般的な管理…
型 ←→ 命題 ←→ 対象 関数（要素含む） ←→ 定理（証拠含む） ←→ 射 関数コンビネータ ←→ 定理コネクティブ？（言及も命名もされない） ←→ オペレーター／コンビネータ リーズニング・コマンド 対応物がないゲーム・コマンド 圏論的に整理するなら もの〈シン…
B -A が before, after のオプション。-B 3 -A 3 は単に -3 でも同じ。-C は -2 つまり -B 2 -A 2 と同じ。 mathlib > git branch * master mathlib > git rev-parse master 8618f40d51539454fe06511d5c8504a77f30c598 mathlib > grep -A 3 -B 3 8618 ..\..\…
