PCを買うよりも新しい机を買おうと思い直した。
PCを新調しようと定期的に思いついてしまうが、いや、結局今のマシンでも十分であるし、その金で机を新しくしたほうがいいと思い直した。 (つよつよPCを作るくらいなら、AWSでremote 開発環境を作った方が安く済む。また、PCの資産としての価値は低いから。)
現在の机はIKEAのもので、だいぶぼろぼろになっている。また、机の広さも足りなさを感じている。
diary
午前中。
チキンのトマト煮を作った。 間違えてカットトマトではなくホールトマト缶を買っていたことに気づいたが、うまく作れた。
FEBCで日曜礼拝を聞く。
午後は頭痛がひどくて、そして虚無が襲い掛かってきた。何にも手がつかなくなった。
感情をコントロールするためには、体を動かす必要があるが、その気持ちすらわかない場合にどうすればいいのだろうか。
愛の実現のために
信仰は望んでいる事柄を確信し、見えない事実を確認すること。つまり、神の存在や神の愛を確認できる。
行いが伴わないなら、信仰はそれだけでは死んだもの。信仰という心から神へ愛を伝えるチャネルを成長させるためには、行い・活動が必要である。信仰が愛を導き、行動がその愛の実現を導く。 御言葉を読み、神が私達の魂に入り込む様を見、祈るという行動こそが、神様に愛を本物で成熟したものへと涵養する。
私達が神を愛するのは、神がまず私達を愛してくださったから。神からの愛は、信仰や行動による報酬ではない。
私は他人とその心や魂の存在を疑っている。だから、他人を愛することへの確信がない。だから、信仰を持ち、行動をし、神を通して、その存在に確信を持ち、愛を実現させる。
今日の勉強
sml
『Standard ML 入門』
- pp. 259 - 261
- 筆者が、なにをやるか、どうやるかを明示してくれているので、読者の自分は、自分が有能なのではと勘違いしてしまっているところがある。
- 問18.30
- CopyDirStreamの以前の実装があるので、リストアップはできそう。
- 実装する方針は立てた。
isabelle
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
というのが使えることがわかった。