2016-11-27

Implicit argument が絡んで型検査を通らない例

型検査（推論？）がうまくいってもよさそうだけどうまくいかない話です．挙動は Coq 8.5pl2 で確認しました．他のバージョンでどうかは調べていません．

Set Implicit Arguments してから，なんか依存型を定義します．

Coq < Set Implicit Arguments.

Coq < Inductive Fin : nat -> Set :=
| F0 n : Fin (S n)
| FS n : Fin n -> Fin (S n).
Coq < Coq < Fin is defined
Fin_rect is defined
Fin_ind is defined
Fin_rec is defined

Coq < Fixpoint Fin' (n : nat) : Set :=
  match n with 0 => Empty_set | S n' => sum unit (Fin' n') end.
Coq < Fin' is defined
Fin' is recursively defined (decreasing on 1st argument)

自然数で添字付けられた集合族です．返ってくる物の中身はわりと何でもよくて，それぞれ Inductive と Fixpoint で定義されているところが重要な気がします．

それで，これらを引数に取る関数を何か作ります．ここでは面倒なので変数を宣言してしまいます．戻り値は Prop にしておきましたが，別に何でもよさそうです．

Coq < Parameter P : forall n (i : Fin' n), Fin n -> Prop.
P is assumed

Coq < Print P.
*** [ P : forall n : nat, Fin' n -> Fin n -> Prop ]

Argument n is implicit
Argument scopes are [nat_scope _ _]

P の第一引数の n は implict になります．第三引数の型から推論できそうなのでまあそうでしょうという気がします．ちょっと使ってみます．

Coq < Check (P (inl tt) (F0 0)).
Toplevel input, characters 10-16:
> Check (P (inl tt) (F0 0)).
>           ^^^^^^
Error:
The term "inl tt" has type "(unit + ?B)%type"
while it is expected to have type "Fin' ?n".

うまくいかないようです．(inl tt) の型は (unit + ?B) だけど (Fin ?n) が要求されていると言われています．実際には，第三引数の型が (Fin 1) でこいつは inductive type なので第一引数が 1 であることが（たぶん）わかり，これを第二引数の型の n に代入すれば (Fin' 1) となりますが，これは (unit + unit) に簡約できます．以上のように推論すると型が合っていることがわかる気がしますが，そんなことはしてくれないようです．

明示的に型を書くか引数を与えてやるとチェックは通ります．

Coq < Check (P (inl tt : Fin' 1) (F0 0)).
P (inl tt : Fin' 1) (F0 0)
     : Prop

Coq < Check (P (n := 1) (inl tt) (F0 0)).
P (inl tt) (F0 0)
     : Prop

でもちょっと面倒だし，読みにくくなりがち．

試しに P の引数の順番を変えてみると，

Coq < Parameter P' : forall n (i : Fin n), Fin' n -> Prop.
P' is assumed

Coq < Print P'.
*** [ P' : forall n : nat, Fin n -> Fin' n -> Prop ]

Argument n is implicit
Argument scopes are [nat_scope _ _]

Coq < Check (P' (F0 0) (inl tt)).
P' (F0 0) (inl tt)
     : Prop

こっちは問題ないようです．ということは型検査アルゴリズムが項を処理する順番の問題とかだろうか．もし引数を左からチェックするのだとすると，最初の例では n がわからない状態で (inl tt) の型検査をすることになるので，型が合わないように見える．今の例だと先に (F0 0) を検査するので，n = 1 とわかり，その後 (inl tt) を見るので型が合うと判断できる．本当にそういう実装になってるかどうか知りませんが．

ついでに両方とも inductive でない方の型にしてみると，

Coq < Parameter P'' : forall n (i : Fin' n), Fin' n -> Prop.
P'' is assumed

Coq < Print P''.
*** [ P'' : forall n : nat, Fin' n -> Fin' n -> Prop ]

Argument scopes are [nat_scope _ _]

これは n が implicit でなくなります．Fin' n のような実引数が与えられると簡約されるものは，n が何だったか後からわからなくなる可能性があるから，まあそれが自然かという気がします（オプションでいろいろ制御できる）．

2016-10-21

かたい電車

15分間隔で電車が走っている路線でA駅からB駅へ向かい，その後30分間隔で電車が走っている路線に乗り換えてC駅に行くことを考える．

A駅でいつもより一本（つまり15分）早い電車に乗るとどうなるか．おそらくB駅における乗り換えでいつもより15分長く待って，いつもと同じ時間の電車に乗り換え，C駅に着くのはいつもと同じ時間になるだろう．あたりまえなんだけどあたりまえじゃない，という感触があって，おもしろい．

定期的に電車に乗っていた時期が昔からほとんどない．いつも歩いて移動している．だからだろうか，5分早く出れば5分，15分早く出れば15分早く着くのが当然のように思っている．しかし電車はそうではない．そのことに気付いたとき，そうか，電車はかたいのだ，と思った．

正則関数はかたい，と言われることがある．局所的な情報だけで全体が決まってしまう．それに対して連続関数はやわらかい．ウリゾーンの補題がそのやわらかさを示している．

それになぞらえて言うと，電車はかたく，徒歩はやわらかいのだ．飛行機は電車よりももっとかたい．同じ電車でも，都会では田舎よりもやわらかいだろう．

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