2018-03-17

TaPL読書録 #3

TaPL 技術系日記

前回: hkdnet.hatenablog.com

今回は4章終わりまで。
私物ノートPCのエンターキーがぶっ壊れているため今回のメモは控えめ。

定理3.5.12.

整礎集合の1要素へとマッピングできる関数 f を用いて無限降下列にならないことを示す論法は他の箇所でも見た気がする。

演習3.5.13.

(1) 雑に一意性を損ねること、正規形に関して影響を及ぼさないことがわかればよい。
(2) 1ステップ評価の一意性は損ねるが、多ステップ評価の一意性を損ねないところがミソ。

これは解答の補題とその訳注が面白い。

補題A.1.

ダイヤモンド性について。停止尺度の観点から評価によりかならず停止尺度が下がるのにもかかわらず、s -> t, s -> u において t -> u となるようなことがあるのか疑問に感じて発言した。が、停止尺度として示されていた項のサイズは必ず1ずつ下がるわけではないので十分にありえる話だった。

f:id:hkdnet:20180317144536j:plain

訳注について具体例をもって示す。 E-IFFALSEとE-FUNNY2が同時に成り立つような項について考える。

t2 -> t2' において if false then t2 else t3

E-IFFALSE を用いて評価した場合は t3 E-IFFUNNY2 を用いて評価した場合は if false then t2' else t3 であるがこれは再度 E-IFFALSE を用いて評価することで t3 となる。

これはダイヤモンドではなく、「三角形」であると言える。

f:id:hkdnet:20180317144552j:plain

本では次に数値という概念で拡張する。

prod 0 -> 0 なる評価に意図を感じる。

演習3.5.16.

演習としては行き詰まり状態と wrong が多ステップ評価の元同値であること、すなわち「行き詰まり状態であれば wrong と評価されること」と「wrong と評価される前の項は行き詰まり状態であること」が示せればよい。

演習3.5.17.

こちらも iff であることを示せばよい

演習3.5.18.

E-IF, E-IFTRUE, E-IFFALSE を取り除いて5つの評価規則を追加する。画像参照。
t3の評価を行う評価規則の左辺で t2 ではなく v2 であるところに注意。

f:id:hkdnet:20180317144421j:plain

補題A.8.

f:id:hkdnet:20180317144644j:plain

succ t ->* succ v のときに t ->* v とステップ数が変わってないので「他の項構築子についても同様である」が誤りでないかという指摘があった。のだけど succ の付け外しも評価に含むんじゃねーかなといまは思いつつある。

次回は5章全部。

2018-03-11

どうかくE22とjit

イベント記技術系日記 Ruby

問題: 辞書順に数を並べる 2018.3.3

実装: github.com

とりあえずナイーブに解いたやつ。鍋谷さんは「Rubyでは解けないくらいの計算量にしたつもりだった」と言っていたが案外解けている。

$ ruby -v
ruby 2.6.0preview1 (2018-02-24 trunk 62554) [x86_64-darwin17]

MacBook Retina, 12inch, 2017 1.4GHz Core i7 メモリ16GB

$ time ruby test.rb
ok 1
ok 2
ok 3
ok 4
ok 5
ok 6
ok 7
ok 8
ok 9
ok 10
ok 11
ok 12
ok 13
ok 14
ok 15
ok 16
ok 17
ok 18
ok 19
ok 20
ok 21
ok 22
ok 23
ok 24
ok 25
ok 26
ok 27
ok 28
ok 29
ok 30
ok 31
ok 32
ok 33
ok 34
ok 35
ok 36
ok 37
NG: 0
ruby test.rb  829.58s user 107.90s system 91% cpu 17:05.94 total

jit 版

$ time ruby --jit test.rb
ok 1
ok 2
ok 3
ok 4
ok 5
ok 6
ok 7
ok 8
ok 9
ok 10
ok 11
ok 12
ok 13
ok 14
ok 15
ok 16
ok 17
ok 18
ok 19
ok 20
ok 21
ok 22
ok 23
ok 24
ok 25
ok 26
ok 27
ok 28
ok 29
ok 30
ok 31
ok 32
ok 33
ok 34
ok 35
ok 36
ok 37
NG: 0
ruby --jit test.rb  752.21s user 114.54s system 95% cpu 15:06.41 total

約10%の高速化、な気がする (あまりベンチマークに詳しくない)

別解法を考えた。枝刈りバンバンしていくことでなんとかならないか、というやつ。
そもそも実装がよくわからんけどミスっているのと「xが大きいときにはやくならないですね」という指摘を受けてばたんきゅ〜
n進数なのに木構造を使わなかったのはちょっとダメな気がした。

2018-03-04

Ruby の ! について

技術系日記 Ruby

はいどうも

! メソッド

Ruby における ! ってご存知ですか？
Ruby は演算子っぽいようなものもメソッドとして実装されているという話があったりします。

1 + 1 # Integer の + メソッドが呼ばれている

class Integer
  # 上書き
  def +(other)
    42
  end
end

1 + 1 # => 42

! も BasicObject のメソッドとして定義されています。

/**
 *  call-seq:
 *     !obj    -> true or false
 *
 *  Boolean negate.
 *--
 * \private
 *++
 */

MJIT_FUNC_EXPORTED VALUE
rb_obj_not(VALUE obj)
{
    return RTEST(obj) ? Qfalse : Qtrue;
}
// ...略
    rb_define_method(rb_cBasicObject, "!", rb_obj_not, 0);

class BasicObject
  def !(*)
    raise 'bang dayo-nn'
  end
end

!1
# Traceback (most recent call last):
#         1: from basicobject.rb:7:in `<main>'
# basicobject.rb:3:in `!': bang dayo-nn (RuntimeError)

ところで

クラス内でのメソッド呼び出しについては以下のようになりますよね。

class Foo
  def foo
    bar(1) # Foo#bar への呼び出しになる
  end

  def bar(arg)
    puts arg
  end
end

Foo.new.foo # => 1 が出力される

ということはこれで Foo#! が呼ばれる気がするじゃないですか

class Foo
  def foo
    !(true)
  end

  def !(arg)
    puts '! called'
    false
  end
end

Foo.new.foo # なんもでない
puts 'done'

でもそうはならないんですよね。

なんで？

parseされたときの結果を見ればわかりますが、 ! メソッドのレシーバーは nd_lit: 1 であることがわかります。

$ ruby --dump=parse -e '!(1)'
###########################################################
## Do NOT use this node dump for any purpose other than  ##
## debug and research.  Compatibility is not guaranteed. ##
###########################################################

# @ NODE_SCOPE (line: 1, location: (1,0)-(1,4))
# +- nd_tbl: (empty)
# +- nd_args:
# |   (null node)
# +- nd_body:
#     @ NODE_OPCALL (line: 1, location: (1,0)-(1,4))*
#     +- nd_mid: :!
#     +- nd_recv:
#     |   @ NODE_LIT (line: 1, location: (1,2)-(1,3))*
#     |   +- nd_lit: 1
#     +- nd_args:
#         (null node)

!(1) はメソッド ! 呼び出しの引数が 1 ではなく、(1) (= 1)への ! メソッド呼び出し扱いになるんですね。

parserの気持ちがわからない。
以上、昔この issue を見てよくわかんないなーと思って調べたことの dump です。

github.com

なおこの issue を理解するには更に if + regex literal のときの挙動を理解しておく必要があります。

また if の条件式が正規表現のリテラルである時には特別に $_ =~ リテラル であるかのように評価されます。

https://docs.ruby-lang.org/ja/2.5.0/doc/spec=2fcontrol.html#if

補足

Ruby の動作は ruby 2.6.0preview1 (2018-02-24 trunk 62554) [x86_64-darwin17] 、
CRubyのソースコードは ac44ae58c697971e14e72493da2cfdd9a4e3b458 時点のものを基準としています。

2018-02-23

ランダム性は心の弱さ -- Rails においてテストデータをランダムに作ることについて

Ruby 技術系日記

お気持ち

やめよう

何がおきたか

単純化するとこんな感じのコードがあって爆死した¹。

describe Foo do
  let(:left_foo) { Foo.new(value: 1000, bar: left_bar) }
  let(:left_bar) { BarMaster.all.sample }
  let(:right_foo) { Foo.new(value: 100, bar: right_bar) }
  let(:right_bar) { BarMaster.all.sample }

  it { expect(left_foo).to > right_foo } # left と right の bar が同じであるケースのとき落ちる
end

あるいはこんなでもいい

describe Foo do
  let(:left_foo) { Foo.new(value: rand(100)) }
  let(:right_foo) { Foo.new(value: 0) }

  it { expect(left_foo).to > right_foo } # rand(100) の値域が 0..99 なので 0 を引くと落ちる
end

なぜ避けるべきか

テストというのは書けばよいものではない。動作を担保し、オブジェクトに対する期待を明らかにするものである。
どのデータでも通ることを期待するならすべてのデータについてテストを回すべきだし、そうでないならそのテストで期待するものを満たす最小限のもので回すべきだ。
テストパターンにおけるランダム性の導入は、そうした最小の期待への考慮を放棄している、あるいは対象を正しく理解できていないように感じられる²。
なお QuickCheck のようなものを否定するわけではない。しかし QuickCheck のようなものは仕組みとして提供されるほうが望ましく、 Rails アプリケーションにおいてそのようなテストフレームワークを使っているのは稀だと思う。というか例があるなら聞きたい

実際には request spec がこのように書かれており、request spec で何を担保するのかというところが曖昧なようにも見えた。

お気持ち再掲

ランダムなデータにするのはやめて代表値を選んで使おう。

ほんとによくわかってないので質問しますが、テストにおいてマスタのデータがどれでもいいからって `foo_masters.sample` とかでランダム性をいれるのってメリットあります？
— はくどー (@HKDnet) 2018年1月26日

テストで何を担保するべきかが判断できないから「マスタからランダムに選んじゃおw」って気持ちになるんだと思っています
— はくどー (@HKDnet) 2018年2月19日

業務で出会ったコードで業務臭を消して単純化するのは難しい↩
個人の感想です↩

2018-02-18

TaPL読書録 #2

TaPL 技術系日記

hkdnet.hatenablog.com

引き続きTaPL読書録です。今回は3.4.まで。

この項の構文は succ true や if 0 then 0 else 0 のような怪しげな項の形成を許すことに注意されたい(p.18)

怪しげw
「型なし算術式」なのでこの手のものを許可せざるを得ない。
評価のところまですすめたとき、評価の左辺(辺か？)にマッチせず捨て置かれることがわかる。

... この定義は複合的な部分式に付ける括弧の使用について何もいっていない(p.19)

else のない if などが導入された場合に曖昧性が出始める、とのこと。

定義3.2.3.

演習3.2.5. より、 lim のような記法が定義されていれば i -> ∞ における S_i が S と一致するはずだがそのような記法が導入されていないので和集合をとる記法になっているのかな？という話が出た。

補題3.3.3. 証明 tの深さに関する帰納法を用いる。

深さなのだろうか？ size に関する演算が多く、サイズに関する帰納法なのでは？という指摘があったが、おそらくこれは深さに関する帰納法で正しい。「t = succ t1 を満たす t, t1 において depth(t) > depth(t1) が常に成立する」ということを暗黙的に用いて帰納法を用いている、と解釈した。

定理3.3.4. 証明(演習)

しれっと演習がまじっていて気づいていない人もいた。
基本的には補題3.3.3.の証明と同じ形式で進めればよい。のだが、基底部のケースがちょっと不明瞭……

https://github.com/hkdnet/tapl-exercise/blob/master/Ex3.3.4.md#s-%E3%81%8C%E5%AE%9A%E6%95%B0%E3%81%AE%E5%A0%B4%E5%90%88

例えば述語 P を iszero とおくと iszero 0 は true であるが、iszero true や iszero false は評価できないので成り立たない¹。
しかし、s = true, false, 0 のとき depth(r) < depth(s) なる r は存在しないため、仮定法で用いる命題は成立するので、なにかおかしい気がする……。
定数群に対して必ず成り立つ述語でないといけないのかな？

この定理がどう役に立つのか？全てに成り立つ性質が示せて嬉しいか？という疑問も出た。おそらく、今後拡張が進むなかで定数部にxを含まないときにはこの性質が示せるがxを含むときには示せない、みたいな使われ方をするのでは？という話になった。

...書き出された証明を確認するより簡単である(p.23)

原文でも easier と書かれていることを確認した。

表示的意味論にとっての鬼門は... (p.24 †3)

鬼門は原文では "bête noire"だそうで。 https://ejje.weblio.jp/content/b%C3%AAte+noire

項 if true then (if false then false else false) else true) はif true then false else true` には評価されない(p.26)

if true then t1 else t2 でt1, t2から評価する規則はなく、E-IFTRUE のみしか使えないということを言っている。

次回は4章の終わりまで。

true に評価されないならば成り立たない、でいいよね？↩

2018-02-11

入社していくらか経ったので自分がどんな価値を出してたのか確認したよ

はいどうも。入社してから7ヶ月くらい経ってるんですが、俺って何したんだっけ？どういう価値を提供したんだっけ？というのをふと確認したくなったので確認しました。今回はそれを外に出せる部分だけ出しておこうと思います。

業務中にメインで使っているレポジトリは1つなので¹ざっとPRのタイトルを抜き出して分類してまとめました。
定期的に振り返るとか苦手でまとめてざっと傾向見るくらいがちょうどいいのかもという試みです。

ざっと集計したところ404PR作っていたそうです。うちマージされなかったのが23個。マージされてないのは、POC的に「こんなんどう？」って出したあとで閉じたり、CI落ちてる原因を確かめるために試行錯誤してたり、書いてみたけどやっぱ微妙で大幅な方針転換が必要だったりという感じです。

f:id:hkdnet:20180211215917p:plain

Release っていうのはリリースするのに必要なものであったり、masterの変更をマイルストーンにマージしたりみたいなそういうやつなので実質あんまりなんもしてないやつです。²

Wording は文言変更とか、なんかちょろいの全般。Fix がバグ修正で Feature が機能追加っぽいやつです。動作が変わらない系は、Refactoring はリファクタですが、テスト追加のみだとSpecっていう分類にしてます。Disposedは上述の捨てられたやつ³。Others は、gem update とかそういう分類しにくいやつです。

Feature は8-11月くらいにやってたんですが、25%あっておもったよりも多いですね。最近バグ修正とかが多めだったから実際より少なめに見積もってたのかも。このへんを深くみるために月次で分けました。

f:id:hkdnet:20180211220517p:plain

日付はマージされた日で見ています。9999/12はDisposedです⁴。

10月は新機能開発の追い込みで頑張ってた感じが見て取れますね。1月とかはRelease系が多いですね。
Fix系が増えてくるとだいたい調査とかであーうーとか唸っている時間が多くなるので、機能追加の終盤である(= 考えることが少なめである)10月の機能開発よりPR数が減るんでしょうか。確かに最近は調査で頭を抱えてる時間が長かったような気もします。

これ以外に、(公開はできませんが)この機能追加した、こういうの直したみたいなリストも作っています。給与とかが決まるような1 on 1のときとかに使えるとアピールするのに便利かなーという気持ちで継続的に整備していこうかなと。

話は変わって集計方法について。

今回は適当にgolangで抜いてきたのをプレーンテキストにして google spreadsheets でタグ付けしてました。でもこういうのって時々やりたくなるんでなんかフレームワーク化というか、汎用的にできたらなーと思ってぺちぺち改良をしようとしています。

上のを抜いてきたときのバージョンではないですが一番それっぽかったときの gist を貼っておきます。

main.go · GitHub

interfaceとかを定義していろいろ可変にしたそうな雰囲気が感じられますね。またこのプロジェクトに進展があったらブログで紹介しようと思います。

他レポジトリも読んだりはするけどPRはたぶん片手(10進法)で数えられる程度しか送ってない↩
デリバリーをなんもしてないというとアレなんだけど、まあ難しくないし、僕がやらなくても誰かやるし……。面倒事を率先してやっているとは言えるかもしれない(55PR)↩
あまり正しい英語ではない気がしている↩
マージされずに閉じられているのだけど空欄にするとソートがアレだったので↩

2018-02-04

オフラインリアルタイムどう書くE21 に参加して負けてきました

イベント記技術系日記 Ruby

yhpg.doorkeeper.jp

負けました。敗因はなんだろ……。方針が定まりきらなかったのが敗因なのかなー。

プレイヤーベースで考えると打ったときに、そのタイミングでアタリを引いたのか、次のターンでアタリを引いたのかの場合分けがめんどくさそうだなーと思いつつ、じゃあどうするんだろー、という感じ。
今回は平行世界をたくさん用意して、リボルバーのタマの詰め方を全通り作って、アタリを引いた人と一致するパターンが正解ということにしています。
無限ループに入ってるかどうかは雑に何周したかをカウントして、まわりすぎだったら終わるって感じでやってます。

引っかかったのは、playerのidxとidで番号が1つズレているのでそれの管理ミスと、残弾数がズレてるケースを削るのを忘れてるとかそのへん。

コミットしてなかったので当時の状態がわからないけど最終形はこんな感じでした。

misc/solver.rb at master · hkdnet/misc · GitHub

勝てなさそうな印象の割にがんばれたけど負けてて悔しいですね。しょんぼり