天泣記

2017-02-07 (Tue)

#1 math-comp: remove documentation for subfilter. #106

<URL:https://github.com/math-comp/math-comp/pull/106>

2017-01-08 (Sun)

#2 Coq の eq (3)

「Leibniz equality は任意の述語について成り立つ性質で、なんとなく、Coq の eq より強力に感じられる」とか、「こういう具体的な手順で定義した関係は、Leibniz equality よりも弱い気がする」とか書いたが、しばらく考えた結論として、私はどうも「任意の述語」というところに強さを感じているようで、そこに間違いがあったようだ。

述語の中では eq を使えるので、eq で区別できるものはなんでも述語で区別できる。そして、もし eq で区別できないものを区別する仕掛けがほかに存在しないのであれば、eq で区別できないものはどんな述語でも区別できない。

というわけで、「eq で区別できないものを区別する仕掛けがほかに存在しない」という条件を満たせば、eq がどんな同値関係であっても eq と述語で区別できるものは同じになる、つまり、eq は Leibniz equality になるのだな。この場合、任意の述語といっても eq とちょうど同じ強さになるのは eq が使えて、それ以外にはもっと強力なものがない、というだけの話で、まぁそうだな、という感じで納得できた。

そして、convertible なものをなんらかの方法で区別する仕掛けは (述語として使えるものは) 存在しないので、eq を convertible な関係としている現状では、実際に eq と Leibniz equality が等価になっている、ということだと理解した。

「eq で区別できないものを区別する仕掛け」の具体例としては、1 + 1 と 2 を区別する仕掛けが考えられる。以下のように定義した x, y を考える。

Definition x := 1 + 1.
Definition y := 2.

1 + 1 と 2 は convertible なので、x = y は reflexivity で証明できる。

Goal x = y.
Proof.
  reflexivity.
Qed.

では、x と y を区別できないかというと、そんなことはない。Print で表示してみれば、x は + を使っており、y は + を使っていないという違いを確認できる。

Coq < Print x.
x = 1 + 1
     : nat

Coq < Print y.
y = 2
     : nat

ということで、「Print して + が含まれているかどうか調べる」という述語があれば、x と y は異なる結果 (前者は成り立ち、後者は成り立たない) になるだろう。それが可能だと、矛盾 (False) を証明できるので、困る。(矛盾を証明できると、任意の命題を証明できてしまう (Principle of Explosion, 爆発原理) ので、有用な意味がなくなってしまう。)

ちょっと一般化して、そういう述語 (x = y であり、かつ、P x であり、かつ、P y でない、というような P) が存在すると、False を証明できることは Coq で確認できる。

Goal (exists (A : Type) (P : A -> Prop) (x y : A), x = y /\ P x /\ ~ P y) -> False.
Proof.
  intro H.
  destruct H as [A [P [x [y [Hxy [Px nPy]]]]]].
  case nPy.
  case Hxy.
  apply Px.
Qed.

矛盾を証明できるのは困ったことなので、そのような述語を導入することはできない。ということで Coq はそのような仕掛けを導入しないし、もしやってしまったらそれはバグである。

ところで、Coq では公理を追加できる。Coq.Logic.ProofIrrelevance にはすでに触れたが、排中律を導入する Coq.Logic.Classical_Prop や 関数の外延的等価性を導入する Coq.Logic.FunctionalExtensionality あたりは有名な気がする。coq-8.6/theories を grep してみると、Coq.Reals.Raxioms が実数のために 14個公理を追加していてなかなか多い感じである。

関数の外延的等価性や ProofIrrelevance などが追加する公理は、convertible ではないものを eq にする公理である。こういう追加が eq と Leibniz equality の等価性に影響するかというと、「eq で区別できないものを区別する仕掛けがほかに存在しない」という条件が満たされている限り、等価性は保たれるのだろう。

この条件を満たせなくなるような追加の具体例を考えると、値を区別できる仕掛けとして match があって、match で自然数の 0 と 0 以外を区別できるので、たとえば 0 = 1 という公理を追加してしまうことが考えられる。というわけで、そういう公理を加えると、以下のように False を証明できてしまう。

Axiom Eq01 : 0 = 1.

Goal False.
Proof.
  apply (@absurd (0 = 1)).
    apply Eq01.
  apply O_S.
Qed.
#1 Coq の eq (2)

reflexivity では (そのままでは) 証明できないが、eq であるような、単純な例を作ってみた。

Definition I1 := I.
Definition I2 : True.
  exact I.
Qed.

Goal I1 = I2.
  Fail reflexivity.
  case I2.
  reflexivity.
Qed.

I1 と I2 というのを True 型の値として定義する。True 型には値が I というひとつしかないので、どちらも値は I であるが、I1 はふつうに定義するのに対し、I2 は proof editing mode で、exact I として I を与え、Qed で終わる。これにより、I2 は unfold できなくなり、単なる reflexivity では I1 = I2 を証明できなくなる。

しかし、case I2 とすると、I2 を True のコンストラクタの種類ごとに場合分けし、でもコンストラクタは I しかないので、I2 が I であることが判明する。そうすると reflexivity で証明できるようになる。

eq_irrelevance の話はこれに同じ話がもっと複雑な状況で発生しているのだろう。たぶん。

ちなみに、Qed じゃなくて、Opaque で unfold できないようにするのは、reflexivity には影響しないようだ。

2017-01-06 (Fri)

#1 Coq の eq

Coq はカリーハワード対応を利用して、命題を型、その命題の証明をその型のプログラムとして表現する。たしかに、証明を受け取って証明を返す関数が含意の証明であるとか、and や or を帰納的データ型 (いくつかのコンストラクタで型を定義するやつ) で表現できるというのは納得できる。

しかし、値の等しさはどうだろうか。x = y というようなやつである。そのへんはよく分かっていないので少し調べてみた。

Coq における x = y は eq という帰納的データ型であり以下のように定義される。

Inductive eq (A:Type) (x:A) : A -> Prop :=
    eq_refl : x = x :>A
where "x = y :> A" := (@eq A x y) : type_scope.

Notation "x = y" := (x = y :>_) : type_scope.

Arguments eq {A} x _.

見かけをいじるために Notation や Arguments による細工が行われているが、それらをばっさり無視すると、以下の定義になる。

Inductive eq (A:Type) (x:A) : A -> Prop :=
    eq_refl : eq A x x.

つまり、eq という型は eq_refl というコンストラクタをひとつ持つ型である。

Notation により、x = y :> A と書くと eq A x y と解釈されるとか、x = y とだけ書くと eq _ x y となって _ の部分は推論にまかせるという指定がされている。また、Arguments により、eq 自身も A は省略するように指定されている。(@eq の @ は引数を省略しないという指示である)

ここで x の型は A であり、A の型 は Type である。A が Type ということは、A が nat など普通の値の型の可能性があり、つまり x は値かもしれない。つまり eq は値を引数にとる (値に依存する) ので依存型である。

たとえば、eq_refl 5 という式の型推論結果を表示させると、以下のように、5 = 5 という型になることがわかる。つまり、eq_refl 5 というプログラムは 5 = 5 という命題の証明である。5 という値が型の中に現れるのが依存型っぽい。まぁ、証明を書くと命題を教えてくれるというのはあまり役に立つ感じではないが。

Coq < Set Printing Implicit.

Coq < Check eq_refl 5.
@eq_refl nat 5
     : 5 = 5

プログラムの中に明示的に型を書いて、その型が正しいかどうか Coq に検査させることもできる。以下では、eq_refl 5 に 5 = 5 という型を書いて、それが Coq に受け入れられるので、eq_refl 5 は 5 = 5 の証明として正しいということが確認できている。これは、証明の正しさを機械が確認してくれるということで、複雑な証明については役に立ちそうである。

Coq < Check eq_refl 5 : 5 = 5.
@eq_refl nat 5 : 5 = 5
     : 5 = 5

さらに、5 のかわりに 7-2、3+2、2+3 と書いてもうまくいく。これは、eq_refl (7-2) は 3+2 = 2+3 という命題の証明として正しいと Coq が認めたことになる。

Coq < Check eq_refl (7-2) : 3+2 = 2+3.
@eq_refl nat (7 - 2) : 3 + 2 = 2 + 3
     : 3 + 2 = 2 + 3

eqの説明によれば、eq は Leibniz equality だそうである。Leibniz equality は x and y are equal iff every property on A which is true of x is also true of y ということで、Coq 的には、forall (A : Type) (x y : A), x = y <-> (forall (P : A -> Prop), P x -> P y) と表現できるだろう。

Wikipedia の Equality (mathematics) によれば、Leibniz equality はもともと Given any x and y, x = y if and only if, given any predicate P, P(x) if and only if P(y). というもので、P x -> P y ではなく、P x <-> P y というものだったようだ。こちらのほうが x と y が対称で、どんな述語によっても x と y を区別できない、という気分がよく表されているように思える。ただ、P x -> P y でも等価らしい。たしかに、P が「どんな述語」でもよいので、P = ~Q として ~Q(x) -> ~Q(y) を考えれば、対偶が Q(y) -> Q(x) になり、逆は導けるということでそれはそうだろう。(でも、Coq だと (直観主義だと) 対偶が等価であるとは証明できないので、違う説明が必要な気はする)

なお、「どんな述語」といっても、できることは制限されているように思える。もし、x と y の定義をデータとして取り出すようなことが可能なら、内部で使われている変数名の違いなど、明らかに外に影響を与えない違いを検出することができてしまう。たぶん、関数なら適切な型の引数に適用すること、帰納的データ型の値ならどのコンストラクタで作られているか調べることといった、まともなことしかできないのは前提なのだろう。

さて、個人的な印象としては、Leibniz equality は任意の述語について成り立つ性質で、なんとなく、Coq の eq より強力に感じられる。eq は本当に Leibniz equality なのだろうか。

確認してみよう。

まず、Leibniz equality ならば eq である、ということを証明してみると、以下のように可能だった。Leibniz equality は任意の述語について成り立つ性質なので、うまく述語を選ぶと、x = y が出てくる。

Lemma L1 : forall (A : Type) (x y : A), (forall (P : A -> Prop), P x -> P y) -> x = y.
Proof.
  intros A x y H.
  apply (H (fun z => x = z)).
  reflexivity.
Qed.

生成された証明を表示させてみると以下のようになる。apply に書いたものがそのまま含まれていてそれっぽい。eq_refl は reflexivity という tactic から出てきたものだろう。 reflexivity のドキュメントによると、reflexivity は apply refl_equal に等しく、 refl_equal は eq_refl の Notation による別記法のようだ。

Print L1.
(*
L1 =
fun (A : Type) (x y : A) (H : forall P : A -> Prop, P x -> P y) => H (fun z : A => x = z) eq_refl
     : forall (A : Type) (x y : A), (forall P : A -> Prop, P x -> P y) -> x = y
*)

逆の、eq ならば Leibniz equality である、というのも証明してみると、これも可能だった。証明の途中のゴールの変化を観察すると、case H で P y が P x に変化する。H : x = y なので、(H は x = y という型の値なので) H という値は eq 型のいずれかのコンストラクタで生成されたはずである。case はコンストラクタの種類で場合分けを行うが、eq のコンストラクタは eq_refl のひとつしかないので、H が eq_refl で生成されたことが判明するだけである。eq_refl で生成されたということは、その値は x = x という型であるはずで、つまり y は x と同じものであることが判明し、Coq はゴールの P y を P x に変えてくれる。その結果、前提にある P x を適用できて、証明を終えられる。こういうふうに Coq が P y を P x に変えてくれるから、任意の述語について成り立つという強力な性質を証明できるということなのだろう。

Lemma L2 : forall (A : Type) (x y : A), x = y -> (forall (P : A -> Prop), P x -> P y).
Proof.
  intros A x y H P Px.
  case H. (* translates the goal P y to P x *)
  apply Px.
Qed.

生成された証明を表示させてみると以下のようになる。case で場合分けしたので、match が生成されている。match で H の場合分けを行うときに、in (_ = y0) で H の型の右辺を y0 で参照できるようにして、return (P y0) で、match 全体の型を P y0 としている。

match の外側の制約としては、P y 型の値を返さなければならない。H の型は x = y なので、y0 で参照できるようにした右辺は y であり、P y0 は P y となるのでこの制約を満たす。

match の内側では、唯一のコンストラクタの eq_refl の場合、H は x = x 型なので、x と y は同じもので、P x を返せば P y を返したのと同じことになる、のだと思う。ここで、「同じもの」というのはどのくらい同じなのかというのが気になる。eq_refl (7-2) という値が 3+2 = 2+3 という型の値であることを上で述べたように、完全に同じ形でなければならないというわけではないらしい。完全に同じ形でない場合も同じと考えるということは、許される違いを検出することは P の中では禁止されているということになるのだろうな。

Print L2.
(*
L2 =
fun (A : Type) (x y : A) (H : x = y) (P : A -> Prop) (Px : P x) =>
match H in (_ = y0) return (P y0) with
| eq_refl => Px
end
     : forall (A : Type) (x y : A), x = y -> forall P : A -> Prop, P x -> P y
*)

いちおう、eq と Leibniz equality が等価であることを証明しておくと、以下のようになる。両方向の証明がすでにあるので、等価 (iff, <->) を split で分解してそれぞれを使うだけである。

Lemma L : forall (A : Type) (x y : A), x = y <-> (forall (P : A -> Prop), P x -> P y).
Proof.
  constructor. (* conj *)
    apply L2.
  apply L1.
Qed.

証明を表示してみると以下のようになる。iff は両方向の証明を and でつなぐだけなので、and のコンストラクタの conj で、上記のふたつの証明を受け取ってひとつの証明にしているだけである。

Print L.
(*
L =
fun (A : Type) (x y : A) => conj (L2 A x y) (L1 A x y)
     : forall (A : Type) (x y : A), x = y <-> (forall P : A -> Prop, P x -> P y)
*)

ところで、reflexivity は apply eq_refl と同じだが、 reflexivity のドキュメントには、t = u で、t と u が convertible であることを検査して、そうであるならばゴールを解決する、と書いてある。

convertible とはなにかというと、マニュアルの 4.3 Conversion rulesに書いてある。β-reduction, ι-reduction, δ-reduction, ζ-reduction, η-expansion で変形して同じ形にたどりつけるもの、のようだ。

たぶん、こういう具体的な手順で定義した関係は、Leibniz equality よりも弱い気がする。つまり、convertible ではないが、どんな述語でも区別できないもの、というものが存在するのではないか。もしそういうものが存在するとすると、それは eq の意味で等しいのだろうか。(なお、変数が入っているもの、例えば a + b = b + a などが convertible でないのはしょうがないので、ここで気になっているのは変数が入っていないものについてである。)

そういうのを具体的に試してみたいと思って考えたところ、Ssreflect の eq_irrelevance を使う例を思いついた。

証明が同じという命題も eq で書くことができる。同じ命題の証明であればどんな方法で証明してあっても気にしないのが普通だが、いろんな証明 (であるところのプログラム) が convertible であるとは限らない。しかし、Ssreflect は特定の形の命題の証明はどんな証明でも eq の意味で等しいという定理 eq_irrelevance を提供している。(これは、Coq 本体の Coq.Logic.ProofIrrelevance とは異なる。こちらは公理を追加する。Ssreflect の eq_irrelevance は公理を追加せず、ただし、特定の形の命題に限定される。)

以下では、1 = 1 という命題をふたつの方法で証明する。

まず、最初は by [] で証明する。これは、Ssreflect の書き方だが、生成される証明は eq_refl 1 であり、reflexivity で証明したのと同じである。

From mathcomp Require Import ssreflect eqtype ssrbool ssrnat.

Lemma L11a : 1 = 1.
Proof.
  by [].
Defined.
Print L11a.
(*
L11a = @Logic.eq_refl nat 1
     : 1 = 1
*)

もうひとつは Ssreflect っぽく、1 = 1 を 1 == 1 に変換してから証明している。まぁ、この場合には証明が複雑になるという以上の意味はない。

Lemma L11b : 1 = 1.
Proof.
  by apply/eqP.
Defined.
Print L11b.
(*
L11b =
(fun _evar_0_ : is_true (1 == 1) => @elimT (1 = 1) (1 == 1) (@eqP nat_eqType 1 1) _evar_0_)
  (eqxx (T:=nat_eqType) 1)
     : 1 = 1
*)

これらの証明が等しいことは、reflexivity では証明できないが、eq_irrelevance で証明できる。

Lemma L11 : L11a = L11b.
  Fail reflexivity.
  by apply eq_irrelevance.
Qed.
Print L11.
(*
L11 = @eq_irrelevance nat_eqType 1 1 L11a L11b
     : L11a = L11b
*)

というわけで、reflexivity では証明できないが、eq である、という例はある。

reflexivity (eq_refl) では証明できないが、eq_irrelevance では証明できるというのは、Check でも確認できる。

Fail Check @Logic.eq_refl (1 = 1) L11a : @eq (1 = 1) L11a L11b.
Check @eq_irrelevance nat_eqType 1 1 L11a L11b : @eq (1 = 1) L11a L11b.

なお、上記の L11a と L11b の証明が Qed でなく Defined で終わっているのは、reflexivity で L11a とL11b を unfold して中身を調べるようにするためである。そうやって調べられるようにしないと、中身が同じであっても reflexivity では証明できなかったからだが、そういう可視性の問題で証明できたりできなかったりするのが上の結論に影響を与えていないかはちょっと心配。

もしその心配が問題ないとすると、eq_refl で作れない値が eq 型の値として認められるということで、それはそれで変な気はする。もしかして、上の心配があたっているのだろうか。

reflexivity では証明できないが、eq であるような、もっと単純な例はないかな。

追記:

Ssreflect をいじって、eqP, eq_refl, introTF, elimTF, elimT, iffP, idP, eqnP を unfold 可能にしたら (Qed を Defined に変えたら)、L11a = L11b を reflexivity で証明できた。

したがって、L11a と L11b は (十分に unfold できれば) convertible ということがわかった。つまり、心配は当たっていた。

うぅむ、変数が入っていなくて eq なものはすべて (十分に unfold できれば) convertible なのではないかという気がしてきた。

2016-12-23 (Fri)

#1 鬼雲の非包含オペレータ

昔、プロシンで発表した、非包含オペレータを鬼雲がサポートしてくれた。けっこう嬉しい。

<URL:https://github.com/k-takata/Onigmo/issues/82>

2016-11-02 (Wed)

#1 整数をkeyにしてみる

とりあえず無駄に利用しているメモリは削るか、ということで、今までは key を文字列にしていたのを、整数にしてみた。

% ./ruby -rPAPI -e '
events = %w[PAPI_L1_DCM PAPI_L2_DCM PAPI_L3_TCM]
evset = PAPI::EventSet.new
evset.add_named(events)
puts "n,l1,l2,l3"
rep1 = 100
rep2 = 100
nn = 1.0
ns = []
while nn < 2e4
  ns << nn.to_i
  nn = nn*1.001
end
ns = ns * rep1
ns.shuffle!
GC.disable
ns.each {|n|
  h = {}
  h[h.size] = true while h.size < n
  l1sum = l2sum = l3sum = 0
  GC.start
  rep2.times {|i|
    k = rand(n)
    evset.start; evset.stop
    evset.start
    h[k]
    evrec = evset.stop
    l1sum += evrec[0]
    l2sum += evrec[1]
    l3sum += evrec[2]
  }
  l1mean = l1sum.to_f / rep2
  l2mean = l2sum.to_f / rep2
  l3mean = l3sum.to_f / rep2
  puts "#{n},#{l1mean},#{l2mean},#{l3mean}"
}' > hash-lookup-cache-intkey.csv

L1 cache miss は以下のようになった。うぅむ、なんですかねこの折れ線は。

hash-lookup-cache-intkey-l1.R:

library(ggplot2)
library(plyr)
d <- read.csv("2016-11/hash-lookup-cache-intkey.csv.xz")
dl1 <- ddply(d, .(n), colwise(mean, .(l1)))
p <- ggplot(dl1, aes(n, l1)) +
  geom_point() +
  scale_x_log10(breaks = 5*2**(0:24)) +
  ylab("mean(L1 cache miss)")
print(p)

hash-lookup-cache-intkey-l1.png

L2 cache miss は以下のようになった。これも折れ線になっている。

hash-lookup-cache-intkey-l2.R:

library(ggplot2)
library(plyr)
d <- read.csv("2016-11/hash-lookup-cache-intkey.csv.xz")
dl2 <- ddply(d, .(n), colwise(mean, .(l2)))
p <- ggplot(dl2, aes(n, l2)) +
  geom_point() +
  scale_x_log10(breaks = 5*2**(0:24)) +
  ylab("mean(L2 cache miss)")
print(p)

hash-lookup-cache-intkey-l2.png

L3 cache miss は以下のようになった。これは曲線のままだな。

hash-lookup-cache-intkey-l3.R:

library(ggplot2)
library(plyr)
d <- read.csv("2016-11/hash-lookup-cache-intkey.csv.xz")
dl3 <- ddply(d, .(n), colwise(mean, .(l3)))
p <- ggplot(dl3, aes(n, l3)) +
  geom_point() +
  scale_x_log10(breaks = 5*2**(0:24)) +
  ylab("mean(L3 cache miss)")
print(p)

hash-lookup-cache-intkey-l3.png

L1/L2 cache miss の折れ線はなんだろうな。周期から考えて、rehash に関係しているとは思うのだが。(最初の rehash の n=80 を含め、rehash の直前で miss が急激に増えているのはどういう理屈なのだろうか。

なお、key を変えても、miss が目立ち始めるサイズはたいして変わらず、理屈と合わないという点に関しては変化は見られなかった。



田中哲