golden-luckyの日記

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

読み手と書き手にとっての『n月刊ラムダノート』

読み手にとっての『n月刊ラムダノート』

今期は「とにかく『n月刊ラムダノート』の企画をがんばる」を目標に設定しています。 『n月刊ラムダノート』というのは、当社の不定期刊行誌で、次のような特徴があります。

  • A5版で20ページ~50ページの解説記事を3つくらい収録
  • それぞれ雑誌記事やブログに比べるとだいぶ本格的だけど、論文よりは気軽に読める

こんなふうに特徴を列挙しても、それだけだと具体的なイメージがわきにくいと思うので、ぜひ実物を見てください! たとえば今年発行した各号には次のような記事が掲載されています(いずれも公式ブログの紹介からの引用)。

『n月刊ラムダノート』Vol.4 No.3(2024)の内容
『n月刊ラムダノート』Vol.4 No.2(2024)の内容
『n月刊ラムダノート』Vol.4 No.1(2024)の内容

どれも「いつか知りたい、でもキーワード解説や雑誌の特集ではわかった気にしかなれない、かといって入門書をしっかり読む時間もない」というトピックばかりですよね! コンピューター技術の分野には、こうした「休日の午前中にちょっと真剣に読んだらめっちゃ充実する」とでも言うべき読み物がもっとあっていいと思っていて、それが『n月刊ラムダノート』で実現できればなと考えながら発行しています。

出版企画の三つ組

とはいえ、理念だけで出版は実現できないのも現実。 『n月刊ラムダノート』も企画にはずっと苦悩していて、なかなか「定期」刊行誌になれそうもありません。

これは本誌に限らないのですが、出版の企画は「こういう解説を読みたい人がたくさんいるだろう」といった着想ではありません。 そうした着想からスタートするにせよ、実現に向けて不可欠な要素はほかにもあって、具体的には「構成」と「書き手」です。 言い換えると、「構成」と「書き手」、そして「着想」の三つ組がそろってはじめて企画になります。

着想 <-> 構成
  \      /
   書き手

編集者には、着想がいろいろ思いつく人もいれば、構成を練るのが得意な人もいれば、書き手とつながるのがうまい人もいます。 しかし、どれか1つが得意なだけで企画ができるわけではないので、得手不得手を補完しつつ三つ組をぶんぶん回すしかありません。 最強なのは書き手本人が着想と構成もぶんぶんやれる場合で、でも最近は同人誌とかウェブでの公開とか書き手にとっての手段が多様化しているから、出版社で本や記事を書いてもらう動機が昔に比べると示しにくい気がしています。 提示できる動機としては、対価や露出が考えられるけど、小さい出版社だと対価はともかく露出に期待してもらうのは難しい。

編集者としてのぼく個人は、「編集」を動機にしてもらえるように頑張っているつもりです。とはいえ「編集されること」は書き手にとってメリットとして自明ではないので、これを潜在的な書き手に認識してもらう手段が悩ましい。

書き手にとっての『n月刊ラムダノート』

実は『n月刊ラムダノート』は、この「編集されること」のメリットを潜在的な書き手に体験してもらう機会になれるんじゃないかなと考えています。 一冊の本だと「企画の三つ組を揃える」、「書き上げる」、「編集する」のイテレーションがけっこう重いけど、30ページくらいの記事なら比較的軽くなります。 企画自体も軽めに始動できるので、潜在的な書き手にとっても、「こういうの書けそう」とか「書いてみた」から「不特定多数が読むことを想定した日本語にして公開する」までのイテレーションを体験してもらうことで編集が入ることのメリットを見定めてもらう機会にしてもらえるかなと。

もちろんこれは編集者にもメリットがあって、本として完成するまでのイテレーションの重さを考えると躊躇するような企画にも取り組みやすくなります。 多様化する題材へのキャッチアップが大変といった別の悩みもあるのですが、これはむしろ編集者としての筋トレには役立つという見方もできるのでがんばる。 まあ、本よりだいぶ収益性が低いといった経営的な課題はあるのですが、それも企画の機会が増えることで補えるかなと。

それでも難しいのは、このイテレーションを体験してもらう潜在的な書き手、もう少し正確に言うと「書きたくて、かつ書ける人」にそもそも巡り合うことだったりします。 書くという行為にかかる時間や体力を考えると気軽にお願いしにくかったり、そもそも何を書いてもらうべきか(着想と構想)に対する自分の視野がなかなか狭かったり、自分側の原因はわかっているのでそこらへんはがんばっていくとして、潜在的な書き手の皆さんからのご相談もお待ちしています。

書きたいこと、書けることがあって、このイテレーションで編集のメリットを体験してみたいという方がいましたら、こちらを参考に気軽に寄稿を検討してみてください!

商業品質の日本語

編集者は「日本語を直す」機会が多い仕事である。 しかし文章というものは内容、つまり「何を言いたいか」だけで成立するものではないので、表現、つまり「どう言いたいか」も尊重する必要がある。 やみくもに内容が正しい別の表現で書き換えていいわけではない。

それでもわれわれは日本語を直す。 そして「直す」と言うからには、そこに何かしら解消が必要な課題を見ている。

編集者は、原稿のどのような状態を「課題」として認識するのだろうか。 人によって違いはあるだろうけど、ぼくの方針は「下記のような印象を想定読者にもたらしうる部分が原稿に残らないことを目指す」だと言える。

  • この書き方だと読み手に不要な時間を割かせてしまいそうだなあ
  • この書き方だと読み手が挫折しそうだなあ
  • この書き方だと勘違いされそうだなあ

上記のような印象を読み手が抱かないようにするために何をするかというと、文意を保存した変換を作成する。 文体とか語り口も、できるだけ維持する(ただし読み手にとって益がない修辞を回避したり、いわゆるトンマナを整えたりはする)。 その変換結果を修正案として執筆者に確認してもらい、それをたたき台にしてさらに書き直してもらったり、それでよければ取り込んでもらったりする。

もちろん、文意を保存した変換を作るからには、ぼく自身が文意を読み取れなければならない。 いちおう編集者である自分に文意が取れないとしたら、対象読者の多くにとっても読み解くのが厄介な文章ということになるので、説明の仕方から再考してもらうべきだろう。 そのように主張したり、そもそも文意を保存した変換を作ったりするためには、自分の前提知識を「対象読者の底辺と同じ程度」にまで引き上げる必要があるので、そこはがんばる。

ここからが本題だ。 ぼくは、こうやって執筆者と編集者とで揉んだ文章がはじめて「商業品質の日本語」になりうると考えている。 言い換えると、原稿の文意の理解を諦めて表面的な日本語としてのそれっぽさを整える作業によっては、商業品質の日本語は実現できないだろうと考えている。

逆に、出版物が商業品質の日本語になっているかどうかは、文意の伝わり具合によって評価できると思っている。 「文意の伝わり具合」を評価する指標としては、たとえば下記のようなバロメーターが使えるだろう(数字が大きいほど高評価)。

  1. 文意を読み解けない
  2. わかっている人が読めば文意が察せれる
  3. わかっている人が読めば誤読しない
  4. 何度か読み返して文意を察せられる人がそれなりにいる
  5. 読み流して文意を察せられる人がそれなりにいる
  6. 読み流しても誤読しにくい

少なくとも専門書では、商業品質の日本語の最低条件は上記の「3」だと思う。 そして著者と編集者には、上記の「5」以上を目指して推敲することが求められると思う。

大型書店が好きな自分にとって理想的なアプリだったhonto withのこと

ほぼすべての個人が専用の情報端末を持ち歩く社会でありながら、印刷製本された「紙書籍」というパッケージの形で知識や物語に接することを好む人がまだまだ十分に多く、その小売りに特化した店舗が「書店」として成立できていた2024年、それでも年々縮小する需要の前に小規模な書店はすでに次々と姿を消し、紙書籍を求める人たちの受け皿として役割を果たしていたのは都市部に残された大型書店だった。それら大型書店の広大な店頭には無数の紙書籍が並び、しかもそれは毎日のように増大していく。なぜなら紙書籍は、それを生み出すことを生業とする出版社にとって、たとえ読者の手に渡ることがなくても流通に載せさえすれば収益になる商材でもあったからだ。産業の末路である。

紙書籍を好む人の多くは大型書店が好きだったと思う。コンセプトが明確でエッジを効かせた小規模書店への憧れはあるけれど、必ずしも選書や店主が個人のバイブスに合うとは限らず、そもそも互いに内容が無関係のタイトルが無数にあって共通してるのは紙書籍というパッケージの形くらいという商品特性もあって、どうせなら一か所に全部集まってくれているほうがうれしい。大型書店には、あまたの紙書籍を自分の目で自由に選ぶ楽しさがある

とはいえ、大型書店は文字通り大型だ。自分が求めているタイトルがすでに具体的に決まっている場合に大型書店でそれを探し出すのはかなりしんどい。比較的最近発行された紙書籍であれば店側もそれなりに見つけやすい位置に配架してくれているけれど、そうでない紙書籍を大型書店の何百本もの棚を行ったり来たりしながら何時間も睨んで探していると、足も眼も痛くなる。より深刻な問題として、お腹が痛くなる。最後には仕方なく店員さんに声をかけたり、店頭の在庫検索端末にタイトルを打ち込んだりする。しかし、紙書籍のタイトルの文字列を正確に覚えていられる人や、メモを持ち歩けるような人ならともかく、あやふやにしか覚えてなかったり、あまつさえ装丁の雰囲気でしか把握してなかったりすると、恥ずかしい思いをしたり、端末の前でまごまごして気まずい思いをしたりすることになる。紙書籍を大型書店で探すのは、時間も肉体も精神も酷使する贅沢な活動なのだ。

こうした不快さを回避する手段として、紙書籍が好きで大型書店をよく訪れていた人の中には、もっぱらオンライン書店を利用するようになったという人が少なくないように思う。でもそれでいいのだろうか。いやむしろ大型書店はそれでいいのだろうか。よくないだろう。

こうした大型書店の顧客体験をかなり改善するサービスとして、honto withというスマホアプリがあった1スマホは紙書籍という商品にとって、可処分時間を奪い合うという意味で競合だろう。さらに店舗という小売り形態からすると、電子書籍のプラットフォームという意味でも競合になる。紙書籍の内容をカメラで撮影するといった行為も防がなければならない。それでも来店時に顧客が手にしている可能性が高いスマホは、もっぱら紙書籍を扱う店舗であったとしても、快適な顧客体験を提供する手段としては活用できる。honto withはそういう事実を正しく認識した人たちが開発したであろう、大型書店を頻繁に利用するユーザにとって痒い所に手が届くアプリだった。

honto withのどのへんがよかったのか、ぼく個人の使い方の一例を紹介しようと思う。

まず、自分は紙書籍のタイトルをツイッターBlueskyで知ることが多いのだが、気になったタイトルを見掛けたらとりあえずhontoのWebサイトで検索して「ほしい本」として登録しておく。ここでは登録をするだけで購入はしない。

honto.jpの「ほしい本に追加」ボタン

後日、丸善ジュンク堂に行ったら、スマホを取り出してhonto withアプリを立ち上げる。すると「欲しい本」タブが開いて、そこに過日「ほしい本」として登録していたタイトルたちがずらっと出てくる。明確な目的もなくふらふら店内を徘徊するのも悪くはないんだけど、「ああ、これこれ、この本が気になってたんだ!」というシグナルがあると、それだけでテンションが爆上がりする(前提として、丸善ジュンク堂に入るときには欲しい本が具体的に脳内にあるわけじゃなく、ただなんとなく大型書店を楽しみに行っているので、来店時に「ほしい本」に登録してた紙書籍のことはだいたい意識していない)。

honto withアプリの「欲しい本」タブ

honto withの「欲しい本」タブにはタイトルと書誌情報しかないので、これを店内を歩き回って探さなければならない。よくいく店舗のよくいく棚であれば、なんとなく土地勘があるので迷わず探せたりするけれど、「欲しい本」タブにそんな本はあまりない。しかしhonto withでタイトルをクリックして個別の商品ページに行くと、そこに「近くの書店で探す」というメニューが出る。

honto withの「近くの書店で探す」メニュー

このメニューを開くと、あらかじめ登録しておいた書店や現在地の近くの書店が表示されて、「その書店に在庫があるか、在庫がある場合はどの棚にあるか」が示される。あとは自分がいる書店でその棚に行き、そこから本を探し出せばいい。もちろん、棚が判明してもその棚には別の本もいっぱい並んでいるので、それほどさくっと目的の本が手に入るという利便性はないわけだけど、むしろその過程で周囲にある他の紙書籍のタイトルを眺めたり手に取ったりしたいから大型書店に来ているんだよ!

honto withアプリにおける在庫表示

honto withは、アプリの挙動や導線から察するに、この自分のような大型書店の使い方をしている人のユースケースをだいぶよく検討したアプリだったと思う。さらに、honto自体の機能として書店での取り置きができたり、店頭で購入したタイトルが自動的に管理できたり、溜まったポイントで電子書籍を入手できたりもして、これらも地味に「書店で紙書籍を買う」という体験を高めてくれるものだった。店頭にある紙書籍の現物のバーコードを撮影してそこから「ほしい本」に追加するという導線まであった。まさに紙書籍の店舗に求められる理想的なDXの姿のひとつだったと言っていいと思う。

でも残念ながらhonto withは2024年5月31日でサービスを終了するという発表があった。紙書籍の通販はすでに終了していたので予兆はあったとはいえ、アプリごとなくなるとは思っていなかった。Webブラウザで利用できるhonto.jpの機能はどうなるかわからないけれど、棚まで明示してくれる機能はいまでもhonto withにしかないので、少なくとも上記のような使い方ができなくなることは確定だろう。せめて登録している「ほしい本」だけは引き続き閲覧できるようであってほしい…。

いろいろ事情はあるはずだし、一利用者としてはもっと前にこういう使い方を示して少しでもユーザー増に貢献すべきだったかみたいなことを思わないでもないけれど、店舗でオープンに販売されている紙書籍を手に取って購入するという文化の一つの頂点にいまいるのかもしれないと感じたので、記録のつもりでhonto withのことを書き残しておくことにしました。honto withの開発と運営に携わってこられた皆様、ほんとうにありがとうございました。


  1. 「honto」という名称がついたアプリには「honto with」のほかに「hontoビューア」というものもあるが、これはhontoで販売している電子書籍を利用するためのものなので、紙書籍とはまったく関係がない。紙書籍のためのアプリは「honto with」のほうである。

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

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


「ラムダノートの本の読み方(私論)」シリーズはこれで第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の入門というわけではなく、プログラミング言語そのものという泥沼トピックへの入口として書かれた本であることがうかがい知れるでしょう。