オプティックに関する文書を読んでいると、ラテン文字を丸で囲んだ記号が登場するんですよね。まず、MathJaxでどうやって書いたらいいのだろう？ enclose というMathJax拡張があるので、それを使ってみます。次のようにマクロ〈ユーザー作成コマンド〉を定義…
「依存型とΣ-Δ-Π随伴、そしてカン拡張」の冒頭にて： 「依存積型」と「依存和型」に関しては、もうサンザンだよー、あったく...[snip]...ふんとに「依存ナントカ型」って紛らわしいよねぇ。それで、「依存ナントカ型」と言うのはやめます。...[snip]...今後…
型クラスの多重継承やオーバーロード解決機能を考えるにあたって、「忘却グラフに追憶スパンをアタッチする」という定式化がいいような気がします。それを説明します。この記事は“とりあえず・取り急ぎ”書いたもので、自己完結的な解説にはなっていません。…
最近、プライベートに という記法を使っていて具合がいいので、これについて説明します。内容： 圏＝n-圏 n-離散圏と圏の離散化 圏の切り捨て 圏の次元調整 次元調整記法の使い方事例 次元を上げる例 次元を下げる例 高次元部分が不明な例 圏＝n-圏単に「圏…
米田テンソル計算の内容について書こうと思ったら、けっこう色々準備が必要みたい。「圏論からの準備」というより、もっとツマラナイこと、しかし無視できないことに関する細々とした準備です。記述や計算のためのツマラナイ道具（いや、ツマラナクないが）…
ストリング図とテンソル計算に関して僕が言えること、言いたいことは「やってみてください」です。ある意味“機械的な作業”なので、やれば出来ます。ボブ・クック教授に言わせれば「幼稚園児でも出来る」（「幼稚園児のための量子力学とその周辺」参照）。も…
今回は、僕の雑感のようなものです。若干茫漠とした短い話ですが、抽象的オプティックの世界を俯瞰してみます。内容： オプティックとは何か？ オプティックの世界 最初の記事＋シリーズ目次 オプティックとは何か？オプティックは、ソフトウェアの理論・技…
マリオ・ロマン〈Mario Román〉の論文に触発されて、コエンド計算を古典テンソル計算風にアレンジできるんじゃないかと思い始めました。今まで折に触れて考えたり使ったりしてきた絵算の技法と米田ご利益ツールズを動員すれば、割と気持ちいい計算体系が作れ…
レンズ／オプティックを記述する道具としてテレオロジー圏が便利そうです。紹介しておきます。内容： 参考文献 アクテゴリー〈加群圏〉 テレオロジー圏とストリング図 テレオロジー圏の定義 最初の記事＋シリーズ目次 参考文献テレオロジー圏〈teleological …
レンズ／オプティックについて次の記事を書きました。 圏論的レンズ 最初の一歩： ストリング図を中心に 圏論的レンズ 2： 具象オプティック 圏論的レンズ 訂正と補足： 具象レンズ＝具象オプティック これらの記事を（読むのではなく）眺めてもらえれば分か…
「圏論的レンズ 2： 具象オプティック」において、次のように書きました。 具象オプティックを定義すると、具象レンズは特殊な具象オプティックとみなせます。「圏論的レンズ 最初の一歩： ストリング図を中心に」において、具象レンズの圏 の形式的定義は省…
「圏論的レンズ 最初の一歩： ストリング図を中心に」において、元祖レンズと具象レンズを紹介しました。元祖レンズを少し一般化すると具象レンズになるのでした。この記事では、具象レンズをさらに少し一般化して具象オプティックを導入します。[追記]この…
プログラミングにおいて、レンズ〈lens〉と呼ばれる構造が使われる機会が増えているようです。古典的なレンズが幾つかの方向に一般化されていて、「レンズってなに？」と聞かれても答えにくい状況になっています。一番簡単な（と僕が思っている）ストレージ…
テキストの計算をほとんどしない（「ほとんどできない」とも言う）檜山が、絵算〈ストリング図計算〉のコツと小技を書いてみますよ。似た趣旨の過去記事に次があります。 絵算をはじめた人への注意 ストリング図の基本概念と描き方 今回の記事は、一般的入門…
計算や証明で場合分けをすることがあります。場合分けされた命題があったとき、それぞれのケースとなる命題達を論理ORして解釈すべきか？ それとも論理ANDして解釈すべきか？ どっちでしょう。「場合分けなんだから、そりゃ論理ORでしょ」と答える人が多そう…
