セミナー

とりあえず人名

カントール 1845 -- 1918 ヒルベルト 1862 -- 1943 ラッセル 1872 -- 1970 ハスケル・カリー 1900 -- 1982 ノイマン 1903 -- 1957 チャーチ 1903 -- 1995 ゲーデル 1906 -- 1978 ゲンツェン 1909 -- 1945 チューリング 1912 -- 1954

MiniLisp → MiniPL〈MPL〉

Lisp由来であることを強調する必要はない。MiniLisp - (新) 檜山正幸のキマイラ飼育記 メモ編 で書いた以外の構成素: var宣言、または初期化構文 let式 if文、case文、while文 ブロックスコープ構造 論理言語のインタープリター実装 $`\newcommand{\MPL}{\m…

MiniLisp

データ型 Nat Bool String Nil Basic := Nat | Bool | String | Nil Tree(X) List(X) 基本関数 Nat, Bool, String の色々 Tree: left, right, pair, isBasic List: fst, rest, cons, nth, isNil プログラム式の評価:$`\quad (p, \rho) \overset{E}{\mapsto}…

演繹システムの記法など

ラムダ記法+適用:$`\quad (\lambda x\in X. P(x))(a) \equiv (P(x) \mid x = a)`$証明可能性:$`\quad \vdash_S (P(x) \mid x = a)`$エミュレーション:$`\quad \vdash_T \sigma(\ulcorner p \urcorner, a) \iff \vdash_S p(a)`$自己エミュレーション:$`\…

2005年7月の課題

課題と参考文献: インスティチューションがうまく使えない - 檜山正幸のキマイラ飼育記 (はてなBlog) 2005年7月の疑問・課題 はじめての圏論 その第5歩:変換キューの圏 - 檜山正幸のキマイラ飼育記 (はてなBlog) はじめての圏論 第6歩:有限変換キューと半…

コンピュータ形式化と問題点・課題

数学の時代区分 エジプト/バビロニア/中国の時代 事実と手法の集積 ギリシャ、ユークリッドは紀元前300年前後アレクサンドリアの人、 公理と証明の発明 19世紀 古典述語論理と集合論による厳密化・体系化、ヒルベルト ? コンピュータで検証可能な記述 問…

レンズ/オプティックの描画法

いずれの描画法でも、平面を順方向エリアと逆方向エリアに区切っている。この区切り線を中心線と呼ぶことにする。代表的な3つの描画法を述べる。もちろん、他の選択肢もある。描画の約束によりファントム交差/ファントムカーブは生じる。相互変換には鏡映変…

選択肢の結合としてのコンテナの結合積

アリーナ1 {旅行 → {1日目, 2日目, 3日目}} $`y^3`$ アリーナ2 {和 → {焼き魚, 煮魚, 刺し身}, 洋 → {グリルチキン}, 中華 → {エビチリ, 麻婆豆腐}} $`y^3 + y + y^2`$ アリーナ3 {和 → {羊羹, わらび餅}, 洋 → {ショートケーキ, モンブラン, ババロア}} $`y…

トレース付き圏と両側テレオロジー圏

トレース付きモノイド圏の新しい定義 圏論的レンズ 4: テレオロジー圏 トレース付き圏の公理を次のように名付ける。 バニシング バンドリング (通常はバニシング 2) タイトニング スライディング ヤンキング スーパーポージング テレオロジー圏のトートロ…

アクツェル推論系と不動点とアリーナ計算

確かムーアは論理式の集合の上の閉包作用素として演繹系を定義したと思う。アクツェルの推論系〈inference system〉の定義は以下のよう: 判断〈judgement〉の集合 U 演繹ルール〈deduction rule〉は A⊆U と c∈U の組 (A, c) 、これを A/c とも書く。 A を演…

コンステレーション計算

フラットコンステレーション=ストリング図テンプレート⊇ワイヤリング図 ソリッドディスク=ストリング図⊇無ノード・ワイヤリング図=スパイダー図 外サークル=ストリング図のキャンバス境界 内サークル達=ストリング図テンプレートのスロット境界達 中間…

アリーナ計算とコンステレーション計算

右の欄はローヴェアの代数セオリー。 アリーナ コンステレーション 代数指標 カローラ テンプレート オペレーション アリーナ テンプレートキット 指標 ツリー コンステレーション 項 フォレスト コンステレーションキット 割り当て〈代入〉系 リーフ スロッ…

コンテナの図法とメンタルモデル

コンテナをアリーナ=カローラ・フォレストで図示するとして: ツリーをグラフと見るとき、通常グラフ解釈かオープングラフ解釈か? リーフをどう描くか? ドット、アロー、ワイヤー ルートをどう描くか? ドット、アロー、ワイヤー ツリーとルートを別物と…

レンズ用語

困っている。 何がプレーンレンズ〈バニラレンズ〉か分からない。 元祖レンズの有法則/無法則は、まーハッキリしている。 単相レンズ〈monomorphic lens〉と双相レンズ〈ニ相レンズ | bimorphic lens〉の区別はあるが、一般的とも言えない。ヘッジーズ〈Hea…

続・表計算

そうそう、セルに型が付くのだった。セルに型フィールドと値フィールドがある。特定番地のセルのフィールドに値が入っていることを$`\quad \text{A2.Val} = 7\\ \quad \text{A2.Typ} = {\bf N} %`$まとめて$`\quad \text{A2} = (7 : {\bf Nat})`$次の機能が…

例え話に表計算

ヒエー、僕は使ったことない。 表計算ソフト〈スプレッドシート〉が便利なのは、入力に対する自動計算/自動再計算をやってくれるから。 高機能かつDomainSpecificな電卓〈カリキュレーター〉として使える。 セル番地は A1, C30 のように英字と数字の並び、…

記号負け

顔負け 貫禄負け 気圧される 圧倒される 威圧される 威嚇される 怖気づく 萎縮する 恐怖を感じる 親しみを持てない 劣勢に立たされる 例えば:$`{\displaystyle \int_{x = a}^b \frac{df}{dx}(x)\, dx = \Big[ f(x) \Big]_{x = a}^b}`$

コンテナと遷移系

コンテナ〈ファミリー〉の演算と特別な射: {{ディリクレ}?{テンソル}?}!積 $`\otimes`$ : コンテナ&レンズ演算〈(0 | 1)-オペレーター〉、遷移系の演算とも考えられる。 ジョイン $`\triangleleft, \triangleright`$ : 遷移系の演算、遷移系だけ考えると…

計算の構造

構文論: 基本概念 別名 ラベル 名前, 変数, 不定元, 定数, 識別子 シング n-射, もの, 実体, 具体物 割り当て 束縛, 代入, 関連付け〈association〉 リテラル 定数, 名前, 記号 コネクティブ 演算{子}?記号 コンビネーション 項, 式, 図式 ※ 論理のリテラル…

真偽値の集合Prop何でもよい

CoqでもLeanでもPropを使うが、Prepの正体は何でもよくて、デカルト閉半環圏(の対象集合)であればよい。自然数上に定義された述語 p は p: Nat → Prop だが、その実体が次のいずれでも、さらに他の何かでもいい。$`\quad p:{\bf N} \to {\bf B} \text{ in …

lawless signature に法則を付け足すときの記法

構文は: law 2-ラベル :: 閉じた論理式または variable 変数の型宣言 law 2-ラベル :: 自由変数を含む論理式法則の圏論的実体〈シング〉は2-射なので、法則名は2-ラベルとする。事例: signature LawlessMonoid within Set { sort U operation e: 1 → U ope…

区別できない症候群

名前〈記号〉とモノを区別できない。a と [​[a]​] (スコットブラケット)で区別する。 命題と主張を区別できない。P と |- P で区別する。 要素と集合を区別できない。a ∈ A で区別する。 内包と外延を区別できない。A = {x∈A | P(x)} で区別する。 所属と…

指標とモデルによる記述

section 分数の定義と掛け算 { declare 0-mor F in Set define F := Int×(Int\{0}) declare 0-mor 1 in F // オーバーロード define 1 := (1, 1) declare 1-mor m : F×F → F in Set reserve a, b, c ∈F reserve x, y ∈Int define m := λ(a, b).( (a_1×b_1, …

談話構造

話し手の態度(意図の復元可能性): 話し手基準: 自分(話し手)なら、この言い方で分かる(復元可能)。 聞き手基準: 聞き手は、この言い方で分かる(復元可能)だろう。 主要な責任: 話し手責任: コミュニケーションを成立させる責任は話し手にある。…

コンストラクタ

(n, k)→(m, l)-コンストラクタ F とは: C はn-圏、|C|_k は C のk-射の集合 D はm-圏、|D|_l は D のl-射の集合 F: |C|_k ⊇→ |D|_l が、CからDへの(n, k)→(m, l)-コンストラクタ 部分写像でないときはフルコンストラクタ 例: (0, 0)→(0, 0)-コンストラクタ…

ストリング図とコンステレーションの次元

コンステレーションの図示にいおて、1次元キャンバスの場合も2次元に描く習慣があるのか? -- これは混乱のもとだな、良くない。 1次元穴あきキャンバス: 区間に穴が開いている。穴は幅0でも有限幅でもいい。穴の境界にプロファイル情報が載るが、それは A …

コンステレーション関係

terminology _ vocabulary コンステレーション { サークル ポート マーカー 向き付きサークル〈oriented circle〉 順序付きサークル = 向き付きマーカー付きサークル 方向付きサークル〈directed circle〉 方向付き順序付きサークル〈directed ordered circl…

シグマ型とパイ型

用法1 用法2 用法3 シグマ型 依存ペア型 依存積型 依存和型 パイ型 依存関数型 依存指数型 依存積型 description _ procedure Sigma from a Type A and a Family (F : A → |Set|) produces a Type S { // 省略 } procedure Pi from a Type A and a Family (F…

用語法定義

ボキャブラリーをノードとして、コンテキストを辺とする有向グラフを考える。木と同様に、リーフノード〈シンクノード | sink node〉という概念を使う。 リーフノードを基礎ボキャブラリー〈ground vocabulary〉と呼ぶ。 基礎ボキャブラリーではないボキャブ…

用語や学習法関連

TrRun4: 檜山トレラン4 X01 アットマークによる識別ヒント - HackMD 檜山トレラン4 E01 名付けのジレンマ - HackMD 檜山トレラン4 D01 混乱しがちな言葉 - HackMD 檜山トレラン4 B02 名前の使用法と導入時の半形式的記述 - HackMD 檜山トレラン4 B08 0-文法 …