プログラミング言語をひとつ与えることは、結局は指標を与えることと同じで、問題は指標から自由圏を作る一種の閉包演算<->のほうだな。どのような種類の自由圏（エルブラン圏、項集合）を与えるかがプログラミング言語構文の特徴付けになる。閉包演算<->は…

指標圏に境界概念とグルーイングを導入して、コボルディズム的な二重圏だと考える。インスティチューションをこの二重圏の上で定義する。すると、Mod、Sen、Spec、Theo（Sen上に作る順序集合）なども拡張されるだろう。さらに、証明系ProofやプログラムProg…

有向グラフとしての指標Σと部分有向グラフΦ、Ψを一緒にした(Σ, Φ, Ψ)を射とするコボルディズム圏を考えることができる。このコボルディズムでは次元概念は役割を演じない。圏Cに対してΣ代数圏 C-AlgΣは、関手圏C<Σ>として定義する。コボルディズム指標(Σ, Φ,…

もう少し考えよう。有向グラフとしての指標Σ（有限に限らない！）、部分有向グラフΦ、Ψを一緒に考える。|Φ| = B を基本(basic)ソート、|Ψ| = D を公開定義（public defined）ソートと呼ぶ。別な部分グラフΔ⊆Σがあるとして、Δの辺はコンストラクタ演算記号と…

指標は単なる有向グラフと考えてよい（そう考えるべき！）。境界付きグラフがあるんだから境界付き指標があってもいい。BHKのconstructor-based指標Σを考える。ソートにはlooseとconstrainedがあるが、これをbasicとdefinedと呼び替える。basicソートとbasic…

Bidoit/Hennicker/Kurzはさすがに書くのに長すぎるからBHKと略記する。

ゴグエン（Goguen）達がエルブラン定理について書いているのだが： Title: A Hidden Herbrand Theorem (1998) Authors: Joseph Goguen, Grant Malcolm, Tom Kemp URL: http://citeseer.ist.psu.edu/293075.html 18ページ Title: A Hidden Herbrand Theorem: …

ビドォイト／ヘンニッカー／カーツ（Bidoit/Hennicker/Kurz）に従うとして、指標Σが観測的なら、余代数を定義する関手 Θ:SetS→SetSが定義される。指標Σが構成的（constructor-based）なら代数を定義する関手Ω:SetS→SetSも定義される。それに項関手TermΣ:SetS…

Title: Duality for Some Categories of Coalgebras (2001) Author: Robert Goldblatt URL: http://citeseer.ist.psu.edu/482873.html 20ページ、印刷したような気もするが忘れた Title: What is the Coalgebraic Analogue of Birkhoff's Variety Theorem? (…

ビドォイト／ヘンニッカー／カーツ（Bidoit/Hennicker/Kurz）双対性を調べてみたい理由は、これがXMLにモロに適用できそうだから。XMLを順序付き多ソート代数とそのモデルで定式化することは以前から考えていることだが、構文定義文法とオブジェクト指向風AP…

ビドォイト／ヘンニッカー／カーツ（Bidoit/Hennicker/Kurz）双対性に関して： Title: On the Duality between Observability and Reachability (2001) Authors: M. Bidoit, R. Hennicker, A. Kurz URL: http://citeseer.ist.psu.edu/bidoit01duality.html 2…

待てよ、前のエントリーと同じこと、スペクトルとモデルの関係について以前書いたのだった。 「コンパクト空間と論理／モデル論」 「仕様技術への道 -- インスティチューションを縮めてみる」 ある形式系が採用している論理が古典論理なら、そのリンデンバウ…

Sをソート集合、Vを変数記号の集合で、V→Sでソート付き変数が定義されているとする。ρ:S→|C|がSの圏Cでの解釈として、ρによりVを圏Cに上江州アタッチできる。これを詳しく記述。 終状態セットが複数あるオートマトン。

指標を単なる有向グラフと考えるのはとてもいいとわかってきた。等式的セオリーまず、等式的セオリーとグラフのあいだには次の関係がある。 指標 圏の生成グラフ ソート 対象の生成集合 関数記号 射の生成集合 項形成規則 自由構成 項 射 等式系 グラフの（…

本編のコレだけど、部分関数／部分演算を等式的一階述語論理でどう扱うかの例題として面白いかもしれない。次のような体系も考えるといいかも。 domu（id(dom(-))に対応）とcoduを持つ体系 「…が存在する」を意味する述語E(-)を持つ体系

「セオリーと証明の圏」とか「圏論的形式言語理論の問題」とかに謎なことが書いてある。今読むと分からん！ 解釈し直さないと。命題論理の場合のリンデンバウム（Lindenbaum）代数はハッキリしている。ブール代数（束）とかハイティング代数（束）だ。この場…

本編で、"What is a logic, and what is a proof?" (April 8, 2005) by Lutz Strassburger（http://citeseer.ist.psu.edu/723320.html）を紹介したことがある（けっこう良く書けている）のだけど、（ほぼ）同じ題名の論文： Title: What is a Logic? Authors…

すごくラフに書くけど、後でチャント書くべし（TODO）。古典的なΣ代数の圏、ローヴェル（Lawvere）の代数セオリー、Monoid(C) = CΔという事実などの拡張を論じる。Σを指標（単に何の制限もない有向グラフと見る！）として、グラフΣから自由生成された圏FreeC…

google:"generalized congruence" category functor で探してみると： Title: GENERALIZED CONGRUENCES. EPIMORPHISMS IN Cat Authors: MAREK A. BEDNARCZYK, ANDRZEJ M. BORZYSZKOWSKI, WIESLAW PAWLOWSKI URL: http://www.tac.mta.ca/tac/volumes/1999/n11…

小ネタ。左自律圏のM×M*（または、右自律圏の*M×M）にはモノイド構造が入る。乗法と単位は次で与える。

ブレイド関係式は「アルチン（Artin）の関係式」と呼んでいいと思う。間違いのはずはない。それに対応する対称（置換）の関係式も僕はアルチンの関係式と呼んでいたが、誰だか別の人の名前が付いていた。どこかで見た、比較的最近見た。が、思い出せない。誰…

Gがグラフで、aがその頂点。aから出る辺で隣接している頂点集合をNo(a)として、aのout近傍頂点集合と呼ぶ。{a}∪No(a)の誘導部分グラフを、aのout近傍（グラフ）と呼ぶ。aのin近傍Ni(a)も同様に定義できる。f:G→Hがグラフの準同型として、aはGの頂点。このと…

pre-automatonとは、始状態も終状態も持たない(Σ, S, δ)のことらしい。これはラベル付き遷移系と同じだと思う。 "Monadic SecondOrder Logic, Graphs and Unfoldings of Transition Systems"から： Let n, m ∈N and m ≧ 1. A transition system of type (n, …

エルブラン・モデルから考えた圏の始類（initial class）、または図形的な印象からは始面（initial facet）。 単純対象と半単純圏 圏合同とエルブラン／リンデンバウム構成

伝統的エルブラン理論を定義し直したいのだけど、とりあえず伝統的エルブラン理論の概念・用語をまとめておく。構文は、変数、定数、関数、述語（記号達）で構成する。関数と述語を最初から明白に区別するのが特徴。変数、定数、関数で項を作り、それと述語…

Title: Homology of Higher Dimensional Automata (1992) Authors: Eric Goubault, Thomas P. Jensen URL: http://citeseer.ist.psu.edu/goubault92homology.html ザッと読んだ。だいぶ古いので、その後の発展があるんだが、それにしてもイマイチな感じ。 ホ…

ノードや辺にラベルがない穴（プレイスホルダ）付きツリー（空ツリーは考えないほうが楽）を0個以上並べた列を考える。これはヘッジ。長さがmで穴が（正確にそのまま勘定して）n個あるヘッジの全体をH(n, m)とすると、これは対象類N上の圏となる。さらに、モ…

圏Cと指標Σに対して、ΣからC係数で自由生成した圏C[Σ]がとても使えそうな気がしている。が、現状、おぼろげな定義以外に何もわからない。まず、Σ=(Σ0, Σ1)という集合の組を考える。記号の濫用で、Σ1を単にΣと書き、Σ0のほうは|Σ|と書くことにする。Σ、|Σ|が…

なんか、いろんな立場からいろんな定義があるな。これから定義を収集して、まとめよう。

Title: S_4-symmetry of 6j-symbols and Frobenius-Schur indicators in rigid monoidal C^*-categories Authors: J. Fuchs, A.Ch. Ganchev, K. Szlachanyi, P. Vecsernyes http://arxiv.org/abs/physics/9803038 全部で37ページだが、本文は21ページ。残り…