niszetの日記

アナログCMOS系雑用エンジニアが頑張る備忘録系日記

定理証明手習いを読んだ

とりあえず1周目

まえおき

定理証明手習いは"The Little Prover"の翻訳版です。出版社さんのページはこちら。物理本のみ、電子書籍のみ、両方の3つがあります。

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

本書の特徴は↑のページに簡潔に書かれているので、子の記事よりもそちらを読んだ方が良いのではと思います。

また、正誤情報があります。2つほど。1つ目のatomの方は先に知っておいた方が混乱がなくて良いでしょう。この分量で2つしかないのはすごい少ないと思う。

github.com

感想

さて、本書はSchemerシリーズ?のうちの一冊のようです。この本を読むためにLispの深い知識はそれほど必要ないですが、基本的な文法は本文中では特に説明されないのでそのレベルは事前に知っていた方が良いです。私はlisp方言のひとつを使ったことがあるので基本的な書き方は知っていますが、正しいlisperではないので(C言語風のシンタックスシュガーがあったので殆どそっちで書いていたほど)lisp言語的に不明な点は都度調べていました。

また、定理証明手習い+感想で検索したところ、こちらの記事がhitしました。読み進めていく過程の記事もあるので、詰まった部分があったら参考にすると良いかも…(私はそれら記事は未読)

http://kb84tkhr.hatenablog.com/entry/2017/12/30/170715

1周読んだだけで理解できるとは思っていないのですが、私の現時点での理解では与えられた主張を公理や証明済み定理を使って証明をしていく。証明とは最終的に`tで終わることを示すことで、恒真式だと考えれば良さそう。いくつかの法則を使えば、式を値まで評価せずに構文的な対応関係だけから簡約化が出来る。これはある意味で遅延評価的であって、最終的に値まで評価済みの場合は関数を適用するなどをしている。

基本的には記述の置き換えの形で証明を進めていくので、式変形を追うのはそれほど大変ではない。ただし、過去の定理等を覚えてない場合は都度読みに戻らないといけない(私はそうでした)が。

中盤から後半で再帰帰納法を使うようになっていくが、この時点で前半の理解があいまいだと辛くなってくるので、必要なら前の章に戻って読み直すと良さそう。突然式が爆発的に増えるときは大体帰納法の式展開なのでそのページにしるしをつけて見直すと良さそう。式のミスはないので、じっくり置き換えて変換していけば正しい変形が出来るはずです。

前提を作るのは8章以降になるので、そこまでは与えられた前提に対して黙々と証明をしていきます。もくもくもくもく。。。

よくある?論理学の本で最初から全てを与えられていく形式ではなく、手を動かしながら一つずつ証明をこなしていくことで理解を深めていく感じですね。連言は8章、含意は9章で言葉が出てきますが、そこまでそういったことを意識せずにやってました。いわれてみれば、そうだな…と。

あと、この本は索引が凄いことになってます。注釈書かれている言葉が索引に入ってたり(普通はないと思う)。面白いのでちょっと眺めてみてください。困ったら索引から引けると思うので、困ったら索引を見ましょう。 また、本文は青と赤の色が使われている箇所があり、今どこに注目すればよいかが分かりやすいです。印刷も見やすい。あと表紙のゾウ?が可愛いですね。

また、最近興味が出てきた形式手法の証明はこの定理証明手習いで得たものが活きるのではと思っています(まだわからない。あとこの本をやってから形式手法に興味が出てきたので鶏と卵の関係)

と、とりとめもなく書いてしまいましたが、とても良書でした。本のタイトルからは自分にとってとても遠い本なのでは?と思っていたのですが、なんだかんだで一気に読み切ってしまいました(逆に、間をあけて読むのは難しいですが…忘れてしまうので)

まだ理解が浅いので、もう少し理解が深まったところでまた感想を書くかもしれません。呟くだけかもしれないけど。

(Pandoc) VSCode向けにPandocのLuaフィルタ用のsnippetを作ってみた

VSCodeのExtensionってお手軽に作れますね…

VSCodeの使いこなしが足りないと思ってちょっと最近 C&R出版のこの本を読んで使い方を学んでいます。

www.c-r.com

これの最後に自作の拡張を登録するというのがあったのでやってみました。ひとまず自分がまだわかっている方にいるはずのPandoc関係で、コード書く方でサポート用のパッケージが欲しいなと思っていたので、Lua filter向けにまずはsnippetを作ってみようということで、出来ました。

marketplace.visualstudio.com

色々と罠があったので、追って知見は放出しますが、それ以外はかなり気軽に登録、公開が出来て良いですね…。

まだ出来ることの全体を把握できていないので中途半端な出来ですが、とりあえず使いながら更新していけばよいかな…と思っています。GitHub上にrepo作ったのでissueとかあれば(英語で)お願いします。

これとは別にPandoc's Markdownの面倒くさい記法を肩代わりしてくれるようなのも作ろうかなーと思っています。追々ね。

VSCode本はもう一冊購入したので、そちらもあわせて読んでいきたいですね…。

VSCodeの拡張のlanguage-configuration.jsonのmarkerは1文字以上記号が含まれないといけない?(メモ)

明記された資料が見つからない…

VSCode向けの拡張を作っていて、Pandoc's Markdown:::で囲う部分をfoldしたかったのだが…。

特にそういうことは書かれていないのだけど、色々試しているとそんな感じの挙動をした。片方に1文字でも英字?が入っていれば他が記号でfoldingは可能なのだが…。

code.visualstudio.com

ということで、language serverの方を見ていかないといけないかも…。ということで、今度はこちらを読み始めることに。最後の章がLSPに関する話なので、これを読んでいくのです…

gihyo.jp

Pandoc界隈2人目のsponsorとなったniszetであった

記録を付けていこう。

書いたまま放置していたんですが、この日記を書いた1/10の前日?、niszetはtarleb氏のsponsorになったのでした。

f:id:niszet:20200109195548p:plain

これでPandoc界隈の2人に毎月☕を配る係?になったわけです。

tarleb氏はPandocのLua filterまわりのすごいcontributorで、最近だとJIRA Readerを一人で書いてしまうとか、すべてを列挙するのが難しいくらい色々やってます。私がPandocのLua filter関係のモジュールのバグ(関数名がマニュアル記載のモノと違う)についてレポートしたら、PR投げてみそってことでやらせてもらったのもあって、とても親しみを感じています(単純なniszet氏)

ということで、みんなも気軽にsponsorになったらいいんじゃないかな、という日記でした。

(Pandoc) テンプレートにあるスタイルの件の補足

一体何が正しいのでしょうか…。

以前こんな記事を書いたのですが、reference.docxをあらかじめ作っておく場合と-t docx でファイルを出力した場合とで、実際にはどの程度の差があるのかを見ておきます。

niszet.hatenablog.com

あらかじめ、適当な入力ファイル(空でも良い)から -t docx -o test.docx で test.docx という名前でファイルを保存しておきます。Rのofficerパッケージでスタイルを確認できるのでこれを使います。結果はdata.frameになっているので、dplyrパッケージで差分を確認できます。

> library(officer)
> library(magrittr)
> officer::read_docx("test.docx") %>% officer::styles_info()
   style_type             style_id             style_name is_custom is_default
1   paragraph               Normal                 Normal     FALSE       TRUE
2   paragraph             BodyText              Body Text     FALSE      FALSE
3   paragraph       FirstParagraph        First Paragraph      TRUE      FALSE
4   paragraph              Compact                Compact      TRUE      FALSE
5   paragraph                Title                  Title     FALSE      FALSE
6   paragraph             Subtitle               Subtitle     FALSE      FALSE
7   paragraph               Author                 Author      TRUE      FALSE
8   paragraph                 Date                   Date     FALSE      FALSE
9   paragraph             Abstract               Abstract      TRUE      FALSE
10  paragraph         Bibliography           Bibliography     FALSE      FALSE
11  paragraph             Heading1              Heading 1     FALSE      FALSE
12  paragraph             Heading2              Heading 2     FALSE      FALSE
13  paragraph             Heading3              Heading 3     FALSE      FALSE
14  paragraph             Heading4              Heading 4     FALSE      FALSE
15  paragraph             Heading5              Heading 5     FALSE      FALSE
16  paragraph             Heading6              Heading 6     FALSE      FALSE
17  paragraph             Heading7              Heading 7     FALSE      FALSE
18  paragraph             Heading8              Heading 8     FALSE      FALSE
19  paragraph             Heading9              Heading 9     FALSE      FALSE
20  paragraph            BlockText             Block Text     FALSE      FALSE
21  paragraph         FootnoteText          Footnote Text     FALSE      FALSE
22  character DefaultParagraphFont Default Paragraph Font     FALSE       TRUE
23      table                Table                  Table     FALSE       TRUE
24  paragraph       DefinitionTerm        Definition Term      TRUE      FALSE
25  paragraph           Definition             Definition      TRUE      FALSE
26  paragraph              Caption                Caption     FALSE      FALSE
27  paragraph         TableCaption          Table Caption      TRUE      FALSE
28  paragraph         ImageCaption          Image Caption      TRUE      FALSE
29  paragraph               Figure                 Figure      TRUE      FALSE
30  paragraph      CaptionedFigure       Captioned Figure      TRUE      FALSE
31  character         BodyTextChar         Body Text Char      TRUE      FALSE
32  character         VerbatimChar          Verbatim Char      TRUE      FALSE
33  character    FootnoteReference     Footnote Reference     FALSE      FALSE
34  character            Hyperlink              Hyperlink     FALSE      FALSE
35  paragraph           TOCHeading            TOC Heading     FALSE      FALSE
36  paragraph           SourceCode            Source Code      TRUE      FALSE
37  character           KeywordTok             KeywordTok      TRUE      FALSE
38  character          DataTypeTok            DataTypeTok      TRUE      FALSE
39  character            DecValTok              DecValTok      TRUE      FALSE
40  character             BaseNTok               BaseNTok      TRUE      FALSE
41  character             FloatTok               FloatTok      TRUE      FALSE
42  character          ConstantTok            ConstantTok      TRUE      FALSE
43  character              CharTok                CharTok      TRUE      FALSE
44  character       SpecialCharTok         SpecialCharTok      TRUE      FALSE
45  character            StringTok              StringTok      TRUE      FALSE
46  character    VerbatimStringTok      VerbatimStringTok      TRUE      FALSE
47  character     SpecialStringTok       SpecialStringTok      TRUE      FALSE
48  character            ImportTok              ImportTok      TRUE      FALSE
49  character           CommentTok             CommentTok      TRUE      FALSE
50  character     DocumentationTok       DocumentationTok      TRUE      FALSE
51  character        AnnotationTok          AnnotationTok      TRUE      FALSE
52  character        CommentVarTok          CommentVarTok      TRUE      FALSE
53  character             OtherTok               OtherTok      TRUE      FALSE
54  character          FunctionTok            FunctionTok      TRUE      FALSE
55  character          VariableTok            VariableTok      TRUE      FALSE
56  character       ControlFlowTok         ControlFlowTok      TRUE      FALSE
57  character          OperatorTok            OperatorTok      TRUE      FALSE
58  character           BuiltInTok             BuiltInTok      TRUE      FALSE
59  character         ExtensionTok           ExtensionTok      TRUE      FALSE
60  character      PreprocessorTok        PreprocessorTok      TRUE      FALSE
61  character         AttributeTok           AttributeTok      TRUE      FALSE
62  character      RegionMarkerTok        RegionMarkerTok      TRUE      FALSE
63  character       InformationTok         InformationTok      TRUE      FALSE
64  character           WarningTok             WarningTok      TRUE      FALSE
65  character             AlertTok               AlertTok      TRUE      FALSE
66  character             ErrorTok               ErrorTok      TRUE      FALSE
67  character            NormalTok              NormalTok      TRUE      FALSE

こちらはマニュアルのとおりにテンプレートを生成した場合のテンプレートに含まれるスタイルの一覧。

> officer::read_docx("custom-reference.docx") %>% officer::styles_info()
   style_type             style_id             style_name is_custom is_default
1   paragraph               Normal                 Normal     FALSE       TRUE
2   paragraph             BodyText              Body Text     FALSE      FALSE
3   paragraph       FirstParagraph        First Paragraph      TRUE      FALSE
4   paragraph              Compact                Compact      TRUE      FALSE
5   paragraph                Title                  Title     FALSE      FALSE
6   paragraph             Subtitle               Subtitle     FALSE      FALSE
7   paragraph               Author                 Author      TRUE      FALSE
8   paragraph                 Date                   Date     FALSE      FALSE
9   paragraph             Abstract               Abstract      TRUE      FALSE
10  paragraph         Bibliography           Bibliography     FALSE      FALSE
11  paragraph             Heading1              Heading 1     FALSE      FALSE
12  paragraph             Heading2              Heading 2     FALSE      FALSE
13  paragraph             Heading3              Heading 3     FALSE      FALSE
14  paragraph             Heading4              Heading 4     FALSE      FALSE
15  paragraph             Heading5              Heading 5     FALSE      FALSE
16  paragraph             Heading6              Heading 6     FALSE      FALSE
17  paragraph             Heading7              Heading 7     FALSE      FALSE
18  paragraph             Heading8              Heading 8     FALSE      FALSE
19  paragraph             Heading9              Heading 9     FALSE      FALSE
20  paragraph            BlockText             Block Text     FALSE      FALSE
21  paragraph         FootnoteText          Footnote Text     FALSE      FALSE
22  character DefaultParagraphFont Default Paragraph Font     FALSE       TRUE
23      table                Table                  Table     FALSE       TRUE
24  paragraph       DefinitionTerm        Definition Term      TRUE      FALSE
25  paragraph           Definition             Definition      TRUE      FALSE
26  paragraph              Caption                Caption     FALSE      FALSE
27  paragraph         TableCaption          Table Caption      TRUE      FALSE
28  paragraph         ImageCaption          Image Caption      TRUE      FALSE
29  paragraph               Figure                 Figure      TRUE      FALSE
30  paragraph      CaptionedFigure       Captioned Figure      TRUE      FALSE
31  character         BodyTextChar         Body Text Char      TRUE      FALSE
32  character         VerbatimChar          Verbatim Char      TRUE      FALSE
33  character    FootnoteReference     Footnote Reference     FALSE      FALSE
34  character            Hyperlink              Hyperlink     FALSE      FALSE
35  paragraph           TOCHeading            TOC Heading     FALSE      FALSE

で、これだと差分が良くわからないので、dplyr::anti_join()を使って差分を出します。

library(dplyr)
> dplyr::anti_join(gendoc, refdoc)
Joining, by = c("style_type", "style_id", "style_name", "is_custom", "is_default")
   style_type          style_id        style_name is_custom is_default
1   paragraph        SourceCode       Source Code      TRUE      FALSE
2   character        KeywordTok        KeywordTok      TRUE      FALSE
3   character       DataTypeTok       DataTypeTok      TRUE      FALSE
4   character         DecValTok         DecValTok      TRUE      FALSE
5   character          BaseNTok          BaseNTok      TRUE      FALSE
6   character          FloatTok          FloatTok      TRUE      FALSE
7   character       ConstantTok       ConstantTok      TRUE      FALSE
8   character           CharTok           CharTok      TRUE      FALSE
9   character    SpecialCharTok    SpecialCharTok      TRUE      FALSE
10  character         StringTok         StringTok      TRUE      FALSE
11  character VerbatimStringTok VerbatimStringTok      TRUE      FALSE
12  character  SpecialStringTok  SpecialStringTok      TRUE      FALSE
13  character         ImportTok         ImportTok      TRUE      FALSE
14  character        CommentTok        CommentTok      TRUE      FALSE
15  character  DocumentationTok  DocumentationTok      TRUE      FALSE
16  character     AnnotationTok     AnnotationTok      TRUE      FALSE
17  character     CommentVarTok     CommentVarTok      TRUE      FALSE
18  character          OtherTok          OtherTok      TRUE      FALSE
19  character       FunctionTok       FunctionTok      TRUE      FALSE
20  character       VariableTok       VariableTok      TRUE      FALSE
21  character    ControlFlowTok    ControlFlowTok      TRUE      FALSE
22  character       OperatorTok       OperatorTok      TRUE      FALSE
23  character        BuiltInTok        BuiltInTok      TRUE      FALSE
24  character      ExtensionTok      ExtensionTok      TRUE      FALSE
25  character   PreprocessorTok   PreprocessorTok      TRUE      FALSE
26  character      AttributeTok      AttributeTok      TRUE      FALSE
27  character   RegionMarkerTok   RegionMarkerTok      TRUE      FALSE
28  character    InformationTok    InformationTok      TRUE      FALSE
29  character        WarningTok        WarningTok      TRUE      FALSE
30  character          AlertTok          AlertTok      TRUE      FALSE
31  character          ErrorTok          ErrorTok      TRUE      FALSE
32  character         NormalTok         NormalTok      TRUE      FALSE

となります。スタイル名がTok で終わるものはコードのハイライト用の文字スタイルになり、全部で31種類あります。

> dplyr::anti_join(gendoc, refdoc) %>% filter(str_detect(.$style_name, "Tok")) %>% count()
Joining, by = c("style_type", "style_id", "style_name", "is_custom", "is_default")
# A tibble: 1 x 1
      n
  <int>
1    31

残る1つは"Source Code"でこれは段落スタイル。これがテンプレートを生成した際に含まれないスタイルです。これはマニュアルにも載っていません。

さて、スタイル一覧はマニュアルに記載がありますが、このマニュアルにあってPandocのHaskellのコードからは読み取れなかったスタイルは以下の2つです。単に私の抜けかもしれないですが…。

  • Caption
  • Default Paragraph Font

また、ソースコードに記載があるが、-t docx を指定して生成したdocx、reference.docx に存在しないスタイルは下記の2つです。

  • CommentText
  • CommentReference

実際のスタイル名は" "で分かれていると思いますが、文字列としてコードにあるのはこちらでした。

この辺りは想定しているものと同じになっているのかがわからないので、discussで聞いてみようと思って1週間が経ちました。そろそろ聞きますね…。

(Pandoc) Pandoc 2.9.2 の _G(メモ)

Lua filterも色々と改良されているので常に調べていかねばならない。

Pandoc 2.9.2 で Luaフィルタ内から_Gに参照した際にアクセスできるモジュールやグローバル変数の一覧です。あとで自分で参照する用。

コードはこれ。

function Doc (e)
  -- print(_G)
  for k, v in pairs(_G) do
    print(k,v)
  end

結果はコレ。

io      table: 00000000071de8a0
PANDOC_READER_OPTIONS   table: 0000000007254760
select  function: 0000000003b0f550
require function: 00000000071de6e0
tonumber        function: 0000000003b0f5f0
_VERSION        Lua 5.3
make_indexing_function  function: 00000000071f5360
next    function: 0000000003b0fb30
dofile  function: 0000000003b101c0
collectgarbage  function: 0000000003b0fd30
coroutine       table: 00000000071de720
getmetatable    function: 0000000003b10160
os      table: 00000000071e1ce0
add_accessors   function: 0000000007254ee0
assert  function: 0000000003b10240
ipairs  function: 0000000003b0fae0
rawlen  function: 0000000003b0f8d0
FORMAT  html
xpcall  function: 0000000003b0fe00
print   function: 0000000003b0f980
loadfile        function: 0000000003b100f0
rawget  function: 0000000003b0f880
string  table: 00000000071e1b60
Doc     function: 000000000724ed00
_G      table: 00000000072cee90
setmetatable    function: 0000000003b0fec0
PANDOC_SCRIPT_FILE      debug.lua
PANDOC_API_VERSION      1.20
pcall   function: 0000000003b103a0
augment_attr_setter     function: 000000000724f7b0
pandoc  table: 00000000071f9a20
debug   table: 00000000071e1620
utf8    table: 00000000071e15a0
type    function: 0000000003b0f4c0
rawequal        function: 0000000003b0f930
tostring        function: 0000000003b0f520
error   function: 0000000003b0fca0
load    function: 0000000003b0fff0
table   table: 00000000071de860
package table: 00000000071dea20
PANDOC_VERSION  2.9.2
PANDOC_STATE    Pandoc CommonState: 00000000071de808
math    table: 00000000071e1760
rawset  function: 0000000003b0f820
pairs   function: 0000000003b102c0

前回は下記の記事、

niszet.hatenablog.com

でちょっと調べていましたが、この時の_Gと差分を見ると augment_attr_setterが追加されているようです。それ以外は同じかな。その下にあるものは変わっているかもしれませんが。pandoc.pandocの中身は一致。思ったより差異がなくてちょっと残念…

コードのコメントを見るとモンキーパッチって書いてあるのでaugment_attr_setterは今後も安定して使えるかは不明です。何か良いアイディアがあればPR送るのも良いかもしれませんね。私は持ってませんが…。

(Pandoc) Pandoc 2.9.2 時点でLua filter側からPandocの実行時のオプション等は拾えない (メモ)

備忘録です

昨日数時間かけてLuaフィルタ中で使用できる各種モジュール、ログを生成してみるとか色々やってみましたが、現時点Pandoc 2.9.2 ではLuaフィルタの内部からPandocの実行時のオプション、引数その他を得る方法はなさそうです。

いくつかの情報、例えばFORMATとかは与えられているので、PandocからLuaの方へ情報を引き渡してあげることで初めて見えるようになるのだと思います。ReaderのオプションやStateも送られては来るのですが・・・

Pandoc の variable (-v) とか指定したテンプレートファイルの情報が得られれば(Lua)filterでもっと色々出来るのですが(とはいえ、あまりにフィルタ側に色々持たせるとそれはそれで本末転倒というか、複雑さが増すし(意図したものでないとしても)悪いことされるリスクは増えるので、なんとも…。

時間かけた割に収穫がなかったのでせめて供養に日記でも…という内容でした。