天泣記

2015-01-27 (Tue)

順列組み合わせについてもけっこう悩んだ。ふたつのリストが順列組み合わせの関係にあるという Permutation という述語は以下のように定義される。

Inductive Permutation : list A -> list A -> Prop :=
| perm_nil: Permutation [] []
| perm_skip x l l' : Permutat|on l l' -> Permutation (x::l) (x::l')
| perm_swap x y l : Permutation (y::x::l) (x::y::l)
| perm_trans l l' l'' : Permutation l l' -> Permutation l' l'' -> Permutation l l''.

空リストと空リストは順列組み合わせ (perm_nil)、順列組み合わせとなっている l, l' があったときに先頭に同じ要素を前置したものは順列組み合わせ (perm_skip)、長さ2以上のリストで、先頭の2要素をひっくり返したものは順列組み合わせ (perm_swap)、推移律 (perm_trans)

これらで生成されるものが順列組み合わせであることは明らかなのだが、すべての順列組み合わせがこれらで生成できるというのは納得できなかった

納得するまでにけっこう時間がかかったのだが、こういうことだろう。

先頭要素が異なるリスト a::l と b::l' が順列組み合わせなら、l の中には b が入っているはずで、そうすると l と b::l'' が順列組み合わせになるように l'' を選べる。そうやって選んだ l'' を使うと、perm_skip により a::l と a::b::l'' は順列組合わせ。a::b::l'' と b::a::l'' は perm_swap により順列組み合わせ。a::l'' と l' は順列組み合わせのはずなので、perm_skip により b::a::l'' と b::l' も順列組み合わせ。だからひとつ短いリストの順列組み合わせの関係に帰着できる。

ここで、「はず」というのが 2回でてくる。l と b::l'' および a::l'' と l' の順列組み合わせの関係は、リストの長さがひとつ短いものに対する関係なので、帰納法みたいな感じで仮定してよい。というか、これはリストの長さに関する帰納法をやっているわけだよな。

#1 Coq の False

最近、少し Coq を勉強していて、False について納得するのに困難を感じていた。

悩んでいた話を忘れる前に書いておこう。

False は矛盾を表現する命題である
命題と型、証明とプログラム (型つきラムダ計算の項) が対応しているというカリー-ハワード同型対応という関係が知られている
False は命題なので型でもある
Coq で False は Inductive False : Prop :=. と定義されている。これはコンストラクタが存在しない代数的データ型である
コンストラクタがないので、値はない (値を生成することはできない)
矛盾から任意の命題が導けるという命題は、False 型を受け取って A 型を返す関数型 (False -> A) に対応する
False -> A を Coq で証明すると次のプログラムが生成される
```
fun (A : Prop) (H : False) => match H return A with end : forall A : Prop, False -> A
```
これは False 型の引数 H を受け取って、A 型を返す関数である。この関数が存在することによって False -> A が証明されたことになる
match 式の with と end のあいだには各コンストラクタに対応して分岐する節が入るが、False にはコンストラクタがないので空になっている
match 式自体の型は A とされているが、それと矛盾するものはなにもない (分岐がひとつもない) ので問題はない
そんな分岐がない分岐は実行できないし問題大有りだろうと感じるわけだが、そもそも False 型の値は存在しないので、引数を用意できず、この関数を呼び出すことはできないのでやっぱり問題はない
また、False は矛盾なので、証明できないはずである。False を証明しようとすると、False 型のプログラムを生成することになる。それはできちゃうんじゃないの、と最初思ったのだが、結局はできないっぽいのが感じられるようになった。まずコンストラクタはないので使えない。上のように任意の命題を導くことができるケースでは (A に False を割り当てることにより) False 型を生成できるが、それはもともと False 型の引数があるからで、矛盾から矛盾を導けるのは問題ない (False 型の引数がないのであれば、空の match 式は使えない)

2014-12-27 (Sat)

#3 端末における反転の使い方

結局、端末で反転 (文字の背景をデフォルトではない色にすること) はとても目立つため、いちばん目立ってほしいところに使うのは問題ないけれど、それ以外の場所に使うと（とくに使いすぎると）そっちが目立ってしまってよろしくない、という話なのだろう。

#2 test-unit の色の改善

と、書いたら、すとうさんがかなり直してくれて、以下のようになった。

ここで目立っているものは以下の順だろう。

最後のサマリ行
失敗した行
Failure

最後のサマリの行はユーザから見るといつもそこにあるので、ここまで目立たなくてもいいと思う。

失敗した行と Failure はどちらも失敗と対応している。どちらかが十分に目立てば、もっとも目立つものと失敗が対応することになる。

すとうさんは実際に失敗したところが気になるということなので、失敗した行のほうが目立つのは理にかなっているのだろう。

というわけで、その意図を進めるのであれば、サマリ行と Failure をもうちょっと目立たないようにするのがよいのではないか。

#1 test-unit の色の使い方はよくない

Ruby 2.2 から、(Ruby の外部で) require 'test/unit' とすると gem の test-unit が使われるようになって、しばらく使っていたのだが、どうも出力から素早く情報を読み取れない。

最初は慣れていないせいかな、と思っていたのだが、時間がたっても相変わらずで、これはたぶん出力が良くないのだということで、すこし真面目に考えてみた。

以下のテストを考える。

% cat tst.rb
require 'test/unit'

class C < Test::Unit::TestCase
  def test_a
    assert_equal(1, 2)
  end

  def test_b
    assert_equal(1, 1)
  end

  def test_c
    assert_equal(1, 3)
    raise
  end
end

これを Ruby 2.1 と Ruby 2.2 で比較してみた。

出力からまず読み取れる情報はまず個々の文字よりも大きな形や色である。というわけで、出力をぼかしてみてみよう。

Ruby 2.1 では以下のような結果になる。

Ruby 2.2 では以下のような結果になる。

これからいくつかのことがわかる。

Ruby 2.2 のほうが出力が大きく、大きな画面 (あるいはスクロール) を必要とする
Ruby 2.1 では、もっとも目立つのは赤い部分で、これは2箇所あり、2つの失敗と対応している
Ruby 2.2 では、もっとも目立つのは赤の長い横線で、これは5本あり、2つの失敗とは対応していない
Ruby 2.1 も Ruby 2.2 も色の使い方は赤と緑の組み合わせで、もっとも多い色覚異常にとって識別性がよくない

テストが失敗した時には、たいていの場合、結局はぜんぶ直すわけだが、どのテストから直すかという選択は必要で、そのためにそれぞれの失敗を眺めることになる。そのときに、個々の失敗をすばやく認識できるとありがたい。Ruby 2.1 ではもっとも目立つ部分が失敗と対応していてそれが容易だったが、Ruby 2.2 ではもっとも目立つ部分は失敗と対応しなくなっていて、これはよくないと思う。結局のところ、テストの結果の表示は、失敗の並びなので、もっとも目立つ構造を個々の失敗が対応していないというのは結果の構造の認識を困難にしている

思うに、色の使い方はずいぶんと改善の余地があるのではないだろうか。

なお、ぼかさない結果は以下のようになる。

これをみると、Ruby 2.2 で出力が大きいのは、失敗した場所のソースを表示していること、予期された結果と実際の結果を 2回 (... expected but was ... と diff で) 表示しているのが原因である。

ソースの表示は、役に立つこともあるだろう。

結果を 2回表示しているのは、このケースではほぼ同じ情報を 2回表示しているだけで役に立っていない。役に立つ場合もあるのだろうが、役に立たない場合は表示しないでくれるとよいのだが。

考えた結果、個人的にもっとも気に入らないのは色の使い方で、失敗をすばやくみてとるのに不適切ということだと感じられる。

2014-12-12 (Fri)

もしかすると、Ruby に16進小数を入れても実際的な非互換性は生じないのかもしれない。

16進小数というのは 0x123.456 みたいなものである。

16進なので a-f も使えて、0xabc.def みたいなこともできる。

16進小数の利点は、浮動小数点数を正確かつコンパクトに表現できることである。IEEE754 の浮動小数点の仮数部は 2進数なので、これを桁を合わせて 16進にしたものが 16進小数で、浮動小数点数を正確に指定したいというときに役に立つ。

ここで問題になるのが、現在 0xabc.def は 0xabc という整数 (2278) に対する def メソッドの呼び出しとして解釈されるので、これを 16進小数として解釈する (0xabcdef / (16**3).to_f つまり約2748.8708) と、意味が変わってしまうので非互換になる、という点である。

この非互換性は実際に問題になるだろうか。

まず、現在 Integer クラスには 16進数に使える文字 ( 0-9a-fA-F に加えて区切りの意味で _ も使える) だけで構成されているメソッドは存在しない。

% ruby -e 'p Integer.instance_methods.reject {|n| /\A[0-9a-fA-F_]+\z/ !~ n.to_s }'
[]

しかし、Ruby では既存のクラスにメソッドを付け加えることができる (オープンクラス) ので、もしかしたら既存のコードが付け加えて使っているかもしれない。

そこで、既存の gem を全文検索してちょっと調べてみる。(1ヶ月くらい前に gem mirror して得た gem の各最新版を展開して milkode で全文検索できるようにしてある。)

% gmilk -s rb 0x|egrep '0x[0-9a-fA-F_]+\.[a-fA-F_][0-9a-fA-F_]*([^0-9a-zA-Z_]|$)'
Because number of records is large, Milkode use external tool. (Same as 'gmilk -e grep')
/extdisk/akr/ruby/rubygems/latest-gems/gnu_mpc-0.9.0/spec/atan_spec.rb:107:    expect(actual.imag).to eq GMP::F.new("-0x8.a7e33db93ecf18@-34", 57, 16)
/extdisk/akr/ruby/rubygems/latest-gems/metasm-1.0.1/tests/preprocessor.rb:263:              t_float['0x1.e4']

ひっかかったのは文字列の中だけなので、どうやら、16進小数とみなしうるコードは既存の gem の中にはないようである。

また、Ruby 2.1 から数値には i (虚数) と r (有理数) という suffix がつけられるようになったが、これらは a-f の範囲外なのでこれも衝突しない。

これは使えるようにしちゃってもいいのかもしれない。

2014-11-30 (Sun)

#2 Casuistry

読んだ後、検索していて、トゥールミンの議論モデルの変容 --- 批判から寛容へ --- を見つけて読んだ。これもおもしろい。

トゥールミンの新しい著作で、モデルから裏付けがなくなっているのはなぜか、という話。

ある推論規則が適用可能であることに合意するためには、裏付けが論拠を正当化することを合意しなければならず、それが受け入れられなければ合意できない、という状況ばかりではない、という話だと理解した。

ものごとの見方・考え方が異なるひとは、裏付けと論拠の関係を合意することは無理なことがあり、それでも合意を行うにはどうしたらいいか。

そういうひとでも個々の典型的な状況については合意が可能な場合、微妙な状況についての合意は無理でも、典型的な状況について一般化された合意は可能という話だと理解した。この合意は裏付けと論拠の関係について合意したわけではないが、それでも合意の一種ではある。

で、その方法が Casuistry というものらしい。(日本語だと決疑論)

しかし、そもそもなんで裏付けを共有していないのに典型的な状況について合意が可能なのか考えると、この話が医療倫理あたりの話からきているからかな。そのあたりは、もともと個々の事例から (直接に、あるいは文化などを経由して) 個人の倫理が作られるだろうから、典型的な事例についてはその良し悪しは個人に依存せずに決まる、つまり、個人がどのような裏付けをもとに判断しているかには依存しないのだろう。

#1 トゥールミンの「議論の技法」

最近、トゥールミンの「議論の技法」を読んだ。

ふつうの主張や議論は、論理学では扱えない話のほうが多い、ということを延々と書いてある、という感想を持った。

論理学では前提から結論を導く方法を論じているわけだが、現実で問題になるのはそもそも前提が正しいかどうかだ、という話。

論理学で要求されるような完全に正しい前提は、とくに「すべての X は Y」というような形(全称)の推論規則については現実世界にはほとんどない、ということが主張されていたように思う。

まぁ、たとえば「すべての人間は死ぬ」とかでもこれが論理学の意味合いで正しいということをいうのは難しい。

この規則についていえば、正しいということはいえないけれど、だいたいのひとにとってはこれを納得するのは簡単だ。だから、納得したひと同士であれば、「ソクラテスは人間である」「すべての人間は死ぬ」というふたつから、「ソクラテスは死ぬ」という結論を得て合意することができる。

もちろん、「ソクラテスは人間である」というほうも納得しないといけないけれど、そちらは全称でないため難しくない。

一般化すると、ある主張に使われている前提を受け入れている人とは合意が可能だ、ということになる。

全称の推論規則はかならずしも全員が納得するかどうかは難しい場合もあるので、これを分解して推論規則自体(論拠W)と、それが正しいと思われる理由(裏付けB)に分割して、その違いを意識するように強調している、というのがトゥールミンモデルかなぁ、と思った。(推論規則が完全ではないため結論も完全ではなく、「だいたい」などといった限定Q と、結論が成り立たない例外Rも必要になる。)

「すべての人間は死ぬ」という推論規則の裏付けは... 生きている人間はたくさん居るので、(人間が絶滅するまでは) すべてのケースについて正しいということは確認できない。それなのになぜ納得できるのか考えてみると「200歳まで生きた人間の記録がない」とか「不死を求めた権力者も結局死んでいる」とか、そういうあたりかなぁ

2014-10-24 (Fri)

#1 Hash.new の集計

Hash.new はどのように使われているのか

% time gmilk -a 'Hash.new' |sed 's/^.*Hash.new */Hash.new /'|sort|uniq -c|sort -n|tail -100
Because number of records is large, Milkode use external tool. (Same as 'gmilk -e grep')
     26 Hash.new { |h,k| h[k] = h.length }
     26 Hash.new {|h, k| h[k] = [] }
     26 Hash.new {|h, k| h[k] = {}}
     26 Hash.new {|hash, key| hash[key] = lambda {|entry| CoercibleString.coerce(entry)}}
     27 Hash.new (hash)
     27 Hash.new (self, env, @default_options)
     27 Hash.new { |hash, key|
     27 Hash.new { |hash,key| hash[key] = {} }
     28 Hash.new ) { |row| ... }
     28 Hash.new { |h,k| h[k] = '' }
     29 Hash.new ("ETag" => 'HELLO', "content-length" => '123')
     29 Hash.new (*args)
     29 Hash.new (0) }
     29 Hash.new (false)) do |methods, attr|
     29 Hash.new , pirate.changes
     30 Hash.new ()
     30 Hash.new , node.attributes
     30 Hash.new { |h,k| h[k] = Mutex.new }
     30 Hash.new }.should raise_error(ArgumentError)
     31 Hash.new (header)
     32 Hash.new (false).update(
     32 Hash.new ;
     33 Hash.new ) }
     34 Hash.new ("default")
     34 Hash.new (self, env)
     35 Hash.new (0)]
     35 Hash.new { |hash,key| hash[key] = [] }
     36 Hash.new ({
     36 Hash.new { |h, k|
     37 Hash.new (0)) { |h,part| h[part.first] += part.last; h }
     37 Hash.new ]
     37 Hash.new { |h, k| h[k] = Array.new }
     37 Hash.new {|h,base|
     38 Hash.new { |h, k| h[k] = Set.new }
     39 Hash.new (0.0)
     39 Hash.new { |h, k| h[k] = Type.new(k) unless k.blank? }
     42 Hash.new { [] }
     43 Hash.new { 0 }
     43 Hash.new { |h,k| h[k] = 0 }
     43 Hash.new { |h,pid| h[pid] = {} }
     44 Hash.new (1)
     44 Hash.new (self)
     44 Hash.new do |hash, key|
     44 Hash.new {|h,k| h[k] = 0}
     46 Hash.new (nil)
     46 Hash.new , &block)
     46 Hash.new {|hash,key| hash[key.to_s] if Symbol === key }
     47 Hash.new ("foo" => ["bar", "baz"])
     47 Hash.new (output)
     48 Hash.new ("")
     48 Hash.new {|hash, key| hash[key] = []}
     50 Hash.new (Codepoint.new)
     50 Hash.new .tap do |hash|
     50 Hash.new Hash(getRuntime());
     53 Hash.new ("Foo-Bar" => "baz")
     54 Hash.new { |h,k|
     56 Hash.new (default)
     56 Hash.new do |h, table_name|
     58 Hash.new ("Content-MD5" => "d5ff4e2a0 ...")
     58 Hash.new unless defined?(@_cycles)
     59 Hash.new (default).merge!(self)
     60 Hash.new ([]))
     60 Hash.new (default).merge(self)
     63 Hash.new { |hash, key| hash[key] = {} }
     65 Hash.new { |hash, key| hash[key] = Array.new }
     66 Hash.new (
     67 Hash.new (0)
     67 Hash.new { |h, k| h[k] = 0 }
     69 Hash.new { |h, k| h[k] = k.chr }
     75 Hash.new { |h,k| h[k] = Array.new }
     76 Hash.new {|h,k| h[k] = {}}
     84 Hash.new ('')
     95 Hash.new ({})
     99 Hash.new { |h, k| h[k] = {} }
    102 Hash.new {|h, k| h[k] = []}
    103 Hash.new do |h, k|
    108 Hash.new , params
    119 Hash.new Hash(runtime);
    121 Hash.new ,
    126 Hash.new do |h,k|
    133 Hash.new {|h,k| h[k] = [] }
    136 Hash.new (false)
    139 Hash.new 0
    144 Hash.new ([])
    160 Hash.new ("foo" => "bar")
    162 Hash.new do |hash, region|
    162 Hash.new do |region_hash, key|
    261 Hash.new (headers)
    262 Hash.new { |hash, key| hash[key] = [] }
    285 Hash.new { |h,k| h[k] = {} }
    308 Hash.new {|h,k| h[k] = []}
    429 Hash.new ()
    448 Hash.new { |h, k| h[k] = [] }
    789 Hash.new { |h,k| h[k] = [] }
    827 Hash.new
   1015 Hash.new }
   1038 Hash.new do |hash, key|
   1220 Hash.new )
   1672 Hash.new (0)
  17878 Hash.new
gmilk -a 'Hash.new'  1.42s user 0.20s system 98% cpu 1.645 total
sed 's/^.*Hash.new */Hash.new /'  0.10s user 0.00s system 6% cpu 1.644 total
sort  0.14s user 0.00s system 8% cpu 1.782 total
uniq -c  0.00s user 0.01s system 0% cpu 1.782 total
sort -n  0.02s user 0.00s system 1% cpu 1.799 total
tail -100  0.00s user 0.00s system 0% cpu 1.798 total

Hash.new { |h,k| h[k] = [] } がとても多いな。

2014-10-22 (Wed)

#1 メソッドチェーンの集計

どのようなメソッドのチェーンが多いだろうか。つまり、obj.m1.m2 というような呼び出しで、m1 と m2 の組み合わせは何が多いだろうか。

というわけで調べてみた。Ripper.sexp で構文木を取り出して、そのような式をてきとうに (完璧を目指さずに) 取り出すのは以下のように簡単にできる。

% cat extract-call-seq.rb
#!/usr/bin/ruby

# usage:
#   extract-call-seq.rb file.rb ...

require 'ripper'

def method_call_name(tree)
  if tree.is_a?(Array) &&
     tree[0] == :call &&
     tree[3].is_a?(Array) &&
     tree[3][0] == :@ident &&
     tree[3][1].is_a?(String)
    n = tree[3][1]
    n.sub!(/\A\s*\./, '') # [ruby-dev:48684] [Bug #10411]
    if /\A[a-z_A-Z][a-z_A-Z0-9]*[!?]?\z/ !~ n
      warn "unexpected method name: #{n.inspect}"
    end
    n
  else
    nil
  end
end

def check(tree)
  meth2 = method_call_name(tree)
  if meth2
    meth1 = method_call_name(tree[1])
    if meth1
      puts "#{meth1} #{meth2}"
    end
  end
end

def extract(tree)
  return unless tree.is_a? Array
  check(tree)
  tree.each {|elt|
    extract(elt)
  }
end

def main
  STDERR.puts ARGV.inspect
  ARGV.each {|fn|
    STDERR.puts fn.inspect
    extract(Ripper.sexp(File.read(fn)))
  }
end

main

各 gem の最新版を展開してあるので、そこにある *.rb なファイル全部に適用して集計すると上位100個は以下のようになる。いくつかコメントもつけてみた。

367550 u normalize            なんか機械生成されたコードみたい
 27444 size should            rspec の類ですかね
 25358 class name             クラスの名前を使うのはよくわかる
 20018 name should            rspec
 16083 should be              rspec
 15603 to_s should            rspec
 13568 length should          rspec
 13178 body should            rspec
 11638 count should           rspec 多すぎ
 11395 to_s gsub
 10983 now to_i               Time.now.to_i だとすると、これは使ってほしくないんだけどなぁ
  9990 class to_s
  9241 class should           rspec
  8884 should not             rspec
  8600 to_s split
  8479 keys each              Hash なら each_key もあるけど、破壊的変更が必要なときに hash.keys.each を使うこともあるのはわかる
  8295 to_s downcase
  7918 compact join
  7744 interval end
  7657 class new
  7579 status should
  7495 endpoint const_get
  6863 to_s upcase
  6667 value should
  6590 once with
  6584 last is_a?             引数の最後が Hash かどうかの検査とか?
  6538 now utc
  6429 keys sort
  6222 backtrace join
  6164 routes draw
  6116 sort each
  5900 should raise
  5884 any_instance expects
  5791 name to_s
  5611 id should
  5597 first should
  5560 to_s strip
  5481 first name
  5340 errors on
  5313 message should
  4917 to_i to_s              整数の文字列ってこんなに使うのだな
  4831 flatten compact
  4704 first is_a?
  4699 new tap
  4642 sort should
  4349 any_instance stub
  4339 should equal
  4338 downcase to_sym
  4315 keys first
  4270 now to_f
  4251 keys include?
  4229 now strftime
  4005 type should
  4001 text should
  3968 elements each
  3952 title should
  3865 any_instance stubs
  3811 flatten each
  3766 to_s sub
  3756 root join
  3743 id to_s
  3716 application config
  3665 be ok
  3646 sort join
  3642 values first
  3466 first id
  3454 application routes
  3424 to_s empty?
  3414 children first
  3326 once and_return
  3313 to_s camelize
  3304 path should
  3269 sql should
  3268 first to_s
  3266 keys map
  3062 to_s underscore
  3049 to_a should
  3030 be nil
  2987 errors full_messages
  2986 name underscore
  2970 strip empty?
  2963 children each
  2914 errors add
  2904 name split
  2838 sqls should
  2830 name to_sym
  2824 url should
  2800 flatten map
  2794 to_s capitalize
  2793 values each
  2793 class send
  2784 flatten uniq
  2780 logger debug
  2779 should match
  2762 any_instance should_receive
  2740 string should
  2738 all should
  2722 keys join
  2694 all each
  2671 not be

うんまぁ rspec は多いですね。

そういえば、all_symbols がどう使われているのかという話が前に (開発者会議で) あったな。

24 all_symbols count
10 all_symbols map
 8 all_symbols collect
 4 all_symbols size
 3 all_symbols select
 2 all_symbols sort_by
 2 all_symbols length
 1 all_symbols should
 1 all_symbols is_a?
 1 all_symbols clone
 1 all_symbols all?

数を数えることが多いというのはわかる。

天泣記