golden-luckyの日記

ツイッターより長くなるやつ

『定理証明手習い』の読み方(私論)

本記事は、ラムダノートで発売している『定理証明手習い』を買っていただいた方に「読んで」とお願いするための「私家版、読み方のおすすめ」です。そもそも定理証明とか自分には関係ないしっていう人も多いと思うので、「気になるけど買ってない」という方に興味を持ってもらうことも目的としています。


「ラムダノートの本の読み方(私論)」シリーズはこれで第3回なのですが、前回からは丸1年も空いてしまいました。この間に『実践プロパティベーステスト』を出版し、プログラムの挙動を検証する本について語れることが増えたので、そのあたりの世界観自体から話を始めていきたいと思います。

テストケースを手作りして挙動を確かめる

配列を逆順にしたものが欲しいとします。

たとえばPythonであれば、配列aryを逆順にしたものはary.reverse()で得られます。 スライスを使ってary[::-1]としてもいいでしょう。 reversed(ary)を使うことも考えられます。

普段、私たちがこうした便利な機能を使っているときは、単純に言語処理系の実装を信じています。 そんな基本的な機能を開発している人たちがミスに気づかないとも思えないし、世界中のみんなが使っている機能で実際にこれまでバグが出ていないのだから、きっと今もこれからも正しく動作するでしょう。

しかし、もし自分の手で関数を実装するしかないとしたら、その挙動が正しいことを無邪気に信じるわけにもいきません。

ここでは例として、自然数からなる配列を逆順にする関数を次のようにして再帰的に定義したとしましょう。

def reverse(xs):
    if not xs:
        return []
    else:
        return reverse(xs[1:]) + [xs[0]]

この関数の挙動について確信するための最初の一歩は、テストケースをいくつか書いてユニットテストしてみることかもしれません。

assert reverse([]) == []
assert reverse([1]) == [1]
assert reverse([1, 2, 3, 4, 5]) == [5, 4, 3, 2, 1]

とはいえ、これっぽっちの単純な値に対する挙動を確かめるだけでは、想像もつかないような値でもこの関数が正しいかどうかは確信できませんよね。 もっともっとテストケースを増やす必要があります。

しかも、できるだけ「思いもよらない値」に対するテストケースがほしい。 定義した関数が、自分の想像力を越える値に対しても意図した動作をするかどうかを調べるには、自分の頭で考えたテストケースを追加していくだけではきりがなさそうです。

性質からテストケースを自動生成するプロパティベーステスト

そこでプロパティベーステストです。 プロパティベーステストでは、人間はプログラムが満たすべきではなく性質のほうを考えて、その性質を確かめられるような値をフレームワーク機械的に大量に生成させます。 性質から値を生成するのに疑似乱数を使って、十分に大量の値を生成すれば、自分の頭では想像できなかった値が含まれる可能性も高いでしょう。 それらの値を使ってテストを実行することで、微妙なコーナーケースも勝手に網羅されるようにしようというわけです。

PythonにもHypothesisというプロパティベーステストのためのフレームワークがあるようなので、これを使ったプロパティベーステストの例をChatGPTに書いてもらいました。

from hypothesis import given, settings
from hypothesis.strategies import lists, integers

@given(lists(integers()))
@settings(max_examples=1000)
def test_reverse_property(xs):
    reversed_xs = reverse(xs)
    # リストが逆順になっているか?
    for i in range(len(xs)):
        print(xs)
        assert reversed_xs[i] == xs[len(xs) - i - 1]

test_reverse_property()

上記の例では、自分が定義した再帰的なreverseで試しに使ってみる値として、自然数からなるリストを生成させています。 そして、生成された値を使ってみた結果が本当に逆順になっているかどうかをfor文で確認するというプログラムのようです。

これをpytestで試してみたところ、下記のような結果になりました。 pytestでは--hypothesis-show-statisticsオプションを明示しないと統計情報が出ないようなのと、Hypothesisによって生成された事例を標準出力に見るには-sオプションが必須という点でちょっとはまりましたが、とりあえず1000の値を無作為に生成することによるプロパティベーステストはできているようです。

$ pytest --hypothesis-show-statistics -s
(中略)
============================ Hypothesis Statistics =============================

test_reverse.py::test_reverse_property:

  - during reuse phase (0.00 seconds):
    - Typical runtimes: < 1ms, of which < 1ms in data generation
    - 2 passing examples, 0 failing examples, 0 invalid examples

  - during generate phase (2.73 seconds):
    - Typical runtimes: ~ 0-2 ms, of which ~ 0-2 ms in data generation
    - 998 passing examples, 0 failing examples, 24 invalid examples

  - Stopped because settings.max_examples=1000

これで自作のreverseの定義にもだいぶ確信がもてるようになりました!

さらにプロパティベーステストでは、値ではなく性質のほうを考えるという特性から、「人間がプログラムの仕様について勘違いをしてないかがわかる」という強みもあります。 そうしたプロパティベーステストの発展的話題については、『実践プロパティベーステスト』という書籍でさらに高度な手法がいろいろ紹介されているので、興味がある方はそちらをぜひお求めください。 いまのところ最強のプロパティベーステストフレームワークErlang/Elixir向けのものなので、それらの言語による解説ではありますが、他の言語でもかなりのところまで実践できるようです。

プログラムの性質を値によらず「証明」する

いったん別の本の宣伝を挟んだところで、ここまでの話の要点を書き出しておきます。

  • ユニットテストでは、プログラムが満たすべき値を考えて、それらの値を使った結果を確認する
  • プロパティベーステストでは、プログラムが満たすべき性質を考えて、それに見合った値を無作為に生成し、それらの値を使った結果を確認する

このように並べて見ると、ユニットテストとプロパティベーステストでは「人間が何を考えるか」は違いますが、「値を使ってみて確かめる」という観点ではよく似ています。 プログラムの挙動を確認したいのだから、いずれにしても何らかの値を使ってみて確かめることになるでしょう。

しかしプログラムによっては、値を実際に使って確認してみなくても、その性質を形式的に確信できるはずであるようなものがあります。 たとえば、配列を反転させる関数であれば、値によらず「2回使うと元に戻る」という性質が満たされているべきでしょう。 「2回使うと元に戻る」関数のすべてが「配列を反転させる」という動作を実現するものかどうかは別の話ですが、そのつもりで書いた関数について「2回使うと元に戻る」という事実を値によらず証明できるなら、その性質を具体的な値を使ってみることで確認するよりも、かなり強力に正しいプログラムであることが確信できます。

現物をたくさん調べて確かめるのではなく、そうした性質を数学の定理のように「証明」しようというわけです。

というわけで、ここから今日の本題である定理証明です。 残念ながらPythonでは現実的にそのような芸当は(たぶん)できないので、ここからは例としてLisp系の架空のプログラミング言語を使います。

このLisp系の架空の言語では、冒頭に挙げたPythonによるreverse再帰的な実装をそのまま引き写して、次のような関数としてリストに対するreverseが定義できるとします。

(defun reverse (xs)
  (if (atom xs)
      xs
      (cons (reverse (cdr xs)) (car xs))))

そして「任意のリストxsに対してreverseを2回使うと元に戻る」という性質は、次のような式として書けるとします。

(equal 
  (reverse (reverse xs))
  xs)

もし上式を評価した結果が、xsの値によらず't、つまり真になるなら、「任意のリストxsに対してreverseを2回使うと元に戻る」という性質が確かに検証できたことになるでしょう。これが定理証明です!

証明してみよう

前項では都合よくでっちあげた架空のLisp系言語の例を持ち出して「これが定理証明です!」と言いましたが、「そんなん言われても単なる机上の空論じゃんよ」という感じですよね。

実を言うと、前項の例ではいろいろ大事なところをごまかしています。 まず、atomconscarcdrといった「組み込み関数」について、何も具体的な挙動を明記していません。 証明というからには、そうした細部の意味をしっかり固める必要があります。

たとえば、そうした組み込み関数にはあらゆる値に対して必ず何らかの値を返して停止するという性質(「全域性」とか「停止性」などと呼ばれます)が必要です。 ふつうのLispの実装におけるcarcdrにはこの性質がないので、SchemeCommon Lispをそのまま使って前項のノリで定理証明をすることは実はできません。

また、reverse再帰的に定義されているので、その性質を証明するには帰納法が必要になります。 したがって、(equal (reverse (reverse xs)) xs)という単一の式によって表される性質ではなく、次のような「帰納法の主張」に変形して、この評価結果を'tにすることが証明になります。

(if (atom xs)
    (equal (reverse (reverse xs)) xs)
    (if (equal (reverse (reverse (cdr xs))) (cdr xs))
        (equal (reverse (reverse xs)) xs)
        't))

ためしに(atom xs)の場合を証明してみましょう。高校数学で数学的帰納法をやったときに「基底部」と「帰納部」に分けて証明したのを覚えている人も多いと思いますが、これはその「基底部」の証明に相当します。

上式でいうと2行めが基底部なので、見やすいようにそこだけを取り出します。 これを変形していって、結果的に'tにできれば、基底部の証明完了です。

(equal (reverse (reverse xs)) xs)

まずは内側のreverseを定義で置き換えます。

(equal (reverse 
         (if (atom xs)
             xs
             (cons (reverse (cdr xs)) (cons (car xs) '()))))
       xs)

いま調べているのは基底部で、つまり(atom xs)なので、2行めのif式の条件は真です。したがってこうなります。

(equal (reverse xs) xs)

再びreverseを定義で置き換えます。

(equal (if (atom xs)
           xs
           (cons (reverse (cdr xs)) (cons (car xs) '())))
       xs)

やはり(atom xs)なので、if式の条件は真ですから、こうなります。

(equal xs xs)

これは'tなので、この場合についての証明はこれで完了です!

続きは『定理証明手習い』で

前項では、いかにも簡単そうに式変形を進めましたが、これは簡単な例だから簡単というだけで、実際にはこんな簡単にはいきません。 reverseの性質についての証明も、前項で終わりではなく、まだ「帰納部」に対する証明が残っています(前述したように、本当はさらに全域性についても証明が必要)。

改めて帰納部だけを取り出すとこんな式になっていて、いかにも手を動かして式変形するのは面倒そうですね。ミスも起きそう。

    (if (equal (reverse (reverse (cdr xs))) (cdr xs))
        (equal (reverse (reverse xs)) xs)
        't))

そこで、こうした「そこそこ複雑な主張を式変形していって'tにする」という形での証明の流れを、先生と生徒の対話を通して一歩ずつ学べる本があります。それが『定理証明手習い』です。 同書では、さらに証明における式変形を機械的に支援してくれる仕組みも用意されていて、それも利用できるようになっています。 いわゆる「定理証明支援系」です。 定理証明支援系の実装で何が考慮されているのかを含めて、値ではなく証明によってプログラムの確からしさを検証するとはどういうことなのかを体験できるのが『定理証明手習い』が本としておもしろいところです。

現実的な効能?

証明によるプログラムの検証という、まだなじみがない人が多いであろう考え方に触れる第一歩として手に取ってほしい『定理証明手習い』ですが、これ一冊で実務に定理証明を導入できるという本でないのも事実です。 ただ、それでも本書で触れられる考え方を知ることには、少なからず効能があると思います。 具体的には、「証明(のようなこと)をしてみる」という選択肢を手に入れてもらうのが、本書の役割としてあるのかなと考えています。

たとえば、本記事で定義した架空のLisp系言語におけるreverseには実は重大な欠陥があって、どんなにがんばっても帰納部に対する証明が得られません。 実際、ふつうのLispではこのように定義してreverseだと「2回使うと元に戻る」という性質を満たせないのです。 そのため、ちゃぶ台をひっくり返すようですが、実際に手を動かしてみると証明に行き詰まります。

しかし、やはり実際に手を動かしてみるとわかりますが、証明に行き詰まる過程で「その定義のどこに問題があるか」に気が付けます。 「何かが決定的におかしい」と気づけることで、より正しい実装へと舵を切れるかもしれません。 本記事のreverseにおける問題は、consにより「本物のリスト」が作られるような書き方をしてしまっていることです。 Lispにおけるconsで作られるのは「本物のリスト」ではなく、コンスペアなどと呼ばれるちょっと癖のあるデータ構造なので、Pythonの配列と同じ要領でリストの再帰的な定義を雑に書くとはまるのです。

「下位の詳細がどうなっていれば証明が通るだろうか?」という観点で実装を検証すること自体が、問題を理解するうえで役に立つことはあると思っていて、そのようなアプローチのひとつとして定理証明という方法の存在を知っていることに価値があるような気がしています。 個人的に『定理証明手習い』は、そのためのさらにきっかけになるような本だと考えています。

ちなみに、「正しいreverseを2回すると元に戻る」をちゃんと証明するには何が必要か気になる人は、以下の記事で今井宜洋さんによるCoqでの解説が読めます。

『定理証明手習い』を読んだあとなら、Coqが何のために何をしてくれるものなのか、ちょっぴり解像度が上がって見えてくるはずです。 逆に、Coqを触ってみたあとに『定理証明手習い』を読むと、謎かけのようにも見える本書のやり取りの味わいが増すはずです。

SNSの居心地をよくする

2023年、Twitterは名目上消失しました。 ずっとMastodonFacebookに馴染めなくて困っていたのですが、Blueskyのアカウントを作れたことでなんとか救われました。

いまのところBlueskyは自分にとって「居心地がいいSNS」になっています。 Blueskyの居心地をよくするうえで自分にとって役立った機能として「フィード」と呼ばれるものがあるので、これについてpyspa Advent Calendar 2023 - Adventarの一記事として書かせてもらおうと思います。

フォローするアカウントを増やすの難しい

SNSで自分がふだん目にするコンテンツの大半は「他のアカウントをフォローする」ことによって形作られます。 逆に言うと、アカウントのフォローを増やさないとコンテンツも増えにくい。 特にSNSのアカウントを取得してしばらくの間は、フォローしてる人が少ないのでアクセスしてもいまいち面白くない状態が続きます。

投稿だけが主目的ならフォローを増やさなくていい気もするけど、変わり映えしないタイムラインはアクセスの機会そのものを減らすので、投稿の頻度も減りがちです。 やはりアクセスするたびに何か新鮮な刺激があるほうがいい。

かといって、SNSで他のアカウントをフォローするのは勇気がいる行為です。 自分の場合、2ホップくらいで共通の知り合いがいそうであったりしないと、なかなかフォローボタンを押す勇気を絞り出せません。

そもそも、ぐっとくるアカウントを見つけ出すこと自体が難しい。 最近の巨大プラットフォームが、フォローしていないアカウントによる投稿をタイムラインに混ぜたがるのも、新規ユーザーがこの状態になってアクセスしなくなってしまうのを避けたいがためでしょう。

プラットフォームが押し付けてくる投稿は微妙だけど…

プラットフォームが押し付けてくる投稿は、確かにコンテンツを単純に増やしてはくれます。 しかし、興味のない有名人とか、なんか怒ってる人とか、嘘や刺激で耳目を集めたい人とか、そういうアカウントの投稿は残念なコンテンツでしかないので、かえって居心地を悪くします。

幸い、Blueskyのタイムラインには、プラットフォームが押し付けてくる投稿は混じりません(いまのところ)。 おかげで古き良きSNSの雰囲気を保てています。

ただしそれだけだと、「フォロー数が少ないとタイムラインが活発にならない」という困難は残ります。 結局のところ、自分がTwitterを離れられないのは、長年にわたって慎重にフォローを増やしてきた歴史があり、それによって自分にとって居心地のいいタイムラインを作れたからなんですよね。 その状態でプラットフォームから興味のない投稿を押し付けられてるから、自分にとってTwitterは微妙な感じになってしまっているわけです。

でも、これからTwitterのようなものを始める人、つまりBlueskyを始めたばかりの自分のような人には、なんらかの形で最初から賑わいがあるタイムラインがあるほうがいいかもしれません。 ありがた迷惑な機能は、迷惑な側面を極限まで減らせるなら、ほとんど限りなく単純にありがたい機能でもあるはずなのです。

タイムラインをアカウント単位で作るものといつから錯覚していた?

実はBlueskyのタイムラインにはTwitterとは根本的に違う部分があります。 それは、タイムラインを作る手段が「他のアカウントのフォロー」だけではない、という点です。

現在のBlueskyのタイムラインは「フィード」と呼ばれる仕組みで実現されています。 技術的な仕組みはまじめに調べてないのですが、フィードは要するに「条件で決まる一連の投稿」のようなものです。 Blueskyのデフォルトのタイムライン(「Following」)も、条件として「自分がフォローしているアカウントの投稿」を指定したものだと言えます。

フィードがすごいのは、Twitterのような「興味あるアカウントからなるタイムライン」だけでなく、「興味あるトピックからなるタイムライン」も作れるところです。 たとえば、条件として「正規表現 #/読んだ本/ にマッチする投稿」なんかを設定したフィードが作れます。 これにより「"読んだ本"という文字列を含む投稿からなるタイムライン」が作れるわけです。 Twitterのリストに似ていますが、アカウント単位ではなくトピック単位でも作成できるので、はるかに便利。

しかも、こうして作った独自のフィードは他のユーザーも自由に閲覧できるように公開できます。 公開されているフィードは、デフォルトのタイムラインである「Following」と並列にホーム画面にピン止めできるので、タブのように切り替えて自分のタイムラインとして使えます。 さまざまな人が開発した無数のフィードが公開されているので、気に入ったものを自分のホームにピン止めするだけで、自分が好きな話題をだらだら眺めるためのタイムラインができるのです!

「本とかを読む」フィードを作った

自分も、自分にとって居心地がいいフィードを作って公開しています。 「こんな本を読んだよ」、「こんな本が読みたいよ」、「こんな本を買ったよ」、「こんなシチュエーションで本を読んでるよ」みたいな日本語の投稿が集まってくる、「本とかを読む」フィードです。

bsky.app

(2023年12月時点ではBlueskyのアカウントがないとリンク先がなんも見えないかもしれなくて申し訳ない。)

自分にとっていい感じの投稿が活発に流れてくるタイムラインができたことで、自分にとってのBlueskyの居心地は爆上げしました。 いまではデフォルトのタイムラインはときどきしか見ていなくて、もっぱらこのフィードを見ています。

個人的に「本とかを読む」フィードで特に気に入っているのは、眺めているだけでしばしば本屋さんにいるような気分になれることです。 実際、今年はこのフィードで知った本を何冊か買ったり読んだりしました。

自分では読まないようなジャンルの本が楽しく読まれている雰囲気をうかがい知れるのもこのフィードで気に入っているところです。 そのために特定のジャンルを積極的にはじくようなフィルタは極力入れないようにしています。

ただ、本について語っている投稿をなるべく幅広く取り込もうとすると、(主に自分にとって)居心地が悪い状態になるので、悩ましいこともあります。 たとえば先週、とある翻訳書の発行が中止されるという事件があり、本を読むこと自体よりも「本が出版されることの意義」みたいな方向で何かを語りたい投稿がわっと増えてしまって居心地が悪くなりました。 忙しくてBluesky自体をあまり見ていなかったので対応が遅れましたが、ふだんは気がついたら調整しているので、いまは立ち直っているはずです。

あと、情報収集とか社会批判とかが目的ではないので、制作側による宣伝めいた投稿や出版三者をめぐる業界ネタがあまり多く流れないようにすることにも気を使っています。 とはいえ、新刊情報をはじめ書籍自体の紹介はやはり多めに流れているほうがうれしいので、このへんもバランスをとるのに苦労しているところです。

Twitterの居心地がフォローの妙味で決まっていたので、BlueskyをはじめとするTwitterクローンの居心地もフォローで決まると思っていたのですが、少なくともBlueskyにはフィードという機能があり、今のところ自分にはそれがはまっている感じです。 これからBlueskyも人がますます増えていくので、いつまで「本とかを読む」フィードの居心地を維持できるかわかりませんが、みなさんもいい感じのフィードを作って公開していきましょう!

『RubyでつくるRuby』の読み方(私論)

本記事は、ラムダノートで発売している『RubyでつくるRuby』を買っていただいた方に「読んで」とお願いするための「私家版、読み方のおすすめ」です。また、この本は当社の本のなかでも過小評価されているところがあると思うので、「気になるけど買ってない」という方に興味を持ってもらうことも目的としています。


本書『RubyでつくるRuby』を買った人にも、まだ買っていない人にも、とにかくまず意識してほしいのですが、この本はRubyの解説書ではありません

じゃあなんの本かっていうと、これは「そもそもプログラミング言語でプログラムを書くって、なに?」という根本的な問いへの取り組み方を教えてくれる本です。

もう一度言いますが、この本はRubyの解説書ではありません。なので、「Rubyを使うつもりはなくて、PythonとかJavaScriptが好き」っていう人や、「それらのプログラミング言語をいままさに勉強している」という駆け出しエンジニア、その段階から抜け出すための次の一歩を探している人、そういう、「Rubyとあんまり関係ない人」にも読んでほしい本です。いやむしろ、そういう人こそが読むべき本だとさえ言いたい。

もう一度繰り返しますが、この本はRubyの解説書ではありません。なので、この本を読んでも、Rubyによるプログラミングには詳しくなれません(Rubyに詳しくなりたい人には『研鑽Rubyプログラミング』がおすすめ)。その代わり、たった100ページちょっとで「(Rubyに限らず)プログラミング言語はどういう仕組みになっているのか」を知る入口に立てます。

というわけで、以降では、Rubyに興味があるかないかに関係なく次のような悩みを抱えている方々が本書をどう読むのがおすすめか個人的な意見を書いてみたいと思います。

「プログラムの書き方がいつまでたっても覚えられない」という人

「プログラミングの勉強をしてる」という人の話を聞いてみると、「やりたいことを解決するための書き方」を覚える努力をしているように見えることがあります。覚える努力をしているわけでなくても、「プログラミングできる」と「プログラムの書き方を知ってること」を半同一視してしまっている人も少なくないのではないでしょうか。

「特定のプログラミング言語でアプリケーションをささっと作れるようになる」ためには、そういう勉強も必要なのは言うまでもありません。でも、そこでちょっと立ち止まってみてほしいのですが、昨今、「特定のプログラミング言語の書き方に詳しい」だけで済むことはそう多くありません。さまざまなプログラミング言語について知る必要があるたびに、「その言語での書き方をたくさん覚える」をがんばるしかないのでしょうか?

これが英語や中国語のような自然言語だと、わりとそういう感じに「特定の言語の使い方を覚える」をがんばるしかないところだと思います。 でもプログラミング言語は、かならずしもそうではありません。多くのプログラミング言語は、それなりに共通する考え方の基盤に沿って作られているので、その考え方を知っているだけで、だいぶ「新しい言語」に対する見え方が変わります。

実を言うと、大学の情報科とかで勉強するのも特定のプログラミング言語の書き方ではなく、そういう「多くのプログラミング言語の作りの背景にある共通する考え方」だったりします。なので、大学で使うような計算機科学の教科書とかを読むと、それを勉強できたりします。でも、教科書を一人で読むのはなかなか大変ですよね。

その点『RubyでつくるRuby』なら、説明を頭から読んで練習問題を一通りやってみることで、そういう計算機科学の教科書に書かれてるような話のさわりを体験できます。この本でつくるのは本物のプログラミング言語Rubyのうちでも「多くのプログラミング言語の作りの背景にある共通する考え方」の部分だけですし、教科書的に退屈な部分は潔くカットしつつ、飲み込みにくい概念にはイラストもたくさん入っているので、なんとか踏ん張って第6章までは読みとおしてみてください。

「どうしてプログラミング言語でプログラムが書けるのかわからなくて夜しか眠れない」という人

プログラミングの入門書にある例題を書き写して「なるほど同じ結果になるな」って確認できたけど、「だから何?」って思ってしまうこと、ありますよね。「"Hello World" を出力しろ」というプログラムを書いて、それをコンピューターで実行したら "Hello World" が出力されるっていうのは、それだけを見ると面白くもなんともありません。

でもよくよく考えてみると、「あるプログラミング言語ソースコードを書くと、それがコンピューターで実行されて結果が出てくる」って、ちょっと不安になるくらい何が起きているのか意味不明じゃないですか? そもそも、「プログラミング言語で書いたソースコード」と、「コンピューターで動くプログラム」は、同じものなんでしょうか? PythonRubyで書くソースコードは違うけど、どちらも「コンピューターで動くプログラム」なんでしょうか?

そういえば、PythonRubyで書いたプログラムを実行するには、pythonとかrubyみたいなコマンドを使います。そういうコマンドで「プログラミング言語で書いたソースコード」を「コンピューターで動くプログラム」にしてる気がしますが、pythonとかrubyみたいなコマンドはどうやって動いてるんでしょうか? っていうか、pythonとかrubyみたいなコマンドはどうやって作られてるんでしょうか?

こういう不思議の連鎖って、いったん躓くとなかなか抜けられず、先に進めなくなりがちですよね。

RubyでつくるRuby』は、そういう「プログラミング言語というものの不思議さ」を直接味わえるようになっています。この本でつくるRuby(の機能縮小版)は、pythonとかrubyみたいなコマンドのように、「プログラミング言語で書いたソースコード」を「コンピューターで動くプログラム」として実行するための機能を持ったプログラムです。しかも「この本でつくるRuby」というプログラミング言語で書いたソースコードも、「この本でつくるRuby」というプログラムで動かせます。

この不思議な関係は、実のところ、現代のコンピューターにおいてプログラムを開発したり実行したりする世界観そのものでもあります。『RubyでつくるRuby』は、わずか100ページちょっとでそこまで辿りつけてしまう本なのです。ぜひ、自分でコードを書きつつ、最後の第9章まで通読してみてください。

プログラミング言語を作ってみたい」という人

しつこく繰り返しますが、この本はRubyの本ではありません。そうはいっても、みなさんが使えるようになりたいプログラミング言語PythonとかJavaScriptかもしれず、残念ながらこの本にはPythonJavaScriptのことは書かれていません。最近ではRubyというプログラミング言語のことを「Webのエンジニア募集でたまに名前を見かけるやつ」くらいにみなしている人もいるような気がします。そういう人にとって『RubyでつくるRuby』は役に立たない本なのでしょうか?

そういう方におすすめなのは、『RubyでつくるRuby』を読みながら『PythonでつくるPython』とか『JavaScriptでつくるJavaScript』を自分でやってみることです。これには次の2つの意味でものすごい教育効果があると思います。

  • それぞれの言語のソースコードの文字列を読み込んで抽象構文木に変換するパーザを自分で書くことになる
  • それぞれの言語の挙動を、とくにRubyとの対比で、いま以上によく知れる

1つめの話は、本書を読むだけでは手が出ない話題なので、これは上級コースになります。でも、裏を返すと、本書はそういう上級コースの人でも楽しめる内容だとも言えます。

さらに、「この本でつくるRuby」を拡張していろいろな実験をしてみるのもおすすめの上級コースです。たとえば著者本人の手で漸進型が導入された拡張が作られたりしています。Rubyといえば動的型付き言語なので、これはもはやRubyではありません。でも、そんな感じで「Rubyよりむしろプログラミング言語そのものに興味があるすべての人」にとっておすすめの本が『RubyでつくるRuby』なのです。


最後に、『RubyでつくるRuby』がRubyに興味のない人にとっても価値がある本であるにもかかわらずRubyを題材として採用している理由についても触れておきましょう。これは、本書の著者である @mametter 氏の強みがRubyだからです。

しかし、著者はRubyしか知らない人ではありません。C言語のある種のプログラムに関しては世界の第一人者で、なんなら「"Hello World" のように自明なアプリケーションではないコードを書くのに使ったプログラミング言語の数」でも世界でトップクラスに入るような人です。このことからも、本書がRubyの入門というわけではなく、プログラミング言語そのものという泥沼トピックへの入口として書かれた本であることがうかがい知れるでしょう。

2023年賀状(PostScript定期)

ちょっと趣向を変えて、今年は具象です。 乱数を使って1枚ずつ仕上がりを変えるみたいな小細工も今年はやめた。

github.com

楕円を三つ組み合わせているだけなんだけど、文字列のパスと楕円のパスとで切り出しが入れ子になってるのと、それを楕円ごとにやらないといけないので、丁寧なgsave/grestoreが必要でめんどくさい。 グラデーションは、色空間をRGBではなくHSVにするだけで途中にどす黒い領域は発生しなくなるんだけど、一次関数で変化をつけるといまいち知覚的にきれいに見えなかったので、対数を使っている。文字列と背景とでそれぞれ別々にグラデーションを適用するのもめんどくさかった。 例年に比べて地味なのに、めんどくさい度は高かった気がする。

『プロフェッショナルSSL/TLS』の読み方(私論)

本記事は、ラムダノートで発売している『プロフェッショナルSSL/TLS』を買っていただいた方向けに「読んで」とお願いするための「私家版、読み方のおすすめ」です。本なので、どう読んでもらってもいいんですが、「買ったはものの積読になっている」という方の背中を押せればと思います。


この本は、プロトコルであるTLSの解説書であると同時に、「インターネットで安全にやっていく」ための感覚のベースラインを与えてくれる本です。 そういうつもりで、まずは第1章を読んでみてください。 知ってる話も知らない話もあると思いますが、20ページくらいしかないので、とりあえず読みましょう。 ここを読むと、現代のTLS以前の古典的な暗号、ハッシュ、認証について、安全かどうかを考えるためのフレームワークが得られます。 カタログ的ではないので、そういうのは期待しないでください。 なお、現在のバージョンには「認証付き暗号」という重要な概念が抜けていますが、これについては次の第2章(および最新の電子版に収録された付録A)で出てきます。

第1章を読んだら、TLS 1.3に関する付録AがあるPDFをおもちであれば、そこを読みましょう。 ない人は、TLS 1.2ベースになりますが、そのまま第2章へ。 本書はTLSの「プロトコルとしての仕様」を説明する本ではないんですが、なにはともあれTLSプロトコルとしてのノリは把握しておく必要があります。 この章(もしくは付録)については、多少ぴんとこない話があっても読み飛ばして、とりあえず目をとおしてください。 そういう「この章だけを読んでもぴんとこない」部分も、あとの章を読むと「そういうことね」と思えるはずです。

次の第3章も、とりあえず「ぴんとこない部分」は飛ばしていいので、目をとおしましょう。 TLSというプロトコルは、インターネットにおいてはPKIというインフラの上で使うことを前提になっていて、ここはそのPKIの話です。 この章も、どのみちあとで何度も立ち戻ってくることになるので、初見は「だいたいこういうことが書いてあるんだな」という軽い気持ちでまずは目を通してください。

第4章から第7章は、主に歴史の話です。 ほんとは歴史の話というわけではなく、歴史をとおして「なんでいまのTLSPKIがこういう姿になっているか」を知るための章なんですが、歴史の話と思って読むとさらさら読めるはずです。 この部分を読みながら、「あれこれはなんの話だっけ?」とおもったら第1章から第3章や付録Aの該当部分に検索や索引を頼りに立ち戻って「なるほどね」と思う、というのが、本書の効率的な読み方かと思います。

が、実はもっと効率的な読み方もあります。それは、次の第8章を中心とした読み方です。 第4章から第7章は、分脈を知るには不可欠なんですが、分脈はいいからまずは具体的な話をしてくれ、というときもあるでしょう。 そういうときは、「第8章から読む」というかなり乱暴な読み方もありです。 もちろん、それで意味がわからない部分については第1章から第3章や付録A、あるいは第4章から第7章に向き合ってください。

第9章以降は、かなりボリュームはあるものの、最初はボーナスステージという扱いで、「実務で必要になったら読む」でもいいと思います。 とくに第13章以降は、現在ではすべての人に必要な情報というわけでもないので、ここを読み切らなくても「読んだ」といって大丈夫です。

というわけで、この本は、ふつうのエンジニアがTLSについて知っておくと捗るすべてのことが書かれた本です。 文字通り「すべて」なんですが、「ふつうのエンジニアが知っておくといいこと」っていうのがポイントで、「前のほうに書いてある細部を全部を頭に入れておかないと読み進められない」という本ではないので、上記のような「本の構成」を把握しながらさくさく読み進めると、ボリュームのわりには「よめるよめるぞ」となる本ではないかと思います。 もちろん、実際に手を動かす段になるとわからないことがいろいろ出てくるはずですが、少なくとも「なにを調べたらいいか」あたりの勘はつくはず。

買った人はぜひ読んでみてください!

ラムダノート第8期を迎えました

2015年12月に自分で出版社を立ち上げたとき、うっすらと決めていた覚悟は、「ひとまず10年は続ける」でした。

それまで15年くらい、技術系版元として歴史も規模もそこそこある出版社で企画編集をやっていたので、「だいたい何部くらい売れれば一人なら食っていける」といった程度の雑な算段はあったものの、かっちりした事業計画があったわけでもなく、「まあ、しばらくは前職の退職金を食いつぶしながら最初の何冊かを作ればいいかな」などと気軽に考えながら、むかし作った本の読者だったり有識者レビュアーだったりでお世話になっていた時雨堂という会社に遊びにいき、そんな浮ついた起業計画を雑談のつもりでしたら、社長の @voluntus に「お金出すよ」と言われ、「えっ」って戸惑っているうちに税理士さんを紹介してもらい、定款ができて、気づいたら ラムダノートという出版社 ができていました。

あれから満7年。2022年12月にラムダノートは第8期を迎えることになりました。会社をスタートできたのは時雨堂のおかげ、本を出せたのは著者や訳者のおかげ、なによりもこうして「本を売ってやっていく」ができているのは本を買ってくれる読者のおかげです。

10年という当初のぼんやりした目標まではもうひと頑張りありますが、よく考えたらコンピューターとネットワークの出版社なんだから節目の基数は2であるべきだし、1000_2周年をむかえるこのタイミングで感謝祭として大セールをやっています。協賛は再び時雨堂です。クーポンコード「時雨堂と一緒にラムダノートの8周年突入をお祝いしよう!」を入力すると電子書籍がほぼすべて半額。ほんとうにありがとうございます。

余談ですが、この「クーポンコードによる宣伝」という協賛の企画を思いついたのも時雨堂社長の @voluntus です。天才かと思った。

このクーポンコードの文字列「時雨堂と一緒にラムダノートの8周年突入をお祝いしよう!」は、お買い物で使ってもらうたびに当社のバックヤードに流れるので、みなさんにお祝いしてもらっている感も半端ありません。ほんとうにほんとうにありがとうございます。

さて、今回の大セールは12月19日まで引き続き開催中なので、ふりかえりにはちょっと気が早いのですが、今日までの段階で個人的に感じたいろいろをいったんダンプしておこうと思います。

セールの効果1:売り上げがすごい

ある程度は期待していた部分ではあるのですが、すでに直販サイトの平均的な売り上げの数か月分に達しています。おかげで、おそらく創業以来はじめて、期初の現金にやや余裕がある状態を迎えることができそうです。だいたい毎年、年末から年初にかけて現金が枯渇するのですよね…。当社の支払いサイクルの事情ではあるのですが、1月~2月と8月~9月にまとまった現金が必要で、メンタルがつらい。今年は例年になく穏やかな気持ちで正月を迎えられそうです。キーボードつくろうかな。

セールの効果2:潜在需要がすごい

売り上げについては、実は怖い気持ちもあって、「これ、来月からみんな本買ってくれないんじゃないかな…」という。アパレル系は年2回のセールで年間の売り上げを稼ぎ出すというし、電子書籍の世界でも半額セールや無料セールを定期的にやっているし、これはもうそういうものと考えるべきなのかもしれないけれど、セールをやるとわかっているショップではどうしたってセールを待ってしまいますよね…。当社の直販サイトでこれからセールを定期的にやるつもりはまったくないのですが、これだけ長期間のセールをやっていると、潜在的にラムダノートの本に興味があった人がすべて本を手にしてしまうかもしれない。

しかし、これは逆に考えると、「潜在的にラムダノートの本に興味があった人」がこんなにいたのかという素朴な驚きでもありました。専門書の編集者みたいな仕事を長年していると、「需要は限られている」という意識が骨の髄までしみついていて、ついつい実売部数についても「こんなものだろう」で思考停止してしまうんですが、そんなことなかったんだなあと。いつもよりお得っていう効果はあるにせよ、そもそも興味がないものに払えるお金はゼロ円なわけで、需要がしっかりあるという事実を目の当たりにさせてもらいました。

セールの効果3:知ってもらえた、思い出してもらえた

潜在需要が見えた背景には2つの要因があると考えています。1つは、当社が本として販売している情報に対価を払う意思はあったけど、それを当社で買えるという事実にそもそも気づいていなかった人がいたということ。もう1つは、当社で売ってる本のことは知っていたけど、買う機会を逃していた人がいたということ。いずれも、セールをやる前から「そういう人もいるだろうなあ」とぼんやりは想像していたわけですが、実際にセールを開始した後のツイッターなどの反響や、いわゆる直販サイトへのセッション流入数やコンバージョン率の上昇、まったく新規のお客様の割合などから類推するに、ぜんぜん想像以上でした。今回のセールは、短期での売り上げや、協賛の時雨堂を知ってもらう機会になったのみならず、「ラムダノート」という出版社の名前を知る人を中長期でかなり増やしてくれたのだろうなと実感しています。忘れないでね!

セールの効果4:刺激

当社としては、今回のセールを機に当社を新しく知ってもらった人や思い出してくれた人は、これから「当社が出す本」に期待していただいている状態だと考えています。正直なところ、丸7年間走りっぱなしだったので個人的にはちょっとお疲れ気味ではあるのですが、ここでめげずに新しい企画をやっていくぞという気持ちをセールへの反響や「時雨堂と一緒にラムダノートの8周年突入をお祝いしよう!」というクーポンの文字列に支えてもらっている自覚があります。まだセール期間が1週間あるので、引き続きどんどんご利用ください! あと、これからまたべらぼうに面白い新刊も出していくので、セール終了後も引き続き新刊情報をお見逃しなく! 今年は結局新刊を出せなかったn月刊ラムダノートもやるよ! 新刊情報については、メールとかはしていないので、 公式Twitter もしくは 直販サイトのお知らせページRSS購読してね。