delirious thoughts

by Kentaro Kuribayashi

ペパボのエンジニアたちとランチしながら「ペパボってぶっちゃけどうよ?」って話せる取り組みを始めます

エントリー前に社内の雰囲気を知ってもらうための新たな取組み、『ペパランチョン』制度を開始いたしました! | お知らせ | ニュース | GMOペパボ株式会社」というわけで、エンジニア採用における新しい取り組みを始めました。

 GMOペパボでは、エンジニア中途採用に興味のお持ちの方を対象に、採用制度における新たな取組み『ペパランチョン』を開始いたしました。

『ペパランチョン』は、求人媒体やWebサイトだけではなかなかお伝えすることが難しい社内の雰囲気や社員の働き方を、エントリー前に知っていただくための制度です。

「ペパボのエンジニアってどんな技術に興味があるの?」「“もっとおもしろくできる”ってどんなことやるの?」などのエントリー前に頭に浮かぶ素朴な疑問に、ペパボエンジニア社員が一緒にランチをしながらお答えいたします。

ペパボのエンジニア採用に興味をお持ちの方は、ぜひお気軽に『ペパランチョン』制度をご利用ください!

というわけで、ペパボに少しでもご興味のある方は是非コンタクトください。

2014年9月に読んだ本をブクログでふりかえる

今月は19冊。

高橋伸夫『殻―脱じり貧の経営』を読んで、その主張するところ自体にも感銘を覚えつつも、ENIACまわりの、明らかに自分の趣味だろという詳細な話に刺激されて、古い計算機・ソフトウェアへの興味が再燃してしまった。そのあおりで『コンピューター200年史―情報マシーン開発物語』などを読んだり、古書をあれこれ買い集めたりした。面白い。

そんな折、『アンダースタンディング コンピュテーション―単純な機械から不可能なプログラムまで』をいただいたので早速読んだところ、これまでなかなか理解できなかった計算理論(それもまた、上記の計算機たちと同じ時代の産物だ)についてなんとなくわかった気がして、とてもよかった。そのあたりは書評に書いた

藤村龍至さんの初の単著『批判的工学主義の建築:ソーシャル・アーキテクチャをめざして』は、超線形プロセスの頃からさらに発展を続ける思考・実践について、状況に対する認識と著者の問題意識の深化とともにまとめて読めてよかった(それぞれについてはあちこちで散発的に読んだ内容ではあったものの)。

その他、『目玉焼きの黄身 いつつぶす?』はあんまり期待せずになんとなく読み始めたらすごく面白くて得した気分がしたし、『ビジネスモデル全史』は前作の『経営戦略全史』に続いて大量の情報が要領よく紹介されていてよかったと思う。

kentaroの本棚 - 2014年09月 (19作品)
のりりん(9)
鬼頭莫宏
読了日:09月28日
評価3

powered by booklog

型システムの意義(TAPL第1章より)

『アンダースタンディング コンピュテーション』に続いて、『型システム入門―プログラミング言語と型の理論』を読む。

型システムの定義

システムが仕様通りに動作するかどうかを保証する形式手法と呼ばれるものにはいろいろあるけど、利用が難しい。もっと簡単に使えるような軽量形式手法として普及しており、確立されてもいるのが型システムである。

型システムとは、プログラムの書く部分を、それが計算する値の種類に沿って分類することにより、プログラムがある種の振る舞いを起こさないことを保証する、計算量的に扱いやすい構文的な手法である。

(本書 p.1より)

型システム(型理論)には、論理学・数学におけるいろんな理論からの流れもあるけど、本書では、上記の定義にある通り、プログラムの動作に関する推論のためのツールという側面にフォーカスしてみていく。また、型システムを、プログラミングにおける項を値の性質によって分類し、実行中にそれらの項がどう振る舞うかの静的な近似を求めるためのものとみなす。

型システムの効用

型システムで何ができるかについて、以下6つを挙げる。

  1. エラーの検出
  2. 抽象化
  3. ドキュメント化
  4. 言語の安全性
  5. 効率性
  6. その他

エラーの検出

ある種のエラーを早期に検出できること。具体的には、異なる型どうしで計算しようとしてしまう不注意のようなものから、科学計算で単位を勘違いする概念上の誤りのようなことまで。ここで「ある種の」といっているのは、たとえば、ゼロ除算であるとか、配列へのアクセスが範囲内に収まっているかといった実行時のエラーなどのような、実行時エラーを除く、ということ。

ただ、このメリットを享受するには、プログラマが適切にデータ構造を型付けして表現しなければならない。たとえば、複雑なデータ構造をなんでもリストで表現してしまっては、せっかくの型システムが活かされなくなってしまう。

抽象化

大規模なシステムをモジュール化するに際して、型がモジュール(クラスなども含む)間のインタフェイスを曖昧さなく定義するのに役立つ。また、型がもたらすそのような抽象性により、実装と切り離して設計や議論を行うことができる。

ドキュメント化

設計者にとってのみならず、プログラムを読む側にも型は有用である。コメントと違い、コードに埋め込まれ、コンパイルするたびに検査されるため、実装とドキュメントとに齟齬をきたすこともない。

言語の安全性

言語の「安全性」とは何か?

平たく言えば、安全な言語とはプログラミングの最中にうっかり自分の足を撃つことが不可能な言語であると定義できる。

この直感的な定義を少し洗練すれば、安全な言語とは自らがもたらす抽象を保護するものであるといえるだろう。

具体的には、Cのように、メモリの抽象としての配列を提供しつつも、配列の範囲外へのアクセスが可能であるような言語は「安全」ではないということ。

ただし、静的型安全性がすなわち言語の安全性というわけではない。動的型検査を行う言語であっても、実行時に安全でない操作をチェックすることで、ここでいう安全性を達成することができる。

効率性

コンパイラは、型情報により適切な機械語命令を用いることができ、また、前述の動的検査を除去することができる等、最適化を行える。

その他

プログラミングだけでなく、ネットワークのセキュリティ、プログラムの解析ツール、自動定理証明、DTDXMLスキーマといった分野に、あれこれと応用されている(よくわからない)。

型システム入門 −プログラミング言語と型の理論−

型システム入門 −プログラミング言語と型の理論−

  • 作者: Benjamin C. Pierce,住井英二郎,遠藤侑介,酒井政裕,今井敬吾,黒木裕介,今井宜洋,才川隆文,今井健男
  • 出版社/メーカー: オーム社
  • 発売日: 2013/03/26
  • メディア: 単行本(ソフトカバー)
  • クリック: 68回
  • この商品を含むブログ (9件) を見る

『企業数理のすべて』(第1章 指数と対数)

指数と対数の復習です。

目次: 『企業数理のすべて』を読む(目次)

1.1 累乗(べき乗)

累乗といえば複利計算ですよね。

1年間の金利rが、n年間にわたって適用可能な倍、1年複利計算は

(1+r)(1+r)...(1+r) = (1+r)^n

なので、{H}を預金した時、n年後に受け取る金額はH(1+r)^nとなる。

例題1.1 無リスクな割引債価格

割引債(ゼロクーポン債)とは、「満期Tまでの間にクーポンなどのキャッシュフローの受け取りがない債権のこと」(そんな債権になんの価値があるのかわからんが)。

そういうわけで、

  • 満期Tにおいて
  • 確実に額面金額1円の支払いを受ける割引債の
  • 時点t(t \leq T)における
  • 価格をZ_0(t,T)

とする。要するに、なんかごちゃごちゃ書かれているけど、Z_0(t,T)は、t時点での現在価値と等しい。

この割引債を時点tH単位購入すると、

  • 時点tでの価値はZ_0(t,T)H
  • 満期Tでの価値はH

ここでZ_0(t,T)Hを変形すると、

 \displaystyle Z_0(t,T) = \frac{H}{\frac{1}{Z_0(t,T)}}

この\displaystyle \frac{1}{Z_0(t,T)}を「ニューメレール(基準財)」とすることが多い、とのこと。「基準財」ってなんだ……(というか、本では「基準材」って書かれている)。

このあと、裁定機会のない完全市場でが、金利で割り引いた金額になるよって書かれてる。

例題1.2 スポット金利とフォワード金利

なにいってんのかわからない。

例題1.3 DCF法(Discounted Cash Flow法)

スポット金利の違いによって、将来のキャッシュフローに対する評価がかわるよ。

たとえば、

  • 1年後(t_1=1)に100万円(C(t_1)=100)が得られる
  • 2年後(t_2=2)に102万円(C(t_2)=102)が得られる
  • 期間1年と2年のスポット金利を、それぞれr(0,1) = 3%r(0,2) = 3%

とした時、それぞれのキャッシュフローの現在価値は

  • \displaystyle B_0(0,1) = \frac{C(t_1)}{(1+r(0,1))^1} = \frac{C(t_1)}{(1+0.03)} = 97.087
  • \displaystyle B_0(0,2) = \frac{C(t_2)}{(1+r(0,2))^2} = \frac{C(t_2)}{(1+0.03)^2} = 96.145

となり、B_0(0,1) > B_0(0,2)となる。

そうだね。

企業数理のすべて―プランニングからリスクマネジメントへの応用―

企業数理のすべて―プランニングからリスクマネジメントへの応用―

『企業数理のすべて』を読む(目次)

最近、いろいろと計画を立てる上で、いかに将来の不確実性とバランスしながらやってけばいいか考えることが多くなってきたので、できるだけ定量的に考えられるようにしたいなってんで、『企業数理のすべて―プランニングからリスクマネジメントへの応用』を読むことにしました。

文系プログラマでもコンピュテーションをアンダースタンディングできた!!1 - 書評『アンダースタンディング コンピュテーション』

タイトルは煽りです。

『アンダースタンディング コンピュテーション―単純な機械から不可能なプログラムまで』をご恵贈いただきました。ありがとうございます。

本書の扱う計算理論と呼ばれる分野には、前職の同僚たちがそういうのに詳しかったこともあってずっと興味を持ってはいたものの、いくつかの教科書的な本を繙いては読み進めずに挫折することを繰り返していました。その意味で、監訳者あとがきの「これなら私でも読める」という言葉は、自分自身の思いでもあると感じました(もちろん、笹田さんの「私でも」と、僕のそれとではおおいに異なることはいうまでもありませんが)。

計算とは何か?それはつまり「コンピュータの行うこと」であるのは間違いないことではあるものの、私たちプログラマが日々書いているプログラムが、どのような意味を持ち、どういう過程を経てその「計算」にたどり着くのかについて、すらすらと答えられるひとは多くはないでしょう。もちろん、そのようなことを知らずとも優れた仕事を行うことは可能でしょうけれども、いったんひっかかった疑問に、なにかしらの答えを見出したいと思うのもまた、自然なことです。

本書ではそれを、以下の題材を取り上げつつ、プリミティブなところからひとつづつ積み上げて解説していきます。

扱われている内容自体は、教科書的な書籍をいくつか組み合わせればカバーされるようなものであるかもしれませんが、本書はそうした教科書たちとは異なり、内容を形式的に述べるよりもむしろ、Rubyのコードで直接的に示すことでわかりやすさを採っているというのが特徴でしょう。たとえば、操作的意味論について

操作的意味論とは、プログラミングがある種の装置上でどのように実行されるのか、その規則を定義することによって、プログラミング言語の意 味を記述する方法です。

と述べつつも、その「規則」を形式的に説明するよりもむしろ、

1つの方法は、構文を小さなステップ(スモールステップ)で繰り返し簡約(reduce)することによって、プログラムを評価する機械を考えることです。ステップを経るたびに、プログラムは最終結果、最終的にそれが意味するものへと近づいていきます。

と、SIMPLEという単純なプログラミング言語を元に、その抽象構文木(Abstract Syntax Tree)がどのように簡約されていくかの規則を簡単なRubyプログラムで書き表すことによって、「プログラムの意味」を直感的に理解させてくれます。

また、簡単な機械から説き起こし、そうした「別の仕事をやりたくなるたびに新しい機械を設計するのではなく、入力からプログラムを読み込んで、そこに書かれた仕事をやるような単一の機械」としての万能性を持つ、チューリングマシンと等価である計算能力を持つシステムを示す第6章では、

  • 変数の参照
  • procの生成
  • procの呼び出し

のみ、すなわち、型なしラムダ計算と同様のスタイルのRubyプログラムによって説明することで、個人的には、これまでどうやっても理解にいたらなかったラムダ計算というものが、少なくとも記述についていくことによってなんとなくはわかるものになったという意味で、非常にありがたいものでした。

さらに、そのラムダ計算同様の「万能性」を持つ様々な「規則のシステム」が紹介されるわけですが(そこには、ライフゲームなども含まれる)、ラムダ計算よりもさらにシンプルに見えるSKIコンビネータ計算やIotaが、ラムダ計算と等価である(すなわち、それらを使ってラムダ計算の表示的意味論を与えることができる)というのは、我々の(?)行っている計算というものは、畢竟、ある構造をいかに簡約するかという規則と、その実行にまでシンプルにできるのか!と衝撃を覚えました。

ところで昨今は、JavaScriptに静的型付けをサポートするタイプのaltJSが多数出てきていたり、RubyPythonにおいて型注釈の導入が議論されていたり(RubyPython)など、いわゆる動的言語のコミュニティにおいても静的型付けに対する関心が高まっているように見受けられます。本書では、決定不可能性問題を近似的に解決する手法としての抽象解釈、その具体的な方法としての静的意味論について述べられており、その方面への関心からも興味深い内容が語られています。

変数に静的な型を付けることのメリットというのはいろいろあるのでしょうが、その中でもここで述べられるのは、あるプログラムがどのように実行されるのかは、実行してみなければわからない、すなわち静的解析によっては決定不可能であるという根本的な不可能性に対して、我々人間が、現実の世界を抽象化した地図によっておおいに恩恵を受けるのと同じように、静的型付けによる近似的な計算により、プログラムを実行せずともある範囲での安全性を確かめられるということです。極端にいえば、IDEの支援を受けられるとかコンパイル時に型チェックできるのは便利だなぐらいにしか思ってなかったので、蒙きを啓かれました。

そういったわけで、ごく限られた機能を持つ小さな機械から始まって、一般的なプログラムを実行できるという万能性を持つ機械と、それと等価なプログラムによるシステム、そしてそれらが本質的に抱えている計算不可能性を通じて、型理論のさわりにまでいたる本書は、幅広い内容を扱いつつも、単にそうした分野に興味を持っているだけの初学者を過度に恐れさせる形式性を避け、ある程度までの理解へとすんなり導いてくれるという、稀有な本であるように思えました。僕と同じように、計算理論について知ってみたくていろいろ挑戦したけど挫折しまくってきた人々に、間違いなくおすすめしたい本です。

監訳者によるサポートとして「本書の次に読むもの」が提供されているのですが、このあとは、計算理論についてのなにか教科書的な本と、買ったきり放置してある『型システム入門』を読んでみたいなと思いました。いつになったら理解できるのか、さっぱりわからないけど……。

花金かつ給料日はスーパー花金

花金と給料日が重なるとめでたい。世にいうところの「スーパー花金」である。これをプログラムによって求めよというお題が提案された。

というわけで、酒のつまみに適当に書いてみた。

ルール

  • 花金はFizz
  • 給料日はBuzz
  • 花金かつ給料日は「スーパー花金」なのでFizzBuzz

実行例

弊社の場合、給料日は10日なので、2014年1月には以下のようになる。

$ go run hanakin.go -payday 10 -month 1 -year 2014
2014 January
====================
1
2
Fizz
4
5
6
7
8
9
FizzBuzz
11
12
13
14
15
16
Fizz
18
19
20
21
22
23
Fizz
25
26
27
28
29
30
Fizz

発展

  1. 給料日が休日の場合、その直前の平日が給与支給日になる会社が多いだろう(弊社もそう)。たとえば、10日が給料日だが、10日が日曜日の場合は8日が給料日、という場合。hanakinスクリプトをその場合にも対応せよ。
  2. フォーマットをcalコマンドに合わせよ。
  3. 給料日が、三連休があとに続く金曜日である場合を「スーパーウルトラ花金」と定義する。その際に、FizzBuzz!!1と出力するようプログラムを改修せよ。