当ブログをスマホで開くと文字がめちゃくちゃ小さくなって読みづらくなることがわかった。ページを拡大したら自動的に改行位置が変わって読み手がフォントサイズを調整できればいいと思ったが、とりあえず現状では起こらない。
さっそくGoogle ChromeのF12(開発者ツール)で調査。Chromeのツールでスマホ表示をシミュレートすることができるのでそれで直そうという算段。いわゆるレスポンシブデザインとやらを自分で実装するのは初めてだったので「css smartphone」でググると日本語の初心者向けっぽい有象無象がたくさん出てくる。
W3CSchoolsは2ページ目の3件目ぐらいに出てきた。読んだら画面の幅でスマホ表示とそうでないものとを切り替えるらしい。てっきりUser Agentか何かで切り替えるものだと思っていた。というかそういうサイトもあったはず。
それで参考にするページにGitHubを選択したが、Chromeのシミュとスマホ実機とで表示されるフォントサイズが違う！僕のスマホ実機のフォントサイズの設定に関連が疑われるが、設定をいじって試行錯誤する時間はなかったのでとりあえず放置。
ラムダ計算では添字の名前が変わっただけの式(α-equivalence)を同一視するのが便利なのだが、そもそも添字に名前を振らず、一番近い添字への番号を書く記法であるDe Bruijn index がある。
現在の僕のプログラムだと既存のラムダ式からGenetic Algorithm(GA)で出てくる交叉を使って新しいラムダ式を生成する際に、bound variableがfree variableに化けてしまう問題がある。計算がおかしくなるわけではないが、「解になりえない解候補」になってしまうため可能であれば修正したい。
で、添字に名前を付ける必要がないDe Bruijn indexに注目したわけだが、肝心のsubstitutionのやり方で詰まった。通常の記法との相互変換はまっさきに作れたので、それを代入しながら適当に式変形していけば簡単に導出できるだろうと思っていたがそう簡単にはいかなかった。前述のWikipediaの記事に載っているようだから次はそれを読んでみようと思う。