Notices by きゅーけー (tojoqk@mastodon.tojo.tokyo), page 144

どうも証明木を読むのもなんか苦手みたいで、S 式を書き換えていく方が私には簡単だった。ACL2 はちょうど私の感覚に沿ってる感じがする。

依存型を使った直観主義論理の定理証明支援系は私には合わない感じだった。たぶん、理論的なところじゃなくてインターフェースが悪いんだと思う。

私は S 式を読むのが得意なので ACL2 と相性がもともと良いんだと思う。

型なしの定理証明支援系で使われてるやつって ACL2 以外にあるんかな。

不動点コンビネータ、文脈によって作れた方が嬉しかったり作れない方が嬉しかったりする。

ACL2 はいちおう型なし言語の一つだと思うんだけど、だとしたらすごく面白い話だと思うんだよな。

明日また来てください、本物の型のないプログラミング言語をお見せしますよ

浄土真宗の極楽浄土というのは死後についてあれこれ考えるのを止めさせるためにあるのであって考えさせるためにあるものではないんだ。

冥福の祈りが通じなかったら何か悪いことがあるとでも？死後にそんなクソみたいな設定を作るなっていう話。

そう考えると浄土真宗のお坊さんが冥福を祈るのをやめさせようとするのは妥当か……。

亡くなった方の家族が浄土真宗の場合、お坊さんだけじゃなくて普通に家族の方も不快にする可能性がある。というか私もだいぶ染まっているのでもはや親戚が亡くなったときに冥福を祈られたら苛立つと思う。

「私は哀しい」と個人的な範囲に留めた表明の方がよほど誠実ってもんよ

たとえば恣意的な仮定だけど、大事な人が死んだときあなたが嫌っている胡散臭い新興宗教の流儀で「魂が救済されますように」的なことを言われて本当に嬉しいのか、みたいな話はある

結局物言わぬ死者に何か与えたり望んだりしている時点で、本質的には死者を自分が気持ちよくなるための玩具にしてるんじゃねえのみたいな感想もある。 †守護霊† とかと何が違うのさ

> ようはあんたの祈りパワーには何の効力もないから祈るな。自分にそんな力があると驕るなってことなんだよな。

いや、やっぱこれなかなかやばいな。日本では割と祈りパワーに頼るの一般的だし……。だいたい八百万の神の文化は現代にも普通に浸透しているわけでこういうことを人前で表明するのはちょっと危ないんだよな。

なんかというか日本人は無宗教だと思っているだけで普通に日本に生きているだけで十分宗教的な人になっちゃうんだよな。

浄土真宗って普通に一般人よりも「無宗教」なのであんま舐めない方がいい。

ほんそれ……。

ようはあんたの祈りパワーには何の効力もないから祈るな。自分にそんな力があると驕るなってことなんだよな。

いや、ちゃんとそれが何を言っているのかを真面目に考えると別に浄土真宗でなくても冥福を祈るのって普通に失礼な感じするし浄土真宗の民が文句を言うロジックは理解可能なんだけど、人々は意味を深く考えることなく冥福を祈っているのでそんなことをいっても仕方がないのだ……。

浄土真宗オタクなせいで冥福表現みるたびに何か思ってしまうの病的すぎる。確かに宗教的な主旨としてそれがよくないことは分かるんだけどそれって浄土真宗だけの話だし、そんなに目くじらたてなくてもいいでしょと思う。ただ、日本の浄土真宗率の高さまで考慮するとああ仏教は衰退しているんだな……。とは思うけど。