このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」(http://d.hatena.ne.jp/m-hiyama-memo/)のデータを移行・保存したものであり、今後(2019年1月以降)更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

多圏

Catyのコマンドと変数

http://d.hatena.ne.jp/m-hiyama-memo/20120104/1325638861 : いずれ説明する。 今日説明する。絵に基づいて説明する。 原寸大これがコマンドなわけだが: command body とはPythonコード、またはCatyScriptコードで、コマンドの本体となる定義体(definitio…

スパイダーグラフ:絵は大ざっぱに描くべし

ハブエントリー: スパイダーグラフ (1) 絵がテキストより分かりやすいのは、ノード/ワイヤー数が少ない場合で、ノード/ワイヤーが増えると結局はナンダカワカラナイ。ノード/ワイヤー数を減らすには、絵で表現する情報を絞り込んで余分なことは描かない…

スパイダーグラフ:チャンネルと描画

ハブエントリー: スパイダーグラフ (1) チャンネル(ワイヤーのロール)と図示法。「描画するか」の△は、「設定によっては描画する」こと。 チャンネル in/out 描画するか 色(暫定) 矢印(暫定) 備考 param in △ - inv env in × - - stdin in ○ - normal var…

スパイダーグラフ 補足

いくつか補足しておく。ハブエントリー: スパイダーグラフ (1) 以下の図のインバウンドポートの形状が間違っている。矢印の方向はこれでいいが、白丸が内部に入る。では、白丸はなぜ内部に描くのか? エリアがルートエリアのときは外部を描きようが無いので…

スパイダーグラフ (2)

スパイダーグラフ (1) の続き。スパイダー射の意味論スパイダー射は、f: A → B1, B2, ... Bn という、余域側に複数の型を並べていいプロファイルを持つ。複数の出力チャンネルを持つわけだ。複数の出力の一番お馴染みの例は、標準出力(stdout)と例外(exce…

スパイダーグラフ (1)

スパイダーグラフ (2) スパイダーグラフ 補足 スパイダーグラフ:チャンネルと描画 スパイダーグラフ:絵は大ざっぱに描くべし スパイダーグラフの起原と用途いつ頃からか、直観主義論理の“ある種の双対”となる論理のシーケント計算をスパイダー計算と呼ぶこ…

スパイダー亜圏

亜圏(categoroid)って言葉はやっぱり圏もどきという意味。トレース付き圏とそこから作ったコンパクト閉圏を一緒に計算する計算デバイスとしてスパイダー亜圏ってのを考えることにした。ネーミングはどうにもアレだが、いい名前が思い浮かばない。スパイダ…

多圏からの厳密結合圏

もうセミナーネタとは言いがたいが:モノイド閉圏Cから作ったハロ多圏のなかでは、いくつかの結合が考えられる。 右マッチ結合:多対象の列を右から順に比較して一致する部分を結合する。 左マッチ結合:多対象の列を左から順に比較して一致する部分を結合す…

ハロ多圏、ハロ複圏はモナドなのか?

モノイド圏Cから、適当な方法でハロ多圏やハロ複圏を作れる。どんな多圏/複圏を作るかは用途によりけり。この構成は、モノイド圏のレルムから(なんか適当な性質を持った)多圏/複圏のレルムへの関手になっている。さらに、多圏/複圏のレルム内では生成関…

polycategoryの創始者はザボ

Multicategory の拡張として polycategory というものもある。 M. Szabo が [Sza75] で導入した。

タブリング=パッカー=待ち合わせ同期

タプリングの意味を並列計算やデータフロー計算で考えてみると、2つ以上のデータをパックして1つのデータ(かたまり)にすることだが、これはまた、すべての成分データが揃うまで待つので、データ同期を表していることになる。コア圏とハロ多圏のモデルを使…

ハロ多圏とコア圏

結局、ハロ多圏の多射が項であって、コア圏の射が値だな。多射は図形だが、それは構文的な存在でもあり、項書き換えの対象となる。つまり、書き換え操作が計算であり2-多射でもある。計算の結果を対応さると、式と計算の意味論ができて、多圏のほうには、2-…

モノイド従順多圏、コア圏、計算

Oが基本対象の集合として、Pは、O*にdom/codを持つ多射からなる多圏とする。多射の合成は2種類あり、f: Γ ⇒ Δ,Δ' と g:Δ',Ψ ⇒ Φ に対する f[;Δ']g と、 f:Γ ⇒ Δ',Δ と g:Ψ,Δ' ⇒ Φ に対する f[Δ';]g の2種。適当な公理は満たす。それとは別に、並置によるモノ…

コンパクトシーケントと従順多圏とモノイド圏

まず、コンパクトシーケントとは、コンパクト論理のシーケントで、左辺と右辺のカンマの解釈が同じもの。古典論理のシーケントとは違う。次のような規則を使う。 Γ ⇒ Δ,Δ' Δ',Ψ ⇒ Φ ----------------------------[右Cut] Γ,Ψ ⇒ Δ,Φ Γ ⇒ Δ',Δ Ψ,Δ' ⇒ Φ ------…

コスロウスキーの多圏論文

他でメモった気がするが: Title: A MONADIC APPROACH TO POLYCATEGORIES Author: JURGEN KOSLOWSKI URL: http://www.tac.mta.ca/tac/volumes/14/7/14-07.pdf Title: Morphisms And Modules For Poly-Bicategories (2003) Authors: J. R. B. Cockett, J. Kos…

多圏に関する最近の文献

"Polycategories via pseudo-distributive laws" by Richard Garner (http://arxiv.org/abs/math.CT/0606735)44ページ "MORPHISMS AND MODULES FOR POLY-BICATEGORIES" J.R.B. COCKETT, J. KOSLOWSKI, AND R.A.G. SEELY (http://www.emis.ams.org/journal…

レコード形式指標に対するセオリーとシーケント

名前ベースの多圏を考える。多圏の多対象は、レコード{a1:A1, ..., an:An} だが、A1, ..., Anはプログラムのインターフェース(指標)(の名前)だとする。レコード=多対象に対して、a1, ..., anでプリフィックスされた演算記号を寄せ集めた指標 a1.A1 + ..…

証明、項、射

トレース付きモノイド圏Cに意味を持つような形式的体系の項を考えると、その項はシーケント計算の証明に対応する。証明図の木構造がちょうど項の木構造に対応する。よって、項の変形は証明図の変形になっている。さらに、項の値(意味)は圏Cの射だから、証…

順序ベース多圏と名前ベース多圏、シーケント計算

最近、少しだけ多圏の使い方に慣れてきた。多圏はけっこうバリエーションがある。まず、カットの自由度から、シングルカット多圏とマルチカット多圏がある。シングルカットはワイヤー1本に関してカットする。マルチカットは束(たば;リボン)でカットできる…