2016-09-01から1ヶ月間の記事一覧
モナドの法則（公理）の記述 クライスリ結合の定義と法則の証明 アイレンベルク／ムーア代数の法則（公理）の記述 随伴の定義の記述 随伴からモナド、コモドが誘導されることの証明 随伴からメイト同型が誘導されることの証明 ベックの分配法則から複合モナ…
A : one two, three, ... D : double, quadruple, octuple, ... Aは、ささやかな一律単利 Dは、エグい複利 出てくる圏 Set（またはFinSet） PtSet Aのクライスリ圏でありアイレンベルクムーア圏 極性付き対合付き集合の圏＝不動点のない対合付き集合＝コベク…
悪い記号法／用語法／図示法で悪いメンタルモデルが作られている。それを矯正する。 随伴に慣れる。 良い記法は図式順だが、反図式順も認める。The Book方式はダメ。 演算 The Book 反図式順 図式順 射の適用 f(x) fx x;f 射の結合 gf gf f;g 関手の適用 F(X…
ケーニヒスベルクの橋の問題は、だいたいポアンカレ双対。
1 + 1 AddOne(x) = x + 1 (or Augment(ation)) Double(x) = x + x A(X) = X + 1 D(X) = X + X そして、 A上にモナドを作れる D上にモナドを作れる Aを随伴対で表現できる Dを随伴対で表現できる AとDはベック分配可能である。AD上にモナドを作れる。 Aのクラ…
型クラスのパラメータ問題（トラブルっぽい話）が出てくるのは、指標とモデルの相対性の考察が不足しているせいだと思う。グロタンディーク平坦化を“積分”とみなしてのフビニに定理だと思う。繰り返し積分と同時多重積分の同値性。直積領域の積分ではなくて…
MLのモジュールシステムは禁欲的で、必要最小限の機能だけだが、スッキリしていて好きだ。だが： signatureにパラメータを付けられない。functorは当然にパラメータ（引数）を持つが、functorの値はstructureであってsignatureを値には取れない。 これは当然…
グラフとツリーと余反映的部分圏 - 檜山正幸のキマイラ飼育記 上記の例は、基点付き弧状連結空間の被覆空間の類似物だ。空間Xに被覆空間と射影 C(X)→X が定まる。射影が余反映的構造を決める。距離空間と完備距離空間と距離完備化は反映的部分圏の例になる。…
http://arxiv.org/pdf/0904.3848.pdf の3ページ目にconsolidationの定義が書いてある。 A consolidation for C is a function p: Co×Co → C, p(e, f) = pe,f, where pe,f is an arrow from f to e and pe,e = e.
昨日の 型クラスの比較 - 檜山正幸のキマイラ飼育記 メモ編 への補足説明。既存のものに後からゴチャゴチャ文句を言うのは簡単だ。だから文句言う。コアージョン（coercion - 檜山正幸のキマイラ飼育記 メモ編）は必要悪という意味で必須だから、使うのはい…
公理をひとつも持たないセオリーをダムセオリーと呼ぼう。日本語ではアホ理論。
忠実関手 F:C→D がある事と、C⊆D とみなせる事は違う。事例を示す。集合圏Setの対象（つまり集合）のなかから、基数が可算無限であるモノを全て選び出して類Ωを作る。Ω⊆|Set| であるので、Ωを対象類とするSetの充満部分圏が一意に決まる。その圏をω-Setとす…
Standard MLが圧倒的に良くできているな。オーバーロードを意図してない、型システムじゃない、という問題点はあるが、許せる、許せる。Haskellは「悪いお薬」をキメている。当座はとても元気が出るが、いずれは心身を蝕むアレ。型名に対するコアージョンを…
Scalaの書き方がけっこう良い。 trait Functor[F[_]] { def map[A,B](fa: F[A])(f: A => B) : F[B] }
Haskellと比べて、 class Functor f where fmap :: (a -> b) -> f a -> f b F[_] と書くので、fが型構成子だと明白にわかる。 ブラケットに型（や型構成子）パラメータを入れるので、総称性がハッキリ。 Haskell型変数 a, b は、いつのまにか勝手に入ってい…
関数型プログラミングとオブジェクト指向について、何か書く、かも - 檜山正幸のキマイラ飼育記 関連で少し調べてみたら、ウワーッ、随分とひどいことになってるんだな。 型述語解釈 http://www4.in.tum.de/~wenzelm/papers/constructive_classes.pdf : axio…
型クラスの意味論がイイカゲンなわけだが、それはそうとして、型クラスの現実的に厳しい問題は： 型システムとモジュールシステムの役割分担、相互関係 名前の管理 特に名前の管理が滅茶苦茶に大変なのだが、あまり指摘されない。裸の名前・記号をどう解釈し…
Title: Categorical Programming for Data Types with Restricted Parametricity Authors: Dominic Orchard and Alan Mycroft URL: https://www.doc.ic.ac.uk/~dorchard/drafts/tfp-structures-orchard12.pdf 誤解しているとしか思えない。型クラスのスーパ…
Nimに統一呼び出し構文というのがある。 http://nim-lang.org/docs/manual.html#procedures-method-call-syntax Eiffelでも、プロパティとメソッドをまとめてフィーチャと呼んでいて、プロパティと引数なしメソッドの区別はなかったと思う。
公理付きか公理なしか： 公理付きならセオリー、なしなら指標。 パラメータが1つか複数か： 単パラメータ型クラス（単一の型パラメータを持つ型クラス）と複パラメータ型クラス（複数の型パラメータを持つ型クラス） パラメータを使うかレコードフィールドを…
http://blog.goo.ne.jp/ktonegaw/e/0f47de5854daf4eb38339a73791544a8 にあった。
英辞郎から：consolidation 【名】 〔会社などの〕統合、合同 〔複数のものの〕統合［合同］体 強化、安定化、強固になること 《地学》石化（作用）◆【同】lithification 《地学》〔粘土地盤の〕圧密 《心理学》〔記憶の〕固定（化） 《金融》保ち合い 適当…
古いJava > which java C:\ProgramData\Oracle\Java\javapath\java.exe > java -version java version "1.8.0_31" Java(TM) SE Runtime Environment (build 1.8.0_31-b13) Java HotSpot(TM) Client VM (build 25.31-b07, mixed mode) jdk-8u101-windows-x64.…
カタカナ書きが難しい。コアージョンかコエージョンあたりかな。あるいは、強制、型強制で通すか。
a, b ：グラフの辺 a, b ：アルファベットのレター b : 振る舞い d ： 識別頂点 e ： 分離対象の分離射（予定） f, g, h ： 指標圏の射 i ： 始状態指定 i ： 添字 k ： コンストラクタ射、コンストラクタ-コマンド射 k ： 体 n, m ： 整数 p ： 余分離対象…
一般関手モデル：どこを一般化？ - 檜山正幸のキマイラ飼育記 一般関手モデル：インスティチューションとの関係 - 檜山正幸のキマイラ飼育記 一般関手モデル：「圏の表示」の圏 - 檜山正幸のキマイラ飼育記 一般関手モデル：相対スキーマと相対インスタンス …
とりあえず表。説明はその下。 関手オートマトン 可達性 可識性 圏論 相対分離性 相対余分離性 部分圏 余反映的部分圏 反映的部分圏 エルブラン構成 単純エルブラン構成 二重双対エルブラン構成 分離性は圏に分離対象（separator）または分離対象族（family …
新しい順： 豊饒プロ関手は豊饒な世界を提供するのか - 檜山正幸のキマイラ飼育記 s-完備可換半環上の非可換半代数上の加群の圏に関する随伴性とその応用 - 檜山正幸のキマイラ飼育記 関手オートマトンを説明する記号法に大いに悩む - 檜山正幸のキマイラ飼…
