PCを買うよりも新しい机を買おうと思い直した。

PCを新調しようと定期的に思いついてしまうが、いや、結局今のマシンでも十分であるし、その金で机を新しくしたほうがいいと思い直した。 (つよつよPCを作るくらいなら、AWSでremote 開発環境を作った方が安く済む。また、PCの資産としての価値は低いから。)

現在の机はIKEAのもので、だいぶぼろぼろになっている。また、机の広さも足りなさを感じている。

diary

午前中。

チキンのトマト煮を作った。間違えてカットトマトではなくホールトマト缶を買っていたことに気づいたが、うまく作れた。

FEBCで日曜礼拝を聞く。

午後は頭痛がひどくて、そして虚無が襲い掛かってきた。何にも手がつかなくなった。

感情をコントロールするためには、体を動かす必要があるが、その気持ちすらわかない場合にどうすればいいのだろうか。

愛の実現のために

信仰は望んでいる事柄を確信し、見えない事実を確認すること。つまり、神の存在や神の愛を確認できる。

行いが伴わないなら、信仰はそれだけでは死んだもの。信仰という心から神へ愛を伝えるチャネルを成長させるためには、行い・活動が必要である。信仰が愛を導き、行動がその愛の実現を導く。御言葉を読み、神が私達の魂に入り込む様を見、祈るという行動こそが、神様に愛を本物で成熟したものへと涵養する。

私達が神を愛するのは、神がまず私達を愛してくださったから。神からの愛は、信仰や行動による報酬ではない。

私は他人とその心や魂の存在を疑っている。だから、他人を愛することへの確信がない。だから、信仰を持ち、行動をし、神を通して、その存在に確信を持ち、愛を実現させる。

『Standard ML 入門』

pp. 259 - 261
- 筆者が、なにをやるか、どうやるかを明示してくれているので、読者の自分は、自分が有能なのではと勘違いしてしまっているところがある。
問18.30
- CopyDirStreamの以前の実装があるので、リストアップはできそう。
- 実装する方針は立てた。

Concrete Semantics

Exercise 9.7をとき直そうと思い立つ
- WhileTrueのケースの証明ができなくて詰まっていた
- 先人の回答をカンニングした。
- 条件を間違えていたことに気づいた。
- erase_correctを終えたが、ほか2つの性質については示していない。
Sec_Typingの言わんとしていることを理解していないことがわかったので、次回以降はまた10章に戻る。

カンニングしてわかったこととして、以下の書き方がある。

proof (csses)
    assume "A"
    ...
next
    assume "\not A"
    ...
qed

と同じことは

proof (csses "A")
    case True
    ...
next
    case False
    ...
qed

というのが使えることがわかった。