TojoQK の投稿

ACL2で自然数の和の剰余と剰余同士の和の剰余の等しさを示す

<2022-06-27 月 13:00>

ACL2 で剰余関連の証明の試みをしたときの個人的な覚え書きです。

腕時計 F-201WA の個人的な用途について

<2022-05-29 日 12:40>

CASIO の腕時計 F-201WA の私の使い方について熱く語ります。

自動定理証明器 ACL2 の入門向けに L-99 の1問目を解きました

<2022-05-25 水 18:30>

ACL2 の入門向けに L-99 の一問目を解きました。 なんと動画による解説付きです。

個人PCの TojoQK ユーザーの Laptop の設定

<2022-05-15 日 20:25>

個人PCでプライベートで使っているメインとは別の tojoqk ユーザーを作成したのでその設定を公開しました。 記事を書くときや tojoqk として他者と画面を共有するときなどに使う用のユーザーの設定です。

RSS の旧 URL を新 URL へリダイレクトしました

<2022-04-21 木 13:00>

/feed.xml/index.xml にリダイレクトするように設定しました。 万が一これで RSS リーダー側に何らかの支障を起こしたらすみません。 一応軽くテストをしてみたところ大きな問題はなさそうなので実行しました。

ACL2 でリストの回文に関する性質を証明した

<2022-04-04 月 22:10>

下記の回文に関する定理を証明しました。

(defthm palindrome-sandwich
  (implies (and (true-listp x)
                (true-listp y))
           (equal (palindromep (append y x (reverse y)))
                  (palindromep x))))

ACL2 で鳩の巣の原理を使ってみた

<2022-03-26 土 02:00>

ACL2 で鳩の巣の原理を使った証明ができることを確認します。

この記事は ACL2 を実際に使って定理証明をする作業がどんな感じなのかがよく分かるようになっていると思います。 そのような記事は日本語圏において現在のところ一つもないと思うので大変貴重なものだと思います(自画自賛)。

TODO ACL2 でリストの回転に関する性質を証明してみた

<2022-03-24 木 01:00>

ACL2 でリストの回転に関する性質を証明する記事です。

リストの長さと同じ回数回転すると元のリストと一致することについて証明できていないので、 いつか証明できたらいいなと思ってます。

システム x による支配

<2022-03-19 土 18:00>

システムによる支配について会話劇を用いた解説です。 会社 X とシステム x に色々入れて遊ぼう!

Emacs の時刻表記が日本語から英語に変わる問題の解決法

<2022-03-07 月 21:55>

Emacs の曜日の表記が勝手に日本語から英語に変わってしまう問題を解決します。 結論だけ言うと Emacs の設定ファイルに下記を追加すればとりあえず解決します。

(setq system-time-locale nil)

Web サイトをリニューアルしました

<2022-03-04 金 12:30>

リニューアルしました。といっても私にとってのリニューアルです。 Emacs から静的サイトを生成する方法についても言及してます。

Guile で df コマンドの出力からディスク使用率を確認してみた

<2022-03-03 木 00:22>

Guile で Unix のコマンドの出力を一行づつ読んで処理する具体的な例を紹介します。

Guile ではスタック溢れを気にせず再帰しよう

<2021-09-12 日 21:00>

Guile では再帰するときにスタック溢れに気にしなくて良い件。 ただ、記事では Guile すごいーっていってるけど実は割と多くの Scheme 処理系で同様だったりする。 あとこれは結構デメリットもある。

ACL2 で組み合せの数とその階乗表現の関係について証明してみた

<2021-09-05 日 00:00>

ACL2 で証明したやつ。定理ライブラリでごり押ししててずるい。

ACL2 で全ての組み合わせを求める関数の長さの性質について証明してみた

<2021-09-02 木 00:00>

これは結構自信のある記事。ACL2 ってこんなこともできるんやでってことを示してる。 とはいえ、冷静に考えると再帰の構造が同じなんで当然のことをやってるだけ感はある。

Nextcloud サーバーを構築しました

<2020-08-05 水 06:30>

Nextcloud のサーバーを運用してるぜという話です。

Laminar CI の紹介と Guix System への導入

<2021-08-03 火 10:30>

Laminar CI を使ったらなんか最高だった件です。

Git サーバーをセルフホスティングしてみた

<2021-03-27 土 01:50>

git サーバーを Guix System でセルフホスティングする話です。

開発者による支配から身を守るために自由ソフトウェアを使いましょう

<2020-06-17 水 10:10>

自由ソフトウェアの使用を推奨するための非エンジニア向けの文書です。

[2022-02-25 金] この記事こそ最もリニューアルすべき記事かと思うがなかなかリニューアルをしない。 やるとしたら新記事かな。

SICPを読む前に: Scheme 編

普段 Scheme を使わないプログラマ向けに SICP を快適に読むための文書です(古いかも)

ウェブサイトの見た目を改善しました

<2020-05-08 金 06:45>

[2022-03-04 金] 再度リニューアルし、このときの見た目とはもう変わってます。

org-mode で記事が書けるようになりました

<2020-05-07 木 10:45>

haunt を拡張して org-mode を使って記事を書けるようにしました (Web サイトをリニューアルしました で Emacs の org-publish を使用するように変えたので、 Haunt の利用は止めました)

排中律と二重否定除去をTyped Racketで実装する

<2020-03-26 木 02:20>

Qiita 退会ブームに乗って移行した記事のひとつ。 排中律と二重否定除去をSMLで実装するという記事に便乗したものです。

Serverless Frameworkを使ってRacketのプログラムをAWS Lambdaにデプロイしてみた

<2020-03-26 木 01:50>

Qiita 退会ブームに乗って移行した記事のひとつ。 Serverless Framework を使って Racket のプログラムをデプロイする極端な方法を解説します。

個人用途であっても独自ドメインのメールアドレスを使う理由

<2020-03-15 日 04:55>

こんにちは、世界!

<2020-02-18 火 09:00>

最初に書いた記事です。

著者: Masaya Tojo (masaya@tojo.tokyo)

Twitter: @tojoqk

Mastodon: @tojoqk

RSS を購読する

トップページに戻る