型ファミリーと総和と総積

次は同義語

  1. 多相型
  2. 総称型
  3. 型構成子
  4. パラメータ付き型
  5. インデックス付き型
  6. 型ファミリー

適切な言葉は型値関数、使うのは型ファミリーにする。

型ファミリーとは、Xを集合として、F:X → |C| という写像Cの対象を型と呼べば、型値関数。X⊆|C| のときが総称型。X∈|C| のときがパラメータ付き型。

型ファミリーFから総和型 Σ(F) と総積型 Π(F) を作れるが、Π(F) の構成には「型バンドルとガンマ・オペレーター」が必要。型バンドルとガンマ・オペレーターを導入しないで説明しても分かりにくい!

型バンドルとは、型のあいだの全射のこと。小さい型と大きい型の区別が必要。小さい型=型、大きいかも知れない型=型カインド。総称型は型カインドを域とする型ファミリー。

Seq:N×CC に対して、左カリー化 Seq と右カリー化 Seq を考えると、左カリー化がList、右カリー化がArray。

和を持つラムダ計算

ツリーデータ型のモナドモナドを具体的に書き下すととなると、けっこう難しいようだ。何が障害かというと:

  1. 型がうまく定義できない。
    1. 空型と単位型
    2. 部分集合型、内包的記法
    3. ベキ集合型
    4. 直積型
    5. 指数型
    6. 直和型
    7. 依存和型
    8. 依存積型
    9. 型カインド
  2. 処理がうまく書けない
    1. ラムダ記法
    2. 型付けと型注釈
    3. 型のラムダ抽象
    4. タグ付き値〈タグ付きインスタンス〉 v@t
    5. case-of-or-end文
    6. forsome-use文 インデックス付き型、依存和型のデータを処理する文
    7. tuple-and-end文
    8. cotuple-or-end文

より具体的な細かいこと

  1. f(x), f[x], x.f, fx, f<x> などの違いに惑わされる。
  2. 型カインド(K⊆|C|)、型ファミリー(f:I → |C|) などに馴染みがない。型ファミリーは圏の離散図式。
  3. 依存和型とタグ付き値が扱えない。

型理論だと、独自の用語法・記号法とぎごちない定式化になっている。

わだち圏と論理

わだち圏〈トラック圏 | track category〉は、今風に言えば (2, 1)-圏。

  • k > 2 なk-射は自明
  • k > 1 なk-射は可逆

ホム圏は亜群になるので、亜郡豊饒な圏。特別な例として:

  • ホムセットが亜集合である圏=ホムセットに同値関係が載っている圏

わだち圏をベースに論理を展開できる。

  • 対象=論理式
  • 射=証明図
  • 2-射=証明図の同値変形

現代思想・圏論特集の記事で

丸山先生の記事で、「アブラムスキー・クッカ対応」と書いてあったけど、「クッカ」に近いのか。それと、この対応はもっと昔の人の名前を使って「カリー・ハワード・ランベック対応」がより一般的だと思う。圏論と量子情報・計算を対応づけたのはアブラムスキー・クッカかも知れないけど。

コンピュータサイエンスは無益

言っていることは正しいし、こういう意見の人はけっこう多いけど、まとまった文章がないから助かる。

記事を消してしまう可能性があるので、引用しておく。

コンピューターサイエンスの学習が、駆け出しエンジニアの職業エンジニアになる過程で邪魔となるという話をいたします。

一人前のエンジニアになるのを阻害する、または遅らせる、と。

職業として成立するのは、お金を払ってでも他人に頼みたい面倒ごとがあるからです。

プログラミングというのは、非常に面倒なので、他人にお金を払ってでもやって欲しい人が世の中に大量にいます。(ですから職業として成立しやすいわけです)

誰もやりたくないことを引き受ける。これが職業エンジニアの仕事なのです。

顧客は、お金を払って「自分ではやりたくはない汚れ仕事」を発注する、という発想らしい。

プロサッカー選手でもないのにプロサッカー選手と同じく、サッカーをプレイするのは、それが楽しい行為だからです。これと同じことがコンピューターサイエンスにもいえます。

この比喩はたぶん、

という対比。前提に、

  • 彼/彼女がやっている仕事は、趣味のサッカーとの接点はない。
  • よって、趣味のサッカーは娯楽にはなっても、仕事に益はない。

という推論があるようだ。

続いて、想定される反論への想定される再反論がある。

より優秀なエンジニアになるために必要と聞いたので取り組んでいる。[という反論に対して]

もう一度職業の原則に立ち返っていただきたいのです。コンピューターサイエンスの学習にお金を払ってくれる人はいるでしょうか?残念ながらいないのです。何度でも繰り返しますが、職業エンジニアになるためには、他人がやりたくない面倒事を対価を受け取って代理遂行することが絶対に必要なのです。

やはり、

  • 自分たちエンジニアは、「自分ではやりたくはない汚れ仕事」を押し付けられる側なんだ。

という認識が強い。学習にお金を払うクライアントはいないのはそのとおり。学習の結果得たものにはお金を払う、って発想はないみたいだ。

[自発的学習は]おそらくは他人からの承認を求めているからです。学習という行為自体にその危険が常につきまとっています。

これはそのとおりだと思う、ホントに。だけど、例えば上司が、学習好きの部下に「お前がやっていることは承認欲求に過ぎない」とか言う場面を想像すると胸が痛む。

コンピューターサイエンスの基礎知識が、クライアントの求めるエンジニアリングの下地になるという反論もありえるでしょう。しかし、下地にはならないことが既によく知られています。

これは、「下地にはならない」じゃなくて、「クライアントの求めるエンジニアリング」がコンピュータサイエンスを必要としないレベルのことがある、って話だな。この方は、クライアントの求めることは「自分ではやりたくはない汚れ仕事」の代行だと確信しているようだ。おそらく、そういう「自分ではやりたくはない汚れ仕事」の経験しかないのだろう。「自分ではやりたくはない汚れ仕事」の遂行=プロの仕事 だという認識なんだろう。

商品一覧を綺麗に並べて、それをユーザーがクリックしたら Shopify の API を叩き、決済結果をユーザーにメールで通知することなのです。それにはコンピューターサイエンスは必要ありません。残念ながらあなたはこの手の仕事をあと五年はすることになります。それでもコンピューターサイエンスが下地に必要そうでしょうか?ピザ生地を作るのに、農学の知識は必要なさそうですが。

なるほど。やっぱり「知識もスキルも要らない仕事に知識もスキルも要らない」という“まっとうな話”。現実の仕事のなかで、「自分ではやりたくはない汚れ仕事」で「知識もスキルも要らない仕事」が相当量あることはたぶん事実だろう。その分野に人材が必要なのも当然。そういう人材にはコンピュータサイエンスや学習の習慣は要らないのもホントの話。何も間違っているところは見つからない。

ただ、分量が少ないのかもしれないが、「自分ではやりたくはない汚れ仕事」で「知識もスキルも要らない仕事」ではない仕事があるのも事実。学習者の動機は「あなたにしか出来ないから頼みたい」という意味での仕事をしたいからではないのかな? 「自分ではやりたくはない」じゃなくて、「自分では到底できっこない」からクライアントが依頼するような。

[追記 date="翌日"]
記事は削除されてない。冒頭にリンクが追加されたようだ。

このリンクは何の意図があるのだろう? 本文に変更追加はないようだが‥‥
[/追記]

谷村先生 vs 戸田山先生

@2020-09-30 20:00--22:00 by Zoom

  • vs にならなかった。
  • 谷村先生の絵が力作。
  • パットナムの双子地球が批判されていた。
  • 双子地球の“水”は、心的状態が一致しても外延が一致してない例らしい。
  • SF、ファンタジーとしては面白い気がするが、フィクションとしても詰めが甘いのは確か。
  • 「直観ポンプ」がキーワードらしいが、よく分からなかった。
  • 谷村先生のおばあさんの話(詐欺的な高いお墓や壺)は、話としては唐突だったが、よく分かる!

用語ペアの具体例

用語ペアの関係性」の続き。

  • ⊆: 包含的
  • ⊆→ : 規準的埋め込み可能
  • ⊥: 排他的
  • ∪: 総称
環、可換環、非可換環
数、単項式、多項式
  • 用法 1: 数 ⊆ 単項式 ⊆ 多項式
  • 用法 2: 数 ⊆ 単項式、 単項式 ⊥ 多項式、単項式∪単項式 = ?
  • 用法 3: 数 ⊥ 単項式、 単項式 ⊥ 多項式、数∪単項式 =?、 数∪単項式∪多項式 =?、単項式∪多項式 = ?
単純データ、リストデータ
  • 用法 1: 単純データ ⊥ リストデータ、単純データ ⊆→ リストデータ、単純データ = 非リストデータ
  • 用法 2: 単純データ ⊆ リストデータ

いずれにしても、リストの項目データを単純データと呼ぶと入れ子リストで破綻する。「リスト関手の引数」と「単純な対象」は違う。

モナド的状況のときは:

  • 厳密に包含関係があるか
  • 規準的埋め込みが存在するか

の区別が大事。

原子論理式、複合論理式
  • 用法 1: 原子論理式 ⊆ 複合論理式 = 論理式、原子論理式 ⊥ 非原子論理式
  • 用法 1: 原子論理式 ⊥ 複合論理式、 論理式 = 原子論理式∪複合論理式
有限集合、加算集合
  • 用法 1: 有限集合 ⊆ 加算集合
  • 用法 2: 有限集合 ⊥ 加算集合、たかだか加算集合 = 有限集合∪加算集合
確率的、決定性
  • 非確率的関数 ⊆ 確率的関数 確率的関数\非確率的関数 = 真の確率的関数 = ?否非確率的確率的関数
  • 決定性関数 ⊆ 非決定性関数 非決定性関数\決定性関数 = 真の非決定性関数 = ?否決定性非決定性関数
全域、部分
特異、正則

形容詞+名詞の化学反応

形容詞を 原子=基本=単純 として使おうと思っても:

  • 原子論理式 = 基本論理式 = 単純論理式 : OK
  • 原子定理 = 基本定理 = 単純定理 : 定理という名詞の意味から、基本定理、単純定理は別な連想が働く。

同義語扱いを増やすと、区別したいときに困る。「単純プロファイル」と「リストプロファイル」とかで「単純」を使いたくなるときに、原子=単純 だと困る。

論理の用語法整理の試み 3

まだまだ改善の余地がある。

コンパクト論理に限定するとして、

  •  \mathrm{FreeKCatF}(\mathbb{F}) 論理式=生成対象の集合 F から作った自由コンパクト圏
  •  \mathrm{FreeKCatS}(\mathbb{S}) 原子証明=生成射=シーケントの集合 S から作った自由コンパクト圏

コンパクト圏〈コンパクト閉圏〉は、射の同値書き換え〈equivalent rewrite〉により2-圏となる。コンパクト2-圏がモデルとなる圏(より正確にはモデルのターゲット圏)。

日常語 → テクニカルターム

  1. 命題 → 論理式
  2. 命題 → シーケント
  3. 命題 → 定理のステートメント(論理式、シーケント)
  4. 命題 → 定理
  5. 証明 → 証明図(ストリング図)
  6. 証明 → 証拠式
  7. 証明 → 定理の保証部〈warranty〉
  8. 証明 → リーズニング図(横棒図)
  9. 推論{規則}? → 原子証明{図}?
  10. 推論{規則}? → 原子リーズニング{図}?
  11. 公理 → 原子証明{図}?
  12. 公理 → 原子証拠{式}?
  13. 公理 → 絶対原子証明{図}?
  14. 公理 → 絶対原子証明{図}?の結論命題〈余域対象〉
  15. 公理 → 保証部〈warranty〉が原子証明{図}?である定理
  16. 公理 → 定理ライブラリのインターフェイス〈指標〉の宣言

テクニカルタームの省略・短縮

  1. 証明図 ← グラフィカル形式証明
  2. 証拠式 ← テキスト形式証明
  3. 証明 ← 証明図 ← グラフィカル形式証明
  4. 証拠 ← 証拠式 ← テキスト形式証明
  5. 証拠記号 ← 原子証拠式 ← 原子テキスト形式証明
  6. リーズニング ← リーズニング図
  7. 保証 ← 定理の保証部〈warranty part〉

定理の分類基準

  1. 名前があるかないか(なくてもよい) → 名前付き、無名
  2. ステートメントは論理式かシーケントか → 論理式、シーケント
  3. 保証部は証明図かリーズニング図か → 証明定理、リーズニング定理、どこまでリーズニングを書くかが程度問題
  4. 保証部は原子的か → 公理か否か

定理が公理であるとは、リーズニング定理なら保証部が原子リーズニング図、証明定理なら保証部が原子証明図であるもの。

定理の構成素〈部位〉:

  1. 名前、なくてもよい
  2. ステートメント
  3. 保証部〈ボディ〉
  4. 所属しているライブラリ
  5. 使用しているライブラリ

ライブラリ〈パッケージ、モジュール、セオリー〉構成も重要。従来、セオリー〈クライスリ射〉とセオリーのコドメインが混同されていた気がする。

論理の用語法整理の試み 2

形式的に定義しない言葉

  • 証明 → 証拠{図 | 式}またはリーズニング{図 | 式}
  • 公理 → 原子定理
  • 命題 → 論理式、定理
  • 推論、推論規則 → 原子証拠{図 | 式}、原子リーズニング{図 | 式}

形式的に定義する言葉

  • 項、原子項
  • 論理式、原子論理式
  • 文脈
  • シーケント
  • 証拠{図 | 式}、原子証拠{図 | 式}
  • リーズニング{図 | 式}、原子リーズニング{図 | 式}
  • 論理式定理
  • シーケント定理
  • 論理式定理ライブラリ
  • シーケント定理ライブラリ
  • 論理式定理ライブラリ・インターフェイス
  • シーケント定理ライブラリ・インターフェイス
  • 定理のヘッド(名前はオプショナル)
  • 定理のステートメント
  • 定理のボディ
  • 定理/ライブラリのトランスパイル
  • 証拠{図 | 式}モナド 単位:論理式の集合 → 証拠図の集合
  • リーズニング{図 | 式}モナド 単位:シーケントの集合 → リーズニング図の集合
  • モナド変換子: 証拠図モナド → リーズニング図モナド (ゲンツェン変換子)

パターン

  • パターン変数: 原子論理式変数(ラテン文字)、論理式変数(ラテン大文字)、リスト変数(ギリシャ大文字)、証拠変数(ギリシャ小文字)
  • 論理式パターン(論理式変数)
  • シーケント・パターン(論理式変数、リスト変数)
  • 証拠{図 | 式}パターン(論理式変数、リスト変数)
  • リーズニング{図 | 式}パターン(論理式変数、リスト変数、証拠変数)
  • 論理式定理パターン(名前変数、論理式パターン、証拠パターン)
  • シーケント定理パターン(名前変数、シーケント・パターン、リーズニング図パターン)

オーバーロードか総称か

多義語・曖昧語がオーバーロードのときもあれば、総称のときもある。オーバーロードと総称の境界はハッキリしない。

  • 総称語は全体を意味するのであって、個別ケースにはあまり使われない。
  • オーバーロードされた語は個別ケースに使われるが、複数ケースで同名が使われる。

ハッキリしないね!