https://arxiv.org/abs/1711.08699 48p Functorial Semantics for Relational Theories https://arxiv.org/abs/1909.00069 31p Regular and relational categories: Revisiting 'Cartesian bicategories I' https://arxiv.org/abs/2109.14123 62p Regular Ca…

https://www.mscs.dal.ca/~selinger/papers/graphical.pdf https://ncatlab.org/nlab/show/DisCoPy https://arxiv.org/abs/2204.02284 Free gs-Monoidal Categories and Free Markov Categories https://arxiv.org/abs/1308.3586 Abstract Tensor Systems as…

$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\mvto}{ \twoheadrightarrow } \newcommand{\Iff}{\Leftrightarrow} \newcommand{\Imp}{\Rightarrow} `$関数従属性$`\mrm{FD}(X\to Y)(R) :\Iff \\ \quad \forall t_1, t_1 \in R. \, t_1[X] = t_2[X] \Im…

http://webdam.inria.fr/Alice/pdfs/Chapter-8.pdf より。Movieテーブル title Director Actor Showing〈上映〉テーブル theater screen title snack ： 提供しているスナック（飲料と軽食） 昔は2本立てがあったが、今はほぼない。以前から使っている。学生…

$`\mathfrak{P}(A)`$ \mathfrak{P}(A) $`\wp(A)`$ \wp(A)

テキスト版： ペースティング図版： ストリング図版：

全般的なこと 用途： ドキュメント印刷 vs.写真印刷 方式：インクジェット、レーザー（業務用ドキュメント向け） インク： 染料インク（写真向け）、顔料インク（ドキュメント向け） 基本色シアン、マゼンタ、イエローが染料インク、 ブラックは、染料インク…

画像：*1*2 *3リンクと引用： 火の鳥 未来編 『COM』 1967/12-1968/09 Wikipedia 手塚治虫とデカルト閉圏 https://tezukaosamu.net/jp/manga/399.html より： 猿田博士が暮らすスノーグローブのような半球状のドームは、生命を封じ込めたグローブ=地球そのも…

[CTRL]+クリック UIP ： https://ncatlab.org/nlab/show/uniqueness+of+identity+proofs 哲学的Impredicativity : https://en.wikipedia.org/wiki/Impredicativity IMPREDICATIVE TYPE THEORY : https://arxiv.org/pdf/1911.08174.pdf PREDICATIVE TYPE THEO…

全称変数は、型宣言された変数で、その型の任意のモノを表す。任意変数と言ってもいい。$`\require{color} \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} } \newcommand{\for}{\Keyword{for } } \newcommand{\assume}{\Keyword{assume } } \newco…

URL: https://courses.engr.illinois.edu/cs576/sp2015/doc/isar-overview.pdf Title: A Tutorial Introduction to Structured Isar Proofs Author: Tobias Nipkow ブラケットは檜山が挿入。 a [tactic] proof is a more or less structured sequence of com…

Title: Kalish/Montague and Ja´skowski Natural Deduction Authors: Mohammad M. Ajallooeian, Francis Jeffry Pelletier Pages: 9p URL: https://mirror.las.iastate.edu/tex-archive/macros/latex/contrib/natded/extended_doc.pdf $`\newcommand{\mrm}[1…

Title: A Browsable Format for Proof Presentation Date: June 1996 Authors: Jim Grundy, Turku Centre Pages: 8p URL: https://www.researchgate.net/publication/2359706_A_Browsable_Format_for_Proof_Presentation structured calculational proof に…

曖昧表現は： 名前・記号の借用 例： G = (G, *, 1) 省略 例： G = (G, *) 名前・記号の多義的使用〈オーバーロード〉 曖昧表現の解決は、データベース検索。検索条件はパターンマッチ問題〈ユニフィケーション問題〉となる。パターンマッチ問題を解いて曖昧…

次の計算系がある。 計算対象物 CC圏 CC複圏 CC多圏 （広義）射 ◯ ◯ ◯ コンビネータ △ ◯ ◯ アレンジメント △ ◯ ◯ CCは Cartesian Closed ◯：うまく定式化できる。 △：ある程度は定式化できる。 演算： 射に対して： 結合、直積、カリー化、評価 コンビネータ…

ミクシン指標の導入と削除には、extends ではなくて、次を使う。 employs 宣言 ： 雇用する、採用する include ディレクティブ ： ミクシン（スニペット）を実際に挿入展開する dismisses 宣言 ： 解雇する、免責する。

lambda ： ラムダ抽象 assume backlog ： バックログラムダ抽象 postulate / demand 要請、ラムダ抽象だがバックログだとマークする。ラムダ変数はバックログ変数＝スタブ＝ダミー。 prepare ： 引数の準備 next ： 区切り記号 and_also ： 区切り記号 end …

関数があるとき、引数型と戻り型の仕様が型プロファイル、単にプロファイルとも呼ぶ。プロファイル概念は集合圏の射以外でも考えられる。引数変数を含む項を使って関数を定義するときの $`\cdots \mapsto \cdots`$ は戻り値指定〈return value disignation〉…

/-! ファミリーと多項式 -/ /- →《《《《《《《《《《《《《《《《《《《《 → -/ namespace My /- 型コンストラクタ Fam -/ def Fam (X : Type) := X → Type abbrev FamOver := Fam variable (I : Type) (i j : I) variable (F G : FamOver I) def Sigm {X: …

一応できた。sectionは要らないみたい。 /-! 写像と関係 -/ namespace My /- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> -/ section Logic def MP {A B: Prop} (p:A → B) (a: A) : B := p a def Inst {X: Type} {P: X → Prop} (w: ∀(x: X), P x) (a : X) : P a := w a …

視点移動とフットワーク： 階層的宇宙のなかで自分がどこのいるのか？ 区別する／区別しない（同一視する／しない）、どちらの立場か？ 例： 引数なし関数名と定数名 名前が定数名〈固有名〉か変数名〈不定名〉か？ スコープに依存（事項）。 名前のスコープ…

/- 用語： スタブ： from https://e-words.jp/w/%E3%82%B9%E3%82%BF%E3%83%96.html スタブとは、切り株、半券、（何かが減ったり短くなった）残り、などの意味を持つ英単語。ITの分野では、本物が用意できないときに動作に支障が無いようにとりあえず置いて…

/-! 写像と関係 -/ namespace My /- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> -/ section Logic def MP {A B: Prop} (p:A → B) (a: A) : B := p a def Inst {X: Type} {P: X → Prop} (w: ∀(x: X), P x) (a : X) : P a := w a def Cut {A B C : Prop} (p: A → B) (q: …

最後の行がエラー。 /-- 記法クラス -/ class LE (X : Type) where le : X → X → Prop scoped infix:50 "≦" => LE.le #check LE section LE_Test variable -- セミローカルコンテキストの導入 (A: Type) [LE A] (a b:A) #check a≦b end LE_Test /-- 全順序集…

$`\Gamma \mapsto \psi : T`$ が判断のとき、コンテキストのラベル〈名前〉をすべて取り除いたものを $`\widehat{\Gamma}`$ とする。プロファイルは：$`\quad \widehat{\Gamma}\to T`$$`f := \big\langle \Gamma \mapsto \psi : T\big\rangle`$ が定義のとき…

圏論 型理論 論理 メタ論理 指数 [_, _] [_→_], → ⇒, → (⇒) 項の定義 |→ |→, |- |-, |→ (|-) プロファイル → →, ~~> →, ~~> (→) ホムセット {_→_} {_→_}, {_~~>_} {_→_}, {_~~>_} {_(→)_}

区別するなら ◯、しないなら／出来ないなら ☓、無意味なら - 。プログラミング言語に関しては、定義時と呼び出し時で二つ。△はやる気になればやれるが、普通はやらない、ほぼ☓。 集合圏 デカルト閉圏 TypeScript Lean 4 関数と関数データ ◯ - ◯, ☓ ◯, ☓ 関数…

関数・定理の定義・記述 Γ |- ψ : A 型推論問題の質問 Γ |-? ψ : ? 項推論問題の質問 Γ |-? ? : A プロファイル宣言 Γ |- _ : A （アンダースコアは不定の意味） 単なる省略 Γ |- ψ : _ （不定だが、型推論で確定可能） ホムセット {f | f: Γ |- _ : A} 毎回…

判断・主張と質問・問題の区別ができること。 命題と事実と証拠と証明の区別が出来ること。 証明とリーズニングの区別が出来ること。 ローカル前提とグローバル・コンテストの区別が出来ること。 公理や前提と先送りの区別ができること。 コンテスト環境とバ…

ライブラリとバックログは双対的な存在。ライブラリ／パッケージ管理と同程度にバックログ管理機能が必要。現状、何もしてくれない。Idrisのholeがある程度はバックログ管理。