…F＊Q に引き戻せます。この状態引き戻し操作がΔFです。 ΔF:[B, Set] → [A, Set] in CAT ΔFを基準にして随伴関手トリオ $`\Sigma_F \dashv \Delta_F \dashv \Pi_F`$ を考えると、データマイグレーション関手が得られます。$`\Pi_F `$ がテーブルジョインによる変換、$`\Sigma_F `$ がテーブルユニオンによる変換です。あっ、プログラム検証のホーア論理とプレ条件／ポスト条件の例を忘れた、まっいいや。

…異なったパラダイム ホーア論理とプログラム意味論 しかし、それでも意味論は必要 プログラムとしてのディープラーニングこの論説においてbonotakeさんは、ディープラーニングの現状を要領よくおさらいした後で、ひとつの提案をしています。その提案をまず紹介しましょう。ディープラーニング技術により何らかのタスクを遂行することを、「プログラムの作成／作ったプログラムの実行」と考えよう、とbonotakeさんは言っています。ディープラーニング・ソフトウェアもプログラムなのだ、ということ…

…味論全般ではなくて、ホーアやダイクストラの流儀です。 *4:関数と写像は区別せずに、同義語として用います。 *5:ベイズ確率論が「なんで違った分野のポリシーに従う必要があるんだよ？」というツッコミは当然にあるでしょう。ベイズ確率論とプログラム意味論は、十分に抽象化したレベルで見ると強い類似性があります。その類似性からすると、プログラム意味論の基本原則がベイズ確率論で尊重されてないのは「どうもマズイだろう」という懸念があるのです。 *6:この同型は、“凸空間の自由生成関手と忘却…

…数的に定義できます。ホーア論理〈Hoare logic〉を組み立てることもできます。以下の記事はホーア論理に関するものですが、テストフレームワークを実際に作っていたときに書いた記事なので、現実的な考慮が色々入っていて、理論的な筋は若干見えにくいかも知れません。 非決定性写像の圏におけるホーア式のモデル 非決定性写像の圏におけるホーア式のモデル 踊り場・編 非決定性写像の圏におけるホーア式のモデル いちおう完結・編 クリーネ代数とはちょっと離れますが、ホーア論理の圏論的扱いにつ…

…の内容に近いです。 ホーア論理の圏論的な定式化 さて、集合Xにその上の述語の全体Pred[X]を対応させる関手は、実質的に反変ベキ集合関手Pow*と同じものですが、Pred[X]は圏だと解釈します。集合Xごとに圏がくっついているような構造ですね。改めて、インデックス付き圏としてのPredを定義しましょう。まず、集合圏の部分圏Bを定めます。このBをベース圏（base category）と呼びます。集合圏の特定された終対象を1として、1∈Bは仮定しておきます。したがって、最小のベ…

…スティチューションとホーア論理 Haskellでは型同士の継承をサポートしていませんが、型クラスから型インスタンスへの継承はできるため、それを利用した多態性の実現が可能です。 「型クラスから型インスタンス」は文字通りインスタンス化であって継承とは言わないでしょ。言ってもいいのかな？ …… やっぱり、区別したほうがいいと思います。 いまさらながらだけど、オブジェクトとクラスの関係を究めてみようよ 牛が牧草を食うことを、総称の文脈で語ってみよう 型クラスの話題だとCoqになってし…

…ログラム検証論』にはホーア論理について詳しく書いてありました。日本語の本であんなに詳しいのは他にないんじゃないかな*4。『構成的プログラミングの基礎』のほう*5は、難しくてダメでした ^^;。『プログラム検証論』は共立出版の情報数学講座シリーズの一冊ですが、このオレンジ本シリーズは良い本が多いですね。型付きラムダ計算や領域方程式の解き方なんかは、『プログラム意味論』と『プログラミング言語の基礎理論』の2冊から学べます。プログラム意味論 (情報数学講座)作者:横内 寛文発売日:…

…は、実行文fに対するホーア式 p{f}q と似たようなものです。ガード演算は圏の結合（composition）と整合する必要があるので、次の条件も仮定します。 (f・q);g = f;(q・g) (f・q);(r・g) = (f・(q∧r));g これらを組み合わせると、(f・q);(r・g) = f;((q∧r)・g) も出ます。順次実行「;」、論理AND「∧」、ガード「・」が、ある程度は置き換え可能であることを示しています。論理OR「∨」と足し算「+」は、非決定性の分岐を…

…イヤー流の契約とは、ホーアの表明の変種に過ぎません。しかし、それを提供者（業者）と顧客のあいだの約束事という比喩を使った点がメイヤー先生の秀逸なアイデアです。そもそもメイヤー先生は比喩が大好きで、ときに牧場の牛だのカタマラン・ヨットだのと無理筋になってしまうこともあるのです。今日は僕もメイヤー先生にならって、提供者にとって契約がきびしくなることについて、かなり強引な例え話をしてみます。入力は持ち込みの素材、出力はケーキすこし前に野菜を使ったケーキが話題になりましたが、柿沢安耶…

… と書けます。契約はホーア（Tony Hoare）の表明 P{f}Q と似てます。似てますが違いもあるので注意してください。契約には提供者と顧客の別があるので、契約が破られたときの責任の所在が云々できます。ホーアの表明にはそのような複数の利害関係者は想定してないので、表明が失敗しても「誰のせいだ？」という話は出てきません。ホーアの表明では、Pが偽になっても契約違反だとか失敗だとか騒がないで、通常は成功として穏便に(?)済ませます。ホーアの表明は例外に関しても寛容で、「不測の事…

…のかもアヤシイ。例えば、プロパティの定義にドメインが含まれますが、プロパティのドメインって何？ プログラミング言語の引数型チェックのような制約が働くのでしょうか？ -- それは期待できませんよね。だったら、気分だけの注釈に過ぎないのでしょうか？ それともホーア表明のように解釈すべき？？と、僕の知識と解釈力の不足もあり曖昧な点が多いのですが、フォーマルに書けそうな所もあります（ちょっとは書いてみました）。で、機会と気力があれば、フォーマルな観点からナニゴトか書くかもしれません。

…sとします。さて、「ホーア論理の圏論的な定式化」や「インスティチューションとホーア論理」に、p≦f*(q) という不等式が出てきますが、上の f*(A)≦B はそれとよく似た不等式です。その背景はグロタンディーク構成です。XGraphをベースの圏として、XGraphの対象（有向グラフ）GごとにConstr(G)を対応させると、XGraphの射 f:G→H は、関手（プレ順序の準同型写像）f*:Constr(G)→Constr(H) を誘導します。Constr(f) := f*…

…の実行と考えた場合のホーア表明になっています。述語と部分集合を同一視するなら、U⊆P(f)(V) はホーア式 U{f}V です。ベキ集合のグロタンディーク構成により得られた全体圏は、ホーア式を射とする圏とみなすことができて、ファイブレーション射影は、ホーア式にその制約記述の対象であるプログラムを対応させます。全体圏における結合は、2つのホーア式を前提とする含意の推論（カット規則）です。最近、デイヴィッド・スピヴァック（David I. Spivak）は、データベースの定式化に…

…順序関係になります。ホーア論理を展開するときなどは、この順序が重要になります。が、今回はこれ以上触れません。掛け算 A;B は、2つのプロラムA、Bの順次実行です。特別なプログラムI（大文字アイ、イチに似ている）があるとして、計算法則は以下のとおり。 (A;B);C = A;(B;C) I;A = A;I = A O;A = A;O = O 掛け算は可換でもなくベキ等でもありません。そして、左右からの分配法則が成立します。 (A + B);C = A;C + B;C A;(B…

自分で参照する都合で小さなリンク集を作った； 僕の興味はたぶん次のようなキーワードで示せるのでしょう。 メイヤー 「本文」「目次」 ホーア「本文」「目次」 型理論 「本文」「目次」 インスティチューション 「本文」「目次」 シーケント 「本文」「目次」 仕様記述 「本文」「目次」 次の2つの語は一般的過ぎるかも。ヒットが多すぎる。 論理 「本文」「目次」 ラムダ 「本文」「目次」

…持つ双加群の類似物はホーア論理です。S, Tを2つの状態空間として、Sの部分集合の全体（の適当なサブセット）はブール代数になります。ブール代数は、ほんとの可換環ではありませんが、足し算も掛け算もベキ等な半可換環となります。T上にも同様にブール代数が作れます。SからTへの状態遷移（非決定性）は、SとTのあいだの関係なので、S×T の部分集合とみませます。Rel(S, T) には集合の合併で足し算が入り、左右から先ほどのブール代数達が作用します。これはつまり、2つの可換半環が左右…

…。関係する事例が、「ホーア論理の圏論的な定式化」にあります。ホーアトリプルは、順序に関するグロタンディーク構成から得られると考えられます。圏の圏Catに相当する圏は、順序集合と単調写像の圏Ord、あるいはプレ順序を考えたPreOrdとかです。圏とプロ関手の圏に相当すると思われるORelに関しては「順序付き関係の圏」で触れています。随伴に相当する概念はガロア対応（Galois connection）と呼ばれます。単調写像の組 f:A→B、g:B→A で、f(x)≦b ⇔ x≦g…

…、メイヤーの契約とかホーアトリプルとホーア論理などを用いるでしょうが、単純な等式的論理も有用なことがわかります。仕様記述とテストは区別すべきではない、と僕は考えていますが、その立場でエクスペクテーションベースのテストを眺めると、テストにより等式的論理の原子基礎論理式を積み重ねていることがわかります。このような見方・考え方は、テスト容易性／テスト困難性が何に起因するかを教えてくれます。テストが困難な状況を緩和するにはどうすべきかの方針も与えてくれます。また、次のような問や疑問に…

…記述の具体例として、ホーア式やメイヤーの契約があります。値のあいだの個別の関係 b = f(a) という形ではなくて、入力の範囲となる集合Aと出力の範囲となる集合Bが与えられます。そして、「x∈A ならば f(x)∈B」という論理的主張によって法則が記述されます。もちろん、法則の記述は複数の論理的主張（表明）を使ってもかまいません。番号1, 2, ... に対する「x∈A1 ならば f(x)∈B1」、「x∈A2 ならば f(x)∈B2」、… のような形です。具体的に与えられた…

内容： 型宣言とホーアトリプル 関数定義とホーアトリプル ホーア論理とホーアセオリー 伴意順序 いろいろな概念を統合できるかな 型宣言とホーアトリプルfが関数だとして、f:X→Y という形はfの型宣言だとみなせます。話を簡単にするために、「型とは集合だ」と考えましょう。これから考える集合 A, B, C などは十分にに大きな集合Uの部分集合だとします。コンピュータで計算する関数に関しては、そんなUが存在します。p, q などが論理式だとして、ホーアトリプルを p{f}q の形…

…スティチューションとホーア論理を一緒にしたようなナニカ」は、僕にとっての一つの課題です。この課題については、次のエントリーで述べています。 ホーア論理の圏論的な定式化 真偽構造が付いた圏 -- ホーア論理のために 「インデックス付き圏のフビニ／グロタンディーク同値」では、入れ子になったインデックス付き圏を持ち出しました。入れ子のインデックス付き圏の動機は「大量のモナド類似物（monad-like entities）を一挙に扱う方法」だと書きました。実は、「インスティチューショ…

…eyer）、トニー・ホーア（Tony Hoare）、アラン・コンヌ（Alain Connes）、ユーリ・マニン（Yuri Manin）あたりは、カタカナ書きも定着しているので問題ないでしょう。Bob Coecke最初見たとき、読み方がサッパリわからなかったCoecke。 http://ja.forvo.com/search/Coecke/ クッケにも聞こえるけど、今までどおりクックでよしとします。ボブ・クック。Samson Abramskyボブ・クックの師匠筋。サムソンはいい…

「ホーア論理の圏論的な定式化」において、インスティチューションとホーア論理を一緒にしたようなナニカができないかなぁ、とか言ったので、もう少し考えてみることにします。ただし、最初のステップだけで、インスティチューションを使う段階には至ってません。僕がやりたいことは、「拡張されたホーア論理」の意味論を構成することですが、とりあえず意味論の舞台となる構造を作ることにします。真偽値という概念を圏論的に扱いやすい形にしたモノです。内容： 圏の上に真偽値を乗せる 真偽構造のあいだの準同型…

…ーバーライドなしの）継承 MethodS→MethodT となっています。それから以上の定式化は、状態空間とメソッドのモデルとしては直接的・直感的なものだと思います。多くの現実の実装が採用している方式と同じで、メソッドはthisとかselfとかの暗黙の引数を持つことにより実現されます。大域関数はthisの値がvoidであるメソッドとみなされます。この定式化と、インスティチューション、ホーアトリプル、余代数などの関係を考えてみると面白いかも（あるいは面白くないかも）しれません。

…記事を書きました。 ホーア論理とシーケント計算を混ぜたような意味記述構文 CatyScript コマンド呼び出しの意味論 評価シーケントの論理計算と操作的意味論 なぜ僕は操作的意味論に傾いたか ようするに、CatyScript2.0の意味論の記述方法を考えていた、ってことです（構文の記述はBNFで不満はありません）。CatyScript2.0で追加拡張する機能でたぶん最初に着手するのは変数とコマンド呼び出しです。よって、意味記述も変数とコマンド呼び出しを最初にやるでしょう。つ…

…の意味論」より： 「ホーア論理とシーケント計算を混ぜたような意味記述構文」で述べた記述言語はマー悪くない感じです。ですが、使いやすい記述言語にするにはまだ拡張と改善が必要です。記述言語も記述される対象も、より精密にしたいですね。 気が付いたところを早速に拡張・改善します。内容： 評価シーケント 推論規則、公理、証明 束縛列の操作 束縛列のマージ 評価シーケント計算のまとめ 評価シーケント現状のシーケントの形式は Σ;x{E} → Γ;y です。もともとがホーア論理から出発した…

…法を記述するさて、「ホーア論理とシーケント計算を混ぜたような意味記述構文」を使って、コマンド呼び出しの意味と評価方法を記述してみます。次の3つの推論規則で十分そうです。 Σ;x{A} → Σ;α Σ,α;x{c} → Γ;y ----------------------------------------[command-call] Σ;x{c A} → Γ;y (Native[Command[c]] = f) -------------------------------[…

…tyの論理的意味論：ホーア論理からはじめよう しかし、表示的意味論と論理的意味論を2回書くのは面倒です。一回で済ませたい。そこで、評価の規則と推論の方法を一度に書けるような記述方法を考えることにしました。内容： 今回使うホーアトリプルの定義 束縛の表現 束縛の演算 クロージャの表現 推論規則 束縛の列に関する参照と代入 参照と代入の意味記述 見通しと妄想 今回使うホーアトリプルの定義「Catyの論理的意味論：ホーア論理からはじめよう」では、データの集合A, Bと式Eから、ホー…

…ングに利用するなら、ホーア論理が一番基本的で一番役に立つものだと思います。ホーア論理の圏論的な定式化というと、アブラムスキー達による仕様構造（specification structure）という概念があります。例えば、次の論文の冒頭に仕様構造の記述があります。 Title: A specification structure for deadlock-freedom of synchronous processes (1999) Authors: S. Abramsky ,…

…の記事で取り上げた、ホーア式のモデルや正規言語の話のなかでもベキ等半環が出てきます。 非決定性写像の圏におけるホーア式のモデル 正規表現とオートマトン：イプシロン指標 （イプシロン指標はベキ等半環の準同型） そういえば、HTTPメソッドにさえベキ等概念は登場しますよね。 訂正補足：HTTPメソッド、URL、そして標準化された動詞 ベキ等性はまた、正規化や観測の概念につながります。（ただし、足し算というより掛け算です。） ベキ等、正規化、計算、射影、観測 計算（computat…