http://d.hatena.ne.jp/m-hiyama-memo/20120227/1330299117 から後の2011年の変更拡張： text:verify-chars追加 start.logにロギング _OPTS, _ARGV変数 dribbleファイル機能 smarty-mxの実装 https://bitbucket.org/project_caty/dev/issue/17/smarty-mx lis…

http://d.hatena.ne.jp/m-hiyama-memo/20110623/1308807276 以降で、以前のリポジトリの最後の時期； 2011年6月から8月くらい。上のほうが古くて、下がより新しい。 osモジュール json:fix-on-selection （下に記述） json:fix-on-selection に、インライン…

項空間に代数構造が入るは入るので、これを項代数と呼んでおく。項代数の演算は、項構成子（コンストラクタ）となる。項空間は余代数構造も持っていて（たいていそういうもんだ）、項の分解とか項の特性とかが余代数構造を定義する。項集合空間はもっと代数…

なんだかんだあったば、IPython（http://ipython.org/）のなかでCatyをロードできるようになった。IPythonのインターフェースでCatyを操作できるといいんだが、とりあえず次のようなことはできる。 In [69]: caty.front.console.help() Catyコンソール Usage…

デクスター・コゥゼン（Dexter Kozen）は、なんか独特の（あるいはクセのある）手法を使う。それで論文が読みにくい感じもするのだが、問題意識は今の僕にとってはピッタリだ。set constraintsとかtermset algebraとか再帰的な型を含むsubtypingとか。コゥゼ…

termグラフの圏ありき。 termツリーはtermグラフの特別なもの。 termツリーはテキスト表現を持つ。 「term=termツリー」か「term=termグラフ」かは文脈次第 termsetはtermの集合、ただしtermの普遍集合があり、その部分集合 term空間 = termset termset空間 …

項と項集合はもちろん違うのだが、コゥゼン（Kozen）の項オートマトンと項集合オートマトンとなると、区別がちょっとわかりにくくなる。項集合の全体はコゥゼン代数（termset algebla）となるが、項の全体はそれほどハッキリした代数構造は持たない。まー、…

次のコマンドラインでgithubから落とせる。 ./msysgit/bin/git clone https://github.com/mitsuhiko/werkzeug.git uWSGI用のCatyを少し変更したら、とりあえずwerkzeug上でCatyを動かすことはできた。それはそうと、'werkzeug'って何語で何て読むんだ？ http…

uWSGIの説明中に、Werkzeugってがの出てきて、何だろうと思ったので。 http://werkzeug.pocoo.org/ よくわからんがインストール。 PS C:\Users\hiyama\Work\ProjectCaty> easy_install werkzeug Searching for werkzeug Reading http://pypi.python.org/simp…

http://d.hatena.ne.jp/m-hiyama-memo/20100109/1263025526 http://d.hatena.ne.jp/m-hiyama-memo/20120210/1328853295 これらの続き。いやいやいや、コゥゼン代数やっぱり非常に便利だわ。コゥゼン代数（Kozen algebra）は僕の命名で、コゥゼン自身は terms…

次のようなtyping rulesを設けたとする。 Γ ⇒ f:: A->B Γ ⇒ g:: C->D Γ ⇒ B⊆C ------------------------[パイプ] Γ ⇒ (f | g):: A -> D Γ ⇒ x∈B Γ ⇒ f:: A-> B ------------------------[変数生成] Γ ⇒ (f > x) :: A-> B Γ ⇒ x∈B ------------------------[…

式の構成に従って型付けするが、その構成法は： パイプ |と; 配列構成 [,] オブジェクト構成 {,} タギング @ 変数生成 > 変数参照 % each each --obj 単なるeachと挙動が違う take when分岐 case分岐（難しい） cond分岐はやらない beginブロック repeat cal…

Title: Type Inference for JavaScript Author: Christopher Lyon Anderson URL: http://pubs.doc.ic.ac.uk/chrisandersonphd/chrisandersonphd.pdf pages: 186ページ これは学位論文らしい。長くて読む気がしない。 Fast and Precise Hybrid Type Inference…

http://d.hatena.ne.jp/m-hiyama-memo/20100109/1263025526 で「Σコゥゼン σ-順序代数」てのを導入したが、あれは大事だ。すごく役に立つ。公理が： [ジョイン演算の保存]f(..., x∪y, ...) = f(..., x, ...)∪f(..., y, ...) [全射性（生成性）] ∪f(1, ...,1)…

制限型（restricted type）とか部分集合型（subset type）に対して、何の制限も受けてない（絞り込み条件となる論理式がtrue）型を何と呼ぶべきか。バルク型（bulk type）ってのはどうだろう？ ワインのバルク買いとかのイメージ。

リテラルとは、具体的なデータを直接的に表現する構文の意味だろう。Prologの「リテラル」（原子論理式またはその否定）のような全然別な意味もあるが。普通の感覚だと、数値12や文字列"hello"はリテラル。最近のプログラミング言語では、タプル、リスト、マ…

集合の共通部分（intersection）、記号は∩（キャップ）。 A∩B = {x | (x∈A)∧(x∈B)} ミート（meet）と呼ぶこともある。積集合と呼ぶこともある。共通部分の定義に使う連言（論理AND)を論理積と呼ぶことがあるので、それにあわせて「積」と言いたいこともある…

まずは元祖。 イルカ http://www.youtube.com/watch?v=4IT_ZHGsQXw 伊勢正三 http://www.youtube.com/watch?v=CLuQdc7KyNE かぐや姫 http://www.youtube.com/watch?v=JBWYk6hYHws 伊勢正三＆イルカ http://www.youtube.com/watch?v=gPsc4ItkLRE 実力派。 鬼…

行列を高次元化するといっても、添字を増やしてテンソル計算するような話ではない。それは次元を増やしてない。いや、まー増やしていると言えなくもないが、0次元図形である点を配置する格子の空間の次元を増やしているだけ。行列をうまく定義しようとすると…

http://ttic.uchicago.edu/~pl/classes/CMSC336-Winter08/lectures/lec10.pdf に、次の推論規則が載っていた。 「Xは型です」を X type と書くことにして、 Δ, α type |- τ type ---------------------- Δ |- ∀α.τ Δ, α type; Γ |- e : τ ------------------…

最近考えている手順： スクリプトから有向グラフを作る。あるいは最初から有向グラフが与えられる。 すべてのワイヤー（有向辺＝パイプ）に型注釈を付ける。このとき型付け規則（typing rules）を使う。 限量子で束縛されていた型変数を名前を変えて自由変数…

非対称グラフ単一化って、オートマトンの模倣構成問題だったのだ。メモリを気にしなければ、ノード間の対応（模倣辺）を全部覚えておいて、ダイクストラ法を使えばいい。メモリを使わないように、覚えておかなくていい（後で使わない）記録を削除しようとす…

ここ何ヶ月か（ひょっとして何年？）悩んでいる問題がある。うまくいけば解決するかもしれない。細部の定式化はいくらでもバリエーションがあるのだけど、次のような事実がある。 プログラムの型安全性と集合の連立不等式系の可解性が同値となる。 集合の包…

Aを型項、αを型変数として、多相型を ∀α.A と表すのは定着した習慣になっている。∀をfor allなりfor anyと読み下すとそれなりに意味が通るので、まーいいかと思っていたが、論理の全称記号（全称限量子）が一緒に出てくる文脈だと混乱する。それと、論理の全…

pass<T> :: T -> T; length<T> :: list<T> -> number(minimum=0); dup<T> [integer(minimum=0) n] :: T -> list<T>; //同じデータをn個並べたリスト first<T> :: [T, _*] -> T; //リストの先頭 rest<_T*> :: [_, _T*] -> [_T*] leaves<T> :: tree<T> -> [T*]; //ツリーの末端を集めてリス</t></t></_t*></t></t></t></t></t></t>…