2016-10-17

ホーア論理の代入の規則

わりとわかりにくくて混乱しやすい気がするホーア論理の代入の規則ですが，見方を少し変えるとわかりやすくなります。

普通の規則。

$\{A[e/x]\} \mathtt{x := e} \{A\}$

同値変形してこうする。

$\{\forall x'. x' = e \to A[x'/x]\} \mathtt{x := e} \{A\}$

要するに「代入後の x の値を x' とすれば A[x'/x] である」が事前条件です。Hoare triple の意味を考えればそれが事前条件になるのは当たり前ですね。

こっちのほうがわかりやすいし，この形で認識しておくと x' の条件を変えることでいろいろできます。例えば乱数。

$\{\forall x'. A[x'/x]\} \mathtt{x := rand()} \{A\}$

上限を指定したり。

$\{\forall x'. 0 \le x' < n \to A[x'/x]\} \mathtt{x := rand(n)} \{A\}$

配列。

$\{\forall x'. x'[i] = e \to (\forall j. i \ne j \to x'[j] = x[j]) \to A[x'/x]\} \mathtt{x[i] := e} \{A\}$

配列への同時代入（構文は適当）。

$\small\{\forall x'. (\forall j. 0 \le j \le 3 \to x'[i+j] = y[k+j]) \land (\forall j. \neg(i \le j \le i+3) \to x'[j] = x[j]) \to A[x'/x]\} \mathtt{x[i:i+3] := y[k:k+3]} \{A\}$

2016-08-12

数学の本の話

数学の本はアウトラインがわかればあとは自分でよく考えるだけで本を閉じたまま詳細を構成することができる。しかし数学以外の本はそうとは限らない。例えば歴史の本は歴史の大まかな流れがわかっていても細部を自分の頭で考えても埋めることはできない，気がする。仮にそれらしく埋めたとしても，正しいかどうかを自分で確認することは難しい。

数学の本の詳細（普通は証明が大部分を占める）が自分で構成できるとは，本の中身を見ることなく本に書いてある通りのことが自分で書けるということではない。本に書いてあるのと同じ結論に至る，論理的に正しい詳細が書けるということだ。自分で考えて書いてみた結果が本に書いてある内容と全く同じになるとは限らない。長い証明などは同じになることのほうが珍しい。しかし，自分で書いたことの詳細が本に書いてあるものと一致するかどうかは，ほとんどの場合には問題ではない。この場合に問題なのは，結論が論理的に正しく導かれているかどうかだからだ（あんまり本文の方針から外れてしまうと，後で理解に不都合が生じる可能性はあるが）。

2016-08-08

Hilbert algebra の性質の証明

ちょっと気になってやってみたのをどこかにメモしたくなったので書いた。関数解析じゃなくて論理の方の Hilbert algebra です。

Hilbert algebra の公理

$(A, \rightarrow, 1)$ が Hilbert algebra とは

$\rightarrow: A^2 \rightarrow A$
$1 \in A$
$a \rightarrow b \rightarrow a = 1$
$(a \rightarrow b \rightarrow c) \rightarrow (a \rightarrow b) \rightarrow (a \rightarrow c) = 1$
if $(a \rightarrow b) = (b \rightarrow a) = 1$ then $a = b$

性質

$1 \rightarrow a = a$
$a \rightarrow 1 = 1$
$a \rightarrow a = 1$
$a \rightarrow b \rightarrow c = b \rightarrow a \rightarrow c$
$a \le b \iff a \rightarrow b = 1$ で順序が入り，1 が最大元

などが成り立つ。証明は下に書くけど自分で考えると楽しいかも。

証明

補題: $a \rightarrow b = 1$ かつ $a = 1$ なら $b = 1$

証明: 最後の公理があるので $b \rightarrow 1 = 1 \rightarrow b = 1$ がいえればよいが，
$\begin{array}{rll} b \rightarrow 1 & = & b \rightarrow (a \rightarrow b) & (仮定\ a \rightarrow b = 1) \\ & = & 1 & (\text{公理}) \end{array}$
$\begin{array}{rll} 1 \rightarrow b & = & a \rightarrow b & (仮定\ a = 1) \\ & = & 1 & (仮定)\end{array}$

定理: 直観主義論理の implicational fragment で $\vdash \varphi$ なら， $A \models \varphi = 1$

証明: Hilbert style system での証明に関する帰納法。Modus ponens のときは上の補題を使う。

系: 直観主義論理の implicational fragment で $\vdash \varphi \rightarrow \psi$ かつ $\vdash \psi \rightarrow \varphi$ なら， $A \models \varphi = \psi$

上に書いた主張はこの定理と系から全部出てくる。

2016-03-22

resolution の完全性についての疑問

一階述語論理の resolution の規則って， $l \in C, \neg l' \in C'$ として $\theta$ を $l, l'$ の MGU としたときに
$C, C' \vdash (C\theta \setminus \{l\theta\}) \cup (C'\theta \setminus\{\neg l \theta\})$
と書けて(resolution に $\vdash$ を使うのはあまり普通ではないかもしれないけど)，これだけで反駁完全なのだと思っていました。しかしどうもそうではないようだという気がしてきて，どうやったら本当に完全になるんだろうかということを最近考えました。

まず完全でないと思う理由ですが，例えば $\{ \{p(x), p(y)\}, \{ \neg p(u), \neg p(v) \} \}$ (p は述語記号，x, y, u, v は変数)という節集合を考えます。これが充足不能なのは，論理式で書くと $(\forall x y. p(x) \lor p(y)) \land (\forall u v. \neg p(u) \lor \neg p(v))$ だから明らかでしょう。一方，この節集合からは上の規則を使っても $\{ p(z), \neg p(w) \}$ しか(変数の名前の違いを除いて)新しい節は出てきません。だから空節を導くことはできません。

いくつか見てみた本の中で「論理と計算のしくみ」では違う規則を採用していて，この本では一つずつではなく複数のリテラルをまとめて取り出して unify してよいことになっています。具体的には $\theta$ を $C' \cup D'$ の MGU として
$C \cup C', D \cup \neg D' \vdash (C \cup D)\theta$
のようにしています。これだとさっきの例は $p(x), p(y), p(u), p(v)$ をまとめて unify してやれば空節が出てくるので OK，ということになります。この形の規則だと確かに反駁完全性が成り立つようです。

でもそういう形の規則になっている本は他に見かけないので，これはどういうことだろうかと疑問に思い調べてみました。以下の記述は "Handbook of Automated Reasoning" の Chapter 2 の冒頭(を読んだ記憶)に基づいています。どうやら resolution の手法を最初に考えた Robinson は，確かに最初の形を resolution として定式化していたようですが，それに加えて別にもう一つ規則を用意していたらしいです。その規則は factoring といって， $\theta$ を D の unifier として
$C \cup D \vdash (C \cup D)\theta$
という形をしています(たぶん)。これがあると，
$\{ \{p(x), p(y)\}, \{ \neg p(u), \neg p(v) \} \} \vdash \{ \{p(x)\}, \{ \neg p(u) \} \}$
なので，最初の形の resolution と合わせて空節が導けます。厳密には確かめていませんが，こちらも反駁完全性が成り立ちそうです。

ということは，もともとは resolution と factoring を合わせて反駁完全であるという話だったのに，factoring の方は何らかの理由であまり教科書に書かれなくなってしまったのでしょうか(実際，handbook を読むまで factoring という名前を知らなかった)。https://en.wikipedia.org/wiki/Resolution_(logic) には "The resolution rule, as defined by Robinson, also incorporated factoring, .... The resulting inference rule is refutation-complete, ...." と書いてあるので，そんなに知られていない事実でもなくて，たまたま僕がそのあたりのことが書いてある教科書を読まなかっただけかもしれませんが。

2015-12-30

ダウンロードしてみた本リスト

先日 Springer でいろいろな本が無料ダウンロードできるようになっていた。今はもうできなくなったらしい。どういうことだったのかはよく分からない。twitter を見ても，よく分からないと言っている人がたくさんいる。

何冊か落としたのでメモ。

Marker, Model Theory
Mac Lane, Categories for the Working Mathematician
Jech, Set Theory
Mac Lane & Moerdijk, Sheaves in Geometry and Logic
Cox et al., Ideals, Varieties and Algorithms
Hartshorne, Algebraic Geometry
Halmos, Finite Dimensional Vector Spaces
Shafarevich, Basic Algebraic Geometry 1, 2
Fulton, Algebraic Topology
van Dalen, Logic and Structure
Poizat, A Course in Model Theory
Marcja & Toffalori, A Guide to Classical and Modern Models Theory

2015-11-14

contraction がいらないシーケント計算

「論理と計算のしくみ」を読んでいたら，シーケント計算の推論規則を

∧右，∨左，⊃左は additive
∧左，∨右は multiplicative

にすると命題論理では contraction が不要になるということを知りました。こういう組み合わせは証明論的にはだいぶ気持ち悪いような気がしますが，Wang's algorithm に対応するように推論規則を作るとこうなるようです。

一階述語論理では反例があって， $\exists x ( (P(a) \land P(b) ) \lor \neg P(x) )$ は contraction がないと証明できないようです。∃右規則を

$\displaystyle{ \frac{\Gamma \Rightarrow \Delta, A[t_1], \dots, A[t_n]}{\Gamma \Rightarrow \Delta, \exists xA[x]} }$

として，∀左も同様に変更すると contraction なしで済みそうですが（確認してないけど）。

これは一体，何を意味するのだろうか。

2015-11-12

Awodey 本の訳に変なとこがある

Awodey 本の邦訳について，訳の質が低いという趣旨のレビューがついています。自分で確認したわけではないのですが，このレビュアーの書いていることを信じるならば，確かにあまり丁寧に訳されてはいないようだという印象は受けます。そこに挙げられている点が数学書の翻訳の質を評価する上で重要かどうかはともかく。

そのレビューに対して「数学的な誤りがあると言うが，具体的にどこにあるのか？」というコメントが付いているのを見て，以前眺めたときにおかしな箇所があったことを思い出しました。それでちょっと確認してみたらやっぱりおかしいようなので，とりあえずここに書いてみます。正確には誤りというか，そもそも意味がわからない文が書いてあるということですが，いずれにしても数学の技術的内容に関わることです。

問題の箇所は注意 9.36 にあります。「A を局所スモール完備圏とし，次の条件をみたしているとする」*1として，二つの条件を挙げていますが，その一つ目が次のようになっています。

1. $\mathbf A$ が羃化可能 (well powered): 各々の対象 $A$ は部分対象 $S \rightarrowtail A$ の集合を一つしかもたない

最後の「部分対象の集合を一つしかもたない」は何を意味するのかがわかりません。原書が手元になかったので，原文の元になっているらしい PDF（http://www.andrew.cmu.edu/course/80-413-713/notes/ の chap09.pdf）を見てみると，対応する部分は次のようになっています。

1. $\mathbf A$ is well powered: each object $A$ has at most a set of subobjects $S \rightarrowtail A$

この表現，well powered の定義を知っていればまあわかりますが，意味がとりにくいかもしれません。"at most a set" で「（高々）set size である」を意味しているのだと思います。だから定義全体としては「どの対象についても，その部分対象の全体は集合である（proper class になるほどたくさんは存在しない）」という意味になります。

ちなみに nlab の well-powered category を見ると，定義は

A category C is well-powered if every object has a small poset of subobjects.

となっています。small という語がある分だけ，こっちのほうがわかりやすいかも。

*1:「局所スモール完備圏」はひとまとまりの用語かと思ったら，原文では "locally small, complete category" となっていました。それだったら全部つなげないで「局所スモールかつ完備な圏」とかにすれば紛れがないのにと思いますが，これは好みかもしれません。