本編ネタ
テーゼ： 十分に強力な型システム／型チェッカーを持ったプログラミング言語は、証明記述／証明検証に使える。 型 命題 型変数 命題変数 型定数 命題定数 型構成子 命題結合子 型の値 命題の証拠 計算・関数 証明・定理 計算・関数のプロファイル 証明可能性…
digraph { label="proof" subgraph cluster_not_a { label="not_a" h[shape=triangle] And_left h -> And_left[ label="￢A∧￢B"] } subgraph cluster_not_b { label="not_b" h1[shape=triangle, label="h"] And_right h1 -> And_right[ label="￢A∧￢B"] An…
theorem half_DeMorgan premise h: ￢A∧￢B entails ￢(A∨B) proof we have not_a: ￢A by using And_left with h we have not_b: ￢B by using And_light with h we conclude ￢(A ∨ B) by using Or_tuple with not_a and not_b end 定理 ド・モルガンの半…
入力法は、コマンド "lean4: Show all abbribiations" で表示される。 文字 名前 番号 入力法 用途 “λ” Greek Small Letter Lamda U+03BB \lam ラムダ抽象 “↦” Rightwards Arrow from Bar U+21A6 \map ラムダ抽象の区切り “·” Middle Dot U+00B7 \. 無名ラム…
単語： 直積と直和は双対です。 λ記法 有向グラフ 射 閉圏 関手 双対 域・余域 終対象・始対象 錐・余錐 語句・文： 双対的に、関手の余極限からの射 関手の余極限からの射 双対的に、関手の余極限は余錐の圏の始対象の頂点になっている。余極限への射が一意…
The formal proof on the other side was a big and unreadable 'proof term' 出典： 不明、現在はインターネット上にないようだ。
証明図から証明項に引き写すのは手作業。支援系とかいいながら、ソフトウェアは何も支援してくれない。 /-! example_1.lean -/ namespace Imp def elim_right {A B: Prop} (f:A → B) (a:A) : B := f a def elim_left {A B: Prop} (a:A) (f:A → B) : B := f a…
problem Γ ok? （コンテキスト Γ は正しいか？） judgement Γ ok （コンテキスト Γ は正しい） problem Γ |- t ok? （項 t は、コンテキスト Γ で解釈できるか？） judgementm Γ |- t ok （項 t は、コンテキスト Γ で解釈できる） problem Γ |- ?t : A （型…
命題は型である。← そんなわけないだろ。 命題は型の一種である。 [間違い] 命題はデータ型の一種である。 命題とデータ型は違う。が、命題は型の一種である。 命題は広義の型の一種である。 命題は広義の型の一種であり、データ型も広義の型の一種である。 …
矢印の奪い合い問題 含意を表す 指数型〈関数型 | アロー型〉を表す 射のプロファイルの区切り記号 シーケントの区切り記号（前提と結論） 暫定的解決 含意と指数はカリー／ハワード対応により同一視して → を使う。 射のプロファイルの区切り記号にターンス…
$`\newcommand{\cat}[1]{ \mathcal{#1}} %`$>コアージョングラフは、有向グラフとしての $`\cat{C}`$ の[/単純/な/部分グラフ]である。コアージョングラフ $`G`$ は単純グラフなので、射の両端 $`X, Y`$ が決まれば、射があればそれは一意的に決まる。その射…
インターネットとURIに拘りすぎ → 拘らない 目標が高すぎる → 下方修正 説明が不明瞭 → 明確化 技術的な問題点を順不同、ゴッチャに挙げる： 記述子のIDと記述対象物〈subject | target | descriptum〉のIDがはっきりしない。 埋め込みと分離と参照、抽出と…
Mattias Wadman さん（@mwader、https://github.com/wader）が指摘してくれた（https://twitter.com/mwader/status/1599769763819171840）のは次のネタ。 assignment (.key = 123) update (.key |= .+1) setpath destructing bindings ({a: [1,2]} as {a: [$…
JSON Pointer と JSON patch 作業用の小宇宙 多関係の多圏 関係の二重圏
存在型が混乱しているわけ、シグマ型とイプシロン型 mermaid と graphviz と d3-graphviz 二重圏の事例 デリゲーションとヘルパーとインターフェース
基本アイディアと機能は秀逸だが、コマンドライン・インターフェースの分かりにくさ、説明の曖昧さは悪評が絶えない。名前が不適切。 HEAD は CURRENT だろう。 push, pull が対称ではない。send, fetch と push, pull だろうが、対称化した push = send and…
指標と仕様 - 檜山正幸のキマイラ飼育記 (はてなBlog) パート分けと多パート指標〈multipart signature〉は、テレスコープで解釈できる。法則パートを定義できれば、有法則指標と無法則指標の概念も定義できる。$`(S \sqsubseteq T)`$ のとき、$`S`$ が無法…
本編でいつか書くかも知れない。
https://www.win.tue.nl/automath/archive/pdf/aut103.pdf Telescopic mappings in typed lambda calculus by N.G. de Bruijn ド・ブラウンのテレスコープ https://leanprover.github.io/reference/declarations.html#contexts-and-telescopes Leanのテレス…
相対指標と利用法 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\Within}{ \sqsubseteq } `$指標の圏は $`\cat{Sign}`$ と書く。指標はローマン体大文字。指標…
基本的道具は： Composing Hidden Information Modules over Inclusive Institutions (2004) Joseph Goguen, Grigore Rosu 25p https://fsl.cs.illinois.edu/publications/goguen-rosu-2004-dahl.pdf 特に、"3 Inclusive Institutions" 。$`\newcommand{\cat…
$`\require{color}% \newcommand{\Keyword}[1]{ \textcolor{green}{ \bf #1} }% \newcommand{\When}{\Keyword{when\:\:} }% \newcommand{\And}{ \Keyword{\:\: and \:\:} }% \newcommand{\Then}{ \Keyword{then\: } }% \newcommand{\Holds}{ \Keyword{holds\…
XyJaxを使った例 $`\xymatrix@R-1.8pc@C-2pc{ {} &*{A:Type} & &*{a:A \vdash F(a):Type} & \\ {}\ar@{-}[rrrr] & & & & \\ {} & &* {\prod_{a:A}F(a) : Type} & }`$ \xymatrix@R-1.8pc@C-2pc{ {} &*{A:Type} & &*{a:A \vdash F(a):Type} & \\ {}\ar@{-}[rrr…
「圏論 vs 順序論」の対応表が意外に抜けているので再作成。 順序 圏論 順序集合 圏 自己単調関数 自己関手 閉包作用素 モナド 自己単調関数のプレ不動点〈減少点〉 自己関手の代数 自己単調関数のポスト不動点〈増大点〉 自己関手の余代数 自己単調関数の最…
よくある二項対立的分類： クライアント vs サーバー 生産者 vs 消費者 送信側〈sender〉 vs 受信側〈receiver〉 順行〈順方向〉 vs 逆行〈逆方向〉 内部 vs 外部 変わった分類： エージェント vs 環境 データ vs 反データ 電子 vs 陽電子 電子と陽電子が出…
$`\newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\In}{\text{ in } } \newcommand{\B}[1]{ \{\!| #1 |\!\} } \newcommand{\A}[2]{ \langle\!| #1 \mid #2 |\!\rangle } `$$`\text{Basic} :::\\ \forall A \in |\cat{D}|.\\ \forall M \in |\cat{M}|.\\ \…
トレース付きモノイド圏の新しい定義 圏論的レンズ 4： テレオロジー圏 トレース付き圏の公理を次のように名付ける。 バニシング バンドリング （通常はバニシング 2） タイトニング スライディング ヤンキング スーパーポージング テレオロジー圏のトートロ…
多ソートのストリング図の定式化に極性〈in-out〉と色〈型 | ソート | 対象〉が付いた集合が必要になる。色が {a, b, c} なら (-a, -a, -b, +b, +a) とかが色付き極性付き集合の表記になる。極性は二値なら何でもいいから左右でもよい。(→a, →a, →b, ←b, ←a)…
大きかも知れない圏の2-圏 順序集合の圏 余完備な余デカルト圏 順序完備なミート半束 余連続な自己関手 連続な自己関数 自然変換 関数順序 自己関手のランベック代数 自己単調関数の劣不動点 モナド 閉包作用素 モナドのアイレンベルク／ムーア代数 閉包作用…
そうそう、セルに型が付くのだった。セルに型フィールドと値フィールドがある。特定番地のセルのフィールドに値が入っていることを$`\quad \text{A2.Val} = 7\\ \quad \text{A2.Typ} = {\bf N} %`$まとめて$`\quad \text{A2} = (7 : {\bf Nat})`$次の機能が…
