宣言のみからなるテレスコープ〈依存レコード | 指標〉を純コンテキストと呼ぶことにする。宣言と割り当てが混じったコンテキストを混合コンテキストと呼ぶ。純コンテキスト〈指標〉のあいだの手続きは多型判断〈poly-typejudgement〉と言ってもよい。次が予想される。 純コンテキストのあいだの多型判断は、混合コンテキストと同値である。 さらに： 純コンテキストのあいだの多型判断から混合コンテキストへの変換はパッキング 混合コンテキストから純コンテキストへの変換はアンパッキン…

…ストと思える。また、テレスコープとコンテキストは同義だと思ってもよい。公平〈unbaiased〉なテレスコープ＝コンテキストをカリー化することができる。プログラミング言語の実装は、テレスコープを直接扱うことは出来なくて、カリー化のパック形式が使われる。 アンカリー化したテレスコープ／判断は概念的 カリー化したパック形式は実装 表層構文上は、テレスコープを空白区切りリストで表現できる。 コンテキスト内の宣言と、ステージ上の判断の相互変換（パックとアンパック）が重要だが、暗黙化さ…

…れた〈fenced〉テレスコープになる。コンテキスト／テレスコープの基本は名前の集合で、名前は： 宣言定数名： 代入〈割り当て〉ができない型付きの名前、axiom で導入。 イミュータブル変数名： 代入〈割り当て〉が一度だけできる型付きの名前 variable で導入。引数リストでも導入される。 割り当て済み名前： イミュータブル変数名に割り当てを行ったもの。変更はできない。def, let, have で導入。 ミュータブル変数名： 値の変更ができる名前、let mut で…

…として依存レコード〈テレスコープ〉を考えることが多い。 射のプロファイルとシーケントは同義語として、シーケントの区切り記号もターンスタイル〈turnstile〉を使う。 定義による効果： コンテキストの拡張・増大 定義によって何が生成されるか？ これも曖昧。 define function x:A := tに対して、次の6つのモノが混合コンテキストに追加される。 declared name x : A confiermed typing t:A assigned body x…

…実体は依存レコード＝テレスコープ）は指標〈signature〉。型宣言されたすべての名前に値割り当てしたコンテキストは環境〈environment〉と呼ぶ。混合コンテキストは、指標と環境が混じったもの。混合コンテキストが非接地だとは、未宣言の名前がパターン変数として含まれるもの。しかし、混合コンテキストを環境と呼ぶこともある。計算項の型チェック整合性〈consistency〉と、証明項の正当性〈correctness〉は同じ概念である。以下「≡」は定義等値〈definitio…

…シーケントを使う。 テレスコープ概念 多関係とデータ変換写像の二重圏 トリプルは、関係を構成するペア〈レコード〉の集合（それが関係だが）に述語名で名付けている、と考えるべき。つまり、関係と名付けに分解できる。関係は多関係に一般化する。名付けは、単なるトークンラベルから、プロパティを持つプロパティ・ディクショナリ〈JSONオブジェクト〉による名付けに一般化する。すると、述語の名前の空間に伴意関係が入る。伴意関係と関係の包含関係が強調するように名付ける。関係空間＝関係圏のホムセッ…

…、具体的に構成される 指標の圏のinclusive構造 代数の圏 指標の圏 Sign と代数の圏 Alg を結ぶ自由忘却随伴 アンビエント AMB 、通常は“大きいかも知れな圏の圏” ターゲット、アンビエントの対象、固定しても動かしてもよい Alg → AMB の移送〈transfer〉 誘導されるもの モデル関手 構文モナド＝随伴から作られるモナド 割り当て＝手続きの反対射＝クライスリ射 指標テレスコープ 指標フラグメント 色々なものを関手インスティチューションとして見る。

指標テレスコープがあるとする。$`\newcommand{\Within}{\sqsubseteq} \newcommand{\conc}{\mathop{\#} } \newcommand{\dmid}{\mathrel{\|} } %`$$`\quad \Sigma_1 \Within \Sigma_2 \Within \cdots \Within \Sigma_n`$それ自身が指標でなくても、なんらかの指標を前置して指標が得られる構文的対象物〈syntactic obj…

…導出可能〈derivable〉である。 $`\Delta \vdash p: \Sigma`$ 指標の構成手続き〈ソフト実装〉である。 $`p: \Delta \to \Sigma \text{ in } \mrm{Proc}`$ 上と同じ意味。 相対指標（指標テレスコープ）と指標フラグメントの概念を使うと、インスティチューションやπインスティチューションを再現できるのではないか？ $`\models`$ と $`\vdash`$ の使い方が抽象論理／抽象モデル論を構成する。

長さ1の指標テレスコープ$`\newcommand{\Within}{\sqsubseteq}`$ $`(\emptyset \Within S)`$ 指標の標準分解： 宣言の個数と同じ長さの指標テレスコープ 無法則パートと全体で長さ2の指標テレスコープ 任意の長さの自明テレスコープ 指標テレスコープの最初の指標を基底指標〈base signature〉、最後の指標を全指標〈total signature〉、その他の成分を中間指標〈intermediate signature…

…標〈multipart signature〉は、テレスコープで解釈できる。法則パートを定義できれば、有法則指標と無法則指標の概念も定義できる。$`(S \sqsubseteq T)`$ のとき、$`S`$ が無法則パートで、$`T`$ が法則付き指標。法則パートは差分だが、概念的には出て来ない。パートは部分指標だけでなくて、構文的に指標にはならない差分フラグメントも指す。法則が論理式で書かれるインスティチューションの仕様も、多パート指標、つまり指標テレスコープで書けるだろう。

…る。 $`\mathscr{F} = (\mathbb{F}:\cat{Sign} \dashv \cat{Alg} : \mathbb{U}, J, \cat{T} )`$ $`\mrm{Model}_{\mathscr{F}}`$ $`\mathbb{M}_{\mathscr{F}}`$ $`\mrm{Proc}_{\mathscr{F}}`$ テレスコープを定義するには、指標の圏 $`\cat{Sign}`$ に包含構造〈inclusive structure〉が入る。

…n typed lambda calculus by N.G. de Bruijn ド・ブラウンのテレスコープ https://leanprover.github.io/reference/declarations.html#contexts-and-telescopes Leanのテレスコープ https://leanprover.github.io/reference/lean_reference.pdf PDF "4.2 Contexts and Telescopes"

…S_n)`$ を指標テレスコープと呼ぶ。指標 $`S`$ のモデル $`X`$ を $`(S, X)`$ というペアの形に書く。指標テレスコープの各指標にモデルを添えた形 $`( (S_1, X_1) \Within (S_2, X_2) \Within \cdots \Within (S_n, X_n) )`$ をモデル・テレスコープと呼ぶ。ただし、モデル達 $`X_1, \cdots, X_n`$ は忘却条件〈forgetful condition〉（リスコフ条件）を満た…

…対応があると思う。 テレスコープ ←→ フォレスト テレスコープのシグマ構成圏の対象 ←→ フォレストのパス テレスコープのシグマ構成圏の対象集合 ←→ フォレストのパス集合 テレスコープに関して、レベルk（k - 0, 1, ...）のベース圏を考える。レベル0のベース圏はインデキシング圏。フォレストをツリー化して二人対戦ゲーム状態ツリーと考える。ターンl（l = 0, 1, ..）の手番を考える。 テレスコープのレベルkでのパイ構成 ←→ ゲームのターン(k + 1)での…

…し依存ファミリー〉とテレスコープ〈複項依存ファミリー〉のシグマ構成〈グロタンディーク構成〉が本質的に一致することを主張している。依存版のカリー同型／フビニ定理は、精密に議論する必要がある。これかな？$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{cat}[1]{\mathcal{#1} } `$$`\mrm{Fam}(\int_{x\in A} B(x), \cat{C}) \cong \Pi(\lambda\, x\in A…

… %`$依存複関手はテレスコープ〈telescope〉と呼び、依存高階関手は繰り返しファミリー〈iterated family〉と呼ぶ。長さ2のテレスコープ〈2項依存関手〉の場合を述べる。$`(\cat{C}, F, G)`$ を長さ2のテレスコープとすると、$`G:\int_{\cat{C}} F \to {\bf CAT}`$依存カリー化を次のように定義する。$`G^{\cap F} := \lambda\, x: \cat{C}.\int_{F(x)}G_x(-)`$こ…

テレスコープとグロタンディーク構成とグロタンディーク／フビニの定理の関係：indexed thing = indexed family of things を単にファミリーと呼ぶ。インデックス付き圏もファミリーになる。テレスコープはファミリーに関して定義できる。テレスコープの第1成分から、第n成分はファミリーになる。n = 0 ならインデキシングシングだけ、n = 1 なら単一のファミリーになる。つまり、テレスコープは、グロタンディーク構成／シグマ構成を挟んだファミリーの拡張…

….pdf ここから「テレスコープ」を借用する。ただし、 ド・ブラウンのテレスコープは、テレスコープ{列 | リスト | タプル | レコード}と呼ぶ。 テレスコープは、テレスコープ列を対象とする圏を作る一種のスキーマ。 アイディアは次の論文。 https://staff.math.su.se/palmgren/iterated_presheaves_and_dependent_types_v8.pdf "The Grothendieck construction and mo…

テレスコープの起源は テレスコープ - (新) 檜山正幸のキマイラ飼育記 メモ編 。依存ペアの一般化である依存タプルを定義する。テレスコピックファミリーとは、ファミリーの系列 $`F_0, F_1, \cdots F_n`$ で、次を満たすもの。$`\mathrm{dom}(F_i) = I_i`$ とする。 $`I_0 = {\bf 1} = \{*\}`$ $`I_{i + 1} = \Sigma_{I_i} F_i`$ このとき、$`(x_0, x_1, \cdots,…

Title: Telescopic mappings in typed lambda calculus Author: N.G. de Bruijn Date: 1991 URL: https://www.win.tue.nl/automath/archive/pdf/aut103.pdf In Automath (see [I] ,[3] ,[4]) the implementation of mathematical functions is a simple matte…

↓が起源らしい。 Nicolaas G. de Bruijn, Telescopic mappings in typed lambda calculus, Information and Computation 91 (1991), no. 2, 189–204. https://www.win.tue.nl/automath/archive/pdf/aut103.pdf RICHARD GARNER "TWO-DIMENSIONAL MODELS OF TYPE THEOR…

…葉： [Lean] テレスコープ{リスト}? [Lean] タクティク [論理]シーケント推論規則の逆 [Lean] 環境＝大域コンテキスト [論理] 前提〈premise〉、予備知識〈prerequisite〉 [Lean] ライブラリ [論理] 前提、予備知識、セオリー〈theory〉 [Lean] パッケージ [論理] セオリー〈theory〉 [Lean] ファイル＝モジュール [論理] セオリー〈theory〉 帰結〈consequence〉 リーズニング〈reas…