TojoQK の投稿

TojoQKの日記について

<2022-08-13 Sat>

公開日記を始めました。 日記といっても技術的な話メインにする予定です。 右上からも日記に遷移できます。

ハフマン符号化して復号すると元に戻ることをACL2で証明した

<2022-07-14 Thu 17:15>

ハフマン符号化して復号すると元に戻ることをACL2で証明しました。 全体的に解説は少なめですが、ACL2 の elim ルールについての説明は詳しいと思います。

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

<2022-06-27 Mon 13:00>

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

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

<2022-05-29 Sun 12:40>

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

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

<2022-05-25 Wed 18:30>

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

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

<2022-04-21 Thu 13:00>

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

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

<2022-04-04 Mon 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 Sat 02:00>

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

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

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

<2022-03-24 Thu 01:00>

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

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

システム x による支配

<2022-03-19 Sat 18:00>

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

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

<2022-03-07 Mon 21:55>

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

(setq system-time-locale nil)

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

<2022-03-04 Fri 12:30>

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

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

<2022-03-03 Thu 00:22>

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

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

<2021-09-12 Sun 21:00>

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

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

<2021-09-05 Sun 00:00>

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

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

<2021-09-02 Thu 00:00>

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

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

<2020-08-05 Wed 06:30>

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

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

<2021-08-03 Tue 10:30>

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

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

<2021-03-27 Sat 01:50>

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

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

<2020-06-17 Wed 10:10>

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

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

SICPを読む前に: Scheme 編

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

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

<2020-05-08 Fri 06:45>

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

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

<2020-05-07 Thu 10:45>

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

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

<2020-03-26 Thu 02:20>

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

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

<2020-03-26 Thu 01:50>

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

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

<2020-03-15 Sun 04:55>

こんにちは、世界!

<2020-02-18 Tue 09:00>

最初に書いた記事です。

著者: TojoQK (tojoqk@tojo.tokyo)

Twitter: @tojoqk

Mastodon: @tojoqk, English: @tojo

RSS を購読する

トップページに戻る