(menu-bar-mode 0) (tool-bar-mode 0)値 0, -1, 1を試してみよう。

"Simple EL = Simplel" は、実用性を損なわない範囲内で、できるだけ単純にした式言語である。テンプレート内での使用を想定しているが他の目的でも使えるだろう。JavaScript, JSONの構文の影響を受けている。悩んでいる点参照を表す目印に'$'を使うべきか？…

最近もっぱら実務家（って何だ？）の僕。ついカッとなって（って何だ？）、古本屋で大槻さんの QUANTUM INVARIANTS を衝動買い。しかしこれは、僕の嫌いなハードカバー。もう既に背表紙から紙がはがれかかっている。なんかすぐにバラバラになりそう、、、ト…

最近、メモ編は全然書いてないな。なにしろ、HTMLだのMakefileだの書いているからな、ダハハハハハ。Catがデカルト閉圏であることは周知のことだが、自分で確認してみた。が、これをキーボードで記述するのはエライ大変！ 紙に描いた絵をスキャンして貼り付…

なんでこんなにだるいんだ？それはともかく： 自然演繹 ラムダ計算 デカルト閉圏 ∧導入 タプリング 直積 ∧消去 射影 射影 ⊃導入 ラムダ抽象 Λと指数 ⊃消去 適用 eval T（真） ユニット型 終対象

本日は朝から疲れている。それはそれとして、半完成品＝未完成品のようなもの： テキストのテンプレート 抽象クラス ジェネリックス（パラメータ） DI ビヘイビア（Erlang用語） 一般的フレームワーク

トレースを TrA,BX:C(A×X, B×X)→C(A, B)と書くことにして、Xを固定して、A, Bを動かす。すると、Trが、C(-×X, -×X)⇒C(-, -):Cop×C→Setという自然変換になっている。この事実を書き下すと、両側タイトニング公式となる。同じようにラムダ抽象 ΛA,BX:C(A×X, B)…

本編「デカルト閉圏における絵算 詳細編」に対する等式的計算。 ○○○ = (ba×outa);eval;inb△△△ = Λa'[○○○] = Λa'[(ba×outa);eval;inb]とする。 (Λa'[(ba×outa);eval;inb]×a);[(b'a'×ina);eval;outb] = // Step1 △△△の導入と括弧の付け替え (△△△×a);(b'a'×ina)…

本編「テンソル：なぜ難しいのか」とかでも書いたけど、ベクトル解析／テンソル解析って不満だよなー。実に不満。熱伝導のフラストレーションも、ベクトル解析／テンソル解析のフラストレーションなんだろう。ちょっと再定式化してみようか。って「ちょっと…

昨日： 光、音、熱とかの本を持っているかな、と思ったら、ないな。フーリエ解析とか関係するだろうが、それもないし。 探したら一冊出てきた。 小出昭一郎『物理現象のフーリエ解析』 -- 存在さえ忘れていたけど、なかなか良さそうな本です。で、熱伝導のと…

ちょっと考えてわかったこと： フロイド／ウォーシャル法は半環係数で考えても非常に一般的な方法だ。境界付きグラフ（リグラフ）の始境界であたえられた初期値が無限の未来に終境界にどのような影響を与えるかを計算する。ダイクストラのアルゴリズムは、始…

とかの本を持っているかな、と思ったら、ないな。フーリエ解析とか関係するだろうが、それもないし。古典的で露骨な計算がたくさん出てくる物理数学の本があればいいのかな。最近みかけないなー。

有本さんの本は、深谷さんとの対談だけ読んでほっておいたが、すごく面白いことが書いてある。第2章「最適化とアルゴリズム」の最初を読んで「ホエーッ」と感心。しばらく、このあたり（以下に書く）を調べて考えてもいいと思った。光の粒子性と波動性という…

スライド -- http://www.cs.chalmers.se/~peterd/slides/Uppsala.ps 論文 -- http://www.site.uottawa.ca/~phil/papers/paper_final.pub.ps

混乱を招くこともあるが、Haskellのセクション記法が便利なこと気付いた。 (△b) = λx.(x△b) (a△) = λx.(a△x) 特に、関数結合;に対して使うと： (;f)(u) = u;f 後結合＝前送り (f;)(u) = f;u 前結合＝引き戻し

Title: A CONCRETE INTRODUCTION TO CATEGORIES Author: WILLIAM R. SCHMITT URL: http://home.gwu.edu/~wschmitt/papers/cat.pdf 60ページ タイトル通りに具体的。随伴の紹介がゴール。

まず、Goguen（とTracz）の論文 "An Implementation-Oriented Semantics for Module Composition" (1997) →http://citeseer.ist.psu.edu/539931.html Implementation-Orientedという題名から、現場的かと思ったが、今見たらそうでもない、相当な予備知識が必…

大局的プログラミング（programming in the large）もプログラミングなのだから、当然にプログラミング言語が必要である。が、通常のプログラミング言語に大局的プログラミングが統合された言語は存在しない。仕様記述言語は、GoguenのOBJファミリーをはじめ…

大局的プログラミング（programming in the large）は必要か？ この問は、設計（デザイン）やアーキテクチャが必要か？ という問と同じだから、答はYESに決まっている。とはいえ、大局的プログラミングの定義や捉え方は人によりかなり異なる。僕自身は、設計…

なんらかの、プログラミングに有用な概念なり発想は、 言語機能として取り入れられるのが最善、 ライブラリ／開発ツールでサポートするのが次善、 手法、規約で実践するのは、それしかできないとき。 さて、大局的プログラミング（programming in the large…

本編「レコードの型階層を合理的に説明できるか」の設定でインスティチューションを作ってみる。用語や記号は本編記事に従う。指標圏フィールド名として許されるすべての名前の集合をName（無限集合と仮定）とする。Nameの有限部分集合を指標と呼ぶ。例えば…

余完備性をKleisli圏に持ち上げたい open programs open programs 再び 2005年の夏、えー、こんな昔からTermモナドがプログラムだって知っていたの、僕？ Cospan構成にも言及しているし。以上をふまえて書いた記事： ソースコードの形式化 これ↑で、「コンポ…

protecting 演算（記号）も法則（等式）も追加できない。 extending 演算は追加できるが法則は追加できない。 using 自由

プレ圏（グラフ上に部分的な圏構造）の圏をPrecatとする。さらに、プレ圏に同値関係（一般化合同）が与えられたものを(P, E)として、その全体をEPrecatとする。EPrecatは有限余完備だと期待している。EPrecatが有限余完備ならその上の余スパンの圏が作れる。…

パラメータ付き指標／セオリー（仕様モジュール）とCafeOBJのprotected importって同じような気がする。インポートって余スパンで説明されるような。

どう違う？ 同じような気もするが。

だって。 Title: Observational Truth as a Categorical Modality (2002) Author: Grant Malcolm URL: http://citeseer.ist.psu.edu/573401.html 11ページ

ゴグエン／マルコルム／ケンプ（Joseph Goguen, Grant Malcolm, Tom Kemp）の"A Hidden Herbrand Theorem"(1998)とビドォイト／ヘンニッカー／カーツ（Bidoit/Hennicker/Kurz）の"On Observability and Reachability "を読み比べてみた。 Observational Logi…

普通、指標はグラフとみなせる。グラフや圏の用語と記法を拝借しよう。指標Σに対して、ソートsからソートtへの演算記号の全体をΣ(s, t)と書く。Σ(s, t)は集合。ただし、(s, t)≠(s', t')でもΣ(s, t)∩Σ(s', t') = 空 は仮定しない（オーバーロード許可）。Σ(s,…

エルブラン定理関係で、結局一番短い、 Title: A Hidden Herbrand Theorem (1998) Authors: Joseph Goguen, Grant Malcolm, Tom Kemp URL: http://citeseer.ist.psu.edu/293075.html 18ページ これにした。まず、隠蔽ソートって用語はよくないと思った。これ…