kb84tkhrのブログ

何を書こうか考え中です あ、あと組織とは関係ないってやつです 個人的なやつ

『定理証明手習い』購入

微妙な行き詰まり感からついこれをポチッと・・・ 

『定理証明手習い』www.lambdanote.com

む、埋め込みがうまくいってない?
まあいいか

中身は見ずにポチった
すでにほぼ信仰

電子書籍も紙書籍もあってちょっと迷ったけど応援になるかとも思って両方注文
少々高いのはやむを得まい
正直数が出る本とは思えないし

電子書籍DRMとかのかかってない普通のPDFのように見える
動的に生成してるみたいだけど何をやってたのかなあ
名前でも埋め込んでるのかと思ったけどそういうこともなさそうだ

PDFは古めのKindle Paperwhiteに送ってもまあギリギリ読んでもいいかな、
くらいの字の大きさ
iPadかPCで読むほうが無難か
まあ紙書籍が来るまでの話

ポチっただけなのでまだ感想というほどのものはないけど
この時期にこの本が出たっていうのは何かの縁かもしれない

要するに、この証明支援器によって確かめられるのは「論理式」が確かに論理式であり、「証明」が確かに証明であることだ。(序文)

「論理式」が確かにIsFormであり、「証明」が確かにIsProofであるってことですね!

表紙には名前が出てなくて気づかなかったけど代表取締役自身が訳してるとか
Amazonには出してない(みたい)とか*1はコンパクトにやっていこうってことかしら
なにしろラムダノートさんにはがんばっていただきたい
The Reasoned Schemerにも期待している

*1:書名を間違えて検索してたからでした