かつて、次のURLsで書いた短い記事群をまとめてみた。文章はそのまま。 HoareRules 記述構文 - 檜山正幸のキマイラ飼育記 (はてなBlog) HoareRulesのラベル - 檜山正幸のキマイラ飼育記 (はてなBlog) HoareRulesの関数構文、その意味的区別 - 檜山正幸のキマ…

「プログラマの常識」ってなによ？ - 檜山正幸のキマイラ飼育記 (はてなBlog) 「常識」というよりは「理解の基盤」と「説明の方法」 - 檜山正幸のキマイラ飼育記 (はてなBlog)

他の構文との整合性がなくなってきたとかの理由で、スキーマ構文を変更の予定。将来的には型関数（型変数を持つ型構築子、総称型）も認める方針として、現状では型演算子を多用することにする。構文構成素 型定数：意味が定まった型の名前。string, null, an…

かつて、次のURLsで書いた短い記事群をまとめてみた。文章はそのまま。 もっと仕様の話(1)：かたいことばっかり言ってると… - 檜山正幸のキマイラ飼育記 (はてなBlog) もっと仕様の話(2)：インクリメント仕様をどう書くの - 檜山正幸のキマイラ飼育記 (はて…

かつて、次のURLsで書いた短い記事群をまとめてみた。文章はそのまま。 論理（学）と仕様 - 檜山正幸のキマイラ飼育記 (はてなBlog) 仕様の話(1)：いつもはじまりはホーア式 - 檜山正幸のキマイラ飼育記 (はてなBlog) 仕様の話(2)：呼び出しからメッセージへ…

上が新しい。 概括的な理解と細部への拘り - 檜山正幸のキマイラ飼育記 (はてなBlog) ペラペラの表層、シッカリした内実 - 檜山正幸のキマイラ飼育記 (はてなBlog) なかなか分からない、という能力 - 檜山正幸のキマイラ飼育記 (はてなBlog)

エルゴット繰り返しとコンウェイ不動点の関係をもっとちゃんと理解しないと駄目だ。これは、余デカルト圏とデカルト圏におけるトレースの問題。

付録は短くて独立して読める。 Aは物理的背景、これはダメだ。僕にはチンプンカンプン。 Bは二重圏の形式的な話。例がないが、まー、なんとかなりそう。 Cは厚いタングルの計算、これが一番読みやすそう。絵も山盛りある。

システムコールwriteを使って、stdout（のファイルハンドル）に整数を10進表記で出力する関数 putn(int) を書きましょう（戻り値はどうでもいい）。printfもそのようにして作られている。

abstractだけ眺めて捨て置きな論文がゴミとなってたまるばかりで、なんかゲンナリしている昨今。カーラー／リュウバシェンコ（Thomas Kerler, Volodymyr V. Lyubashenko）の本がなかなか入手できなかった（http://d.hatena.ne.jp/m-hiyama-memo/searchdiary?…

説明文書としてはメチャクチャ出来が悪い。まーいいや。いつか書き直す。[追記]あんまり意味がないところは取消線を付けた。[/追記]●基本事項関係から述語へJはJSONデータ全体の集合だとして、f:Jn→Boolean （Boolean = {true, false}）を関係の特性関数と呼…

圏上のチェーンの畳み込み積 - 檜山正幸のキマイラ飼育記 (はてなBlog) モノイドと圏はやっぱり似ているね - 檜山正幸のキマイラ飼育記 (はてなBlog) もう一度ちゃんと考える価値がある。

総称ラムダとかを参考にすると、次のようになる。ただし、これは厳密結合の推論で、型制約が出てこない。残念ながら、これでは実用にならないが、キレイにまとまる感じはある。S, Tなどは型項（または型表現）、f, gなどはコマンド項、M, Nなどは式（formula…

ベックの法則の定式化がけっこう分かってきた。これはさすがに書いておかないとな。忘れるからな。基本的に（メンタルに）想定しているのは多元環Rと加群Mなんだが、モノイドとモノイド作用なら何でも同じこと。ここでは、モノイド構造さえ考えないでマグマ…

http://www.cs.cornell.edu/~kozen/papers/papers_collapsed.htm ここからいろいろな論文が取れる。set expressionはtype expressionで、set constraintsはtype constraintsだから、そのまま型推論に使える。しかし、termset代数が、エルブラン方式理論であ…

左←→右 は、同じ圏のなかでの双対性、ただし、右は非決定性（ND）な圏なので、決定性の圏を非決定性の圏に埋め込んで双対を考える。上←→下 は、直積・直和の双対性から導かれる対応。異なるモノイド圏のあいだの対応関係（関手ではない）。 ＼ 自明な構造 非…

ステファネスクに従って、用語法をデカルト分配圏からデカルト半環圏（cartesian semiringal category）に変える。記号の説明： θ -- 空集合を域とする唯一の射 ι -- 標準入射 ∇ -- 直和のフォールド＝余対角 λ -- 左unitor自然同型 ρ -- 右unitor自然同型 α…

注意：distributorは用語的に問題があって、distributivityとか言うほうが望ましいだろう。が、-er, -or って語尾はコンピュータ／ソフトウェア屋さんは好きだから、distributor使う。まず普通の足し算に関して： associator自然同型 (A+B)+C ⇒ A+(B+C) 左un…

モニャドセミナー4 資料 抜粋 ＋ 追加 - 檜山正幸のキマイラ飼育記 メモ編も参照。 足し算ぽい：ブーリアンのOR演算 -- 足し算ぽいね、うんうん 足し算ぽい：集合の合併 -- 以下同様 足し算ぽい：max, min 足し算ぽい：特に平坦束、この圏の線形写像はなにか…

「勝たす異論」じゃねーよ。型推論とかいうとつっこまれそうだから、型解析にする。問題はパイプ結合だけ。 型ユニフィケーションをして、SIL命題のセットを出力する SIL命題セットを整理、計算（簡約）する。 SIL命題セットから代入を取り出して、再帰的に…

式Eの計算が、すべての部分式の計算も含めて安全に行われる（と予測できる）とき、《E》 と書く。式Eのすべての部分式とパイプ記号には、番号（一意的ならなんでもいい）が振ってあるとする。異なる番号が同じ場所を指す可能性がある。（[追記]そんなにイッ…

これは、あくまで構文的であり、決して意味的ではないことに注意。意味的な議論は解釈を決めないとできないし、解釈は色々あり、解釈ごとに定義は変わる。基底：コマンド呼び出しと定数 Dom(f::S -> T) = S Dom(c) = null Cod(f::S -> T) = T Cod(c) = sing(…

「文字列（名前）の集合と非負整数値」の組をシグニチャと呼ぶ。次の形で書く； {"foo", "bar"; 2}, {; 3}, {"baz"; 0}, {;0}。シグニチャパターンはオプションシグニチャパターンと引数シグニチャパターンの組である。オプションシグニチャパターンは： 文…

カロウビ展開圏 - 檜山正幸のキマイラ飼育記 (はてなBlog)のコピー与えられた圏Cに対して、新しい圏Kを作ります。その作り方を順に述べます。まず、Kの対象は、Cのベキ等射とします； a∈|K| ⇔ aはCのベキ等射 ⇔ a;a = a inc C。Kの射 f:(A,a)→(B, b) は次の…

モノ（値）かコト（事態、動作）か モノとコトの相互変換 soft-nothing と hard-nothing ⊥の追加、厳密射、リフト 結局は、バンドルと層を使うことになるな。 集合圏の始対象／終対象の非対称性 関数と関数型（べき、指数） 特異値と非特異台 外延的記法によ…

代数幾何の枠組みを他分野に応用するには、ガブリエル／ローゼンバーグ（Gabriel Rosenberg）の再現定理（reconstruction theorem）というのがどうも鍵らしい。可換環からなにやらかにやらして作ったアーベル圏から、もとの環を再構成できる、ということらし…

http://d.hatena.ne.jp/m-hiyama/20061115/1163573135

戻り値Bでエラー（丸括弧で囲む）がEの関数は、A→B+(E)。Eをcatchすると、A→B+E。となると、もともと A→B+E である例外しない関数を A→B+(E) とするのが、場合分けthrowってことになる。when { y∈B => return y, y∈E => throw y}。ある範囲内の射を全部に場…

長男に自転車の練習をさせていた時のことを思い出した。 補助輪を使うかどうか悩んだ 補助輪は止めたけど、ひたすらバランスを取る練習 あぶないので付きっきり ブレーキ、信号、左右確認などはずっと後 PCゲームで交通ルールは学んだ（が、たぶん身に付いて…

/* wrap-around.c */ #include <stdio.h> /* この動作をなにがあっても一生忘れないように、 * 1日数回実行して、通算千回ほどは眺めること。 */ main() { signed char sc = 100; unsigned char uc = 100; int i; for (i = 0; i < 200; i++) { printf("%03d:%4d %4d\n</stdio.h>…