Timeline for it list by senooken, page 49

あと Linux-libre から Linux カーネルに戻すとなんか Bluetooth ヘッドホンが動くという微妙なベネフィットもあるが、やっぱちょっと嫌なんだよな。GNU の推奨する OS 状態ではなくなっちゃうし〜〜〜。

あんまり Guix System に nongnu リポジトリの Linux を入れたくない気持ちがあってなー。

自分自身、せっかくタブレット的にも使える laptop なのになんかとびでてて邪魔かなとは思ってしまっている。

カーネルを Linux から Linux-libre に戻したんだけど、多方面から「その Wifi アダプタは邪魔だ」と言われていてちょっとまた Linux-kernel に戻すか悩んでる。

だれもスマホOS寡占の文脈で Replicant に言及してなかったので Twitter で仕事してきた。

＞ スマホOS寡占が問題なら Replicant というスマホの OS が動作するハードウェアの販売に補助金を出せばいいんじゃないかな。既に自由な OS が存在するわけなんで、そちらを発展させればよい。＞ https://replicant.us

https://twitter.com/tojoqk/status/1516837647804960768?s=20&t=6NonH9GCbycm9fG1Q9tyEQ

Firefox だと気軽に DRM 付きのコンテンツが再生できるわけなんだけど、DRM の善し悪しを脇に置いて DRM 前提のサブスク的なコンテンツが利用可能な環境は生活に多大な悪影響を与えることがあるとして、自由ソフトウェアとは全然関係ない文脈で DRM 縛りを始めた。

Guix System の GNU のリポジトリでは GNU IceCat か ungoogled-chromium しか選択肢がなくて正直なところ ungoogled-chromium の方が使いやすいのは結構致命的な気がするんだよな。GNU IceCat は色々とサイトが動かなかったりして不便なことが多いという現実がある。

他の手段で Firefox をインストールする手段はあるんだけど、なんかそれでは駄目な気持ちがある。(なんか自由ソフトウェアを徹底するモチベが高まってる)

ungoogled-chromium、前よりも拡張機能のインストールが楽になった気がする。気のせいだろうか。以前の私がよく理解してなかったのか、手順が変わったのか分からん……。

Agda の挑戦はまた今度にして二分探索木の記事を書くか(ハフマン符号化の記事は説明しないといけないことが多くなりすぎてつらくなったので一旦中断した)。

やっぱりS式って読みやすいんじゃないのかな。本当にこれってただの慣れの問題なんだろうか。覚えないといけない記号は少なくて済むしネストされている構造はそのままネストされているおかげで理解も簡単だし良いことづくめな気がするんだけど……。

型も関数も S 式で書いて欲しい。なんか複雑で分けわからん……。

Agda のチュートリアル読んでるんだけど、これと比べると ACL2 って簡単なのか難しいのかよく分からないな。

ACL2 と比べて Agda は学習曲線が急激でないという点で簡単なのかもしれないと感じてる。ただ正直、証明を人間が書くので細かすぎてつらい。とはいえ私が Agda のチュートリアルを読んでてきついと感じる理由の 90％ は S 式じゃないからかもしれない……。

Emacs が最強の IDE になっている世界、なんか絶滅の渦に入っている気がする。Agda は VSCode に対応したから絶滅の渦から抜けられたということか……。

知らなった。重要情報じゃん。

Agda、VSCode でも使えるようになったのか……。コミュニティの規模の大きさを感じる……。

いまなら Agda いける気がするし、ちょっと Agda もやってみようと思う。ACL2 のおかげで多くのアルゴリズムは数学的帰納法で証明できると学んだし。

インボイス制度なるものが始まる予定だというのを今日始めてしった。これは結構影響の大きいやつなんだけど、間接税が成立し消費税は消費者が払った税金だと考えているとこれに対して反対する声について理解できないだろうな。

実際には消費税というのは輸出企業等を除いた売上に対する課税であって消費に対して課税されているというのはただの欺瞞に過ぎない。

@tacumi いちおう ACL2 は Common Lisp のサブセットなんで Common Lisp を知っていればだいぶ有利だとは思います。だからといって学習コストが低いとはいえませんが……。

@tacumi ラムダノートさんの本って古本屋に出回ってるもんなんですかね……。

下記の本で著者は完全に ACL2 へと誘導しているのですが訳者の方は Coq へと誘導しているのがつらいところです(涙)。この本を読んでも ACL2 の詳細な使い方は結局学べないのですが、ACL2 を使うに当たって前提として知っておくべきことは学べるという感じなんで良いんですよね(ACL2 だと簡単な定理は自動証明するのでまずその仕組みが謎だし、簡単な定理であば自動証明され自動証明できない場合はどう対処すればいいか分からなくて詰むためいきなり ACL2 を使っても練習にならない)。なので、もしも ACL2 をやるのであればとてもおすすめです。

訳者の方が Coq を勧めているようなのでおそらく他の定理証明支援系に進むにしても役立つ基礎的な内容なのだと思います。

『定理証明手習い』 – 技術書出版と販売のラムダノートhttps://www.lambdanote.com/collections/littleprover

@tacumi ラムダ計算は勉強しなくても大丈夫ですね。学ぶ必要があるのは高校レベルの数学的帰納法の知識と、定理証明の基本的なところ(公理や既存の定理を使って式を変形する)です(場合によっては順序数とかも必要になるのですが……)。あと再は帰関数が書けるのは前提として必要なくらいですね。これらについては『定理証明手習い』という本で学べます。

これだけならまだしも ACL2 になると自動定理証明なので、 自動証明できない定理については、ACL2 に補助定理を教えたりヒントを与えたりしないといけないわけなんですが、補助定理の書き方には細かいルールがあって書き方によって ACL2 の挙動は変わるんですよね……。これを学ぶ学習コストに耐えないと ACL2 は全く使えないといっても過言ではないところが痛いんです。