ステージと知識シーケントは同じもの。ステージは内部にシーケントをホストする。 ステージのコンテキストはステージ矩形の上部にだけ描いて、内部には貫入しない。 ステージのコンテキスト部のレイアウトは知識シーケントと同じ。 ステージは、コンテキスト…

基本的にステージクリア型ゲーム。ビジュアルノベル（選択式アドベンチャーゲーム）の要素も入る。 ステージはツリー状に配置される。親ステージと子ステージ〈サブステージ〉がある。 ステージツリーは、状態遷移により動的に変化する。 ステージにコンテキ…

Ident 公理 Cut オペラッド結合 Weak 水増し Cont 冗長性縮約 contraは矛盾 Perm 交換 CtxAndIntroL CtxAndIntroR CtxtOrIntro CtXImpIntro （LJ変形） CtxNotIntro CtxUnivIntro CtxExIntro TrgAndIntro TrgOrIntroL TrgOrIntroR TrgImpIntro TrgNotIntro T…

型と計算 命題と証明 型演算／構成子 命題結合子 依存型構成子 限量子 型ファミリー (命題ファミリー) インデックス域 論域 インデックス 個体 インデックス変数 限量束縛変数 関数 保証 戻り型 結論命題 ターゲット型 ターゲット命題（質問の） 引数リスト …

Coqの宇宙は {Set, Prop} → Type → Type → ... Leanの宇宙は Prop → Type → Type → ...Typeには番号が付く。別にどっちでもいい。圏論的には次の圏を準備する。$`\newcommand{\mrm}[1]{\mathrm{#1}} `$ $`{\bf Ded}`$ $`{\bf Set}`$ $`{\bf SET}`$ $`{\bf CA…

対応表： 定理記述 関数定義 定理のステートメント 関数{定義}?のヘッド 証明項 計算項 定理記述する 関数定義する から導出された定理 から定義された定理 構文と意味は混同される。 関数そのもの（型の圏の射）と関数定義という構文対象 定理そのもの（命…

まだ未整理だが、とりあえず備忘メモ。まず、対称性がある操作達。 無制限タプル構成 無制限コタプル構成（無制限タプル構成の双対） 有限タプル構成（無制限から制限） 有限コプル構成（有限タプル構成の双対） 依存カリー化 カリー化（依存カリー化の非依…

フォワード・リーズニング用に、ステージと同じコンビネータ・コマンドがある： 連言導入用コンビネータ： 既存のn個の証明から連言への証明を作る。 全称導入用コンビネータ： 既存のパラメータ付き証明から全称への証明を作る。 選言除去用コンビネータ： …

ステージ内に居るシーケントは： 事実シーケント 質問シーケント〈問題シーケント | ゴール〉 やること： 事実シーケントの構成（味方を増強する） 質問シーケントの分解（敵を衰弱させる／消滅させる） ステージの種類は： 連言導入用ステージ（連言成分〈…

次のようなキーワードの名前スコープと使い方について考える。 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〉のことがある。したがった、判断も宣言にエンコード〈パッキング〉できる。宣言＝型宣言を束縛子ということもある。名前を型に束縛するから。しかし、名…

帰納的型の値コンストラクタ記号 帰納的型の型名は、パラメータを持つと型コンストラクタ 構造体型は、単一の値コンストラクタを持つ帰納的型だが、フィールド名をコンストラクタとも言う。 オブジェクト指向のコンストラクタは、単元集合またはパラメータ集…

postulate 公準 prerequisite 要請 assumption 仮定 antecedent 前件 premise 前提〈プロミス〉 hypothesis 仮説 context 文脈 environment 環境

型の導入規則とは、型の生成規則で、型だけではなくて要素の構成規則も含む。 型を型構成子で生成する。 要素を要素〈値〉構成子で生成する。要素生成子は関数である。 型の除去規則とは、型の消費規則で、関数による要素の構成規則（「構成」で間違ってない…

テキスト ピクチャー ラベル（名前) ワイヤー頂点 型（命題含む） 色付きワイヤー 項 ストリング図 宣言 入力端頂点とワイヤー コンテキスト ワイヤーパレット シーケント ノード 公理シーケント 展開不可能ノード 割り当て 展開可能ノード ステージ パレッ…

散文化は prosify。 映像作品を、通常の文章に直して伝えること。 映像作品を鑑賞することは誰でも出来るが、ノベライズ／散文化は難しい。

「状況」、「シーン」なども用語候補だが、「ステージ」を使う。コマンドは、ステージ上の判断／質問を操作する。またステージ自体もコマンドで操作する。同じ名前に対して、フォワードコマンド doXxx とバックワードコマンド undoXxx がある。全般的な管理…

型 ←→ 命題 ←→ 対象 関数（要素含む） ←→ 定理（証拠含む） ←→ 射 関数コンビネータ ←→ 定理コネクティブ？（言及も命名もされない） ←→ オペレーター／コンビネータ リーズニング・コマンド 対応物がないゲーム・コマンド 圏論的に整理するなら もの〈シン…

次を区別しなくてはならない。 命題 証明〈証拠〉 判断〈主張〉シーケント 質問〈問題 | 問い合わせ〉シーケント フォワードリーズニング（推論ルール含む） バックワードリーズニング（バックワード推論ルール含む） 定理は、証拠〈証明〉を引数として証拠…

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

我々は、様々なレベルのコンテキスト（ライブラリ、モジュール／セクション）を行為〈activity〉により拡張していくのだが、拡張のための行為は二種類しかない。 関数定義 （λΠ計算ベース） 帰納的型定義 （CICベース） 関数定義は def で、帰納的型定義は i…