aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitignore2
-rw-r--r--Makefile19
-rw-r--r--guix.scm2
-rw-r--r--haunt.scm27
-rw-r--r--notebooks/about-me.header5
-rw-r--r--notebooks/about-me.ipynb162
-rw-r--r--notebooks/comb-factorial.header4
-rw-r--r--notebooks/comb-factorial.ipynb869
-rw-r--r--notebooks/contact.header5
-rw-r--r--notebooks/contact.ipynb55
-rw-r--r--notebooks/guile-df.header4
-rw-r--r--notebooks/guile-df.ipynb387
-rw-r--r--notebooks/guile-recursion.header4
-rw-r--r--notebooks/guile-recursion.ipynb595
-rw-r--r--notebooks/len-combinations.header4
-rw-r--r--notebooks/len-combinations.ipynb475
-rw-r--r--posts/about-me.md129
-rw-r--r--posts/comb-factorial.md796
-rw-r--r--posts/contact.md82
-rw-r--r--posts/git-tojo-tokyo.md2
-rw-r--r--posts/guile-df.md264
-rw-r--r--posts/guile-recursion.md392
-rw-r--r--posts/laminar-is-best.md117
-rw-r--r--posts/len-combinations.md373
-rw-r--r--posts/mail-and-domain.sxml2
-rw-r--r--static/css/blog.css34
-rw-r--r--static/image/QK-114x114.pngbin7996 -> 280 bytes
-rw-r--r--static/image/QK-120x120.pngbin8108 -> 301 bytes
-rw-r--r--static/image/QK-144x144.pngbin8536 -> 362 bytes
-rw-r--r--static/image/QK-152x152.pngbin8669 -> 397 bytes
-rw-r--r--static/image/QK-16x16.pngbin6476 -> 425 bytes
-rw-r--r--static/image/QK-180x180.pngbin9212 -> 515 bytes
-rw-r--r--static/image/QK-192x192.pngbin9512 -> 524 bytes
-rw-r--r--static/image/QK-32x32.pngbin6704 -> 1101 bytes
-rw-r--r--static/image/QK-52x52.pngbin7001 -> 2297 bytes
-rw-r--r--static/image/QK-57x57.pngbin7067 -> 2637 bytes
-rw-r--r--static/image/QK-60x60.pngbin7114 -> 2857 bytes
-rw-r--r--static/image/QK-72x72.pngbin7307 -> 3803 bytes
-rw-r--r--static/image/QK-76x76.pngbin7367 -> 4131 bytes
-rw-r--r--static/image/QK-96x96.pngbin7672 -> 5987 bytes
-rw-r--r--static/image/QK.pngbin8972 -> 340975 bytes
41 files changed, 4718 insertions, 92 deletions
diff --git a/.gitignore b/.gitignore
index 1320f90..16696e9 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,3 @@
site
+.ipynb_checkpoints
+*~
diff --git a/Makefile b/Makefile
index 211cfec..bd0b507 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,7 @@
.PHONEY: build clean deploy serve
build:
- haunt build
+ LANG=ja_JP.utf-8 haunt build
clean:
rm -rf site
@@ -10,4 +10,19 @@ serve: build
haunt serve --watch
deploy: build
- rsync -av --delete site/ web:/srv/www/
+ rsync -av --delete site/ ci@tojo.tokyo:/srv/www/
+
+deploy-test: build
+ rsync -av --delete site/ ci@tojo.tokyo:/srv/test-www/
+
+notebook:
+ for notebook in notebooks/*.ipynb ;\
+ do \
+ output=posts/$$(echo $$(basename "$${notebook%.ipynb}".md));\
+ header="$${notebook%.ipynb}".header;\
+ { \
+ cat "$$header";\
+ echo "---";\
+ pandoc -t commonmark "$$notebook" | sed -e '/^<div/d' -e '/^<\/div>/d';\
+ } > "$$output" ;\
+ done
diff --git a/guix.scm b/guix.scm
index 7b65ee7..4a0f234 100644
--- a/guix.scm
+++ b/guix.scm
@@ -38,7 +38,7 @@
("make" ,gnu-make)
("giule-commonmark" ,guile3.0-commonmark)
("rsync" ,rsync)
- ("openssh", openssh)))
+ ("openssh" ,openssh)))
(synopsis "TojoQK's web site")
(description "This project is TojoQK's web site.")
(home-page "http://www.tojo.tokyo")
diff --git a/haunt.scm b/haunt.scm
index 5532702..b969361 100644
--- a/haunt.scm
+++ b/haunt.scm
@@ -101,7 +101,11 @@
(nav (@ (class "nav-bar"))
(ul (@ (class "nav-list"))
(li (@ (class "nav-logo"))
- (a (@ (href "/")) "TojoQK"))
+ (a (@ (href "/"))
+ (div (@ (class "nav-logo-main"))
+ (img (@ (class "nav-log-img")
+ (src "/static/image/QK-32x32.png")))
+ "TojoQK")))
(li (@ (class "nav-item"))
(a (@ (href "/about-me.html")) "About me"))
(li (@ (class "nav-item"))
@@ -136,21 +140,22 @@
`((div (h1 (@ (class "post-title"))
(a (@ (href "")) ,(post-ref post 'title)))
(div (@ (class "post-date"))
- "投稿日: ",(date->string/tojoqk (post-date post)))
+ "投稿日: ",(date->string/tojoqk (post-date post))
+ " ("
+ (a (@ (href ,(string-append
+ "https://git.tojo.tokyo/"
+ "www-tojo-tokyo.git/log/"
+ (post-file-name post))))
+ "更新履歴")
+ ")")
,@(cond
((updated->date-or-false (post-ref post 'updated))
=> (lambda (updated)
`((div (@ (class "post-date"))
- "更新日: " ,(date->string/tojoqk updated)
- " ("
- (a (@ (href ,(string-append
- "https://git.tojo.tokyo/"
- "www-tojo-tokyo.git/log/"
- (post-file-name post))))
- "更新履歴")
- ")"))))
+ "更新日: " ,(date->string/tojoqk updated)))))
(else '())))
- (div ,(post-sxml post))
+ (div (@ (class "post"))
+ ,(post-sxml post))
(ul (@ (class "post-end"))
(li (a (@ (href "/")) "投稿の一覧"))
(li (a (@ (href ,(string-append "https://git.tojo.tokyo/www-tojo-tokyo.git/tree/"
diff --git a/notebooks/about-me.header b/notebooks/about-me.header
new file mode 100644
index 0000000..4702141
--- /dev/null
+++ b/notebooks/about-me.header
@@ -0,0 +1,5 @@
+title: About me
+id: about-me
+date: 2020-02-19 00:00
+updated: 2021-09-12 12:00
+description: 自己紹介ページ
diff --git a/notebooks/about-me.ipynb b/notebooks/about-me.ipynb
new file mode 100644
index 0000000..f0c407a
--- /dev/null
+++ b/notebooks/about-me.ipynb
@@ -0,0 +1,162 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "id": "69ec7a03",
+ "metadata": {},
+ "source": [
+ "## 自己紹介"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "f5ac2fed",
+ "metadata": {},
+ "source": [
+ "### 自由ソフトウェア\n",
+ "\n",
+ "[自由ソフトウェア](https://www.gnu.org/philosophy/free-sw.ja.html)が好きでユーザーが自分の環境で動かすプログラムをコントロールできるのが当然の時代が訪れる未来のために貢献していきたいと考えています。\n",
+ "\n",
+ "2020 年の 7 月から Free Software Foundation の Associate Member を続けています。\n",
+ "\n",
+ "[![FSF の Member button](https://static.fsf.org/nosvn/associate/crm/5002583.png)](https://my.fsf.org/join?referrer=5002583) \n",
+ "\n",
+ "FSF は自由ソフトウェア普及させるための活動を精力的に行なっています。あなたも一緒に [FSF を支援](https://my.fsf.org/join?referrer=5002583)しましょう。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "926b14ab",
+ "metadata": {},
+ "source": [
+ "### ACL2 による定理証明\n",
+ "\n",
+ "ACL2 は定理証明支援系の一つで、Common Lisp のサブセットでもあります。最近はこの ACL2 を使って定理証明をするのにはまっています。初見では自分が使えるようになる気がまったくしなかったのですが、ちゃんと勉強すると意外に使えるようになるので結構おすすめです。\n",
+ "\n",
+ "ACL2 を使って書いた定理を [acl2-theorems](https://git.tojo.tokyo/acl2-theorems.git/tree/) リポジトリに置いているのでよかったら見てみてください。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "56dabdf6",
+ "metadata": {},
+ "source": [
+ "### GNU Guile によるプログラミング\n",
+ "\n",
+ "好きなプログラミング言語は GNU の公式の拡張言語である [GNU Guile](https://www.gnu.org/software/guile/) です。Guile は Scheme の処理系の一つです。\n",
+ "日常的なちょっとしたスクリプトを書くのによく使っています。\n",
+ "\n",
+ "Guile は Scheme の処理系の一つですが Scheme の処理系の中で GNU Guile を選択している最大の理由は LGPLv3 か GPLv3 でライブラリを書く文化が成立しているというところです。実際のところプログラムのライセンスを決めるときは、そのプログラミング言語のコミュニティがどういうライセンスを好むのかというので決めることも多いと思います。Guile だとライブラリのライセンスが LGPLv3 か GPLv3 のいずれかの場合が多いし、使いたいライブラリが GPLv3 の場合は必然的に GPLv3 を選択することになります。\n",
+ "よって、他のプログラミング言語と違って社会的な GPLv3 以外を使う圧をなんとなく感じることなく GPLv3 を選択してプログラムを書くことができます。\n",
+ "\n",
+ "技術的な面で GNU Guile の一番良いところは、[末尾再帰でない手続きがスタックオーバーフローしない(システムのメモリを使い尽さない限り)](https://www.gnu.org/software/guile/manual/html_node/Stack-Overflow.html)ことです([Racket も同じです](https://docs.racket-lang.org/guide/Lists__Iteration__and_Recursion.html))。これは明らかによいことでプログラムの書き方を変えます。一般に再帰手続きを末尾再帰に変換するのは効率のためではなくてスタックオーバーフローを恐れるためです。ほとんどの場合、末尾再帰の手続きは理解しにくく汚ないです。それに対して自然な再帰手続きは読みやすく再帰的な処理を綺麗に表現していて本当に美しいものです。よほど効率が悪くなって明らかに問題が生じてしまう場合を除けば再帰の手続きをわざわざ末尾再帰に書き換える必要はありません。末尾再帰の手続きを書くのは実質的に手続き型プログラミングをしているのとほとんど違いがないため、**普通の再帰で問題のないようなプログラミング言語こそ真の意味で関数型プログラミング言語といえるのです**。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "6cf364c9",
+ "metadata": {},
+ "source": [
+ "### GPG の鍵\n",
+ "\n",
+ "下記のコマンドで私の公開鍵を gpg に import できます。\n",
+ "\n",
+ "```\n",
+ "gpg --keyserver=hkps://keyserver.ubuntu.com --recv-keys C76AC7C77FF46F6E42C2D93545AA42647237561E\n",
+ "```\n",
+ "\n",
+ "インポートしたら必ずフィンガープリントが下記と一致することを確認してください。\n",
+ "\n",
+ "`C76A C7C7 7FF4 6F6E 42C2 D935 45AA 4264 7237 561E`"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "a4311730",
+ "metadata": {},
+ "source": [
+ "### 連絡先\n",
+ "\n",
+ "[Contact](https://www.tojo.tokyo/contact.html) ページを参照してください。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "172bea2f",
+ "metadata": {},
+ "source": [
+ "### その他\n",
+ "\n",
+ "* 好きなOS・パッケージマネージャ: [GNU Guix](https://guix.gnu.org/)\n",
+ " * 他のパッケージマネージャはなんか怖くて使えなくなった\n",
+ " * Nix はよさそうだけど興味がなくて使えない…\n",
+ " * システムのアップグレードした後に気軽に rollback できるの最高\n",
+ " * guix environment を使えば簡単に開発環境の環境構築ができるのでみんなこれを使って欲しい\n",
+ " * システムの設定とかパッケージの定義を GNU Guile で書けるの最高過ぎる\n",
+ " * 自分用の Guix チャンネルも作って使ってる\n",
+ " * https://git.tojo.tokyo/tojo-tokyo-guix-channel.git/\n",
+ " * このサイトを表示している Web サーバーも Guix System で動いている\n",
+ " * 設定: https://git.tojo.tokyo/guix-config.git/tree/web/config.scm\n",
+ "* 好きなエディタ: [GNU Emacs](https://guix.gnu.org/)\n",
+ " * Emacs への情熱はそこまでではないけど使っているのにはそれなりの理由がある\n",
+ " * Lisp のコードを良い感じにインデントしてくれるエディタは Emacs くらいしかない\n",
+ " * 他のエディタを使おうとすると Lisp のインデントができないことがすぐに致命的になる\n",
+ " * [Paredit](https://www.emacswiki.org/emacs/ParEdit) が特に最高\n",
+ " * [Magit](https://magit.vc/) という git クライアントがある\n",
+ " * git のコマンドはあんまり覚えてなくてだいたい Magit で操作している\n",
+ " * org-mode は最近使ってない……\n",
+ " * Nextcloud とか Jupyter Notebook を主に使ってる\n",
+ " * 何度か使う習慣を付けようとしたけど何故か私にはあんまり合っていないらしく使うのをやめてしまう\n",
+ " * [Geiser](https://www.nongnu.org/geiser/) という Scheme の開発環境がある\n",
+ " * GNU Guile のプログラムを書くときに使ってる\n",
+ " * これがないと補完とかできないから必要\n",
+ " * ACL2 でも当然のように [Emacs を勧めてくる](https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____EMACS)\n",
+ " * ただ ACL2 の Emacs の設定について理解するのには暫くかかったので Emacs に慣れている人でも最初から Emacs を勧めるべきかは微妙\n",
+ " * 初めて ACL2 を使う場合は [ProofPad](http://new.proofpad.org/) の方がおすすめ\n",
+ " * Emacs のパッケージは GNU Guix で管理するのがおすすめ\n",
+ " * 複数のパッケージマネージャを管理するの大変だし全部 Guix でよい\n",
+ "* 好きなクラウドサービス: [Nextcloud](https://nextcloud.com/)\n",
+ " * 自分でホスティングしている\n",
+ " * もはやこれなしにどうやって生きていけばいいのか分からない\n",
+ " * 単にファイルをクラウドに上げるだけでなくて色々なことができる\n",
+ " * [Notes](https://apps.nextcloud.com/apps/notes)\n",
+ " * ちょっとしたメモを書くのに使ってる\n",
+ " * [カレンダー](https://apps.nextcloud.com/apps/calendar)・[タスク管理](https://apps.nextcloud.com/apps/tasks)\n",
+ " * CalDAV に対応しているので、対応ソフトウェアから利用可能\n",
+ " * [News](https://apps.nextcloud.com/apps/news)\n",
+ " * RSS のフィードを登録できる\n",
+ " * [Maps](https://apps.nextcloud.com/apps/passwords)\n",
+ " * 地図上に自分で撮影した写真を表示できるのがよい\n",
+ " * [Passwords](https://apps.nextcloud.com/apps/passwords)\n",
+ " * 自分で管理していないサーバーにパスワードを預けるのちょっと怖いので自分でホスティングする価値がある\n",
+ " * [Bookmarks](https://apps.nextcloud.com/apps/bookmarks)\n",
+ " * 複数の端末でブックマークを同期できる\n",
+ "* 好きな Window Manager: [xfce4](https://www.xfce.org/)\n",
+ " * タイル型ウィンドウマネージャーとかも試したけど結局私には Xfce4 が一番合っていた\n",
+ " * パネルがいい\n",
+ " * 私にとって必要な機能が過不足なくある\n",
+ "* 使っているVPS: [Vultr](https://www.vultr.com/ja/)\n",
+ " * 2017 年の 7 月からずっと使ってる\n",
+ " * 他のに乗り換える理由が今のところない\n",
+ " * このサイトを表示している Web サーバーも Vultr で動かしてる "
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "Guile",
+ "language": "scheme",
+ "name": "guile"
+ },
+ "language_info": {
+ "codemirror_mode": "scheme",
+ "file_extension": ".scm",
+ "mimetype": "application/x-scheme",
+ "name": "guile",
+ "pygments_lexer": "scheme",
+ "version": "2.0.0"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}
diff --git a/notebooks/comb-factorial.header b/notebooks/comb-factorial.header
new file mode 100644
index 0000000..b94ba5b
--- /dev/null
+++ b/notebooks/comb-factorial.header
@@ -0,0 +1,4 @@
+title: ACL2 で組み合せの数とその階乗表現の関係について証明してみた
+id: comb-factorial
+date: 2021-09-05 13:30
+updated: 2021-09-05 14:00
diff --git a/notebooks/comb-factorial.ipynb b/notebooks/comb-factorial.ipynb
new file mode 100644
index 0000000..9112986
--- /dev/null
+++ b/notebooks/comb-factorial.ipynb
@@ -0,0 +1,869 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "id": "98c0ac77",
+ "metadata": {},
+ "source": [
+ "## はじめに\n",
+ "\n",
+ "本記事は前回の [ACL2 で全ての組み合わせを求める関数の長さの性質について証明してみた -- TojoQK](https://www.tojo.tokyo/len-combinations.html) の続きです。未読の方は先に読んでからお読みください。\n",
+ "\n",
+ "前回、リスト中の要素の全ての組み合わせを求める関数 `combinations` と組み合わせの数を求める関数 `comb` を求め、 `(len (combinations x k))` と `(comb (len x) k)` が等しいことを証明しました。ただし、`combinations` と `comb` の定義は同じ構造をしているため、ACL2 で自動証明ができたといってもありがたみを感じにくい例だったかと思います。\n",
+ "よって、今回は組み合わせの数を階乗で表現した式と前回の `comb` が等しいことを証明します。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "425f5eb2",
+ "metadata": {},
+ "source": [
+ "## 本記事で例示するプログラムのライセンス\n",
+ "\n",
+ "本記事で例示するプログラムのライセンスは3条項BSDであり自由ソフトウェアです。下記にライセンスを明示します。\n",
+ "\n",
+ "\n",
+ "```\n",
+ "Copyright (C) 2021 Masaya Tojo <masaya@tojo.tokyo>\n",
+ "\n",
+ "Redistribution and use in source and binary forms, with or without\n",
+ "modification, are permitted provided that the following conditions are\n",
+ "met:\n",
+ "\n",
+ "1. Redistributions of source code must retain the above copyright\n",
+ "notice, this list of conditions and the following disclaimer.\n",
+ "\n",
+ "2. Redistributions in binary form must reproduce the above copyright\n",
+ "notice, this list of conditions and the following disclaimer in the\n",
+ "documentation and/or other materials provided with the distribution.\n",
+ "\n",
+ "3. Neither the name of the copyright holder nor the names of its\n",
+ "contributors may be used to endorse or promote products derived from\n",
+ "this software without specific prior written permission.\n",
+ "\n",
+ "THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS\n",
+ "\"AS IS\" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT\n",
+ "LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR\n",
+ "A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT\n",
+ "HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,\n",
+ "SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT\n",
+ "LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,\n",
+ "DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY\n",
+ "THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT\n",
+ "(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE\n",
+ "OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.\n",
+ "```"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "37660f5c",
+ "metadata": {},
+ "source": [
+ "## 組み合せの数を求める関数 comb を定義する\n",
+ "\n",
+ "\n",
+ "[前回の記事](https://www.tojo.tokyo/len-combinations.html)で作成した組み合わせの数を求める関数 `comb` です。\n",
+ "関数の定義については[前回の記事](https://www.tojo.tokyo/len-combinations.html)で説明しているので必要であれば参照してください"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "id": "dd5300c3",
+ "metadata": {
+ "scrolled": true
+ },
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "\r\n",
+ "The admission of COMB is trivial, using the relation O< (which is known\r\n",
+ "to be well-founded on the domain recognized by O-P) and the measure\r\n",
+ "(ACL2-COUNT N). We observe that the type of COMB is described by the\r\n",
+ "theorem (AND (INTEGERP (COMB N K)) (<= 0 (COMB N K))). We used primitive\r\n",
+ "type reasoning.\r\n",
+ "\r\n",
+ "Summary\r\n",
+ "Form: ( DEFUN COMB ...)\r\n",
+ "Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))\r\n",
+ "Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.01)\r\n",
+ " COMB\r\n"
+ ]
+ }
+ ],
+ "source": [
+ "(defun comb (n k)\n",
+ " (cond\n",
+ " ((zp k) 1)\n",
+ " ((zp n) 0)\n",
+ " (t (+ (comb (- n 1) k)\n",
+ " (comb (- n 1) (- k 1))))))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "c392ce4e",
+ "metadata": {},
+ "source": [
+ "ただ、前回の `comb` の説明はアルゴリズムに関するものだけで、関数中で使用している `zp` 関数については特に説明していませんでした。`zp` 関数は Common Lisp (ACL2 は Common Lisp のサブセットです)には存在していない関数であり、Common Lisp にもある 0 かどうかを調べる関数の `zerop` とは挙動が異なります。`zp` を使用している理由については ACL2 の関数定義の仕様について軽く説明する必要があります。\n",
+ "\n",
+ "### ACL2 と停止性の証明\n",
+ "\n",
+ "ACL2 では全ての関数は停止しないといけません。ACL2 は `defun` で関数を定義するときに毎回停止性について証明しています(今までの例では一度も停止性の証明に失敗していません)。\n",
+ "重要なのは関数にどのような値を与えても停止しないといけないということです。ACL2 は型なしの言語なので ACL2 で利用可能な全てのデータ型の値が関数に渡る可能性があります。自然数のみを引数に取る関数のつもりで書いていたなどという言い訳は ACL2 には通用しないのです。\n",
+ "`zp` 関数は 0 だけでなく自然数(0を含む)以外の全ての値を `0` として処理します。なので `zerop` とは異なり`(zp -1)` や `(zp 'a)` も `t` です。\n",
+ "`zp` 関数により基底部へ分岐する判定をすることで自然数以外の予期しない値が与えられた場合であっても確実に関数が停止することを証明できるのです。\n",
+ "具体的にどうやって停止性の証明をするのかについてはいつか別に記事を作成して説明しようという気持ちはありますが実際のスケジュールは未定のため、興味のある方は ACL2 のドキュメントを読むか『定理証明手習い』(ラムダノート社)を参照することをおすすめします。\n",
+ "\n",
+ "zp 関数の詳細については [zp 関数のドキュメント](https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=ACL2____ZP) を参照してください。\n",
+ "\n",
+ "また、ACL2 が型なしであることについて不安に感じた静的型付きのプログラミング言語を好む方は [XDOC — Guard](https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=ACL2____GUARD) を軽く読んでみてください。初心者向けの機能ではないのですが、実際に関数に渡る値を静的に制限することができます(停止性の証明時にあらゆる値について考慮しないといけないことは Guard を使用しても変わりません)。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "34b22ae6",
+ "metadata": {},
+ "source": [
+ "### comb の性質\n",
+ "\n",
+ "`comb` と階乗の関係の性質について証明する前に `comb` について既に分かっている性質については先に証明しておきましょう。\n",
+ "特に `comb` の次に説明する階乗表現を定義する際には「k が n よりも大きいときは (comb n k) は 0」という性質を利用します。\n",
+ "なので、下記の `comb-zero` という定理を先に証明しておきます。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "id": "93fe2f8d",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "Goal'\r\n",
+ "\r\n",
+ "([ A key checkpoint:\r\n",
+ "\r\n",
+ "Goal'\r\n",
+ "(IMPLIES (AND (INTEGERP N)\r\n",
+ " (<= 0 N)\r\n",
+ " (INTEGERP K)\r\n",
+ " (<= 0 K)\r\n",
+ " (< N K))\r\n",
+ " (EQUAL (COMB N K) 0))\r\n",
+ "\r\n",
+ "*1 (Goal') is pushed for proof by induction.\r\n",
+ "\r\n",
+ "])\r\n",
+ "\r\n",
+ "Perhaps we can prove *1 by induction. One induction scheme is suggested\r\n",
+ "by this conjecture. \r\n",
+ "\r\n",
+ "We will induct according to a scheme suggested by (COMB N K). This\r\n",
+ "suggestion was produced using the :induction rule COMB. If we let\r\n",
+ "(:P K N) denote *1 above then the induction scheme we'll use is\r\n",
+ "(AND (IMPLIES (AND (NOT (ZP K))\r\n",
+ " (NOT (ZP N))\r\n",
+ " (:P K (+ -1 N))\r\n",
+ " (:P (+ -1 K) (+ -1 N)))\r\n",
+ " (:P K N))\r\n",
+ " (IMPLIES (AND (NOT (ZP K)) (ZP N))\r\n",
+ " (:P K N))\r\n",
+ " (IMPLIES (ZP K) (:P K N))).\r\n",
+ "This induction is justified by the same argument used to admit COMB.\r\n",
+ "Note, however, that the unmeasured variable K is being instantiated.\r\n",
+ "When applied to the goal at hand the above induction scheme produces\r\n",
+ "twelve nontautological subgoals.\r\n",
+ "Subgoal *1/12\r\n",
+ "Subgoal *1/11\r\n",
+ "Subgoal *1/10\r\n",
+ "Subgoal *1/9\r\n",
+ "Subgoal *1/8\r\n",
+ "Subgoal *1/7\r\n",
+ "Subgoal *1/6\r\n",
+ "Subgoal *1/5\r\n",
+ "Subgoal *1/4\r\n",
+ "Subgoal *1/3\r\n",
+ "Subgoal *1/2\r\n",
+ "Subgoal *1/2'\r\n",
+ "Subgoal *1/1\r\n",
+ "\r\n",
+ "*1 is COMPLETED!\r\n",
+ "Thus key checkpoint Goal' is COMPLETED!\r\n",
+ "\r\n",
+ "Q.E.D.\r\n",
+ "\r\n",
+ "Summary\r\n",
+ "Form: ( DEFTHM COMB-ZERO ...)\r\n",
+ "Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)\r\n",
+ " (:DEFINITION COMB)\r\n",
+ " (:DEFINITION NATP)\r\n",
+ " (:DEFINITION NOT)\r\n",
+ " (:EXECUTABLE-COUNTERPART <)\r\n",
+ " (:EXECUTABLE-COUNTERPART BINARY-+)\r\n",
+ " (:EXECUTABLE-COUNTERPART EQUAL)\r\n",
+ " (:EXECUTABLE-COUNTERPART INTEGERP)\r\n",
+ " (:EXECUTABLE-COUNTERPART NOT)\r\n",
+ " (:EXECUTABLE-COUNTERPART TAU-SYSTEM)\r\n",
+ " (:EXECUTABLE-COUNTERPART ZP)\r\n",
+ " (:FAKE-RUNE-FOR-LINEAR NIL)\r\n",
+ " (:FAKE-RUNE-FOR-TYPE-SET NIL)\r\n",
+ " (:INDUCTION COMB))\r\n",
+ "Time: 0.03 seconds (prove: 0.02, print: 0.01, other: 0.00)\r\n",
+ "Prover steps counted: 707\r\n",
+ " COMB-ZERO\r\n"
+ ]
+ }
+ ],
+ "source": [
+ "(defthm comb-zero\n",
+ " (implies (and (natp n)\n",
+ " (natp k)\n",
+ " (< n k))\n",
+ " (equal (comb n k) 0)))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "e9a6ff91",
+ "metadata": {},
+ "source": [
+ "## 階乗を求める関数 factorial を定義する\n",
+ "\n",
+ "階乗の定義は下記の通りです。\n",
+ "\n",
+ "1. 0 の階乗は 1\n",
+ "2. n が 0 より大きい自然数のとき、n の階乗は n と n - 1 の階乗の積\n",
+ "\n",
+ "これをそのまま ACL2に翻訳した `factorial` の定義を示します(厳密には前述した通り基底部の判定に zp 関数を使用するため全く同じというわけではありません)。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "id": "8a618a65",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "\r\n",
+ "The admission of FACTORIAL is trivial, using the relation O< (which\r\n",
+ "is known to be well-founded on the domain recognized by O-P) and the\r\n",
+ "measure (ACL2-COUNT N). We observe that the type of FACTORIAL is described\r\n",
+ "by the theorem (AND (INTEGERP (FACTORIAL N)) (< 0 (FACTORIAL N))).\r\n",
+ "We used the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER and primitive\r\n",
+ "type reasoning.\r\n",
+ "\r\n",
+ "Summary\r\n",
+ "Form: ( DEFUN FACTORIAL ...)\r\n",
+ "Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)\r\n",
+ " (:FAKE-RUNE-FOR-TYPE-SET NIL))\r\n",
+ "Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)\r\n",
+ " FACTORIAL\r\n"
+ ]
+ }
+ ],
+ "source": [
+ "(defun factorial (n)\n",
+ " (if (zp n)\n",
+ " 1\n",
+ " (* n (factorial (- n 1)))))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "ed2dbcb2",
+ "metadata": {},
+ "source": [
+ "## comb-factorial 定理を証明する\n",
+ "\n",
+ "では、comb 関数と階乗の関係について証明してみましょう。\n",
+ "高校の数学 1A にて組み合わせの数について学んだ方は下記の公式について学んだ記憶がある\n",
+ "かもしれません。\n",
+ "\n",
+ "```\n",
+ " n!\n",
+ "--------\n",
+ "(n-k)!k!\n",
+ "```\n",
+ "\n",
+ "何故かについては「組み合せの数 公式」とかで適当に[検索](https://duckduckgo.com/?q=%E7%B5%84%E3%81%BF%E5%90%88%E3%82%8F%E3%81%9B%E3%81%AE%E6%95%B0+%E5%85%AC%E5%BC%8F)してください(やる気なし)。\n",
+ "ということで上記の式を ACL2 に翻訳してみましょう。分母が 0 になったり結果が分数になにならないように調節しています。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "id": "92fc072d",
+ "metadata": {
+ "scrolled": true
+ },
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "\r\n",
+ "ACL2 Warning [Subsume] in ( DEFTHM COMB-FACTORIAL ...): A newly proposed\r\n",
+ ":REWRITE rule generated from COMB-FACTORIAL probably subsumes the previously\r\n",
+ "added :REWRITE rule COMB-ZERO, in the sense that the new rule will\r\n",
+ "now probably be applied whenever the old rule would have been.\r\n",
+ "\r\n",
+ "Goal'\r\n",
+ "Subgoal 4\r\n",
+ "Subgoal 3\r\n",
+ "Subgoal 2\r\n",
+ "Subgoal 2'\r\n",
+ "\r\n",
+ "([ A key checkpoint:\r\n",
+ "\r\n",
+ "Subgoal 2'\r\n",
+ "(IMPLIES (AND (<= 0 N)\r\n",
+ " (NOT (ZP K))\r\n",
+ " (NOT (ZP N))\r\n",
+ " (<= K N))\r\n",
+ " (EQUAL (COMB N K)\r\n",
+ " (* (FACTORIAL N)\r\n",
+ " (/ (* (FACTORIAL K)\r\n",
+ " (FACTORIAL (+ (- K) N)))))))\r\n",
+ "\r\n",
+ "*1 (Subgoal 2') is pushed for proof by induction.\r\n",
+ "\r\n",
+ "])\r\n",
+ "Subgoal 1\r\n",
+ "\r\n",
+ "Perhaps we can prove *1 by induction. Three induction schemes are\r\n",
+ "suggested by this conjecture. Subsumption reduces that number to one.\r\n",
+ "\r\n",
+ "We will induct according to a scheme suggested by (COMB N K). This\r\n",
+ "suggestion was produced using the :induction rules COMB and FACTORIAL.\r\n",
+ "If we let (:P K N) denote *1 above then the induction scheme we'll\r\n",
+ "use is\r\n",
+ "(AND (IMPLIES (AND (NOT (ZP K))\r\n",
+ " (NOT (ZP N))\r\n",
+ " (:P K (+ -1 N))\r\n",
+ " (:P (+ -1 K) (+ -1 N)))\r\n",
+ " (:P K N))\r\n",
+ " (IMPLIES (AND (NOT (ZP K)) (ZP N))\r\n",
+ " (:P K N))\r\n",
+ " (IMPLIES (ZP K) (:P K N))).\r\n",
+ "This induction is justified by the same argument used to admit COMB.\r\n",
+ "Note, however, that the unmeasured variable K is being instantiated.\r\n",
+ "When applied to the goal at hand the above induction scheme produces\r\n",
+ "eight nontautological subgoals.\r\n",
+ "Subgoal *1/8\r\n",
+ "Subgoal *1/8'\r\n",
+ "Subgoal *1/8''\r\n",
+ "\r\n",
+ "Splitter note (see :DOC splitter) for Subgoal *1/8'' (2 subgoals).\r\n",
+ " if-intro: ((:DEFINITION FACTORIAL)\r\n",
+ " (:DEFINITION NOT)\r\n",
+ " (:REWRITE ZP-OPEN))\r\n",
+ "\r\n",
+ "Subgoal *1/8.2\r\n",
+ "Subgoal *1/8.2'\r\n",
+ "Subgoal *1/8.2''\r\n",
+ "Subgoal *1/8.2'''\r\n",
+ "Subgoal *1/8.2'4'\r\n",
+ "Subgoal *1/8.2'5'\r\n",
+ "Subgoal *1/8.2'6'\r\n",
+ "Subgoal *1/8.2'7'\r\n",
+ "Subgoal *1/8.2'8'\r\n",
+ "Subgoal *1/8.2'9'\r\n",
+ "Subgoal *1/8.2'10'\r\n",
+ "Subgoal *1/8.2'11'\r\n",
+ "Subgoal *1/8.2'12'\r\n",
+ "Subgoal *1/8.2'13'\r\n",
+ "Subgoal *1/8.2'14'\r\n",
+ "Subgoal *1/8.2'15'\r\n",
+ "Subgoal *1/8.2'16'\r\n",
+ "Subgoal *1/8.2'17'\r\n",
+ "\r\n",
+ "([ A key checkpoint while proving *1 (descended from Subgoal 2'):\r\n",
+ "\r\n",
+ "Subgoal *1/8.2'\r\n",
+ "(IMPLIES (AND (NOT (ZP K))\r\n",
+ " (NOT (ZP N))\r\n",
+ " (EQUAL (COMB (+ -1 N) K)\r\n",
+ " (* (FACTORIAL (+ -1 N))\r\n",
+ " (/ (* K (FACTORIAL (+ -1 K))\r\n",
+ " (FACTORIAL (+ -1 (- K) N))))))\r\n",
+ " (< 0 (+ (- K) N))\r\n",
+ " (EQUAL (COMB (+ -1 N) (+ -1 K))\r\n",
+ " (* (FACTORIAL (+ -1 N))\r\n",
+ " (/ (* (FACTORIAL (+ -1 K))\r\n",
+ " (+ (- K) N)\r\n",
+ " (FACTORIAL (+ -1 (- K) N))))))\r\n",
+ " (<= 0 N)\r\n",
+ " (<= K N))\r\n",
+ " (EQUAL (+ (COMB (+ -1 N) K)\r\n",
+ " (COMB (+ -1 N) (+ -1 K)))\r\n",
+ " (* N (FACTORIAL (+ -1 N))\r\n",
+ " (/ (* K (FACTORIAL (+ -1 K))\r\n",
+ " (+ (- K) N)\r\n",
+ " (FACTORIAL (+ -1 (- K) N)))))))\r\n",
+ "\r\n",
+ "*1.1 (Subgoal *1/8.2'17') is pushed for proof by induction.\r\n",
+ "\r\n",
+ "])\r\n",
+ "Subgoal *1/8.1\r\n",
+ "Subgoal *1/8.1'\r\n",
+ "Subgoal *1/7\r\n",
+ "Subgoal *1/7'\r\n",
+ "Subgoal *1/7''\r\n",
+ "Subgoal *1/6\r\n",
+ "Subgoal *1/5\r\n",
+ "Subgoal *1/4\r\n",
+ "Subgoal *1/4'\r\n",
+ "Subgoal *1/4''\r\n",
+ "Subgoal *1/4'''\r\n",
+ "Subgoal *1/4'4'\r\n",
+ "Subgoal *1/4'5'\r\n",
+ "Subgoal *1/4'6'\r\n",
+ "Subgoal *1/4'7'\r\n",
+ "Subgoal *1/4'8'\r\n",
+ "\r\n",
+ "([ A key checkpoint while proving *1 (descended from Subgoal 2'):\r\n",
+ "\r\n",
+ "Subgoal *1/4'5'\r\n",
+ "(IMPLIES (AND (NOT (ZP N))\r\n",
+ " (< 0 (+ -1 N))\r\n",
+ " (EQUAL (+ 1 (COMB (+ -2 N) 1))\r\n",
+ " (* (/ (FACTORIAL (+ -2 N)))\r\n",
+ " (+ -1 N)\r\n",
+ " (FACTORIAL (+ -2 N))))\r\n",
+ " (<= 0 N)\r\n",
+ " (<= 1 N))\r\n",
+ " (EQUAL (+ 2 (COMB (+ -2 N) 1)) N))\r\n",
+ "\r\n",
+ "*1.2 (Subgoal *1/4'8') is pushed for proof by induction.\r\n",
+ "\r\n",
+ "])\r\n",
+ "Subgoal *1/3\r\n",
+ "Subgoal *1/3'\r\n",
+ "Subgoal *1/2\r\n",
+ "Subgoal *1/2'\r\n",
+ "Subgoal *1/1\r\n",
+ "\r\n",
+ "So we now return to *1.2, which is\r\n",
+ "\r\n",
+ "(IMPLIES (AND (INTEGERP K)\r\n",
+ " (<= 0 K)\r\n",
+ " (INTEGERP I)\r\n",
+ " (< 0 I)\r\n",
+ " (INTEGERP J)\r\n",
+ " (NOT (ZP N))\r\n",
+ " (EQUAL (+ 1 K)\r\n",
+ " (* (/ (FACTORIAL J)) I (FACTORIAL J)))\r\n",
+ " (<= 0 N)\r\n",
+ " (<= 1 N))\r\n",
+ " (EQUAL (+ 2 K) N)).\r\n",
+ "Subgoal *1.2/3\r\n",
+ "Subgoal *1.2/3'\r\n",
+ "Subgoal *1.2/3''\r\n",
+ "Subgoal *1.2/3'''\r\n",
+ "Subgoal *1.2/3'4'\r\n",
+ "Subgoal *1.2/3'5'\r\n",
+ "Subgoal *1.2/3'6'\r\n",
+ "\r\n",
+ "*1.2.1 (Subgoal *1.2/3'6') is pushed for proof by induction.\r\n",
+ "Subgoal *1.2/2\r\n",
+ "Subgoal *1.2/1\r\n",
+ "Subgoal *1.2/1'\r\n",
+ "Subgoal *1.2/1''\r\n",
+ "Subgoal *1.2/1'''\r\n",
+ "Subgoal *1.2/1'4'\r\n",
+ "\r\n",
+ "*1.2.2 (Subgoal *1.2/1'4') is pushed for proof by induction.\r\n",
+ "\r\n",
+ "So we now return to *1.2.2, which is\r\n",
+ "\r\n",
+ "(IMPLIES (AND (ZP J)\r\n",
+ " (INTEGERP K)\r\n",
+ " (<= 0 K)\r\n",
+ " (INTEGERP J)\r\n",
+ " (NOT (ZP N))\r\n",
+ " (<= 0 N)\r\n",
+ " (<= 1 N))\r\n",
+ " (EQUAL (+ 2 K) N)).\r\n",
+ "\r\n",
+ "No induction schemes are suggested by *1.2.2. Consequently, the proof\r\n",
+ "attempt has failed.\r\n",
+ "\r\n",
+ "Summary\r\n",
+ "Form: ( DEFTHM COMB-FACTORIAL ...)\r\n",
+ "Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)\r\n",
+ " (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)\r\n",
+ " (:DEFINITION COMB)\r\n",
+ " (:DEFINITION FACTORIAL)\r\n",
+ " (:DEFINITION FIX)\r\n",
+ " (:DEFINITION NATP)\r\n",
+ " (:DEFINITION NOT)\r\n",
+ " (:DEFINITION SYNP)\r\n",
+ " (:EXECUTABLE-COUNTERPART <)\r\n",
+ " (:EXECUTABLE-COUNTERPART BINARY-*)\r\n",
+ " (:EXECUTABLE-COUNTERPART BINARY-+)\r\n",
+ " (:EXECUTABLE-COUNTERPART COMB)\r\n",
+ " (:EXECUTABLE-COUNTERPART EQUAL)\r\n",
+ " (:EXECUTABLE-COUNTERPART FACTORIAL)\r\n",
+ " (:EXECUTABLE-COUNTERPART TAU-SYSTEM)\r\n",
+ " (:EXECUTABLE-COUNTERPART UNARY--)\r\n",
+ " (:EXECUTABLE-COUNTERPART UNARY-/)\r\n",
+ " (:EXECUTABLE-COUNTERPART ZP)\r\n",
+ " (:FAKE-RUNE-FOR-LINEAR NIL)\r\n",
+ " (:FAKE-RUNE-FOR-TYPE-SET NIL)\r\n",
+ " (:INDUCTION COMB)\r\n",
+ " (:INDUCTION FACTORIAL)\r\n",
+ " (:REWRITE ASSOCIATIVITY-OF-*)\r\n",
+ " (:REWRITE ASSOCIATIVITY-OF-+)\r\n",
+ " (:REWRITE COMB-ZERO)\r\n",
+ " (:REWRITE COMMUTATIVITY-2-OF-+)\r\n",
+ " (:REWRITE COMMUTATIVITY-OF-*)\r\n",
+ " (:REWRITE COMMUTATIVITY-OF-+)\r\n",
+ " (:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+)\r\n",
+ " (:REWRITE FOLD-CONSTS-IN-+)\r\n",
+ " (:REWRITE INVERSE-OF-*)\r\n",
+ " (:REWRITE INVERSE-OF-+)\r\n",
+ " (:REWRITE UNICITY-OF-0)\r\n",
+ " (:REWRITE UNICITY-OF-1)\r\n",
+ " (:REWRITE ZP-OPEN)\r\n",
+ " (:TYPE-PRESCRIPTION COMB)\r\n",
+ " (:TYPE-PRESCRIPTION FACTORIAL))\r\n",
+ "Splitter rules (see :DOC splitter):\r\n",
+ " if-intro: ((:DEFINITION FACTORIAL)\r\n",
+ " (:DEFINITION NOT)\r\n",
+ " (:REWRITE ZP-OPEN))\r\n",
+ "Warnings: Subsume\r\n",
+ "Time: 0.15 seconds (prove: 0.13, print: 0.01, other: 0.00)\r\n",
+ "Prover steps counted: 15441\r\n",
+ "\r\n",
+ "---\r\n",
+ "The key checkpoint goals, below, may help you to debug this failure.\r\n",
+ "See :DOC failure and see :DOC set-checkpoint-summary-limit.\r\n",
+ "---\r\n",
+ "\r\n",
+ "*** Key checkpoint at the top level: ***\r\n",
+ "\r\n",
+ "Subgoal 2'\r\n",
+ "(IMPLIES (AND (<= 0 N)\r\n",
+ " (NOT (ZP K))\r\n",
+ " (NOT (ZP N))\r\n",
+ " (<= K N))\r\n",
+ " (EQUAL (COMB N K)\r\n",
+ " (* (FACTORIAL N)\r\n",
+ " (/ (* (FACTORIAL K)\r\n",
+ " (FACTORIAL (+ (- K) N)))))))\r\n",
+ "\r\n",
+ "*** Key checkpoints under a top-level induction: ***\r\n",
+ "\r\n",
+ "Subgoal *1/8.2'\r\n",
+ "(IMPLIES (AND (NOT (ZP K))\r\n",
+ " (NOT (ZP N))\r\n",
+ " (EQUAL (COMB (+ -1 N) K)\r\n",
+ " (* (FACTORIAL (+ -1 N))\r\n",
+ " (/ (* K (FACTORIAL (+ -1 K))\r\n",
+ " (FACTORIAL (+ -1 (- K) N))))))\r\n",
+ " (< 0 (+ (- K) N))\r\n",
+ " (EQUAL (COMB (+ -1 N) (+ -1 K))\r\n",
+ " (* (FACTORIAL (+ -1 N))\r\n",
+ " (/ (* (FACTORIAL (+ -1 K))\r\n",
+ " (+ (- K) N)\r\n",
+ " (FACTORIAL (+ -1 (- K) N))))))\r\n",
+ " (<= 0 N)\r\n",
+ " (<= K N))\r\n",
+ " (EQUAL (+ (COMB (+ -1 N) K)\r\n",
+ " (COMB (+ -1 N) (+ -1 K)))\r\n",
+ " (* N (FACTORIAL (+ -1 N))\r\n",
+ " (/ (* K (FACTORIAL (+ -1 K))\r\n",
+ " (+ (- K) N)\r\n",
+ " (FACTORIAL (+ -1 (- K) N)))))))\r\n",
+ "\r\n",
+ "Subgoal *1/4'5'\r\n",
+ "(IMPLIES (AND (NOT (ZP N))\r\n",
+ " (< 0 (+ -1 N))\r\n",
+ " (EQUAL (+ 1 (COMB (+ -2 N) 1))\r\n",
+ " (* (/ (FACTORIAL (+ -2 N)))\r\n",
+ " (+ -1 N)\r\n",
+ " (FACTORIAL (+ -2 N))))\r\n",
+ " (<= 0 N)\r\n",
+ " (<= 1 N))\r\n",
+ " (EQUAL (+ 2 (COMB (+ -2 N) 1)) N))\r\n",
+ "\r\n",
+ "ACL2 Error in ( DEFTHM COMB-FACTORIAL ...): See :DOC failure.\r\n",
+ "\r\n",
+ "******** FAILED ********\r\n"
+ ]
+ }
+ ],
+ "source": [
+ "(defthm comb-factorial\n",
+ " (implies (and (natp n))\n",
+ " (equal (comb n k)\n",
+ " (cond\n",
+ " ((zp k) 1)\n",
+ " ((or (zp n) (< n k)) 0)\n",
+ " (t (/ (factorial n)\n",
+ " (* (factorial (- n k))\n",
+ " (factorial k))))))))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "885696a6",
+ "metadata": {},
+ "source": [
+ "なんと、ACL2 による自動証明は失敗してしまいました。\n",
+ "Key checkpoints の `Subgoal *1/8.2'` のところをみてみましょう。`implies` の第一引数は仮定で第二引数は帰結なのですが、仮定のところに `(EQUAL (COMB (+ -1 N) K) ...)` という式と `(EQUAL (COMB (+ -1 N) (+ -1 K)) ...)` という式があって、帰結の部分に `(COMB (+ -1 N) K)` と `(COMB (+ -1 N) (+ -1 K))` があることに注目してください。\n",
+ "上記の仮定の式を使って帰結の式を置き換えると下記のように FACTORIAL 関数のみを使った式が出てきます(仮定は省略)。\n",
+ "\n",
+ "```\n",
+ "(EQUAL (+ (* (FACTORIAL (+ -1 N))\n",
+ " (/ (* K (FACTORIAL (+ -1 K))\n",
+ " (FACTORIAL (+ -1 (- K) N)))))\n",
+ " (* (FACTORIAL (+ -1 N))\n",
+ " (/ (* (FACTORIAL (+ -1 K))\n",
+ " (+ (- K) N)\n",
+ " (FACTORIAL (+ -1 (- K) N))))))\n",
+ " (* N (FACTORIAL (+ -1 N))\n",
+ " (/ (* K (FACTORIAL (+ -1 K))\n",
+ " (+ (- K) N)\n",
+ " (FACTORIAL (+ -1 (- K) N))))))\n",
+ "```\n",
+ "\n",
+ "これが真であることを示せばいいので、ACL2 で証明するのは不可能ではなさそうな気がしますね(実際、手計算で等しいことを確認しました)。ただ、標準の ACL2 でこういう四則演算をたくさん含んだ式について証明するのはあまり簡単ではありません。\n",
+ "ACL2 ではよく使われる定理ライブラリも一緒に配布されていて、その中に算術に関する証明をするのに大変便利な `arithmetic` という定理ライブラリが入っています。今回はこれを使います。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "id": "d272d8d1",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "\r\n",
+ "Summary\r\n",
+ "Form: ( INCLUDE-BOOK \"arithmetic/top\" ...)\r\n",
+ "Rules: NIL\r\n",
+ "Time: 0.43 seconds (prove: 0.00, print: 0.00, other: 0.43)\r\n",
+ " \"/gnu/store/cj54gk0b9qqxfh0pz8mrh7j8iwrbz4p4-acl2-8.4/lib/acl2/books/arithmetic/top.lisp\"\r\n"
+ ]
+ }
+ ],
+ "source": [
+ "(include-book \"arithmetic/top\" :dir :system)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "03437a41",
+ "metadata": {},
+ "source": [
+ "もう一度 `comb-factorial` の証明を試みます。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "id": "fdb7d4f2",
+ "metadata": {
+ "scrolled": false
+ },
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "\r\n",
+ "ACL2 Warning [Subsume] in ( DEFTHM COMB-FACTORIAL ...): A newly proposed\r\n",
+ ":REWRITE rule generated from COMB-FACTORIAL probably subsumes the previously\r\n",
+ "added :REWRITE rule COMB-ZERO, in the sense that the new rule will\r\n",
+ "now probably be applied whenever the old rule would have been.\r\n",
+ "\r\n",
+ "Goal'\r\n",
+ "Subgoal 2\r\n",
+ "Subgoal 1\r\n",
+ "Subgoal 1'\r\n",
+ "\r\n",
+ "([ A key checkpoint:\r\n",
+ "\r\n",
+ "Subgoal 1'\r\n",
+ "(IMPLIES (AND (NATP N) (NATP K) (<= K N))\r\n",
+ " (EQUAL (FACTORIAL N)\r\n",
+ " (* (FACTORIAL K)\r\n",
+ " (COMB N K)\r\n",
+ " (FACTORIAL (+ (- K) N)))))\r\n",
+ "\r\n",
+ "*1 (Subgoal 1') is pushed for proof by induction.\r\n",
+ "\r\n",
+ "])\r\n",
+ "\r\n",
+ "Perhaps we can prove *1 by induction. Three induction schemes are\r\n",
+ "suggested by this conjecture. Subsumption reduces that number to one.\r\n",
+ "\r\n",
+ "We will induct according to a scheme suggested by (COMB N K). This\r\n",
+ "suggestion was produced using the :induction rules COMB and FACTORIAL.\r\n",
+ "If we let (:P K N) denote *1 above then the induction scheme we'll\r\n",
+ "use is\r\n",
+ "(AND (IMPLIES (AND (NOT (ZP K))\r\n",
+ " (NOT (ZP N))\r\n",
+ " (:P K (+ -1 N))\r\n",
+ " (:P (+ -1 K) (+ -1 N)))\r\n",
+ " (:P K N))\r\n",
+ " (IMPLIES (AND (NOT (ZP K)) (ZP N))\r\n",
+ " (:P K N))\r\n",
+ " (IMPLIES (ZP K) (:P K N))).\r\n",
+ "This induction is justified by the same argument used to admit COMB.\r\n",
+ "Note, however, that the unmeasured variable K is being instantiated.\r\n",
+ "When applied to the goal at hand the above induction scheme produces\r\n",
+ "nine nontautological subgoals.\r\n",
+ "Subgoal *1/9\r\n",
+ "Subgoal *1/9'\r\n",
+ "Subgoal *1/9''\r\n",
+ "\r\n",
+ "Splitter note (see :DOC splitter) for Subgoal *1/9'' (2 subgoals).\r\n",
+ " if-intro: ((:DEFINITION FACTORIAL)\r\n",
+ " (:DEFINITION NOT)\r\n",
+ " (:REWRITE ZP-OPEN))\r\n",
+ "\r\n",
+ "Subgoal *1/9.2\r\n",
+ "Subgoal *1/9.2'\r\n",
+ "Subgoal *1/9.1\r\n",
+ "Subgoal *1/9.1'\r\n",
+ "Subgoal *1/8\r\n",
+ "Subgoal *1/8'\r\n",
+ "Subgoal *1/8''\r\n",
+ "Subgoal *1/7\r\n",
+ "Subgoal *1/6\r\n",
+ "Subgoal *1/5\r\n",
+ "Subgoal *1/4\r\n",
+ "Subgoal *1/3\r\n",
+ "Subgoal *1/2\r\n",
+ "Subgoal *1/1\r\n",
+ "Subgoal *1/1'\r\n",
+ "Subgoal *1/1''\r\n",
+ "\r\n",
+ "*1 is COMPLETED!\r\n",
+ "Thus key checkpoint Subgoal 1' is COMPLETED!\r\n",
+ "\r\n",
+ "Q.E.D.\r\n",
+ "\r\n",
+ "Summary\r\n",
+ "Form: ( DEFTHM COMB-FACTORIAL ...)\r\n",
+ "Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)\r\n",
+ " (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)\r\n",
+ " (:DEFINITION COMB)\r\n",
+ " (:DEFINITION FACTORIAL)\r\n",
+ " (:DEFINITION FIX)\r\n",
+ " (:DEFINITION NOT)\r\n",
+ " (:DEFINITION SYNP)\r\n",
+ " (:EXECUTABLE-COUNTERPART BINARY-*)\r\n",
+ " (:EXECUTABLE-COUNTERPART BINARY-+)\r\n",
+ " (:EXECUTABLE-COUNTERPART FACTORIAL)\r\n",
+ " (:EXECUTABLE-COUNTERPART NATP)\r\n",
+ " (:EXECUTABLE-COUNTERPART NOT)\r\n",
+ " (:EXECUTABLE-COUNTERPART TAU-SYSTEM)\r\n",
+ " (:EXECUTABLE-COUNTERPART UNARY--)\r\n",
+ " (:EXECUTABLE-COUNTERPART ZP)\r\n",
+ " (:FAKE-RUNE-FOR-LINEAR NIL)\r\n",
+ " (:FAKE-RUNE-FOR-TYPE-SET NIL)\r\n",
+ " (:FORWARD-CHAINING NATP-FC-1)\r\n",
+ " (:INDUCTION COMB)\r\n",
+ " (:INDUCTION FACTORIAL)\r\n",
+ " (:REWRITE <-0-+-NEGATIVE-1)\r\n",
+ " (:REWRITE ASSOCIATIVITY-OF-*)\r\n",
+ " (:REWRITE ASSOCIATIVITY-OF-+)\r\n",
+ " (:REWRITE COMB-ZERO)\r\n",
+ " (:REWRITE COMMUTATIVITY-2-OF-*)\r\n",
+ " (:REWRITE COMMUTATIVITY-2-OF-+)\r\n",
+ " (:REWRITE COMMUTATIVITY-OF-*)\r\n",
+ " (:REWRITE COMMUTATIVITY-OF-+)\r\n",
+ " (:REWRITE DISTRIBUTIVITY)\r\n",
+ " (:REWRITE DISTRIBUTIVITY-OF-/-OVER-*)\r\n",
+ " (:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+)\r\n",
+ " (:REWRITE EQUAL-*-/-1)\r\n",
+ " (:REWRITE EQUAL-*-/-2)\r\n",
+ " (:REWRITE EQUAL-*-X-Y-X)\r\n",
+ " (:REWRITE FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-RIGHT)\r\n",
+ " (:REWRITE INVERSE-OF-+)\r\n",
+ " (:REWRITE MINUS-CANCELLATION-ON-LEFT)\r\n",
+ " (:REWRITE TIMES-ZERO)\r\n",
+ " (:REWRITE UNICITY-OF-0)\r\n",
+ " (:REWRITE UNICITY-OF-1)\r\n",
+ " (:REWRITE ZP-OPEN)\r\n",
+ " (:TYPE-PRESCRIPTION COMB)\r\n",
+ " (:TYPE-PRESCRIPTION FACTORIAL)\r\n",
+ " (:TYPE-PRESCRIPTION |x < y => 0 < -x+y|))\r\n",
+ "Splitter rules (see :DOC splitter):\r\n",
+ " if-intro: ((:DEFINITION FACTORIAL)\r\n",
+ " (:DEFINITION NOT)\r\n",
+ " (:REWRITE ZP-OPEN))\r\n",
+ "Warnings: Subsume\r\n",
+ "Time: 0.06 seconds (prove: 0.06, print: 0.01, other: 0.00)\r\n",
+ "Prover steps counted: 4875\r\n",
+ " COMB-FACTORIAL\r\n"
+ ]
+ }
+ ],
+ "source": [
+ "(defthm comb-factorial\n",
+ " (implies (and (natp n)\n",
+ " (natp k))\n",
+ " (equal (comb n k)\n",
+ " (if (< n k)\n",
+ " 0\n",
+ " (/ (factorial n)\n",
+ " (* (factorial (- n k))\n",
+ " (factorial k)))))))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "45e33120",
+ "metadata": {},
+ "source": [
+ "証明に成功しました。定理ライブラリの力は凄いですね。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "87d4963c",
+ "metadata": {},
+ "source": [
+ "## おわりに\n",
+ "\n",
+ "[前回](https://www.tojo.tokyo/len-combinations.html)作成した組み合わせの数を求める関数とその階乗表現が等しいことを証明できました。\n",
+ "本当は `comb-factorial` の証明に失敗したときの出力を見てから補助定理 `comb-zero` を作成する流れにしたかったのですが、証明の失敗時に出力されていた Key Checkpoints をいくら眺めてもなぜ `comb-zero` が必要なのかを説明するのが難しかったので、ちょっと無理矢理ですが先に `comb-zero` を証明しておく流れにしました。\n",
+ "\n",
+ "Key Checkpoints を読んで必要な補助定理を作成する例としては今回のはちょっと難しすぎたので、また別の機会に簡単な例を出せたらいいなと考えています。\n",
+ "\n",
+ "ただ、ACL2 に関心のある方は私の記事を読むよりかは [ACL2 のチュートリアル](https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____ACL2-TUTORIAL) を参照したり、『定理証明手習い』(ラムダノート社) を読んで勉強するのがおすすめです。『定理証明手習い』(ラムダノート社) では ACL2 の使い方について学ぶことはできないのですが、 ACL2 を使うのに必要な前提知識について学べるのでおすすめです。"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ACL2",
+ "language": "acl2",
+ "name": "acl2"
+ },
+ "language_info": {
+ "codemirror_mode": "commonlisp",
+ "file_extension": ".lisp",
+ "mimetype": "text/x-common-lisp",
+ "name": "acl2"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}
diff --git a/notebooks/contact.header b/notebooks/contact.header
new file mode 100644
index 0000000..14082d6
--- /dev/null
+++ b/notebooks/contact.header
@@ -0,0 +1,5 @@
+title: 連絡先
+id: contact
+date: 2020-02-19 00:00
+updated: 2021-09-11 12:00
+description: tojo.tokyo に問い合わせをしたいときに見てください
diff --git a/notebooks/contact.ipynb b/notebooks/contact.ipynb
new file mode 100644
index 0000000..c2e9dbd
--- /dev/null
+++ b/notebooks/contact.ipynb
@@ -0,0 +1,55 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "id": "9047c246",
+ "metadata": {},
+ "source": [
+ "## メール\n",
+ "\n",
+ "* masaya@tojo.tokyo にメールを送ってください\n",
+ "* 必要であれば下記の GPG 鍵を使って暗号化して送信してください\n",
+ "\n",
+ "### GnuPG の鍵\n",
+ "\n",
+ "下記のコマンドで私の公開鍵を gpg に import できます。\n",
+ "\n",
+ "```\n",
+ "gpg --keyserver=hkps://keyserver.ubuntu.com --recv-keys C76AC7C77FF46F6E42C2D93545AA42647237561E\n",
+ "```\n",
+ "\n",
+ "インポートしたら必ずフィンガープリントが下記と一致することを確認してください。\n",
+ "\n",
+ "`C76A C7C7 7FF4 6F6E 42C2 D935 45AA 4264 7237 561E`\n",
+ "\n",
+ "## Mastodon (or 他の Activity Pub 実装)\n",
+ "\n",
+ "* [tojoqk@mastodon.tojo.tokyo](https://mastodon.tojo.tokyo/@tojoqk) ユーザーにメンションもしくは DM してください\n",
+ "\n",
+ "\n",
+ "## Twitter\n",
+ "\n",
+ "* メールが届かない、もしくは返信がない場合に利用してください\n",
+ "* [tojoqk](https://twitter.com/tojoqk) ユーザーに DM してください\n",
+ " * 通知を有効にしていないため気づくのに時間がかかる可能性があります"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "Guile",
+ "language": "scheme",
+ "name": "guile"
+ },
+ "language_info": {
+ "codemirror_mode": "scheme",
+ "file_extension": ".scm",
+ "mimetype": "application/x-scheme",
+ "name": "guile",
+ "pygments_lexer": "scheme",
+ "version": "2.0.0"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}
diff --git a/notebooks/guile-df.header b/notebooks/guile-df.header
new file mode 100644
index 0000000..12e8331
--- /dev/null
+++ b/notebooks/guile-df.header
@@ -0,0 +1,4 @@
+title: Guile で df コマンドの出力からディスク使用率を確認してみた
+id: guile-df
+date: 2021-09-12 00:15
+description: Guile で Unix のコマンドの出力を一行づつ読んで処理する具体的な例を紹介します
diff --git a/notebooks/guile-df.ipynb b/notebooks/guile-df.ipynb
new file mode 100644
index 0000000..5339d95
--- /dev/null
+++ b/notebooks/guile-df.ipynb
@@ -0,0 +1,387 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "id": "1b63a034",
+ "metadata": {},
+ "source": [
+ "## はじめに\n",
+ "\n",
+ "[Guix System](https://guix.gnu.org/) で動かしているサーバーのディスク容量を監視するために [Guile](https://www.gnu.org/software/guile/) で `df` コマンドの出力を読んでディスク容量を確認する手続きを Guile で作成したので紹介します。本記事によって Guile でコマンドの出力を一行づつ読んで処理するときのイメージが掴めると思います。なお、本プログラムは異常時の処理を書いていない雑なものなので参考にする場合は注意をお願いいたします。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "60dddb34",
+ "metadata": {},
+ "source": [
+ "## 本文中のプログラムのライセンス\n",
+ "\n",
+ "本記事で例示するプログラムのライセンスは GPLv3 (or later) です。ライセンスの詳細は [monitoring](https://git.tojo.tokyo/monitoring.git/) リポジトリの [COPYING](https://git.tojo.tokyo/monitoring.git/tree/COPYING) ファイルと [`tojo-tokyo/monitoring.scm`](https://git.tojo.tokyo/monitoring.git/tree/tojo-tokyo/monitoring.scm?id=9dadbd397af96b53b14050e741618657f6d7bf33) ファイルのヘッダの部分を参照してください。\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "1e23cfd1",
+ "metadata": {},
+ "source": [
+ "## パイプを開いて df の出力を読む\n",
+ "\n",
+ "まずは Guile から `df` コマンドを呼び出してみましょう パイプを開くために [`open-input-pipe`](https://www.gnu.org/software/guile/manual/html_node/Pipes.html) 手続きを使います。\n",
+ "`open-input-pipe` には `(ice-9 popen)` モジュールが必要で、ポートから文字を読み込むのに [`(ice-9 textual-ports)`](https://www.gnu.org/software/guile/manual/html_node/Textual-I_002fO.html) モジュールの手続きを利用しています。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "id": "c7b90f1e",
+ "metadata": {
+ "scrolled": true
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Filesystem 1K-blocks Used Available Use% Mounted on\n",
+ "none 492120 0 492120 0% /dev\n",
+ "/dev/vda3 24377696 10096084 13020252 44% /\n",
+ "tmpfs 501932 0 501932 0% /dev/shm\n",
+ "0"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {
+ "text/plain": "Filesystem 1K-blocks Used Available Use% Mounted on\nnone 492120 0 492120 0% /dev\n/dev/vda3 24377696 10096084 13020252 44% /\ntmpfs 501932 0 501932 0% /dev/shm\n0"
+ },
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(use-modules (ice-9 popen)\n",
+ " (ice-9 textual-ports))\n",
+ "\n",
+ "(let ((port (open-input-pipe \"df\")))\n",
+ " (display (get-string-all port))\n",
+ " (close-pipe port))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "c8471031",
+ "metadata": {},
+ "source": [
+ "ヘッダ行が先頭に一つありそれより下の行に1個以上の空白で区切られた値として必要な情報が出力されるようです。ヘッダ行は無視することにしてそれ以下を Guile の連想リストのリストにできればよさそうです。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "82822706",
+ "metadata": {},
+ "source": [
+ "## 文字列を空白で区切る手続きを作る\n",
+ "\n",
+ "1個以上の空白で区切られた文字列をリストにする手続きを Guile を軽く探したのですが見つけられなかったので自分で作ります。正規表現を扱う [`(ice-9 regex)`](https://www.gnu.org/software/guile/manual/html_node/Regexp-Functions.html) を使って下記のように実装します。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "id": "bb0af6b5",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "(\"hello\" \"world\")"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {
+ "text/plain": "(\"hello\" \"world\")"
+ },
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(use-modules (ice-9 regex))\n",
+ "\n",
+ "(define (split-with-spaces x)\n",
+ " (map match:substring (list-matches \"[^ ]+\" x)))\n",
+ "\n",
+ "(split-with-spaces \" hello world \")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "5457a7b3",
+ "metadata": {},
+ "source": [
+ "空白以外の文字が一個以上連続したものを集めることで空白で区切られた文字列のリストを作っています。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "a58209ba",
+ "metadata": {},
+ "source": [
+ "## df 手続きを実装する\n",
+ "\n",
+ "これから作成する `df` は無引数で呼びだして、`df` コマンドの出力のそれぞれの行を連想リストに変換したものを返す手続きです。\n",
+ "\n",
+ "今回は `split-with-spaces` を使用して下記のように実装しました。\n",
+ "なお、本記事の目的はコマンドの出力をパイプで一行づつ処理をするという Unix でよくある処理を Guile でやる方法を例示することなので意図的に手続き的に書いています。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "id": "7dda9e7d",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "(define (df)\n",
+ " (let ((port (open-input-pipe \"df\")))\n",
+ " (get-line port) ; ヘッダ行を読み飛ばす\n",
+ " (let loop ((line (get-line port))\n",
+ " (table '()))\n",
+ " (cond ((eof-object? line)\n",
+ " (close-pipe port)\n",
+ " table)\n",
+ " (else\n",
+ " (loop (get-line port)\n",
+ " (cons (map cons\n",
+ " '(filesystem 1k-blocks used available use% mounted-on)\n",
+ " (split-with-spaces line))\n",
+ " table)))))))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "7305fb6b",
+ "metadata": {},
+ "source": [
+ "`df` コマンドの出力を一行ずつ読んで連想リストを作成していき、最後まで読みきったらパイプをクローズした後に構築した連想リストのリストを返却します。\n",
+ "\n",
+ "`df` 手続きの結果を整形して出力してみましょう([`format`](https://www.gnu.org/software/guile/manual/html_node/Formatted-Output.html) 手続きのために `(ice-9 format)`, [`match-lambda`](https://www.gnu.org/software/guile/manual/html_node/Pattern-Matching.html) のために `(ice-9 match)` モジュールを使っています)。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "id": "d9dc0a68",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "filesystem: tmpfs\n",
+ "1k-blocks: 501932\n",
+ "used: 0\n",
+ "available: 501932\n",
+ "use%: 0%\n",
+ "mounted-on: /dev/shm\n",
+ "\n",
+ "filesystem: /dev/vda3\n",
+ "1k-blocks: 24377696\n",
+ "used: 10096084\n",
+ "available: 13020252\n",
+ "use%: 44%\n",
+ "mounted-on: /\n",
+ "\n",
+ "filesystem: none\n",
+ "1k-blocks: 492120\n",
+ "used: 0\n",
+ "available: 492120\n",
+ "use%: 0%\n",
+ "mounted-on: /dev\n",
+ "\n"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {
+ "text/plain": "filesystem: tmpfs\n1k-blocks: 501932\nused: 0\navailable: 501932\nuse%: 0%\nmounted-on: /dev/shm\n\nfilesystem: /dev/vda3\n1k-blocks: 24377696\nused: 10096084\navailable: 13020252\nuse%: 44%\nmounted-on: /\n\nfilesystem: none\n1k-blocks: 492120\nused: 0\navailable: 492120\nuse%: 0%\nmounted-on: /dev\n\n"
+ },
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(use-modules (ice-9 match)\n",
+ " (ice-9 format))\n",
+ "\n",
+ "(for-each (lambda (record) \n",
+ " (for-each (match-lambda \n",
+ " ((key . val)\n",
+ " (format #t \"~a: ~a~%\"\n",
+ " (symbol->string key)\n",
+ " val)))\n",
+ " record)\n",
+ " (newline))\n",
+ " (df))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "c2c2e3a0",
+ "metadata": {},
+ "source": [
+ "意図したとおりに実装できているようです。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "42d1870d",
+ "metadata": {},
+ "source": [
+ "## ディスク使用率がしきい値を超えているかを調べる"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "959c2b1b",
+ "metadata": {},
+ "source": [
+ "`df` 手続きを使ってしきい値以上のディスク使用率になっているファイルシステムがあったら真を返す、`disk-use%-over?` 手続きを作ってみましょう。\n",
+ "\n",
+ "私は `/dev/` から始まっているファイルシステムにしか興味ないので、`/dev/` から始まっている文字列かどうかを判定する述語 `prefix-/dev/?` を作成します。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "id": "f44e8fb2",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "(#f #t #f)"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {
+ "text/plain": "(#f #t #f)"
+ },
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(define (prefix-/dev/? x)\n",
+ " (and (string? x)\n",
+ " (<= 5 (string-length x))\n",
+ " (string=? (substring x 0 5) \"/dev/\")))\n",
+ "\n",
+ "(map prefix-/dev/? '(\"/tmp/shm\" \"/dev/hello\" \"/neko/dev\"))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "61a8d4be",
+ "metadata": {},
+ "source": [
+ "`use%` は `%` を含んだ文字列になってしまっていて数値比較をするには扱いにくい状態です。`x%` のような形になっている文字列を数字に変換する手続きを作成します。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "id": "417d7646",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "42"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {
+ "text/plain": "42"
+ },
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(define (use%->number x)\n",
+ " (string->number (string-delete #\\% x)))\n",
+ "\n",
+ "(use%->number \"42%\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "702d1b23",
+ "metadata": {},
+ "source": [
+ "それでは `prefix-/dev/?`、`use%->number` を利用して `disk-use%-over?` を実装してみましょう\n",
+ "(`(srfi srfi-26)` の [`cut` 構文](https://www.gnu.org/software/guile/manual/html_node/SRFI_002d26.html)を使っています。`(cut f <> x)` は `(lambda (y) (f y x))` のように書くのと同じです)。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "id": "ba8b28f4",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "(#t #f)"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {
+ "text/plain": "(#t #f)"
+ },
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(use-modules (srfi srfi-26)\n",
+ " ((srfi srfi-1) #:select (any)))\n",
+ "\n",
+ "(define (disk-use%-over? threshold)\n",
+ " (any (cut < threshold <>)\n",
+ " (map (compose use%->number (cut assoc-ref <> 'use%))\n",
+ " (filter (compose prefix-/dev/? (cut assoc-ref <> 'filesystem))\n",
+ " (df)))))\n",
+ "\n",
+ "(map disk-use%-over? '(40 50))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "77156af7",
+ "metadata": {},
+ "source": [
+ "しきい値が `40` の場合は真を返し、`50` の場合は偽を返しました。`/dev/vda3` の現在のディスク使用率は `44%` なので意図した挙動をしているようです。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "a321cde9",
+ "metadata": {},
+ "source": [
+ "## おわりに\n",
+ "\n",
+ "無事に Guile を使ってディスク使用率を調べる手続きを作成することができました。この Web サイトは Guix System で動いていて現在上記のプログラムを使って実際に監視を実施しています([該当するコード](https://git.tojo.tokyo/guix-config.git/tree/web/config.scm?id=1562b9827baa6a2c78592bd5f9115ed6a8b444b3#n33)、Guix System では [G-Expressions](https://guix.gnu.org/manual/en/html_node/G_002dExpressions.html) という仕組みを利用して定期実行ジョブを Guile で気軽に実装できます)。このように GNU Guile では Unix のコマンドと連携する実用的なプログラムを簡単に書くことができるのでみなさんも是非 GNU Guile を使ってみてください。"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "Guile",
+ "language": "scheme",
+ "name": "guile"
+ },
+ "language_info": {
+ "codemirror_mode": "scheme",
+ "file_extension": ".scm",
+ "mimetype": "application/x-scheme",
+ "name": "guile",
+ "pygments_lexer": "scheme",
+ "version": "2.0.0"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}
diff --git a/notebooks/guile-recursion.header b/notebooks/guile-recursion.header
new file mode 100644
index 0000000..55731df
--- /dev/null
+++ b/notebooks/guile-recursion.header
@@ -0,0 +1,4 @@
+title: Guile ではスタック溢れを気にせず再帰しよう
+id: guile-recursion
+date: 2021-09-12 21:00
+description: Guile ではスタックオーバーフローは起きないので末尾再帰にしなくてもいいという話
diff --git a/notebooks/guile-recursion.ipynb b/notebooks/guile-recursion.ipynb
new file mode 100644
index 0000000..2e66111
--- /dev/null
+++ b/notebooks/guile-recursion.ipynb
@@ -0,0 +1,595 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "id": "bd9a0f87",
+ "metadata": {},
+ "source": [
+ "## はじめに\n",
+ "\n",
+ "関数型プログラミングを学んだ人の多くは、スタックオーバーフローを回避するために再帰関数を末尾再帰の形式に変換する方法について学んでいると思います。Guile では他のプログラミング言語とは事情が異なり再帰をしても[システムのメモリを使い尽すまではスタックオーバーフローが起きません](https://www.gnu.org/software/guile/docs/docs-3.0/guile-ref/Stack-Overflow.html)([Racket も同様](https://docs.racket-lang.org/guide/Lists__Iteration__and_Recursion.html))。なので、一部の例外を除いて Guile でプログラムを書くときは無理に末尾再帰に変形せずに分かりやすくて綺麗な再帰のままにしましょう。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "5a476ec0",
+ "metadata": {},
+ "source": [
+ "## 自然な再帰と末尾再帰の比較\n",
+ "\n",
+ "### リストの長さを計算する再帰的な手続き length\n",
+ "\n",
+ "例としてリスト `x` の長さ(要素の数)を計算する `length` 手続きを Guile で実装することを考えてみましょう。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "id": "8a9e45fb",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "(define (length x)\n",
+ " (if (null? x)\n",
+ " 0\n",
+ " (+ 1 (length (cdr x)))))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "77c55549",
+ "metadata": {},
+ "source": [
+ "`length` の実行例:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "id": "8e3ace64",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "3"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {
+ "text/plain": "3"
+ },
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(length '(a b c))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "251c4f18",
+ "metadata": {},
+ "source": [
+ "### 再帰手続きの読み方\n",
+ "\n",
+ "`length` 手続きは下記のように読み下すことができます。\n",
+ "\n",
+ "`x` の長さ(`length`)とは:\n",
+ "* a. `x` が空リスト(`null?`)のときは `0`\n",
+ "* b. さもなくば、先頭以外(`cdr`)の長さ(`length`)に 1 を足したもの\n",
+ "\n",
+ "a のような自身 `length` を含まない場合のことを基底部、b のような自身を含む場合のことを帰納部と呼びます。\n",
+ "再帰手続きの正しさは基底部と帰納部をそれぞれ読んで「ふむ、確かにそうだな」と思えるのであれば正しいので理解するのはとても簡単です。\n",
+ "このような自然に読める再帰的な定義のことをここでは「自然な再帰」と呼ぶことにします。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "34b5d50b",
+ "metadata": {},
+ "source": [
+ "### 再帰手続きとスタックオーバーフロー\n",
+ "\n",
+ "Guile 以外の多くのプログラミング言語ではこのような再帰手続きにはスタックオーバーフローのリスクがあります。どういうことかというと、手続き呼び出しをしたときに元に戻る場所を覚えておくためコールスタックを使用するのですが多くのプログラミング言語ではコールスタックに上限が設定されています。コールスタックの上限に到達した段階でそれ以上の計算が不能になり途中で計算が停止してしまうのです。そのため、今回の場合リスト `x` がコールスタックの上限よりも大きい場合には `(length x)` を求めることはできません。\n",
+ "この問題を回避するためには末尾呼び出しの形式に変換する必要があります(ただし、末尾呼び出しの最適化が行なわれるプログラミング言語・処理系に限ります。そうでない場合は繰り返しを表現する構文を使って書き換える必要があります。構文上の違いのみでこれから議論する末尾再帰との比較には影響しないので末尾再帰の話を繰り返しに置き換えて読んでいただいても問題ありません)。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "558e0ddb",
+ "metadata": {},
+ "source": [
+ "### 末尾再帰版の length-tail\n",
+ "\n",
+ "ではスタックオーバーフローの回避のために末尾再帰呼び出しの形式に変換したリストの長さを求める手続き `length-tail` を見てみましょう。`len` という引数を追加していて、これには `0` を渡すことを想定しています(Scheme では手続きの中に手続きの定義がかけるので、`len` 引数を隠蔽することも可能なのですが、分かりやすさのためにあえて `len` 引数を残しています)。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "id": "a5e4e1b0",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "(define (length-tail x len)\n",
+ " (if (null? x)\n",
+ " len\n",
+ " (length-tail (cdr x) (+ len 1))))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "5c0b8118",
+ "metadata": {},
+ "source": [
+ "`length-tail` の実行例:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "id": "64f000a7",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "3"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {
+ "text/plain": "3"
+ },
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(length-tail '(a b c) 0)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "ed0f4ab0",
+ "metadata": {},
+ "source": [
+ "### 末尾再帰の手続きは理解が難しい\n",
+ "\n",
+ "`length` では手続きの定義を読み下すだけで理解できましたが、`length-tail` は少し難しいです。なぜなら、`length` の場合は基底部と帰納部をそれぞれ確認して正しいと思うことができましたが、`length-tail` の基底部は `len` であり単独では理解不能です。帰納部も `(length-tail (cdr x) (+ len 1))` とあり正しいかどうかは `len` 変数の値によるということになります。\n",
+ "\n",
+ "`length-tail` を理解するには計算の流れ全体を見なければいけません。\n",
+ "\n",
+ "* a. `len` の初期状態は `0`\n",
+ "* b. `x` を `(cdr x)` で置き換える度に `len` の値は `1` 増加する\n",
+ "* c. `x` が空リスト(`null?`) になったら、 `len` が初期の `x` の長さを表わしているため `len` を返却する\n",
+ " * c1. 初期の `x` が空リストになるには、初期の `x` の長さと同じ回数 b の計算を繰り返したときである\n",
+ " * c2. len の初期状態が 0 のため b を繰り返した回数が len の値となる\n",
+ " * c3. c1, c2 より `x` が空リストのとき len は初期の x の長さを表わしている\n",
+ "\n",
+ "とても考えることが多く難しいことを分かっていただけたでしょうか。`length-tail` という例が極めて簡単であったために難しいことを納得しにくいということはあるかもしれません。それでも、`length` は基底部と帰納部をそれぞれ読むだけでプログラムの正しさについて納得できたのに対し、`length-tail` を理解するにはプログラム全体の流れを追わないとよく分からないというのは大きな違いです。\n",
+ "\n",
+ "このような苦労をして `length-tail` を書くよりも `length` を書いた方が良いと思うでしょう。Guile ではスタックオーバーフローは起きないので問題ありません。 `length` の方を書きましょう。ただし、一点だけ注意があります。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "99f3d843",
+ "metadata": {},
+ "source": [
+ "### 末尾再帰と効率について\n",
+ "\n",
+ "実は Guile を使う場合であっても `length` と `length-tail` 手続きの間には違いがあります。\n",
+ "\n",
+ "`length-tail` では末尾再帰の最適化により呼び出し時の続きの計算を記憶しておく必要がありません。つまり、コールスタックに新しく追加する必要がありません。それに対して `length` では呼び出した後に続く計算を覚えておく必要があるのでコールスタックを消費します。`length` では `length-tail` と違って残りの計算を記憶するために記憶領域を消費してしまうのです。Guile ではコールスタックを消費しきったらヒープ領域を使ってコールスタックを拡張するので、与えるリストが長い場合には `length-tail` よりも `length` の方がメモリを多く使用してしまう可能性があるのです。ただし、メモリを消費するといっても与えるリストと同じくらいしか使わないので大した問題ではないでしょう。よほどメモリの消費に気を使う必要のあるようなケースでしか問題にならないと考えて良いでしょう。\n",
+ "\n",
+ "また、非末尾再帰の方が末尾再帰のよりも常に効率が悪いということではありません。むしろ末尾再帰にしない方が効率が良い場合もあります。手続き `f` とリスト `x` を取り、それぞれの要素を `f` によって変換したリストを返す `map` 手続きについて考えてみましょう。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "id": "5a2fdd3f",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "(define (map f x)\n",
+ " (if (null? x)\n",
+ " '()\n",
+ " (cons (f (car x))\n",
+ " (map f (cdr x)))))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "46359f45",
+ "metadata": {},
+ "source": [
+ "`map` の実行例:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "id": "e29afee1",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "(-1 -2 -3)"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {
+ "text/plain": "(-1 -2 -3)"
+ },
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(map - '(1 2 3))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "cb24caf0",
+ "metadata": {},
+ "source": [
+ "末尾再帰版の `map-tail` を実装してみましょう。`result` 引数には空リストを渡す想定です。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "id": "95da1a6f",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "(define (map-tail f x result)\n",
+ " (if (null? x)\n",
+ " (reverse result)\n",
+ " (map-tail f (cdr x) (cons (f (car x)) result))))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "113926d6",
+ "metadata": {},
+ "source": [
+ "map-tail の実行例:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "id": "a7b49b21",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "(-1 -2 -3)"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {
+ "text/plain": "(-1 -2 -3)"
+ },
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(map-tail - '(1 2 3) '())"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "3fc8259f",
+ "metadata": {},
+ "source": [
+ "`map` と `map-tail` のメモリ効率の違いについて検討してみましょう。`map` の手続きは `map` の呼び出しをするたびにコールスタックを消費し、不足した場合にはコールスタックを拡張するため `x` が長い場合にはメモリを消費する場合があります。それに対して `map-tail` はどうでしょうか。`map-tail` では `result` 引数を `(cons (f (car x)) result)` によって置き換えています。よって `map-tail` でも再帰するたびにメモリを消費していきます。上記から `map` と `map-tail` で `map` がコールスタックを消費するから `map` の方がメモリを多く使うとは必ずしもいえません。\n",
+ "さらに、`map-tail` では基底部で `reverse` を呼び出しています。これは `map-tail` と同じくらいの計算量とメモリを消費するため、`map-tail` の計算の方が時間がかかりそうです。\n",
+ "\n",
+ "試しに実行にかかる時間を計測して比較してみましょう。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "id": "c928cc34",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "1000 個のリストの場合\n",
+ "map(100回):\n",
+ "clock utime stime cutime cstime gctime\n",
+ " 0.04 0.03 0.01 0.00 0.00 0.01\n",
+ "map-tail(100回):\n",
+ "clock utime stime cutime cstime gctime\n",
+ " 0.05 0.05 0.00 0.00 0.00 0.01\n",
+ "\n",
+ "10000 個のリストの場合\n",
+ "map(100回):\n",
+ "clock utime stime cutime cstime gctime\n",
+ " 0.40 0.38 0.01 0.00 0.00 0.10\n",
+ "map-tail(100回):\n",
+ "clock utime stime cutime cstime gctime\n",
+ " 0.52 0.50 0.00 0.00 0.00 0.17\n",
+ "\n",
+ "100000 個のリストの場合\n",
+ "map(100回):\n",
+ "clock utime stime cutime cstime gctime\n",
+ " 3.76 3.45 0.22 0.00 0.00 0.49\n",
+ "map-tail(100回):\n",
+ "clock utime stime cutime cstime gctime\n",
+ " 4.48 4.36 0.01 0.00 0.00 0.95\n",
+ "\n"
+ ]
+ },
+ "execution_count": 9,
+ "metadata": {
+ "text/plain": "1000 個のリストの場合\nmap(100回):\nclock utime stime cutime cstime gctime\n 0.04 0.03 0.01 0.00 0.00 0.01\nmap-tail(100回):\nclock utime stime cutime cstime gctime\n 0.05 0.05 0.00 0.00 0.00 0.01\n\n10000 個のリストの場合\nmap(100回):\nclock utime stime cutime cstime gctime\n 0.40 0.38 0.01 0.00 0.00 0.10\nmap-tail(100回):\nclock utime stime cutime cstime gctime\n 0.52 0.50 0.00 0.00 0.00 0.17\n\n100000 個のリストの場合\nmap(100回):\nclock utime stime cutime cstime gctime\n 3.76 3.45 0.22 0.00 0.00 0.49\nmap-tail(100回):\nclock utime stime cutime cstime gctime\n 4.48 4.36 0.01 0.00 0.00 0.95\n\n"
+ },
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(use-modules (ice-9 time))\n",
+ "\n",
+ "(define-syntax-rule (dotimes (var n) form ...)\n",
+ " (let ((end n))\n",
+ " (do ((var 0 (+ var 1)))\n",
+ " ((<= end var))\n",
+ " form ...)))\n",
+ "\n",
+ "(for-each\n",
+ " (lambda (n)\n",
+ " (define x (iota (expt 10 n)))\n",
+ " (for-each display (list (expt 10 n) \" 個のリストの場合\\n\"))\n",
+ " \n",
+ " (display \"map(100回):\\n\")\n",
+ " (time (dotimes (i 100) (map - x)))\n",
+ "\n",
+ " (display \"map-tail(100回):\\n\")\n",
+ " (time (dotimes (i 100) (map-tail - x '()))) \n",
+ "\n",
+ " (newline))\n",
+ " (iota 3 3))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "276d0fd9",
+ "metadata": {},
+ "source": [
+ "予想通り `map-tail` の方が少し遅いという結果になりました(`map-tail` の実装に引数を破壊する版の `reverse!` を使った場合についても調べたところ、その場合は `map` とほぼ同じ計算時間になることを確認しています。計算時間が変わらないのであれば `map` の方が良いでしょう。また、[Guile のマニュアルの Stack Overflow の節](https://www.gnu.org/software/guile/manual/html_node/Stack-Overflow.html#Stack-Overflow)で `reverse!` を使うと継続安全(continuation-safe)が損なわれ、 `map-tail` の計算が終了した後に `f` の計算が再度実行された場合に正常に動作しなくなるという問題が指摘されています)。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "3788886d",
+ "metadata": {},
+ "source": [
+ "## 自然な再帰だと計算量が爆発してしまうケース\n",
+ "\n",
+ "ここまでの例では Guile でなら自然な再帰で良いと言える例だったのですが、何でもそうという訳ではありません。たまに自然な再帰だと計算量が爆発的に大きくなってしまう場合がありそういった場合には別のアルゴリズムに変更する必要があります。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "770912a1",
+ "metadata": {},
+ "source": [
+ "### リストを反転する手続き\n",
+ "\n",
+ "リストを反転する手続きを自然な再帰で実装してみましょう。特に効率などを考慮しなければ下記のように実装しようと思うかもしれません。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "id": "956af77d",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "(define (reverse x)\n",
+ " (if (null? x)\n",
+ " '()\n",
+ " (append (reverse (cdr x)) (list (car x)))))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "1126971d",
+ "metadata": {},
+ "source": [
+ "`reverse` の実行例:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "id": "0cdaf6cc",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "(c b a)"
+ ]
+ },
+ "execution_count": 11,
+ "metadata": {
+ "text/plain": "(c b a)"
+ },
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(reverse '(a b c))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "ce6c6577",
+ "metadata": {},
+ "source": [
+ "この手続きは自然でたしかに正しいことはコードを読めば理解できるでしょう。ただし、一つ落とし穴があります。Lisp のリストは先頭に要素を追加する場合は `O(1)` の計算量でできるのに対してリストの最後に要素を追加する場合は `O(n)` かかるのです。\n",
+ "この影響でリストが長くなると激的に遅くなります。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "id": "63bedfe3",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "clock utime stime cutime cstime gctime\n",
+ " 7.30 7.10 0.01 0.00 0.00 1.46\n",
+ "done"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {
+ "text/plain": "clock utime stime cutime cstime gctime\n 7.30 7.10 0.01 0.00 0.00 1.46\ndone"
+ },
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(time (reverse (iota 20000)))\n",
+ "'done"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "65ee86fc",
+ "metadata": {},
+ "source": [
+ "これに対してリストの先頭に追加する操作しか行なわない `reverse-tail` を試してみましょう。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "id": "94ab7202",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ "(define (reverse-tail x result)\n",
+ " (if (null? x)\n",
+ " result\n",
+ " (reverse-tail (cdr x)\n",
+ " (cons (car x) result))))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "c184f8de",
+ "metadata": {},
+ "source": [
+ "`reverse-tail` の実行例"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "id": "cd4cac47",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "(c b a)"
+ ]
+ },
+ "execution_count": 14,
+ "metadata": {
+ "text/plain": "(c b a)"
+ },
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(reverse-tail '(a b c) '())"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "468a39bf",
+ "metadata": {},
+ "source": [
+ "`reverse-tail` の実行時間の計測:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "id": "57eb603c",
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "clock utime stime cutime cstime gctime\n",
+ " 0.02 0.02 0.00 0.00 0.00 0.00\n",
+ "done"
+ ]
+ },
+ "execution_count": 15,
+ "metadata": {
+ "text/plain": "clock utime stime cutime cstime gctime\n 0.02 0.02 0.00 0.00 0.00 0.00\ndone"
+ },
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "(time (reverse-tail (iota 50000) '()))\n",
+ "'done"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "17b08877",
+ "metadata": {},
+ "source": [
+ "リストが長い場合は `reverse` と比較すると `reverse-tail` の方が圧倒的に早いのです。\n",
+ "\n",
+ "このように自然な再帰では計算に時間がかかり過ぎてしまう場合もあります。これは末尾再帰かどうかという話ではなくて、アルゴリズムが異なるために生じている違いであり今回の再帰手続きを末尾再帰の手続きに直す必要性の有無とは少しずれた話ではあります。こういう重い計算をしていてそれが問題となる場合には別のアルゴリズムを検討する必要があります。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "ca0c0a7d",
+ "metadata": {},
+ "source": [
+ "## おわりに\n",
+ "\n",
+ "Guile ではシステムのメモリを使い尽すまではスタックオーバーフローは起きないので、一般には自然な再帰をわざわざ末尾再帰の形式に変換してプログラムを読みにくくする必要はありません。末尾再帰に書き換えなくて済むプログラミングライフは大変快適なので、Guile のような再帰でスタックオーバーフローの起こさないプログラミング言語や処理系を探して使ってみてください。"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "Guile",
+ "language": "scheme",
+ "name": "guile"
+ },
+ "language_info": {
+ "codemirror_mode": "scheme",
+ "file_extension": ".scm",
+ "mimetype": "application/x-scheme",
+ "name": "guile",
+ "pygments_lexer": "scheme",
+ "version": "2.0.0"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}
diff --git a/notebooks/len-combinations.header b/notebooks/len-combinations.header
new file mode 100644
index 0000000..0947608
--- /dev/null
+++ b/notebooks/len-combinations.header
@@ -0,0 +1,4 @@
+title: ACL2 で全ての組み合わせを求める関数の長さの性質について証明してみた
+id: len-combinations
+date: 2021-09-02 01:45
+updated: 2021-09-02 10:30
diff --git a/notebooks/len-combinations.ipynb b/notebooks/len-combinations.ipynb
new file mode 100644
index 0000000..6130951
--- /dev/null
+++ b/notebooks/len-combinations.ipynb
@@ -0,0 +1,475 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "id": "98c0ac77",
+ "metadata": {},
+ "source": [
+ "## はじめに\n",
+ "\n",
+ "ACL2 でリストから k 個取り出す全ての組み合わせを求める関数 `combinations` と、組み合わせの数を求める関数 `comb` を定義し、`(equal (len (combinations x n)) (comb (len x) n))` を証明します。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "187456f8",
+ "metadata": {},
+ "source": [
+ "## きっかけ\n",
+ "\n",
+ "[acl2-kernel](https://github.com/tani/acl2-kernel) を使ってブログ記事を書いてみたいというのが本記事の主な動機です。今回良い感じに書けたら、今後も ACL2 でなんかやってみた記事を `acl2-kernel` を使って書いてみようと思います。"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "425f5eb2",
+ "metadata": {},
+ "source": [
+ "## LICENSE\n",
+ "\n",
+ "下記に例示するプログラムのライセンスを明示します。\n",
+ "\n",
+ "```\n",
+ "Copyright (C) 2021 Masaya Tojo <masaya@tojo.tokyo>\n",
+ "\n",
+ "Redistribution and use in source and binary forms, with or without\n",
+ "modification, are permitted provided that the following conditions are\n",
+ "met:\n",
+ "\n",
+ "1. Redistributions of source code must retain the above copyright\n",
+ "notice, this list of conditions and the following disclaimer.\n",
+ "\n",
+ "2. Redistributions in binary form must reproduce the above copyright\n",
+ "notice, this list of conditions and the following disclaimer in the\n",
+ "documentation and/or other materials provided with the distribution.\n",
+ "\n",
+ "3. Neither the name of the copyright holder nor the names of its\n",
+ "contributors may be used to endorse or promote products derived from\n",
+ "this software without specific prior written permission.\n",
+ "\n",
+ "THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS\n",
+ "\"AS IS\" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT\n",
+ "LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR\n",
+ "A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT\n",
+ "HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,\n",
+ "SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT\n",
+ "LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,\n",
+ "DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY\n",
+ "THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT\n",
+ "(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE\n",
+ "OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.\n",
+ "```"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "37660f5c",
+ "metadata": {},
+ "source": [
+ "## combinations 関数を定義する\n",
+ "\n",
+ "リストから k 個の要素を取り出す全ての組み合せを求める関数 `combinations` 関数を定義します。\n",
+ "\n",
+ "### 補助関数 cons-all を定義する\n",
+ "\n",
+ "`combinations` を作成するためには全てのリストの先頭に要素を一つ追加する `cons-all` 関数が必要です。\n",
+ "`cons-all` の停止性は ACL2 が自動証明してくれました。\n",
+ "`cons-all` の第二引数は真リストしか渡らないようにガードを設定していますが、ガードの証明も問題なく自動証明されました。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "id": "dd5300c3",
+ "metadata": {
+ "scrolled": true
+ },
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "\r",
+ "\r",
+ "\r\n",
+ "Summary\r\n",
+ "Form: ( RESET-PREHISTORY NIL ...)\r\n",
+ "Rules: NIL\r\n",
+ "Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)\r\n",
+ " :NEW-PREHISTORY-SET\r\n",
+ "\r",
+ "\r",
+ "\r",
+ "\r",
+ "\r",
+ "\r",
+ "\r",
+ "\r",
+ "\r\n",
+ "The admission of CONS-ALL is trivial, using the relation O< (which\r\n",
+ "is known to be well-founded on the domain recognized by O-P) and the\r\n",
+ "measure (ACL2-COUNT X). We observe that the type of CONS-ALL is described\r\n",
+ "by the theorem (TRUE-LISTP (CONS-ALL E X)). We used primitive type\r\n",
+ "reasoning.\r\n",
+ "\r\n",
+ "Computing the guard conjecture for CONS-ALL....\r\n",
+ "\r\n",
+ "The guard conjecture for CONS-ALL is trivial to prove, given primitive\r\n",
+ "type reasoning. CONS-ALL is compliant with Common Lisp.\r\n",
+ "\r\n",
+ "Summary\r\n",
+ "Form: ( DEFUN CONS-ALL ...)\r\n",
+ "Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))\r\n",
+ "Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)\r\n",
+ " CONS-ALL\r\n",
+ "\r"
+ ]
+ }
+ ],
+ "source": [
+ "(defun cons-all (e x)\n",
+ " (declare (xargs :guard (true-listp x)))\n",
+ " (if (endp x)\n",
+ " nil\n",
+ " (cons (cons e (car x))\n",
+ " (cons-all e (cdr x)))))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "e9a6ff91",
+ "metadata": {},
+ "source": [
+ "### combinations 関数\n",
+ "\n",
+ "リスト x から k 個を取り出す全ての組み合せのリストを求める関数 `combinations` を定義します。\n",
+ "\n",
+ "再帰によって `combinations` 関数を定義します。\n",
+ "`combinations` 関数を作成するにはリストの先頭の要素を含む場合と含まない場合に分けて分離して考えてそれらを連結するのがよいです。\n",
+ "\n",
+ "#### リストの先頭の要素を含む組み合せを求める\n",
+ "\n",
+ "リストの先頭の要素を含む場合は、まずリストの先頭の要素を含まない全ての組み合せを `combinations` 関数により求めます。その後に `cons-all` 関数を用いて全ての組み合せのそれぞれに先頭の要素を追加します。\n",
+ "\n",
+ "```\n",
+ "(cons-all (car x)\n",
+ " (combinations (cdr x) (- n 1)))\n",
+ "```\n",
+ "\n",
+ "#### リストの先頭の要素を含まない組み合せを求める\n",
+ "\n",
+ "リストの先頭の要素を含まない場合は簡単で、下記のように `combinations` 関数を使ってリストの先頭の要素を含めない場合を求めるだけです。\n",
+ "\n",
+ "```\n",
+ "(combinations (cdr x) n)\n",
+ "```\n",
+ "\n",
+ "#### combinations 関数の基底部を考える\n",
+ "\n",
+ "基底部として考えられるケースには与えられた自然数が 0 の場合と与えられたリストが空の場合があります。\n",
+ "リストから 0 個取り出す組み合せはただ一つ存在し、空リストです。よってリストから0個取り出す場合の全ての組み合せは `(list nil)` です。\n",
+ "\n",
+ "空のリストからは 1 以上取り出す組み合せを求めることは不可能です(空リストから 0 個を取り出す組み合せを求めることは可能で結果は上述した通りです)。不可能なわけですから、空リストから 1 以上取り出す場合の全ての組み合せは `nil` です。\n",
+ "\n",
+ "#### combinations 関数\n",
+ "\n",
+ "上記をまとめると、`combinations` 関数は下記のように実装できます。\n",
+ "停止性とガードは補助定理なしで ACL2 が自動証明してくれました。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "id": "9a281282",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "\r",
+ "\r",
+ "\r",
+ "\r",
+ "\r",
+ "\r",
+ "\r",
+ "\r",
+ "\r",
+ "\r",
+ "\r",
+ "\r\n",
+ "The admission of COMBINATIONS is trivial, using the relation O< (which\r\n",
+ "is known to be well-founded on the domain recognized by O-P) and the\r\n",
+ "measure (ACL2-COUNT X). We observe that the type of COMBINATIONS is\r\n",
+ "described by the theorem (TRUE-LISTP (COMBINATIONS X N)). We used\r\n",
+ "the :type-prescription rules BINARY-APPEND and TRUE-LISTP-APPEND.\r\n",
+ "\r\n",
+ "Computing the guard conjecture for COMBINATIONS....\r\n",
+ "\r\n",
+ "The guard conjecture for COMBINATIONS is trivial to prove, given the\r\n",
+ ":compound-recognizer rules NATP-COMPOUND-RECOGNIZER and \r\n",
+ "ZP-COMPOUND-RECOGNIZER, primitive type reasoning and the :type-prescription\r\n",
+ "rules COMBINATIONS and CONS-ALL. COMBINATIONS is compliant with Common\r\n",
+ "Lisp.\r\n",
+ "\r\n",
+ "Summary\r\n",
+ "Form: ( DEFUN COMBINATIONS ...)\r\n",
+ "Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)\r\n",
+ " (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)\r\n",
+ " (:FAKE-RUNE-FOR-TYPE-SET NIL)\r\n",
+ " (:TYPE-PRESCRIPTION BINARY-APPEND)\r\n",
+ " (:TYPE-PRESCRIPTION COMBINATIONS)\r\n",
+ " (:TYPE-PRESCRIPTION CONS-ALL)\r\n",
+ " (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))\r\n",
+ "Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)\r\n",
+ " COMBINATIONS\r\n",
+ "\r"
+ ]
+ }
+ ],
+ "source": [
+ "(defun combinations (x n)\n",
+ " (declare (xargs :guard (and (true-listp x)\n",
+ " (natp n))))\n",
+ " (cond\n",
+ " ((zp n) (list nil))\n",
+ " ((endp x) nil)\n",
+ " (t\n",
+ " (append (cons-all (car x)\n",
+ " (combinations (cdr x) (- n 1)))\n",
+ " (combinations (cdr x) n)))))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "88b9e137",
+ "metadata": {},
+ "source": [
+ "## comb 関数を定義する\n",
+ "\n",
+ "n 個から k 個を取り出す組み合せの数を求める関数を定義します。\n",
+ "`combinations` の定義を参照しながら対応するように記述しましょう。\n",
+ "\n",
+ "* 0 個を取り出す組み合せは空リストただ一つなので、組み合せの数は 1\n",
+ "* 長さ 0 のリストから 1 個以上取り出すことはできないため、組み合せの数は 0\n",
+ "* 先頭要素を含む組み合せの数は `(comb (- n 1) (- k 1))` \n",
+ " * cons-all 関数は与えられたリストの長さを変えないことに注意\n",
+ "* 先頭要素を含まない組み合せの数は `(comb (- n 1) k)`\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "id": "28488f02",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "\r",
+ "\r",
+ "\r",
+ "\r",
+ "\r",
+ "\r\n",
+ "The admission of COMB is trivial, using the relation O< (which is known\r\n",
+ "to be well-founded on the domain recognized by O-P) and the measure\r\n",
+ "(ACL2-COUNT N). We observe that the type of COMB is described by the\r\n",
+ "theorem (AND (INTEGERP (COMB N K)) (<= 0 (COMB N K))). We used primitive\r\n",
+ "type reasoning.\r\n",
+ "\r\n",
+ "Summary\r\n",
+ "Form: ( DEFUN COMB ...)\r\n",
+ "Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))\r\n",
+ "Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)\r\n",
+ " COMB\r\n",
+ "\r"
+ ]
+ }
+ ],
+ "source": [
+ "(defun comb (n k)\n",
+ " (cond\n",
+ " ((zp k) 1)\n",
+ " ((zp n) 0)\n",
+ " (t (+ (comb (- n 1) (- k 1))\n",
+ " (comb (- n 1) k)))))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "529c24b5",
+ "metadata": {},
+ "source": [
+ "## len-combinations 定理\n",
+ "\n",
+ "`(len (combinations x k))` が `(comb (len x) k)` と一致することを証明します。\n",
+ "これは ACL2 が補助定理を必要とせずに自動証明してくれました。"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "id": "3b6ced2b",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "\r",
+ "\r",
+ "\r",
+ "\r",
+ "\r",
+ "\r\n",
+ "*1 (the initial Goal, a key checkpoint) is pushed for proof by induction.\r\n",
+ "\r\n",
+ "Perhaps we can prove *1 by induction. Two induction schemes are suggested\r\n",
+ "by this conjecture. These merge into one derived induction scheme.\r\n",
+ "\r\n",
+ "We will induct according to a scheme suggested by (COMBINATIONS X K).\r\n",
+ "This suggestion was produced using the :induction rules COMBINATIONS\r\n",
+ "and LEN. If we let (:P K X) denote *1 above then the induction scheme\r\n",
+ "we'll use is\r\n",
+ "(AND (IMPLIES (AND (NOT (ZP K))\r\n",
+ " (NOT (ENDP X))\r\n",
+ " (:P (+ -1 K) (CDR X))\r\n",
+ " (:P K (CDR X)))\r\n",
+ " (:P K X))\r\n",
+ " (IMPLIES (AND (NOT (ZP K)) (ENDP X))\r\n",
+ " (:P K X))\r\n",
+ " (IMPLIES (ZP K) (:P K X))).\r\n",
+ "This induction is justified by the same argument used to admit COMBINATIONS.\r\n",
+ "Note, however, that the unmeasured variable K is being instantiated.\r\n",
+ "When applied to the goal at hand the above induction scheme produces\r\n",
+ "three nontautological subgoals.\r\n",
+ "Subgoal *1/3\r\n",
+ "Subgoal *1/3'\r\n",
+ "Subgoal *1/3''\r\n",
+ "Subgoal *1/3'''\r\n",
+ "Subgoal *1/3'4'\r\n",
+ "Subgoal *1/3'5'\r\n",
+ "Subgoal *1/3'6'\r\n",
+ "Subgoal *1/3'7'\r\n",
+ "Subgoal *1/3'8'\r\n",
+ "Subgoal *1/3'9'\r\n",
+ "Subgoal *1/3'10'\r\n",
+ "\r\n",
+ "([ A key checkpoint while proving *1 (descended from Goal):\r\n",
+ "\r\n",
+ "Subgoal *1/3''\r\n",
+ "(IMPLIES (AND (NOT (ZP K))\r\n",
+ " (CONSP X)\r\n",
+ " (EQUAL (LEN (COMBINATIONS (CDR X) (+ -1 K)))\r\n",
+ " (COMB (LEN (CDR X)) (+ -1 K)))\r\n",
+ " (EQUAL (LEN (COMBINATIONS (CDR X) K))\r\n",
+ " (COMB (LEN (CDR X)) K)))\r\n",
+ " (EQUAL (LEN (APPEND (CONS-ALL (CAR X)\r\n",
+ " (COMBINATIONS (CDR X) (+ -1 K)))\r\n",
+ " (COMBINATIONS (CDR X) K)))\r\n",
+ " (+ (COMB (LEN (CDR X)) K)\r\n",
+ " (COMB (LEN (CDR X)) (+ -1 K)))))\r\n",
+ "\r\n",
+ "*1.1 (Subgoal *1/3'10') is pushed for proof by induction.\r\n",
+ "\r\n",
+ "])\r\n",
+ "Subgoal *1/2\r\n",
+ "Subgoal *1/2'\r\n",
+ "Subgoal *1/1\r\n",
+ "\r\n",
+ "So we now return to *1.1, which is\r\n",
+ "\r\n",
+ "(IMPLIES (AND (TRUE-LISTP CS0) (TRUE-LISTP CS))\r\n",
+ " (EQUAL (LEN (APPEND (CONS-ALL X1 CS0) CS))\r\n",
+ " (+ (LEN CS) (LEN CS0)))).\r\n",
+ "Subgoal *1.1/3\r\n",
+ "Subgoal *1.1/3'\r\n",
+ "Subgoal *1.1/2\r\n",
+ "Subgoal *1.1/1\r\n",
+ "Subgoal *1.1/1'\r\n",
+ "\r\n",
+ "*1.1 and *1 are COMPLETED!\r\n",
+ "Thus key checkpoints Subgoal *1/3'' and Goal are COMPLETED!\r\n",
+ "\r\n",
+ "Q.E.D.\r\n",
+ "\r\n",
+ "Summary\r\n",
+ "Form: ( DEFTHM LEN-COMBINATIONS ...)\r\n",
+ "Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)\r\n",
+ " (:DEFINITION BINARY-APPEND)\r\n",
+ " (:DEFINITION COMB)\r\n",
+ " (:DEFINITION COMBINATIONS)\r\n",
+ " (:DEFINITION CONS-ALL)\r\n",
+ " (:DEFINITION ENDP)\r\n",
+ " (:DEFINITION FIX)\r\n",
+ " (:DEFINITION LEN)\r\n",
+ " (:DEFINITION NOT)\r\n",
+ " (:DEFINITION SYNP)\r\n",
+ " (:DEFINITION TRUE-LISTP)\r\n",
+ " (:ELIM CAR-CDR-ELIM)\r\n",
+ " (:EXECUTABLE-COUNTERPART BINARY-+)\r\n",
+ " (:EXECUTABLE-COUNTERPART CONSP)\r\n",
+ " (:EXECUTABLE-COUNTERPART EQUAL)\r\n",
+ " (:EXECUTABLE-COUNTERPART LEN)\r\n",
+ " (:EXECUTABLE-COUNTERPART ZP)\r\n",
+ " (:FAKE-RUNE-FOR-TYPE-SET NIL)\r\n",
+ " (:INDUCTION COMBINATIONS)\r\n",
+ " (:INDUCTION CONS-ALL)\r\n",
+ " (:INDUCTION LEN)\r\n",
+ " (:INDUCTION TRUE-LISTP)\r\n",
+ " (:REWRITE CAR-CONS)\r\n",
+ " (:REWRITE CDR-CONS)\r\n",
+ " (:REWRITE COMMUTATIVITY-2-OF-+)\r\n",
+ " (:REWRITE COMMUTATIVITY-OF-+)\r\n",
+ " (:REWRITE FOLD-CONSTS-IN-+)\r\n",
+ " (:REWRITE UNICITY-OF-0)\r\n",
+ " (:TYPE-PRESCRIPTION COMBINATIONS)\r\n",
+ " (:TYPE-PRESCRIPTION CONS-ALL)\r\n",
+ " (:TYPE-PRESCRIPTION LEN)\r\n",
+ " (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))\r\n",
+ "Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)\r\n",
+ "Prover steps counted: 5105\r\n",
+ " LEN-COMBINATIONS\r\n",
+ "\r"
+ ]
+ }
+ ],
+ "source": [
+ "(defthm len-combinations\n",
+ " (equal (len (combinations x k))\n",
+ " (comb (len x) k)))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "87d4963c",
+ "metadata": {},
+ "source": [
+ "## おわりに\n",
+ "\n",
+ "無事に組み合せを求める関数と組み合せの数を求める関数の関係が意図した通りであることを証明できました。\n",
+ "今回は二つの関数の定義がほとんど同じであったため補助定理を考える必要もなく証明できたのですが、通常はもう少し難しいことが多いです。\n",
+ "\n",
+ "`comb` の定義の方法は他にもあるため、他の定義による組み合せの数と一致するかについての証明を試みても良いかもしれません。"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ACL2",
+ "language": "acl2",
+ "name": "acl2"
+ },
+ "language_info": {
+ "codemirror_mode": "commonlisp",
+ "file_extension": ".lisp",
+ "mimetype": "text/x-common-lisp",
+ "name": "acl2"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}
diff --git a/posts/about-me.md b/posts/about-me.md
index 5e20bde..cb8c60a 100644
--- a/posts/about-me.md
+++ b/posts/about-me.md
@@ -1,14 +1,131 @@
title: About me
id: about-me
date: 2020-02-19 00:00
-updated: 2020-05-08 08:10
-description: TojoQK について
+updated: 2021-09-12 12:00
+description: 自己紹介ページ
---
## 自己紹介
-自由ソフトウェアに関心を持っています。 Scheme というプログラミング言語が好きで、GNU Guile という Scheme
-の処理系に入門中です。
-GNU Guix は自由ソフトウェアと Scheme の両方に関心がある人にとっては最高の OS、パッケージマネージャで、 最近はどうしたら
-GNU Guix を普及させることができるかといったことをよく考えています。
+
+### 自由ソフトウェア
+
+[自由ソフトウェア](https://www.gnu.org/philosophy/free-sw.ja.html)が好きでユーザーが自分の環境で動かすプログラムをコントロールできるのが当然の時代が訪れる未来のために貢献していきたいと考えています。
+
+2020 年の 7 月から Free Software Foundation の Associate Member を続けています。
+
+[![FSF の Member
+button](https://static.fsf.org/nosvn/associate/crm/5002583.png)](https://my.fsf.org/join?referrer=5002583)
+
+FSF は自由ソフトウェア普及させるための活動を精力的に行なっています。あなたも一緒に [FSF
+を支援](https://my.fsf.org/join?referrer=5002583)しましょう。
+
+
+
+### ACL2 による定理証明
+
+ACL2 は定理証明支援系の一つで、Common Lisp のサブセットでもあります。最近はこの ACL2
+を使って定理証明をするのにはまっています。初見では自分が使えるようになる気がまったくしなかったのですが、ちゃんと勉強すると意外に使えるようになるので結構おすすめです。
+
+ACL2 を使って書いた定理を
+[acl2-theorems](https://git.tojo.tokyo/acl2-theorems.git/tree/)
+リポジトリに置いているのでよかったら見てみてください。
+
+
+
+### GNU Guile によるプログラミング
+
+好きなプログラミング言語は GNU の公式の拡張言語である [GNU
+Guile](https://www.gnu.org/software/guile/) です。Guile は Scheme の処理系の一つです。
+日常的なちょっとしたスクリプトを書くのによく使っています。
+
+Guile は Scheme の処理系の一つですが Scheme の処理系の中で GNU Guile を選択している最大の理由は LGPLv3
+か GPLv3
+でライブラリを書く文化が成立しているというところです。実際のところプログラムのライセンスを決めるときは、そのプログラミング言語のコミュニティがどういうライセンスを好むのかというので決めることも多いと思います。Guile
+だとライブラリのライセンスが LGPLv3 か GPLv3 のいずれかの場合が多いし、使いたいライブラリが GPLv3 の場合は必然的に
+GPLv3 を選択することになります。 よって、他のプログラミング言語と違って社会的な GPLv3 以外を使う圧をなんとなく感じることなく
+GPLv3 を選択してプログラムを書くことができます。
+
+技術的な面で GNU Guile
+の一番良いところは、[末尾再帰でない手続きがスタックオーバーフローしない(システムのメモリを使い尽さない限り)](https://www.gnu.org/software/guile/manual/html_node/Stack-Overflow.html)ことです([Racket
+も同じです](https://docs.racket-lang.org/guide/Lists__Iteration__and_Recursion.html))。これは明らかによいことでプログラムの書き方を変えます。一般に再帰手続きを末尾再帰に変換するのは効率のためではなくてスタックオーバーフローを恐れるためです。ほとんどの場合、末尾再帰の手続きは理解しにくく汚ないです。それに対して自然な再帰手続きは読みやすく再帰的な処理を綺麗に表現していて本当に美しいものです。よほど効率が悪くなって明らかに問題が生じてしまう場合を除けば再帰の手続きをわざわざ末尾再帰に書き換える必要はありません。末尾再帰の手続きを書くのは実質的に手続き型プログラミングをしているのとほとんど違いがないため、**普通の再帰で問題のないようなプログラミング言語こそ真の意味で関数型プログラミング言語といえるのです**。
+
+
+
+### GPG の鍵
+
+下記のコマンドで私の公開鍵を gpg に import できます。
+
+ gpg --keyserver=hkps://keyserver.ubuntu.com --recv-keys C76AC7C77FF46F6E42C2D93545AA42647237561E
+
+インポートしたら必ずフィンガープリントが下記と一致することを確認してください。
+
+`C76A C7C7 7FF4 6F6E 42C2 D935 45AA 4264 7237 561E`
+
+
+
+### 連絡先
+
+[Contact](https://www.tojo.tokyo/contact.html) ページを参照してください。
+
+
+
+### その他
+
+ - 好きなOS・パッケージマネージャ: [GNU Guix](https://guix.gnu.org/)
+ - 他のパッケージマネージャはなんか怖くて使えなくなった
+ - Nix はよさそうだけど興味がなくて使えない…
+ - システムのアップグレードした後に気軽に rollback できるの最高
+ - guix environment を使えば簡単に開発環境の環境構築ができるのでみんなこれを使って欲しい
+ - システムの設定とかパッケージの定義を GNU Guile で書けるの最高過ぎる
+ - 自分用の Guix チャンネルも作って使ってる
+ - <https://git.tojo.tokyo/tojo-tokyo-guix-channel.git/>
+ - このサイトを表示している Web サーバーも Guix System で動いている
+ - 設定:
+ <https://git.tojo.tokyo/guix-config.git/tree/web/config.scm>
+ - 好きなエディタ: [GNU Emacs](https://guix.gnu.org/)
+ - Emacs への情熱はそこまでではないけど使っているのにはそれなりの理由がある
+ - Lisp のコードを良い感じにインデントしてくれるエディタは Emacs くらいしかない
+ - 他のエディタを使おうとすると Lisp のインデントができないことがすぐに致命的になる
+ - [Paredit](https://www.emacswiki.org/emacs/ParEdit) が特に最高
+ - [Magit](https://magit.vc/) という git クライアントがある
+ - git のコマンドはあんまり覚えてなくてだいたい Magit で操作している
+ - org-mode は最近使ってない……
+ - Nextcloud とか Jupyter Notebook を主に使ってる
+ - 何度か使う習慣を付けようとしたけど何故か私にはあんまり合っていないらしく使うのをやめてしまう
+ - [Geiser](https://www.nongnu.org/geiser/) という Scheme の開発環境がある
+ - GNU Guile のプログラムを書くときに使ってる
+ - これがないと補完とかできないから必要
+ - ACL2 でも当然のように [Emacs
+ を勧めてくる](https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____EMACS)
+ - ただ ACL2 の Emacs の設定について理解するのには暫くかかったので Emacs に慣れている人でも最初から
+ Emacs を勧めるべきかは微妙
+ - 初めて ACL2 を使う場合は [ProofPad](http://new.proofpad.org/) の方がおすすめ
+ - Emacs のパッケージは GNU Guix で管理するのがおすすめ
+ - 複数のパッケージマネージャを管理するの大変だし全部 Guix でよい
+ - 好きなクラウドサービス: [Nextcloud](https://nextcloud.com/)
+ - 自分でホスティングしている
+ - もはやこれなしにどうやって生きていけばいいのか分からない
+ - 単にファイルをクラウドに上げるだけでなくて色々なことができる
+ - [Notes](https://apps.nextcloud.com/apps/notes)
+ - ちょっとしたメモを書くのに使ってる
+ - [カレンダー](https://apps.nextcloud.com/apps/calendar)・[タスク管理](https://apps.nextcloud.com/apps/tasks)
+ - CalDAV に対応しているので、対応ソフトウェアから利用可能
+ - [News](https://apps.nextcloud.com/apps/news)
+ - RSS のフィードを登録できる
+ - [Maps](https://apps.nextcloud.com/apps/passwords)
+ - 地図上に自分で撮影した写真を表示できるのがよい
+ - [Passwords](https://apps.nextcloud.com/apps/passwords)
+ - 自分で管理していないサーバーにパスワードを預けるのちょっと怖いので自分でホスティングする価値がある
+ - [Bookmarks](https://apps.nextcloud.com/apps/bookmarks)
+ - 複数の端末でブックマークを同期できる
+ - 好きな Window Manager: [xfce4](https://www.xfce.org/)
+ - タイル型ウィンドウマネージャーとかも試したけど結局私には Xfce4 が一番合っていた
+ - パネルがいい
+ - 私にとって必要な機能が過不足なくある
+ - 使っているVPS: [Vultr](https://www.vultr.com/ja/)
+ - 2017 年の 7 月からずっと使ってる
+ - 他のに乗り換える理由が今のところない
+ - このサイトを表示している Web サーバーも Vultr で動かしてる
+
diff --git a/posts/comb-factorial.md b/posts/comb-factorial.md
new file mode 100644
index 0000000..806a998
--- /dev/null
+++ b/posts/comb-factorial.md
@@ -0,0 +1,796 @@
+title: ACL2 で組み合せの数とその階乗表現の関係について証明してみた
+id: comb-factorial
+date: 2021-09-05 13:30
+updated: 2021-09-05 14:00
+---
+
+## はじめに
+
+本記事は前回の [ACL2 で全ての組み合わせを求める関数の長さの性質について証明してみた --
+TojoQK](https://www.tojo.tokyo/len-combinations.html)
+の続きです。未読の方は先に読んでからお読みください。
+
+前回、リスト中の要素の全ての組み合わせを求める関数 `combinations` と組み合わせの数を求める関数 `comb` を求め、
+`(len (combinations x k))` と `(comb (len x) k)`
+が等しいことを証明しました。ただし、`combinations` と
+`comb` の定義は同じ構造をしているため、ACL2 で自動証明ができたといってもありがたみを感じにくい例だったかと思います。
+よって、今回は組み合わせの数を階乗で表現した式と前回の `comb` が等しいことを証明します。
+
+
+
+## 本記事で例示するプログラムのライセンス
+
+本記事で例示するプログラムのライセンスは3条項BSDであり自由ソフトウェアです。下記にライセンスを明示します。
+
+ Copyright (C) 2021 Masaya Tojo <masaya@tojo.tokyo>
+
+ Redistribution and use in source and binary forms, with or without
+ modification, are permitted provided that the following conditions are
+ met:
+
+ 1. Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+
+ 2. Redistributions in binary form must reproduce the above copyright
+ notice, this list of conditions and the following disclaimer in the
+ documentation and/or other materials provided with the distribution.
+
+ 3. Neither the name of the copyright holder nor the names of its
+ contributors may be used to endorse or promote products derived from
+ this software without specific prior written permission.
+
+ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+
+
+## 組み合せの数を求める関数 comb を定義する
+
+[前回の記事](https://www.tojo.tokyo/len-combinations.html)で作成した組み合わせの数を求める関数
+`comb` です。
+関数の定義については[前回の記事](https://www.tojo.tokyo/len-combinations.html)で説明しているので必要であれば参照してください
+
+
+
+``` acl2
+(defun comb (n k)
+ (cond
+ ((zp k) 1)
+ ((zp n) 0)
+ (t (+ (comb (- n 1) k)
+ (comb (- n 1) (- k 1))))))
+```
+
+
+```
+
+The admission of COMB is trivial, using the relation O< (which is known
+to be well-founded on the domain recognized by O-P) and the measure
+(ACL2-COUNT N). We observe that the type of COMB is described by the
+theorem (AND (INTEGERP (COMB N K)) (<= 0 (COMB N K))). We used primitive
+type reasoning.
+
+Summary
+Form: ( DEFUN COMB ...)
+Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
+Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.01)
+ COMB
+```
+
+
+
+
+ただ、前回の `comb` の説明はアルゴリズムに関するものだけで、関数中で使用している `zp`
+関数については特に説明していませんでした。`zp` 関数は
+Common Lisp (ACL2 は Common Lisp のサブセットです)には存在していない関数であり、Common Lisp にもある
+0 かどうかを調べる関数の `zerop` とは挙動が異なります。`zp` を使用している理由については ACL2
+の関数定義の仕様について軽く説明する必要があります。
+
+### ACL2 と停止性の証明
+
+ACL2 では全ての関数は停止しないといけません。ACL2 は `defun`
+で関数を定義するときに毎回停止性について証明しています(今までの例では一度も停止性の証明に失敗していません)。
+重要なのは関数にどのような値を与えても停止しないといけないということです。ACL2 は型なしの言語なので ACL2
+で利用可能な全てのデータ型の値が関数に渡る可能性があります。自然数のみを引数に取る関数のつもりで書いていたなどという言い訳は
+ACL2 には通用しないのです。 `zp` 関数は 0 だけでなく自然数(0を含む)以外の全ての値を `0` として処理します。なので
+`zerop` とは異なり`(zp -1)` や `(zp 'a)` も `t` です。 `zp`
+関数により基底部へ分岐する判定をすることで自然数以外の予期しない値が与えられた場合であっても確実に関数が停止することを証明できるのです。
+具体的にどうやって停止性の証明をするのかについてはいつか別に記事を作成して説明しようという気持ちはありますが実際のスケジュールは未定のため、興味のある方は
+ACL2 のドキュメントを読むか『定理証明手習い』(ラムダノート社)を参照することをおすすめします。
+
+zp 関数の詳細については [zp
+関数のドキュメント](https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=ACL2____ZP)
+を参照してください。
+
+また、ACL2 が型なしであることについて不安に感じた静的型付きのプログラミング言語を好む方は [XDOC —
+Guard](https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=ACL2____GUARD)
+を軽く読んでみてください。初心者向けの機能ではないのですが、実際に関数に渡る値を静的に制限することができます(停止性の証明時にあらゆる値について考慮しないといけないことは
+Guard を使用しても変わりません)。
+
+
+
+### comb の性質
+
+`comb` と階乗の関係の性質について証明する前に `comb` について既に分かっている性質については先に証明しておきましょう。 特に
+`comb` の次に説明する階乗表現を定義する際には「k が n よりも大きいときは (comb n k) は 0」という性質を利用します。
+なので、下記の `comb-zero` という定理を先に証明しておきます。
+
+
+
+``` acl2
+(defthm comb-zero
+ (implies (and (natp n)
+ (natp k)
+ (< n k))
+ (equal (comb n k) 0)))
+```
+
+
+```
+Goal'
+
+([ A key checkpoint:
+
+Goal'
+(IMPLIES (AND (INTEGERP N)
+ (<= 0 N)
+ (INTEGERP K)
+ (<= 0 K)
+ (< N K))
+ (EQUAL (COMB N K) 0))
+
+*1 (Goal') is pushed for proof by induction.
+
+])
+
+Perhaps we can prove *1 by induction. One induction scheme is suggested
+by this conjecture.
+
+We will induct according to a scheme suggested by (COMB N K). This
+suggestion was produced using the :induction rule COMB. If we let
+(:P K N) denote *1 above then the induction scheme we'll use is
+(AND (IMPLIES (AND (NOT (ZP K))
+ (NOT (ZP N))
+ (:P K (+ -1 N))
+ (:P (+ -1 K) (+ -1 N)))
+ (:P K N))
+ (IMPLIES (AND (NOT (ZP K)) (ZP N))
+ (:P K N))
+ (IMPLIES (ZP K) (:P K N))).
+This induction is justified by the same argument used to admit COMB.
+Note, however, that the unmeasured variable K is being instantiated.
+When applied to the goal at hand the above induction scheme produces
+twelve nontautological subgoals.
+Subgoal *1/12
+Subgoal *1/11
+Subgoal *1/10
+Subgoal *1/9
+Subgoal *1/8
+Subgoal *1/7
+Subgoal *1/6
+Subgoal *1/5
+Subgoal *1/4
+Subgoal *1/3
+Subgoal *1/2
+Subgoal *1/2'
+Subgoal *1/1
+
+*1 is COMPLETED!
+Thus key checkpoint Goal' is COMPLETED!
+
+Q.E.D.
+
+Summary
+Form: ( DEFTHM COMB-ZERO ...)
+Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
+ (:DEFINITION COMB)
+ (:DEFINITION NATP)
+ (:DEFINITION NOT)
+ (:EXECUTABLE-COUNTERPART <)
+ (:EXECUTABLE-COUNTERPART BINARY-+)
+ (:EXECUTABLE-COUNTERPART EQUAL)
+ (:EXECUTABLE-COUNTERPART INTEGERP)
+ (:EXECUTABLE-COUNTERPART NOT)
+ (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
+ (:EXECUTABLE-COUNTERPART ZP)
+ (:FAKE-RUNE-FOR-LINEAR NIL)
+ (:FAKE-RUNE-FOR-TYPE-SET NIL)
+ (:INDUCTION COMB))
+Time: 0.03 seconds (prove: 0.02, print: 0.01, other: 0.00)
+Prover steps counted: 707
+ COMB-ZERO
+```
+
+
+
+
+## 階乗を求める関数 factorial を定義する
+
+階乗の定義は下記の通りです。
+
+1. 0 の階乗は 1
+2. n が 0 より大きい自然数のとき、n の階乗は n と n - 1 の階乗の積
+
+これをそのまま ACL2に翻訳した `factorial` の定義を示します(厳密には前述した通り基底部の判定に zp
+関数を使用するため全く同じというわけではありません)。
+
+
+
+``` acl2
+(defun factorial (n)
+ (if (zp n)
+ 1
+ (* n (factorial (- n 1)))))
+```
+
+
+```
+
+The admission of FACTORIAL is trivial, using the relation O< (which
+is known to be well-founded on the domain recognized by O-P) and the
+measure (ACL2-COUNT N). We observe that the type of FACTORIAL is described
+by the theorem (AND (INTEGERP (FACTORIAL N)) (< 0 (FACTORIAL N))).
+We used the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER and primitive
+type reasoning.
+
+Summary
+Form: ( DEFUN FACTORIAL ...)
+Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
+ (:FAKE-RUNE-FOR-TYPE-SET NIL))
+Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
+ FACTORIAL
+```
+
+
+
+
+## comb-factorial 定理を証明する
+
+では、comb 関数と階乗の関係について証明してみましょう。 高校の数学 1A
+にて組み合わせの数について学んだ方は下記の公式について学んだ記憶がある
+かもしれません。
+
+```
+ n!
+--------
+(n-k)!k!
+```
+
+何故かについては「組み合せの数
+公式」とかで適当に[検索](https://duckduckgo.com/?q=%E7%B5%84%E3%81%BF%E5%90%88%E3%82%8F%E3%81%9B%E3%81%AE%E6%95%B0+%E5%85%AC%E5%BC%8F)してください(やる気なし)。
+ということで上記の式を ACL2 に翻訳してみましょう。分母が 0 になったり結果が分数になにならないように調節しています。
+
+
+
+``` acl2
+(defthm comb-factorial
+ (implies (and (natp n))
+ (equal (comb n k)
+ (cond
+ ((zp k) 1)
+ ((or (zp n) (< n k)) 0)
+ (t (/ (factorial n)
+ (* (factorial (- n k))
+ (factorial k))))))))
+```
+
+
+```
+
+ACL2 Warning [Subsume] in ( DEFTHM COMB-FACTORIAL ...): A newly proposed
+:REWRITE rule generated from COMB-FACTORIAL probably subsumes the previously
+added :REWRITE rule COMB-ZERO, in the sense that the new rule will
+now probably be applied whenever the old rule would have been.
+
+Goal'
+Subgoal 4
+Subgoal 3
+Subgoal 2
+Subgoal 2'
+
+([ A key checkpoint:
+
+Subgoal 2'
+(IMPLIES (AND (<= 0 N)
+ (NOT (ZP K))
+ (NOT (ZP N))
+ (<= K N))
+ (EQUAL (COMB N K)
+ (* (FACTORIAL N)
+ (/ (* (FACTORIAL K)
+ (FACTORIAL (+ (- K) N)))))))
+
+*1 (Subgoal 2') is pushed for proof by induction.
+
+])
+Subgoal 1
+
+Perhaps we can prove *1 by induction. Three induction schemes are
+suggested by this conjecture. Subsumption reduces that number to one.
+
+We will induct according to a scheme suggested by (COMB N K). This
+suggestion was produced using the :induction rules COMB and FACTORIAL.
+If we let (:P K N) denote *1 above then the induction scheme we'll
+use is
+(AND (IMPLIES (AND (NOT (ZP K))
+ (NOT (ZP N))
+ (:P K (+ -1 N))
+ (:P (+ -1 K) (+ -1 N)))
+ (:P K N))
+ (IMPLIES (AND (NOT (ZP K)) (ZP N))
+ (:P K N))
+ (IMPLIES (ZP K) (:P K N))).
+This induction is justified by the same argument used to admit COMB.
+Note, however, that the unmeasured variable K is being instantiated.
+When applied to the goal at hand the above induction scheme produces
+eight nontautological subgoals.
+Subgoal *1/8
+Subgoal *1/8'
+Subgoal *1/8''
+
+Splitter note (see :DOC splitter) for Subgoal *1/8'' (2 subgoals).
+ if-intro: ((:DEFINITION FACTORIAL)
+ (:DEFINITION NOT)
+ (:REWRITE ZP-OPEN))
+
+Subgoal *1/8.2
+Subgoal *1/8.2'
+Subgoal *1/8.2''
+Subgoal *1/8.2'''
+Subgoal *1/8.2'4'
+Subgoal *1/8.2'5'
+Subgoal *1/8.2'6'
+Subgoal *1/8.2'7'
+Subgoal *1/8.2'8'
+Subgoal *1/8.2'9'
+Subgoal *1/8.2'10'
+Subgoal *1/8.2'11'
+Subgoal *1/8.2'12'
+Subgoal *1/8.2'13'
+Subgoal *1/8.2'14'
+Subgoal *1/8.2'15'
+Subgoal *1/8.2'16'
+Subgoal *1/8.2'17'
+
+([ A key checkpoint while proving *1 (descended from Subgoal 2'):
+
+Subgoal *1/8.2'
+(IMPLIES (AND (NOT (ZP K))
+ (NOT (ZP N))
+ (EQUAL (COMB (+ -1 N) K)
+ (* (FACTORIAL (+ -1 N))
+ (/ (* K (FACTORIAL (+ -1 K))
+ (FACTORIAL (+ -1 (- K) N))))))
+ (< 0 (+ (- K) N))
+ (EQUAL (COMB (+ -1 N) (+ -1 K))
+ (* (FACTORIAL (+ -1 N))
+ (/ (* (FACTORIAL (+ -1 K))
+ (+ (- K) N)
+ (FACTORIAL (+ -1 (- K) N))))))
+ (<= 0 N)
+ (<= K N))
+ (EQUAL (+ (COMB (+ -1 N) K)
+ (COMB (+ -1 N) (+ -1 K)))
+ (* N (FACTORIAL (+ -1 N))
+ (/ (* K (FACTORIAL (+ -1 K))
+ (+ (- K) N)
+ (FACTORIAL (+ -1 (- K) N)))))))
+
+*1.1 (Subgoal *1/8.2'17') is pushed for proof by induction.
+
+])
+Subgoal *1/8.1
+Subgoal *1/8.1'
+Subgoal *1/7
+Subgoal *1/7'
+Subgoal *1/7''
+Subgoal *1/6
+Subgoal *1/5
+Subgoal *1/4
+Subgoal *1/4'
+Subgoal *1/4''
+Subgoal *1/4'''
+Subgoal *1/4'4'
+Subgoal *1/4'5'
+Subgoal *1/4'6'
+Subgoal *1/4'7'
+Subgoal *1/4'8'
+
+([ A key checkpoint while proving *1 (descended from Subgoal 2'):
+
+Subgoal *1/4'5'
+(IMPLIES (AND (NOT (ZP N))
+ (< 0 (+ -1 N))
+ (EQUAL (+ 1 (COMB (+ -2 N) 1))
+ (* (/ (FACTORIAL (+ -2 N)))
+ (+ -1 N)
+ (FACTORIAL (+ -2 N))))
+ (<= 0 N)
+ (<= 1 N))
+ (EQUAL (+ 2 (COMB (+ -2 N) 1)) N))
+
+*1.2 (Subgoal *1/4'8') is pushed for proof by induction.
+
+])
+Subgoal *1/3
+Subgoal *1/3'
+Subgoal *1/2
+Subgoal *1/2'
+Subgoal *1/1
+
+So we now return to *1.2, which is
+
+(IMPLIES (AND (INTEGERP K)
+ (<= 0 K)
+ (INTEGERP I)
+ (< 0 I)
+ (INTEGERP J)
+ (NOT (ZP N))
+ (EQUAL (+ 1 K)
+ (* (/ (FACTORIAL J)) I (FACTORIAL J)))
+ (<= 0 N)
+ (<= 1 N))
+ (EQUAL (+ 2 K) N)).
+Subgoal *1.2/3
+Subgoal *1.2/3'
+Subgoal *1.2/3''
+Subgoal *1.2/3'''
+Subgoal *1.2/3'4'
+Subgoal *1.2/3'5'
+Subgoal *1.2/3'6'
+
+*1.2.1 (Subgoal *1.2/3'6') is pushed for proof by induction.
+Subgoal *1.2/2
+Subgoal *1.2/1
+Subgoal *1.2/1'
+Subgoal *1.2/1''
+Subgoal *1.2/1'''
+Subgoal *1.2/1'4'
+
+*1.2.2 (Subgoal *1.2/1'4') is pushed for proof by induction.
+
+So we now return to *1.2.2, which is
+
+(IMPLIES (AND (ZP J)
+ (INTEGERP K)
+ (<= 0 K)
+ (INTEGERP J)
+ (NOT (ZP N))
+ (<= 0 N)
+ (<= 1 N))
+ (EQUAL (+ 2 K) N)).
+
+No induction schemes are suggested by *1.2.2. Consequently, the proof
+attempt has failed.
+
+Summary
+Form: ( DEFTHM COMB-FACTORIAL ...)
+Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
+ (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
+ (:DEFINITION COMB)
+ (:DEFINITION FACTORIAL)
+ (:DEFINITION FIX)
+ (:DEFINITION NATP)
+ (:DEFINITION NOT)
+ (:DEFINITION SYNP)
+ (:EXECUTABLE-COUNTERPART <)
+ (:EXECUTABLE-COUNTERPART BINARY-*)
+ (:EXECUTABLE-COUNTERPART BINARY-+)
+ (:EXECUTABLE-COUNTERPART COMB)
+ (:EXECUTABLE-COUNTERPART EQUAL)
+ (:EXECUTABLE-COUNTERPART FACTORIAL)
+ (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
+ (:EXECUTABLE-COUNTERPART UNARY--)
+ (:EXECUTABLE-COUNTERPART UNARY-/)
+ (:EXECUTABLE-COUNTERPART ZP)
+ (:FAKE-RUNE-FOR-LINEAR NIL)
+ (:FAKE-RUNE-FOR-TYPE-SET NIL)
+ (:INDUCTION COMB)
+ (:INDUCTION FACTORIAL)
+ (:REWRITE ASSOCIATIVITY-OF-*)
+ (:REWRITE ASSOCIATIVITY-OF-+)
+ (:REWRITE COMB-ZERO)
+ (:REWRITE COMMUTATIVITY-2-OF-+)
+ (:REWRITE COMMUTATIVITY-OF-*)
+ (:REWRITE COMMUTATIVITY-OF-+)
+ (:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+)
+ (:REWRITE FOLD-CONSTS-IN-+)
+ (:REWRITE INVERSE-OF-*)
+ (:REWRITE INVERSE-OF-+)
+ (:REWRITE UNICITY-OF-0)
+ (:REWRITE UNICITY-OF-1)
+ (:REWRITE ZP-OPEN)
+ (:TYPE-PRESCRIPTION COMB)
+ (:TYPE-PRESCRIPTION FACTORIAL))
+Splitter rules (see :DOC splitter):
+ if-intro: ((:DEFINITION FACTORIAL)
+ (:DEFINITION NOT)
+ (:REWRITE ZP-OPEN))
+Warnings: Subsume
+Time: 0.15 seconds (prove: 0.13, print: 0.01, other: 0.00)
+Prover steps counted: 15441
+
+---
+The key checkpoint goals, below, may help you to debug this failure.
+See :DOC failure and see :DOC set-checkpoint-summary-limit.
+---
+
+*** Key checkpoint at the top level: ***
+
+Subgoal 2'
+(IMPLIES (AND (<= 0 N)
+ (NOT (ZP K))
+ (NOT (ZP N))
+ (<= K N))
+ (EQUAL (COMB N K)
+ (* (FACTORIAL N)
+ (/ (* (FACTORIAL K)
+ (FACTORIAL (+ (- K) N)))))))
+
+*** Key checkpoints under a top-level induction: ***
+
+Subgoal *1/8.2'
+(IMPLIES (AND (NOT (ZP K))
+ (NOT (ZP N))
+ (EQUAL (COMB (+ -1 N) K)
+ (* (FACTORIAL (+ -1 N))
+ (/ (* K (FACTORIAL (+ -1 K))
+ (FACTORIAL (+ -1 (- K) N))))))
+ (< 0 (+ (- K) N))
+ (EQUAL (COMB (+ -1 N) (+ -1 K))
+ (* (FACTORIAL (+ -1 N))
+ (/ (* (FACTORIAL (+ -1 K))
+ (+ (- K) N)
+ (FACTORIAL (+ -1 (- K) N))))))
+ (<= 0 N)
+ (<= K N))
+ (EQUAL (+ (COMB (+ -1 N) K)
+ (COMB (+ -1 N) (+ -1 K)))
+ (* N (FACTORIAL (+ -1 N))
+ (/ (* K (FACTORIAL (+ -1 K))
+ (+ (- K) N)
+ (FACTORIAL (+ -1 (- K) N)))))))
+
+Subgoal *1/4'5'
+(IMPLIES (AND (NOT (ZP N))
+ (< 0 (+ -1 N))
+ (EQUAL (+ 1 (COMB (+ -2 N) 1))
+ (* (/ (FACTORIAL (+ -2 N)))
+ (+ -1 N)
+ (FACTORIAL (+ -2 N))))
+ (<= 0 N)
+ (<= 1 N))
+ (EQUAL (+ 2 (COMB (+ -2 N) 1)) N))
+
+ACL2 Error in ( DEFTHM COMB-FACTORIAL ...): See :DOC failure.
+
+******** FAILED ********
+```
+
+
+
+
+なんと、ACL2 による自動証明は失敗してしまいました。 Key checkpoints の `Subgoal *1/8.2'`
+のところをみてみましょう。`implies` の第一引数は仮定で第二引数は帰結なのですが、仮定のところに
+`(EQUAL (COMB (+ -1 N) K) ...)` という式と `(EQUAL (COMB (+ -1 N) (+ -1 K))
+...)` という式があって、帰結の部分に `(COMB (+ -1 N) K)` と `(COMB (+ -1 N) (+ -1 K))`
+があることに注目してください。 上記の仮定の式を使って帰結の式を置き換えると下記のように FACTORIAL
+関数のみを使った式が出てきます(仮定は省略)。
+
+ (EQUAL (+ (* (FACTORIAL (+ -1 N))
+ (/ (* K (FACTORIAL (+ -1 K))
+ (FACTORIAL (+ -1 (- K) N)))))
+ (* (FACTORIAL (+ -1 N))
+ (/ (* (FACTORIAL (+ -1 K))
+ (+ (- K) N)
+ (FACTORIAL (+ -1 (- K) N))))))
+ (* N (FACTORIAL (+ -1 N))
+ (/ (* K (FACTORIAL (+ -1 K))
+ (+ (- K) N)
+ (FACTORIAL (+ -1 (- K) N))))))
+
+これが真であることを示せばいいので、ACL2
+で証明するのは不可能ではなさそうな気がしますね(実際、手計算で等しいことを確認しました)。ただ、標準の
+ACL2 でこういう四則演算をたくさん含んだ式について証明するのはあまり簡単ではありません。 ACL2
+ではよく使われる定理ライブラリも一緒に配布されていて、その中に算術に関する証明をするのに大変便利な
+`arithmetic` という定理ライブラリが入っています。今回はこれを使います。
+
+
+
+``` acl2
+(include-book "arithmetic/top" :dir :system)
+```
+
+
+```
+
+Summary
+Form: ( INCLUDE-BOOK "arithmetic/top" ...)
+Rules: NIL
+Time: 0.43 seconds (prove: 0.00, print: 0.00, other: 0.43)
+ "/gnu/store/cj54gk0b9qqxfh0pz8mrh7j8iwrbz4p4-acl2-8.4/lib/acl2/books/arithmetic/top.lisp"
+```
+
+
+
+
+もう一度 `comb-factorial` の証明を試みます。
+
+
+
+``` acl2
+(defthm comb-factorial
+ (implies (and (natp n)
+ (natp k))
+ (equal (comb n k)
+ (if (< n k)
+ 0
+ (/ (factorial n)
+ (* (factorial (- n k))
+ (factorial k)))))))
+```
+
+
+```
+
+ACL2 Warning [Subsume] in ( DEFTHM COMB-FACTORIAL ...): A newly proposed
+:REWRITE rule generated from COMB-FACTORIAL probably subsumes the previously
+added :REWRITE rule COMB-ZERO, in the sense that the new rule will
+now probably be applied whenever the old rule would have been.
+
+Goal'
+Subgoal 2
+Subgoal 1
+Subgoal 1'
+
+([ A key checkpoint:
+
+Subgoal 1'
+(IMPLIES (AND (NATP N) (NATP K) (<= K N))
+ (EQUAL (FACTORIAL N)
+ (* (FACTORIAL K)
+ (COMB N K)
+ (FACTORIAL (+ (- K) N)))))
+
+*1 (Subgoal 1') is pushed for proof by induction.
+
+])
+
+Perhaps we can prove *1 by induction. Three induction schemes are
+suggested by this conjecture. Subsumption reduces that number to one.
+
+We will induct according to a scheme suggested by (COMB N K). This
+suggestion was produced using the :induction rules COMB and FACTORIAL.
+If we let (:P K N) denote *1 above then the induction scheme we'll
+use is
+(AND (IMPLIES (AND (NOT (ZP K))
+ (NOT (ZP N))
+ (:P K (+ -1 N))
+ (:P (+ -1 K) (+ -1 N)))
+ (:P K N))
+ (IMPLIES (AND (NOT (ZP K)) (ZP N))
+ (:P K N))
+ (IMPLIES (ZP K) (:P K N))).
+This induction is justified by the same argument used to admit COMB.
+Note, however, that the unmeasured variable K is being instantiated.
+When applied to the goal at hand the above induction scheme produces
+nine nontautological subgoals.
+Subgoal *1/9
+Subgoal *1/9'
+Subgoal *1/9''
+
+Splitter note (see :DOC splitter) for Subgoal *1/9'' (2 subgoals).
+ if-intro: ((:DEFINITION FACTORIAL)
+ (:DEFINITION NOT)
+ (:REWRITE ZP-OPEN))
+
+Subgoal *1/9.2
+Subgoal *1/9.2'
+Subgoal *1/9.1
+Subgoal *1/9.1'
+Subgoal *1/8
+Subgoal *1/8'
+Subgoal *1/8''
+Subgoal *1/7
+Subgoal *1/6
+Subgoal *1/5
+Subgoal *1/4
+Subgoal *1/3
+Subgoal *1/2
+Subgoal *1/1
+Subgoal *1/1'
+Subgoal *1/1''
+
+*1 is COMPLETED!
+Thus key checkpoint Subgoal 1' is COMPLETED!
+
+Q.E.D.
+
+Summary
+Form: ( DEFTHM COMB-FACTORIAL ...)
+Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
+ (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
+ (:DEFINITION COMB)
+ (:DEFINITION FACTORIAL)
+ (:DEFINITION FIX)
+ (:DEFINITION NOT)
+ (:DEFINITION SYNP)
+ (:EXECUTABLE-COUNTERPART BINARY-*)
+ (:EXECUTABLE-COUNTERPART BINARY-+)
+ (:EXECUTABLE-COUNTERPART FACTORIAL)
+ (:EXECUTABLE-COUNTERPART NATP)
+ (:EXECUTABLE-COUNTERPART NOT)
+ (:EXECUTABLE-COUNTERPART TAU-SYSTEM)
+ (:EXECUTABLE-COUNTERPART UNARY--)
+ (:EXECUTABLE-COUNTERPART ZP)
+ (:FAKE-RUNE-FOR-LINEAR NIL)
+ (:FAKE-RUNE-FOR-TYPE-SET NIL)
+ (:FORWARD-CHAINING NATP-FC-1)
+ (:INDUCTION COMB)
+ (:INDUCTION FACTORIAL)
+ (:REWRITE <-0-+-NEGATIVE-1)
+ (:REWRITE ASSOCIATIVITY-OF-*)
+ (:REWRITE ASSOCIATIVITY-OF-+)
+ (:REWRITE COMB-ZERO)
+ (:REWRITE COMMUTATIVITY-2-OF-*)
+ (:REWRITE COMMUTATIVITY-2-OF-+)
+ (:REWRITE COMMUTATIVITY-OF-*)
+ (:REWRITE COMMUTATIVITY-OF-+)
+ (:REWRITE DISTRIBUTIVITY)
+ (:REWRITE DISTRIBUTIVITY-OF-/-OVER-*)
+ (:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+)
+ (:REWRITE EQUAL-*-/-1)
+ (:REWRITE EQUAL-*-/-2)
+ (:REWRITE EQUAL-*-X-Y-X)
+ (:REWRITE FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-RIGHT)
+ (:REWRITE INVERSE-OF-+)
+ (:REWRITE MINUS-CANCELLATION-ON-LEFT)
+ (:REWRITE TIMES-ZERO)
+ (:REWRITE UNICITY-OF-0)
+ (:REWRITE UNICITY-OF-1)
+ (:REWRITE ZP-OPEN)
+ (:TYPE-PRESCRIPTION COMB)
+ (:TYPE-PRESCRIPTION FACTORIAL)
+ (:TYPE-PRESCRIPTION |x < y => 0 < -x+y|))
+Splitter rules (see :DOC splitter):
+ if-intro: ((:DEFINITION FACTORIAL)
+ (:DEFINITION NOT)
+ (:REWRITE ZP-OPEN))
+Warnings: Subsume
+Time: 0.06 seconds (prove: 0.06, print: 0.01, other: 0.00)
+Prover steps counted: 4875
+ COMB-FACTORIAL
+```
+
+
+
+
+証明に成功しました。定理ライブラリの力は凄いですね。
+
+
+
+## おわりに
+
+[前回](https://www.tojo.tokyo/len-combinations.html)作成した組み合わせの数を求める関数とその階乗表現が等しいことを証明できました。
+本当は `comb-factorial` の証明に失敗したときの出力を見てから補助定理 `comb-zero`
+を作成する流れにしたかったのですが、証明の失敗時に出力されていた Key
+Checkpoints をいくら眺めてもなぜ `comb-zero` が必要なのかを説明するのが難しかったので、ちょっと無理矢理ですが先に
+`comb-zero` を証明しておく流れにしました。
+
+Key Checkpoints
+を読んで必要な補助定理を作成する例としては今回のはちょっと難しすぎたので、また別の機会に簡単な例を出せたらいいなと考えています。
+
+ただ、ACL2 に関心のある方は私の記事を読むよりかは [ACL2
+のチュートリアル](https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____ACL2-TUTORIAL)
+を参照したり、『定理証明手習い』(ラムダノート社) を読んで勉強するのがおすすめです。『定理証明手習い』(ラムダノート社) では ACL2
+の使い方について学ぶことはできないのですが、 ACL2 を使うのに必要な前提知識について学べるのでおすすめです。
+
diff --git a/posts/contact.md b/posts/contact.md
index d465da6..71bf0ef 100644
--- a/posts/contact.md
+++ b/posts/contact.md
@@ -1,59 +1,33 @@
title: 連絡先
id: contact
date: 2020-02-19 00:00
-updated: 2020-05-08 07:55
-description: 問い合わせページ
+updated: 2021-09-11 12:00
+description: tojo.tokyo に問い合わせをしたいときに見てください
---
-## メールによる連絡
-
-<masaya@tojo.tokyo> にメールを送ってください。
-現状、インターネットを使用した連絡手段としては最も優れた方法であると考えています。
-
-### 秘密のメッセージを送信したい場合
-
-他の人に見られたくないメッセージを送りたい場合は 下記の公開鍵を使用して暗号化して送信してください。
-(更新し忘れそうなので、もしも有効期限が切れていたら教えてください……)
-
- -----BEGIN PGP PUBLIC KEY BLOCK-----
-
- mQENBF5aSDEBCACc0PNeutt4CtkrSeno2xxk8RArchxUNtvZT50f/Zy+ocAXpBWZ
- /P0FWqDjquYCrXf25QS3FJ6fZMcxFfsnO5DlL8v0L1bWf8QQyF25q0lwy1DO0bdx
- To2BOzv9cN/eAiRjN0BM/Rqh29HxeiFCFGgOlrFllsRMzAv5melB1WJMml0LktSD
- aGZFUrmo/mAnGNxnD5w0cAJBU4DHLds9pdRHZTQE4hBoXhcFDu6uo8Lz/lotUaNj
- Kjwq2adEvZR1Ds8OaFDuyl5hIK2wTXSzN/1HvVGrDrsQ7JZclJvdHXytpoybXhji
- AwARdyhToMATzcLdV4lo/8/u+zU+KmjR5RU7ABEBAAG0H01hc2F5YSBUb2pvIDxt
- YXNheWFAdG9qby50b2t5bz6JAVQEEwEIAD4CGwMFCwkIBwIGFQoJCAsCBBYCAwEC
- HgECF4AWIQTHasfHf/RvbkLC2TVFqkJkcjdWHgUCXrSPIAUJBByt7wAKCRBFqkJk
- cjdWHqMRB/9+4xcsSCR0DOq61T64OP/RGB4tMsqPbMFllKIhICAvhOIerAoIQsQX
- J0u0Uj2yH04LJA4Thnu1XbNs71dZKDKCynJZfenlyk5Z/fZRKmgGT8qP7Q+5n16G
- aM75UPAoPzDxuwsst95BlXFFzcMYLkmGB8hxztRLVSfnSM2OPcoM6BBlhIgeujW1
- PVtohgZg5zdYLDRpVQw38Kr1r4KVX1DOZJJxjBx4O4xWy9/sj0LE7N+2qhq//mn8
- 1iaFuJIB/IkjBme4H2rCIh/Tn6RzXoGC63mRM6eyPVdXqnEPbPnqfjPPz4tRhC9E
- 0yx6iApysBAjEP/EolHZZBJJsjEldyAHuQENBF5aSDEBCAC1mwoJO/fMRqL6Ay5i
- mCQOZ65KC82beG7S2yJySEdBPsVaAmyCNtgKmTneb4F4xyhh2hoJkp5t/DvEcWIK
- p6+YcurbcTFaa/Jd77CO3T9tFx58reVPJrZkRbDMOSvqbnh67c6vG+A6Tu+Gikep
- NojIKqpg0A6L7kaRDxuyes4OkB2RPJ1IkIh6PUI1d3KHtty+QyMxUDgoz55tbo/O
- ZaFpncoPFNHeRs4yAXEVoLWHwPbWxOXl8uZGTj+198tDJ0ogxH5jz2lzZbO1vYam
- Y0t+3hjHe918vA0Vfs1rVjTyP1xcY/QiGcbf/ebTesxliuSVXaMr5U0ezokwjzzl
- 0rSVABEBAAGJATwEGAEIACYCGwwWIQTHasfHf/RvbkLC2TVFqkJkcjdWHgUCXrSP
- QQUJBByuEAAKCRBFqkJkcjdWHtuCCACCLJKcYObemhsYUPr/kx8TJhZaze5qP/Ee
- U5sJ1GcmUZhzuhtl9DT7UBWXoYMhELAqJgAmdV8G5ClCblee4Bf1lpKXvbOfb8U2
- NT6Z9akthcNRFVzZquUHDemf9Kla9M9WzfXiJvm8mT5Lx7mt4FjKINXMw+/xPcYN
- kA5fmrtYWcRJdnl95L/1XnxPndZUkddWBnzJFB1TD0PzCNbMTiZ2+VfslwamOgKR
- ARu/Do7FriLk0zUBfteB1JSr1Ef/yvoAl06L44p/wB4yExvVCGxXnaGK1HL6YKYa
- McpBRBbyU4/V4hQAVBmedeZU5obcgFas3uwgNILEbl2gIMmEq5wF
- =XnQ2
- -----END PGP PUBLIC KEY BLOCK-----
-
-公開鍵は [鍵サーバー](http://keys.gnupg.net/) にも登録されています。
-
-## SNS による連絡
-
-### Mastodon (おすすめ\!)
-
-[TojoQK](https://mastodon.tojo.tokyo/@tojoqk) へのメンションか、DM で連絡してください。
-
-### Twitter
-
-[TojoQK](https://twitter.com/tojoqk) への replay か DM で連絡することができます。
+## メール
+
+ - <masaya@tojo.tokyo> にメールを送ってください
+ - 必要であれば下記の GPG 鍵を使って暗号化して送信してください
+
+### GnuPG の鍵
+
+下記のコマンドで私の公開鍵を gpg に import できます。
+
+ gpg --keyserver=hkps://keyserver.ubuntu.com --recv-keys C76AC7C77FF46F6E42C2D93545AA42647237561E
+
+インポートしたら必ずフィンガープリントが下記と一致することを確認してください。
+
+`C76A C7C7 7FF4 6F6E 42C2 D935 45AA 4264 7237 561E`
+
+## Mastodon (or 他の Activity Pub 実装)
+
+ - [tojoqk@mastodon.tojo.tokyo](https://mastodon.tojo.tokyo/@tojoqk)
+ ユーザーにメンションもしくは DM してください
+
+## Twitter
+
+ - メールが届かない、もしくは返信がない場合に利用してください
+ - [tojoqk](https://twitter.com/tojoqk) ユーザーに DM してください
+ - 通知を有効にしていないため気づくのに時間がかかる可能性があります
+
diff --git a/posts/git-tojo-tokyo.md b/posts/git-tojo-tokyo.md
index 224e061..faf08d4 100644
--- a/posts/git-tojo-tokyo.md
+++ b/posts/git-tojo-tokyo.md
@@ -155,4 +155,4 @@ https でサーバーにアクセスしているのにバックエンドでは h
私生活で依存する外部サービスを一つ減らすことができたという意味でも嬉しい。このサイトにはそれぞれの記事の下の方にある「このページのソースコード」というリンクから記事のソースコードを参照したり、更新された記事については記事タイトルのあたりに「更新履歴」のリンクが表示され git の変更履歴を表示する機能がある。いままではこの機能の実現のために GitLab.com 上の画面に遷移するようにしていたが、今は [https://git.tojo.tokyo](https://git.tojo.tokyo) に遷移するように変更されている。
-GNU Guix System を使えば簡単に git サーバーを構築できるので、みなさんも構築してみてはいかがだろうか。
+[GNU Guix System](https://guix.gnu.org/) を使えば簡単に git サーバーを構築できるので、みなさんも構築してみてはいかがだろうか。
diff --git a/posts/guile-df.md b/posts/guile-df.md
new file mode 100644
index 0000000..391ef35
--- /dev/null
+++ b/posts/guile-df.md
@@ -0,0 +1,264 @@
+title: Guile で df コマンドの出力からディスク使用率を確認してみた
+id: guile-df
+date: 2021-09-12 00:15
+description: Guile で Unix のコマンドの出力を一行づつ読んで処理する具体的な例を紹介します
+---
+
+## はじめに
+
+[Guix System](https://guix.gnu.org/) で動かしているサーバーのディスク容量を監視するために
+[Guile](https://www.gnu.org/software/guile/) で `df`
+コマンドの出力を読んでディスク容量を確認する手続きを
+Guile で作成したので紹介します。本記事によって Guile
+でコマンドの出力を一行づつ読んで処理するときのイメージが掴めると思います。なお、本プログラムは異常時の処理を書いていない雑なものなので参考にする場合は注意をお願いいたします。
+
+
+
+## 本文中のプログラムのライセンス
+
+本記事で例示するプログラムのライセンスは GPLv3 (or later) です。ライセンスの詳細は
+[monitoring](https://git.tojo.tokyo/monitoring.git/) リポジトリの
+[COPYING](https://git.tojo.tokyo/monitoring.git/tree/COPYING) ファイルと
+[`tojo-tokyo/monitoring.scm`](https://git.tojo.tokyo/monitoring.git/tree/tojo-tokyo/monitoring.scm?id=9dadbd397af96b53b14050e741618657f6d7bf33)
+ファイルのヘッダの部分を参照してください。
+
+
+
+## パイプを開いて df の出力を読む
+
+まずは Guile から `df` コマンドを呼び出してみましょう パイプを開くために
+[`open-input-pipe`](https://www.gnu.org/software/guile/manual/html_node/Pipes.html)
+手続きを使います。 `open-input-pipe` には `(ice-9 popen)` モジュールが必要で、ポートから文字を読み込むのに
+[`(ice-9
+textual-ports)`](https://www.gnu.org/software/guile/manual/html_node/Textual-I_002fO.html)
+モジュールの手続きを利用しています。
+
+
+
+``` scheme
+(use-modules (ice-9 popen)
+ (ice-9 textual-ports))
+
+(let ((port (open-input-pipe "df")))
+ (display (get-string-all port))
+ (close-pipe port))
+```
+
+
+ Filesystem 1K-blocks Used Available Use% Mounted on
+ none 492120 0 492120 0% /dev
+ /dev/vda3 24377696 10096084 13020252 44% /
+ tmpfs 501932 0 501932 0% /dev/shm
+ 0
+
+
+
+
+ヘッダ行が先頭に一つありそれより下の行に1個以上の空白で区切られた値として必要な情報が出力されるようです。ヘッダ行は無視することにしてそれ以下を
+Guile の連想リストのリストにできればよさそうです。
+
+
+
+## 文字列を空白で区切る手続きを作る
+
+1個以上の空白で区切られた文字列をリストにする手続きを Guile を軽く探したのですが見つけられなかったので自分で作ります。正規表現を扱う
+[`(ice-9
+regex)`](https://www.gnu.org/software/guile/manual/html_node/Regexp-Functions.html)
+を使って下記のように実装します。
+
+
+
+``` scheme
+(use-modules (ice-9 regex))
+
+(define (split-with-spaces x)
+ (map match:substring (list-matches "[^ ]+" x)))
+
+(split-with-spaces " hello world ")
+```
+
+
+ ("hello" "world")
+
+
+
+
+空白以外の文字が一個以上連続したものを集めることで空白で区切られた文字列のリストを作っています。
+
+
+
+## df 手続きを実装する
+
+これから作成する `df` は無引数で呼びだして、`df` コマンドの出力のそれぞれの行を連想リストに変換したものを返す手続きです。
+
+今回は `split-with-spaces` を使用して下記のように実装しました。
+なお、本記事の目的はコマンドの出力をパイプで一行づつ処理をするという
+Unix でよくある処理を Guile でやる方法を例示することなので意図的に手続き的に書いています。
+
+
+
+``` scheme
+(define (df)
+ (let ((port (open-input-pipe "df")))
+ (get-line port) ; ヘッダ行を読み飛ばす
+ (let loop ((line (get-line port))
+ (table '()))
+ (cond ((eof-object? line)
+ (close-pipe port)
+ table)
+ (else
+ (loop (get-line port)
+ (cons (map cons
+ '(filesystem 1k-blocks used available use% mounted-on)
+ (split-with-spaces line))
+ table)))))))
+```
+
+
+
+`df`
+コマンドの出力を一行ずつ読んで連想リストを作成していき、最後まで読みきったらパイプをクローズした後に構築した連想リストのリストを返却します。
+
+`df`
+手続きの結果を整形して出力してみましょう([`format`](https://www.gnu.org/software/guile/manual/html_node/Formatted-Output.html)
+手続きのために `(ice-9 format)`,
+[`match-lambda`](https://www.gnu.org/software/guile/manual/html_node/Pattern-Matching.html)
+のために `(ice-9 match)` モジュールを使っています)。
+
+
+
+``` scheme
+(use-modules (ice-9 match)
+ (ice-9 format))
+
+(for-each (lambda (record)
+ (for-each (match-lambda
+ ((key . val)
+ (format #t "~a: ~a~%"
+ (symbol->string key)
+ val)))
+ record)
+ (newline))
+ (df))
+```
+
+
+```
+filesystem: tmpfs
+1k-blocks: 501932
+used: 0
+available: 501932
+use%: 0%
+mounted-on: /dev/shm
+
+filesystem: /dev/vda3
+1k-blocks: 24377696
+used: 10096084
+available: 13020252
+use%: 44%
+mounted-on: /
+
+filesystem: none
+1k-blocks: 492120
+used: 0
+available: 492120
+use%: 0%
+mounted-on: /dev
+
+```
+
+
+
+
+意図したとおりに実装できているようです。
+
+
+
+## ディスク使用率がしきい値を超えているかを調べる
+
+
+
+`df` 手続きを使ってしきい値以上のディスク使用率になっているファイルシステムがあったら真を返す、`disk-use%-over?`
+手続きを作ってみましょう。
+
+私は `/dev/` から始まっているファイルシステムにしか興味ないので、`/dev/` から始まっている文字列かどうかを判定する述語
+`prefix-/dev/?` を作成します。
+
+
+
+``` scheme
+(define (prefix-/dev/? x)
+ (and (string? x)
+ (<= 5 (string-length x))
+ (string=? (substring x 0 5) "/dev/")))
+
+(map prefix-/dev/? '("/tmp/shm" "/dev/hello" "/neko/dev"))
+```
+
+
+ (#f #t #f)
+
+
+
+
+`use%` は `%` を含んだ文字列になってしまっていて数値比較をするには扱いにくい状態です。`x%`
+のような形になっている文字列を数字に変換する手続きを作成します。
+
+
+
+``` scheme
+(define (use%->number x)
+ (string->number (string-delete #\% x)))
+
+(use%->number "42%")
+```
+
+
+```
+42
+```
+
+
+
+
+それでは `prefix-/dev/?`、`use%->number` を利用して `disk-use%-over?` を実装してみましょう
+(`(srfi srfi-26)` の [`cut`
+構文](https://www.gnu.org/software/guile/manual/html_node/SRFI_002d26.html)を使っています。`(cut
+f <> x)` は `(lambda (y) (f y x))` のように書くのと同じです)。
+
+
+
+``` scheme
+(use-modules (srfi srfi-26)
+ ((srfi srfi-1) #:select (any)))
+
+(define (disk-use%-over? threshold)
+ (any (cut < threshold <>)
+ (map (compose use%->number (cut assoc-ref <> 'use%))
+ (filter (compose prefix-/dev/? (cut assoc-ref <> 'filesystem))
+ (df)))))
+
+(map disk-use%-over? '(40 50))
+```
+
+
+ (#t #f)
+
+
+
+
+しきい値が `40` の場合は真を返し、`50` の場合は偽を返しました。`/dev/vda3` の現在のディスク使用率は `44%`
+なので意図した挙動をしているようです。
+
+
+
+## おわりに
+
+無事に Guile を使ってディスク使用率を調べる手続きを作成することができました。この Web サイトは Guix System
+で動いていて現在上記のプログラムを使って実際に監視を実施しています([該当するコード](https://git.tojo.tokyo/guix-config.git/tree/web/config.scm?id=1562b9827baa6a2c78592bd5f9115ed6a8b444b3#n33)、Guix
+System では
+[G-Expressions](https://guix.gnu.org/manual/en/html_node/G_002dExpressions.html)
+という仕組みを利用して定期実行ジョブを Guile で気軽に実装できます)。このように GNU Guile では Unix
+のコマンドと連携する実用的なプログラムを簡単に書くことができるのでみなさんも是非 GNU Guile
+を使ってみてください。
+
diff --git a/posts/guile-recursion.md b/posts/guile-recursion.md
new file mode 100644
index 0000000..e0863b8
--- /dev/null
+++ b/posts/guile-recursion.md
@@ -0,0 +1,392 @@
+title: Guile ではスタック溢れを気にせず再帰しよう
+id: guile-recursion
+date: 2021-09-12 21:00
+description: Guile ではスタックオーバーフローは起きないので末尾再帰にしなくてもいいという話
+---
+
+## はじめに
+
+関数型プログラミングを学んだ人の多くは、スタックオーバーフローを回避するために再帰関数を末尾再帰の形式に変換する方法について学んでいると思います。Guile
+では他のプログラミング言語とは事情が異なり再帰をしても[システムのメモリを使い尽すまではスタックオーバーフローが起きません](https://www.gnu.org/software/guile/docs/docs-3.0/guile-ref/Stack-Overflow.html)([Racket
+も同様](https://docs.racket-lang.org/guide/Lists__Iteration__and_Recursion.html))。なので、一部の例外を除いて
+Guile でプログラムを書くときは無理に末尾再帰に変形せずに分かりやすくて綺麗な再帰のままにしましょう。
+
+
+
+## 自然な再帰と末尾再帰の比較
+
+### リストの長さを計算する再帰的な手続き length
+
+例としてリスト `x` の長さ(要素の数)を計算する `length` 手続きを Guile で実装することを考えてみましょう。
+
+
+
+``` scheme
+(define (length x)
+ (if (null? x)
+ 0
+ (+ 1 (length (cdr x)))))
+```
+
+
+
+`length` の実行例:
+
+
+
+``` scheme
+(length '(a b c))
+```
+
+
+```
+3
+```
+
+
+
+
+### 再帰手続きの読み方
+
+`length` 手続きは下記のように読み下すことができます。
+
+`x` の長さ(`length`)とは:
+
+ - a. `x` が空リスト(`null?`)のときは `0`
+ - b. さもなくば、先頭以外(`cdr`)の長さ(`length`)に 1 を足したもの
+
+a のような自身 `length` を含まない場合のことを基底部、b のような自身を含む場合のことを帰納部と呼びます。
+再帰手続きの正しさは基底部と帰納部をそれぞれ読んで「ふむ、確かにそうだな」と思えるのであれば正しいので理解するのはとても簡単です。
+このような自然に読める再帰的な定義のことをここでは「自然な再帰」と呼ぶことにします。
+
+
+
+### 再帰手続きとスタックオーバーフロー
+
+Guile
+以外の多くのプログラミング言語ではこのような再帰手続きにはスタックオーバーフローのリスクがあります。どういうことかというと、手続き呼び出しをしたときに元に戻る場所を覚えておくためコールスタックを使用するのですが多くのプログラミング言語ではコールスタックに上限が設定されています。コールスタックの上限に到達した段階でそれ以上の計算が不能になり途中で計算が停止してしまうのです。そのため、今回の場合リスト
+`x` がコールスタックの上限よりも大きい場合には `(length x)` を求めることはできません。
+この問題を回避するためには末尾呼び出しの形式に変換する必要があります(ただし、末尾呼び出しの最適化が行なわれるプログラミング言語・処理系に限ります。そうでない場合は繰り返しを表現する構文を使って書き換える必要があります。構文上の違いのみでこれから議論する末尾再帰との比較には影響しないので末尾再帰の話を繰り返しに置き換えて読んでいただいても問題ありません)。
+
+
+
+### 末尾再帰版の length-tail
+
+ではスタックオーバーフローの回避のために末尾再帰呼び出しの形式に変換したリストの長さを求める手続き `length-tail`
+を見てみましょう。`len` という引数を追加していて、これには `0`
+を渡すことを想定しています(Scheme
+では手続きの中に手続きの定義がかけるので、`len`
+引数を隠蔽することも可能なのですが、分かりやすさのためにあえて `len` 引数を残しています)。
+
+
+
+``` scheme
+(define (length-tail x len)
+ (if (null? x)
+ len
+ (length-tail (cdr x) (+ len 1))))
+```
+
+
+
+`length-tail` の実行例:
+
+
+
+``` scheme
+(length-tail '(a b c) 0)
+```
+
+
+```
+3
+```
+
+
+
+
+### 末尾再帰の手続きは理解が難しい
+
+`length` では手続きの定義を読み下すだけで理解できましたが、`length-tail` は少し難しいです。なぜなら、`length`
+の場合は基底部と帰納部をそれぞれ確認して正しいと思うことができましたが、`length-tail` の基底部は `len`
+であり単独では理解不能です。帰納部も `(length-tail (cdr x) (+ len 1))`
+とあり正しいかどうかは `len` 変数の値によるということになります。
+
+`length-tail` を理解するには計算の流れ全体を見なければいけません。
+
+ - a. `len` の初期状態は `0`
+ - b. `x` を `(cdr x)` で置き換える度に `len` の値は `1` 増加する
+ - c. `x` が空リスト(`null?`) になったら、 `len` が初期の `x` の長さを表わしているため `len` を返却する
+ - c1. 初期の `x` が空リストになるには、初期の `x` の長さと同じ回数 b の計算を繰り返したときである
+ - c2. len の初期状態が 0 のため b を繰り返した回数が len の値となる
+ - c3. c1, c2 より `x` が空リストのとき len は初期の x の長さを表わしている
+
+とても考えることが多く難しいことを分かっていただけたでしょうか。`length-tail`
+という例が極めて簡単であったために難しいことを納得しにくいということはあるかもしれません。それでも、`length`
+は基底部と帰納部をそれぞれ読むだけでプログラムの正しさについて納得できたのに対し、`length-tail`
+を理解するにはプログラム全体の流れを追わないとよく分からないというのは大きな違いです。
+
+このような苦労をして `length-tail` を書くよりも `length` を書いた方が良いと思うでしょう。Guile
+ではスタックオーバーフローは起きないので問題ありません。 `length`
+の方を書きましょう。ただし、一点だけ注意があります。
+
+
+
+### 末尾再帰と効率について
+
+実は Guile を使う場合であっても `length` と `length-tail` 手続きの間には違いがあります。
+
+`length-tail`
+では末尾再帰の最適化により呼び出し時の続きの計算を記憶しておく必要がありません。つまり、コールスタックに新しく追加する必要がありません。それに対して
+`length` では呼び出した後に続く計算を覚えておく必要があるのでコールスタックを消費します。`length` では
+`length-tail` と違って残りの計算を記憶するために記憶領域を消費してしまうのです。Guile
+ではコールスタックを消費しきったらヒープ領域を使ってコールスタックを拡張するので、与えるリストが長い場合には
+`length-tail` よりも `length`
+の方がメモリを多く使用してしまう可能性があるのです。ただし、メモリを消費するといっても与えるリストと同じくらいしか使わないので大した問題ではないでしょう。よほどメモリの消費に気を使う必要のあるようなケースでしか問題にならないと考えて良いでしょう。
+
+また、非末尾再帰の方が末尾再帰のよりも常に効率が悪いということではありません。むしろ末尾再帰にしない方が効率が良い場合もあります。手続き `f`
+とリスト `x` を取り、それぞれの要素を `f` によって変換したリストを返す `map` 手続きについて考えてみましょう。
+
+
+
+``` scheme
+(define (map f x)
+ (if (null? x)
+ '()
+ (cons (f (car x))
+ (map f (cdr x)))))
+```
+
+
+
+`map` の実行例:
+
+
+
+``` scheme
+(map - '(1 2 3))
+```
+
+
+ (-1 -2 -3)
+
+
+
+
+末尾再帰版の `map-tail` を実装してみましょう。`result` 引数には空リストを渡す想定です。
+
+
+
+``` scheme
+(define (map-tail f x result)
+ (if (null? x)
+ (reverse result)
+ (map-tail f (cdr x) (cons (f (car x)) result))))
+```
+
+
+
+map-tail の実行例:
+
+
+
+``` scheme
+(map-tail - '(1 2 3) '())
+```
+
+
+ (-1 -2 -3)
+
+
+
+
+`map` と `map-tail` のメモリ効率の違いについて検討してみましょう。`map` の手続きは `map`
+の呼び出しをするたびにコールスタックを消費し、不足した場合にはコールスタックを拡張するため
+`x` が長い場合にはメモリを消費する場合があります。それに対して `map-tail` はどうでしょうか。`map-tail` では
+`result` 引数を `(cons (f (car x)) result)` によって置き換えています。よって `map-tail`
+でも再帰するたびにメモリを消費していきます。上記から `map` と `map-tail` で `map`
+がコールスタックを消費するから `map` の方がメモリを多く使うとは必ずしもいえません。
+さらに、`map-tail` では基底部で `reverse` を呼び出しています。これは `map-tail`
+と同じくらいの計算量とメモリを消費するため、`map-tail` の計算の方が時間がかかりそうです。
+
+試しに実行にかかる時間を計測して比較してみましょう。
+
+
+
+``` scheme
+(use-modules (ice-9 time))
+
+(define-syntax-rule (dotimes (var n) form ...)
+ (let ((end n))
+ (do ((var 0 (+ var 1)))
+ ((<= end var))
+ form ...)))
+
+(for-each
+ (lambda (n)
+ (define x (iota (expt 10 n)))
+ (for-each display (list (expt 10 n) " 個のリストの場合\n"))
+
+ (display "map(100回):\n")
+ (time (dotimes (i 100) (map - x)))
+
+ (display "map-tail(100回):\n")
+ (time (dotimes (i 100) (map-tail - x '())))
+
+ (newline))
+ (iota 3 3))
+```
+
+
+```
+1000 個のリストの場合
+map(100回):
+clock utime stime cutime cstime gctime
+ 0.04 0.03 0.01 0.00 0.00 0.01
+map-tail(100回):
+clock utime stime cutime cstime gctime
+ 0.05 0.05 0.00 0.00 0.00 0.01
+
+10000 個のリストの場合
+map(100回):
+clock utime stime cutime cstime gctime
+ 0.40 0.38 0.01 0.00 0.00 0.10
+map-tail(100回):
+clock utime stime cutime cstime gctime
+ 0.52 0.50 0.00 0.00 0.00 0.17
+
+100000 個のリストの場合
+map(100回):
+clock utime stime cutime cstime gctime
+ 3.76 3.45 0.22 0.00 0.00 0.49
+map-tail(100回):
+clock utime stime cutime cstime gctime
+ 4.48 4.36 0.01 0.00 0.00 0.95
+
+```
+
+
+
+
+予想通り `map-tail` の方が少し遅いという結果になりました(`map-tail` の実装に引数を破壊する版の `reverse!`
+を使った場合についても調べたところ、その場合は `map` とほぼ同じ計算時間になることを確認しています。計算時間が変わらないのであれば
+`map` の方が良いでしょう。また、[Guile のマニュアルの Stack Overflow
+の節](https://www.gnu.org/software/guile/manual/html_node/Stack-Overflow.html#Stack-Overflow)で
+`reverse!` を使うと継続安全(continuation-safe)が損なわれ、 `map-tail` の計算が終了した後に `f`
+の計算が再度実行された場合に正常に動作しなくなるという問題が指摘されています)。
+
+
+
+## 自然な再帰だと計算量が爆発してしまうケース
+
+ここまでの例では Guile
+でなら自然な再帰で良いと言える例だったのですが、何でもそうという訳ではありません。たまに自然な再帰だと計算量が爆発的に大きくなってしまう場合がありそういった場合には別のアルゴリズムに変更する必要があります。
+
+
+
+### リストを反転する手続き
+
+リストを反転する手続きを自然な再帰で実装してみましょう。特に効率などを考慮しなければ下記のように実装しようと思うかもしれません。
+
+
+
+``` scheme
+(define (reverse x)
+ (if (null? x)
+ '()
+ (append (reverse (cdr x)) (list (car x)))))
+```
+
+
+
+`reverse` の実行例:
+
+
+
+``` scheme
+(reverse '(a b c))
+```
+
+
+ (c b a)
+
+
+
+
+この手続きは自然でたしかに正しいことはコードを読めば理解できるでしょう。ただし、一つ落とし穴があります。Lisp
+のリストは先頭に要素を追加する場合は `O(1)`
+の計算量でできるのに対してリストの最後に要素を追加する場合は `O(n)`
+かかるのです。 この影響でリストが長くなると激的に遅くなります。
+
+
+
+``` scheme
+(time (reverse (iota 20000)))
+'done
+```
+
+
+ clock utime stime cutime cstime gctime
+ 7.30 7.10 0.01 0.00 0.00 1.46
+ done
+
+
+
+
+これに対してリストの先頭に追加する操作しか行なわない `reverse-tail` を試してみましょう。
+
+
+
+``` scheme
+(define (reverse-tail x result)
+ (if (null? x)
+ result
+ (reverse-tail (cdr x)
+ (cons (car x) result))))
+```
+
+
+
+`reverse-tail` の実行例
+
+
+
+``` scheme
+(reverse-tail '(a b c) '())
+```
+
+
+ (c b a)
+
+
+
+
+`reverse-tail` の実行時間の計測:
+
+
+
+``` scheme
+(time (reverse-tail (iota 50000) '()))
+'done
+```
+
+
+ clock utime stime cutime cstime gctime
+ 0.02 0.02 0.00 0.00 0.00 0.00
+ done
+
+
+
+
+リストが長い場合は `reverse` と比較すると `reverse-tail` の方が圧倒的に早いのです。
+
+このように自然な再帰では計算に時間がかかり過ぎてしまう場合もあります。これは末尾再帰かどうかという話ではなくて、アルゴリズムが異なるために生じている違いであり今回の再帰手続きを末尾再帰の手続きに直す必要性の有無とは少しずれた話ではあります。こういう重い計算をしていてそれが問題となる場合には別のアルゴリズムを検討する必要があります。
+
+
+
+## おわりに
+
+Guile
+ではシステムのメモリを使い尽すまではスタックオーバーフローは起きないので、一般には自然な再帰をわざわざ末尾再帰の形式に変換してプログラムを読みにくくする必要はありません。末尾再帰に書き換えなくて済むプログラミングライフは大変快適なので、Guile
+のような再帰でスタックオーバーフローの起こさないプログラミング言語や処理系を探して使ってみてください。
+
diff --git a/posts/laminar-is-best.md b/posts/laminar-is-best.md
new file mode 100644
index 0000000..59ee5c7
--- /dev/null
+++ b/posts/laminar-is-best.md
@@ -0,0 +1,117 @@
+title: Laminar CI の紹介と Guix System への導入
+id: laminar-is-best
+date: 2021-08-03 10:30
+updated: 2021-08-02 11:50
+description: Laminar を導入して CI サーバーを構築した話
+---
+
+Laminar という軽量 CI を使って [ci.tojo.tokyo](https://ci.tojo.tokyo) という CI サーバーを構築したので、Laminar と Guix System への導入方法について紹介する。
+
+## 動機
+
+自前の git サーバーを構築したが、しばらく運用をしていると CI (Continuous Integration) 環境が欲しくなった。趣味では基本的に一人で開発をしているので他の開発者の変更と統合したテストをしたいなどという気持ちは全くないが、git リポジトリに push したら勝手にテストをしてくれたり、デプロイをしてくれるような良い感じの環境が欲しくなったのだ。
+
+それとは別に、現在 ACL2 で定理証明をするのにもはまっていて、証明した結果を共有するときにコードだけではなくて ACL2 の出力結果を気軽に共有できる環境が欲しいと思っていたのも大きな理由の一つである。
+
+
+## きっかけ
+
+CI が欲しいなーと思いながら、[Guix](https://guix.gnu.org/) のマニュアルの [Continuous Integration (GNU Guix Reference Manual)](https://guix.gnu.org/manual/en/html_node/Continuous-Integration.html) という節を読んでいたところ、Cuirass と Laminar というソフトウェアが載っていたのに気づいた。Cuirass は GNU Guix に対して継続的インテグレーションをするやつなので私が求めているものとは違うものだが、laminar はちょうど欲しいと思っていた軽量の CI を実現するものだった。
+
+## Laminar とは
+
+[Laminar](https://laminar.ohwg.net/) はジョブの自動化やトラッキング機能を提供し、良い感じの Web インターフェースでジョブの実行結果等を表示してくれるツールだ。
+
+これだけであれば一般的な CI ツールと同じだが、Laminar の使用方法は他の CI ツールとは全く異なる。
+
+Laminar には:
+
+* Web UI の管理画面による設定が**ない**
+* YAML 等による CI の設定用ファイルが**ない**
+* 無駄な車輪の再発明が**ない**
+
+Web UI による設定画面が存在するとそれだけで設定のバージョン管理が難しくなるのでない方がよい。また管理画面が存在すると、公開時のセキュリティ上のリスクについて悩まないといけなくなってしまう。
+
+CI を設定するために YAML 等で表現された謎の CI 設定用言語を学べとかいわれるとなんでそのツールを使うためだけに表現力の貧弱な設定用言語を使わなくてはならんのだと感じる(GNU Guix を見倣って欲しいものである)ので YAML の設定ファイルはない方がよい。
+
+そして、一般的に CI について勉強していると一番よく思うのが「なんでそんな簡単なことをそんな複雑にしてるんだ……」という問題で、既存のツールを使えば簡単にできることを中途半端に再発明することで無駄な学習を強要し、さらに無駄に表現力が狭められていることで融通の効かない不便な仕組みの中に閉じ込められてしまう。
+
+Laminar には**そういった無駄な車輪の再発明が一切なく**、既存のツールをフルに生かすことができる Hackable な CI ツールなのだ。
+
+では、Laminar ではどうやって他の CI に必要な機能を実現しているのだろうか。この章では Laminar のアプローチについて紹介する。
+
+### Laminar でのジョブの設定方法
+
+では Laminar ではどうやって CI にジョブを設定するかというと、基本的には LAMINAR_HOME ディレクトリ(デフォルトは /var/lib/laminar) の cfg ディレクトリに、 `<ジョブの名前>.run` というファイル名の実行可能なスクリプトを置くだけである。
+そしてコマンド `laminarc queue <ジョブの名前>` を実行するとジョブがキューに入り `laminar` ユーザーで実行され、Web UI に結果が良い感じに表示される。
+
+### git への push を hooks するにはどうする?
+
+git サーバーと同居する場合は [Git Hooks を使う](https://git-scm.com/book/ja/v2/Git-%E3%81%AE%E3%82%AB%E3%82%B9%E3%82%BF%E3%83%9E%E3%82%A4%E3%82%BA-Git-%E3%83%95%E3%83%83%E3%82%AF)。
+私は git サーバーと同居させる選択をしたのでこれで終わりだが、そうでない場合についても対応可能なようなのでその場合は公式ドキュメントを参照すると良いだろう。
+
+### ジョブの定期実行はどうする?
+
+cron を使う。GNU Guix System を利用している場合は GNU mcron を使うのがいいだろう(参照: [Scheduled Job Execution (GNU Guix Reference Manual)](https://guix.gnu.org/manual/en/html_node/Scheduled-Job-Execution.html))。
+
+### Docker でジョブを実行するにはどうする?
+
+Laminar は別に Docker をサポートしていない。しかし、ジョブのスクリプト中に `docker run` をすればよいとある。
+たしかにこれで駄目な理由は特に考えられないので、CI 側で Docker をサポートするのは無駄である。
+
+また、Guix ユーザーであれば Docker よりも [guix environment](https://guix.gnu.org/manual/en/html_node/Invoking-guix-environment.html) を使いたいと思うだろう(例: [deploy-www-tojo-tokyo ジョブ](https://git.tojo.tokyo/ci.git/tree/jobs/deploy-www-tojo-tokyo.run?id=580db52c3004cfdbd56aa2c8861c8fbc9fb5cdd8#n5))。にもかかわらず公式で Docker をサポートされたり、Docker を使用することを過剰に推奨されるとうっとうしいだけなので、Laminar が無駄に Docker サポートをしないという方針は良いものである。
+
+### 他のジョブから同期的に別のジョブを呼ぶにはどうするの?
+
+ジョブのスクリプト中に `laminarc run <別のジョブ>` と書けばよい。それだけで別のジョブを呼んでくれるし、Web UI からは元のジョブの実行結果から別のジョブの実行結果にジャンプできるし、逆に別のジョブの実行結果から呼び出し元のジョブの実行結果にジャンプすることもできる。
+
+### パラメータ付きのジョブを作るにはどうしたらいい?
+
+環境変数を使う。`lamiarc queue <ジョブの名前> key=value` とすればパラメータを付けてジョブを呼びだせる。
+
+## ci.tojo.tokyo の構築
+
+ci.tojo.tokyo での構築の方法について紹介する。
+
+### Laminar サーバーの構築
+
+Laminar は Guix System の Service として登録されているので、単に Service の設定をシステムの設定に追加するだけである([guix-config のコミット](https://git.tojo.tokyo/guix-config.git/commit/?id=6caebdd7a6d8703e4db6461e6ce390bf40c314f3), cgit サーバー側の設定の変更も混じっているがこれは気にしないでいただきたい……)。
+
+### ジョブの設定
+
+CI の設定は [ci.git](https://git.tojo.tokyo/ci.git/about/) リポジトリに記載している通りである。ただ、Guix System で利用する際に一点注意が必要な点があったのでそこだけ説明する。
+
+#### Guix System の環境変数の設定
+
+ジョブの設定だが Guix Environment を使うユーザーには注意が必要な点がある。
+ジョブは laminar ユーザーで実行されるのだが、PATH 環境変数がリセットされた環境でジョブが実行される。
+guix では shebang に `/usr/bin/sh` と `/usr/bin/env` しか使えないが、`/usr/bin/env` を使っても PATH 環境変数がリセットされているためなんのジョブも呼び出すこともできない。
+Laminar には必要な環境変数を静的に設定する方法(`$LAMINAR_HOME/cfg/env` に記載)が提供されているが、Guix System のユーザーは下記のようにして環境変数を設定したいと思うだろう。
+
+```
+GUIX_PROFILE="/var/lib/laminar/.config/guix/current"
+. "$GUIX_PROFILE/etc/profile"
+```
+
+Laminar では、`$LAMINAR_HOME/cfg/before` に全てのジョブの前に実行される前処理を記述することができるので私は下記のようにスクリプトを配置することで解決した。
+
+[$LAMINAR_HOME/cfg/before](https://git.tojo.tokyo/ci.git/tree/before)
+```
+#!/bin/sh
+set -eu
+
+export PATH="${PATH}:/run/current-system/profile/bin:/run/current-system/profile/sbin"
+
+GUIX_PROFILE="/var/lib/laminar/.config/guix/current"
+. "$GUIX_PROFILE/etc/profile"
+
+env | while read kv; do
+ laminarc set "$kv"
+done
+```
+
+## おわりに
+
+Laminar の概要と、Guix System に Laminar の構築をしてジョブの設定する方法について紹介した。必要な機能が十分揃っている上に、既存のツールを利用できるように設計されているため CI ツールそのものの学習コストは最小である。Guix System の設定に laminar を追加するだけでを導入できるし、CI の実行時に guix environment を使うこともできるから Guix System との相性も抜群である。
+
+他の CI システムと比較してシンプルでかつ利用が簡単なため、既存の CI ツールを使うのが難しいと感じていた方は一度試してみてはいかがだろうか。
diff --git a/posts/len-combinations.md b/posts/len-combinations.md
new file mode 100644
index 0000000..7d0e338
--- /dev/null
+++ b/posts/len-combinations.md
@@ -0,0 +1,373 @@
+title: ACL2 で全ての組み合わせを求める関数の長さの性質について証明してみた
+id: len-combinations
+date: 2021-09-02 01:45
+updated: 2021-09-02 10:30
+---
+
+## はじめに
+
+ACL2 でリストから k 個取り出す全ての組み合わせを求める関数 `combinations` と、組み合わせの数を求める関数 `comb`
+を定義し、`(equal (len (combinations x n)) (comb (len x) n))` を証明します。
+
+
+
+## きっかけ
+
+[acl2-kernel](https://github.com/tani/acl2-kernel)
+を使ってブログ記事を書いてみたいというのが本記事の主な動機です。今回良い感じに書けたら、今後も
+ACL2 でなんかやってみた記事を `acl2-kernel` を使って書いてみようと思います。
+
+
+
+## LICENSE
+
+下記に例示するプログラムのライセンスを明示します。
+
+ Copyright (C) 2021 Masaya Tojo <masaya@tojo.tokyo>
+
+ Redistribution and use in source and binary forms, with or without
+ modification, are permitted provided that the following conditions are
+ met:
+
+ 1. Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+
+ 2. Redistributions in binary form must reproduce the above copyright
+ notice, this list of conditions and the following disclaimer in the
+ documentation and/or other materials provided with the distribution.
+
+ 3. Neither the name of the copyright holder nor the names of its
+ contributors may be used to endorse or promote products derived from
+ this software without specific prior written permission.
+
+ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+
+
+## combinations 関数を定義する
+
+リストから k 個の要素を取り出す全ての組み合せを求める関数 `combinations` 関数を定義します。
+
+### 補助関数 cons-all を定義する
+
+`combinations` を作成するためには全てのリストの先頭に要素を一つ追加する `cons-all` 関数が必要です。
+`cons-all` の停止性は ACL2 が自動証明してくれました。 `cons-all`
+の第二引数は真リストしか渡らないようにガードを設定していますが、ガードの証明も問題なく自動証明されました。
+
+
+
+``` acl2
+(defun cons-all (e x)
+ (declare (xargs :guard (true-listp x)))
+ (if (endp x)
+ nil
+ (cons (cons e (car x))
+ (cons-all e (cdr x)))))
+```
+
+
+```
+
+Summary
+Form: ( RESET-PREHISTORY NIL ...)
+Rules: NIL
+Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
+ :NEW-PREHISTORY-SET
+
+The admission of CONS-ALL is trivial, using the relation O< (which
+is known to be well-founded on the domain recognized by O-P) and the
+measure (ACL2-COUNT X). We observe that the type of CONS-ALL is described
+by the theorem (TRUE-LISTP (CONS-ALL E X)). We used primitive type
+reasoning.
+
+Computing the guard conjecture for CONS-ALL....
+
+The guard conjecture for CONS-ALL is trivial to prove, given primitive
+type reasoning. CONS-ALL is compliant with Common Lisp.
+
+Summary
+Form: ( DEFUN CONS-ALL ...)
+Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
+Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
+ CONS-ALL
+
+```
+
+
+
+
+### combinations 関数
+
+リスト x から k 個を取り出す全ての組み合せのリストを求める関数 `combinations` を定義します。
+
+再帰によって `combinations` 関数を定義します。 `combinations`
+関数を作成するにはリストの先頭の要素を含む場合と含まない場合に分けて分離して考えてそれらを連結するのがよいです。
+
+#### リストの先頭の要素を含む組み合せを求める
+
+リストの先頭の要素を含む場合は、まずリストの先頭の要素を含まない全ての組み合せを `combinations` 関数により求めます。その後に
+`cons-all` 関数を用いて全ての組み合せのそれぞれに先頭の要素を追加します。
+
+ (cons-all (car x)
+ (combinations (cdr x) (- n 1)))
+
+#### リストの先頭の要素を含まない組み合せを求める
+
+リストの先頭の要素を含まない場合は簡単で、下記のように `combinations`
+関数を使ってリストの先頭の要素を含めない場合を求めるだけです。
+
+ (combinations (cdr x) n)
+
+#### combinations 関数の基底部を考える
+
+基底部として考えられるケースには与えられた自然数が 0 の場合と与えられたリストが空の場合があります。 リストから 0
+個取り出す組み合せはただ一つ存在し、空リストです。よってリストから0個取り出す場合の全ての組み合せは
+`(list nil)` です。
+
+空のリストからは 1 以上取り出す組み合せを求めることは不可能です(空リストから 0
+個を取り出す組み合せを求めることは可能で結果は上述した通りです)。不可能なわけですから、空リストから
+1 以上取り出す場合の全ての組み合せは `nil` です。
+
+#### combinations 関数
+
+上記をまとめると、`combinations` 関数は下記のように実装できます。 停止性とガードは補助定理なしで ACL2
+が自動証明してくれました。
+
+
+
+``` acl2
+(defun combinations (x n)
+ (declare (xargs :guard (and (true-listp x)
+ (natp n))))
+ (cond
+ ((zp n) (list nil))
+ ((endp x) nil)
+ (t
+ (append (cons-all (car x)
+ (combinations (cdr x) (- n 1)))
+ (combinations (cdr x) n)))))
+```
+
+
+```
+
+The admission of COMBINATIONS is trivial, using the relation O< (which
+is known to be well-founded on the domain recognized by O-P) and the
+measure (ACL2-COUNT X). We observe that the type of COMBINATIONS is
+described by the theorem (TRUE-LISTP (COMBINATIONS X N)). We used
+the :type-prescription rules BINARY-APPEND and TRUE-LISTP-APPEND.
+
+Computing the guard conjecture for COMBINATIONS....
+
+The guard conjecture for COMBINATIONS is trivial to prove, given the
+:compound-recognizer rules NATP-COMPOUND-RECOGNIZER and
+ZP-COMPOUND-RECOGNIZER, primitive type reasoning and the :type-prescription
+rules COMBINATIONS and CONS-ALL. COMBINATIONS is compliant with Common
+Lisp.
+
+Summary
+Form: ( DEFUN COMBINATIONS ...)
+Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
+ (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
+ (:FAKE-RUNE-FOR-TYPE-SET NIL)
+ (:TYPE-PRESCRIPTION BINARY-APPEND)
+ (:TYPE-PRESCRIPTION COMBINATIONS)
+ (:TYPE-PRESCRIPTION CONS-ALL)
+ (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
+Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
+ COMBINATIONS
+
+```
+
+
+
+
+## comb 関数を定義する
+
+n 個から k 個を取り出す組み合せの数を求める関数を定義します。 `combinations`
+の定義を参照しながら対応するように記述しましょう。
+
+ - 0 個を取り出す組み合せは空リストただ一つなので、組み合せの数は 1
+ - 長さ 0 のリストから 1 個以上取り出すことはできないため、組み合せの数は 0
+ - 先頭要素を含む組み合せの数は `(comb (- n 1) (- k 1))`
+ - cons-all 関数は与えられたリストの長さを変えないことに注意
+ - 先頭要素を含まない組み合せの数は `(comb (- n 1) k)`
+
+
+
+``` acl2
+(defun comb (n k)
+ (cond
+ ((zp k) 1)
+ ((zp n) 0)
+ (t (+ (comb (- n 1) (- k 1))
+ (comb (- n 1) k)))))
+```
+
+
+```
+
+The admission of COMB is trivial, using the relation O< (which is known
+to be well-founded on the domain recognized by O-P) and the measure
+(ACL2-COUNT N). We observe that the type of COMB is described by the
+theorem (AND (INTEGERP (COMB N K)) (<= 0 (COMB N K))). We used primitive
+type reasoning.
+
+Summary
+Form: ( DEFUN COMB ...)
+Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
+Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
+ COMB
+
+```
+
+
+
+
+## len-combinations 定理
+
+`(len (combinations x k))` が `(comb (len x) k)` と一致することを証明します。 これは ACL2
+が補助定理を必要とせずに自動証明してくれました。
+
+
+
+``` acl2
+(defthm len-combinations
+ (equal (len (combinations x k))
+ (comb (len x) k)))
+```
+
+
+```
+
+*1 (the initial Goal, a key checkpoint) is pushed for proof by induction.
+
+Perhaps we can prove *1 by induction. Two induction schemes are suggested
+by this conjecture. These merge into one derived induction scheme.
+
+We will induct according to a scheme suggested by (COMBINATIONS X K).
+This suggestion was produced using the :induction rules COMBINATIONS
+and LEN. If we let (:P K X) denote *1 above then the induction scheme
+we'll use is
+(AND (IMPLIES (AND (NOT (ZP K))
+ (NOT (ENDP X))
+ (:P (+ -1 K) (CDR X))
+ (:P K (CDR X)))
+ (:P K X))
+ (IMPLIES (AND (NOT (ZP K)) (ENDP X))
+ (:P K X))
+ (IMPLIES (ZP K) (:P K X))).
+This induction is justified by the same argument used to admit COMBINATIONS.
+Note, however, that the unmeasured variable K is being instantiated.
+When applied to the goal at hand the above induction scheme produces
+three nontautological subgoals.
+Subgoal *1/3
+Subgoal *1/3'
+Subgoal *1/3''
+Subgoal *1/3'''
+Subgoal *1/3'4'
+Subgoal *1/3'5'
+Subgoal *1/3'6'
+Subgoal *1/3'7'
+Subgoal *1/3'8'
+Subgoal *1/3'9'
+Subgoal *1/3'10'
+
+([ A key checkpoint while proving *1 (descended from Goal):
+
+Subgoal *1/3''
+(IMPLIES (AND (NOT (ZP K))
+ (CONSP X)
+ (EQUAL (LEN (COMBINATIONS (CDR X) (+ -1 K)))
+ (COMB (LEN (CDR X)) (+ -1 K)))
+ (EQUAL (LEN (COMBINATIONS (CDR X) K))
+ (COMB (LEN (CDR X)) K)))
+ (EQUAL (LEN (APPEND (CONS-ALL (CAR X)
+ (COMBINATIONS (CDR X) (+ -1 K)))
+ (COMBINATIONS (CDR X) K)))
+ (+ (COMB (LEN (CDR X)) K)
+ (COMB (LEN (CDR X)) (+ -1 K)))))
+
+*1.1 (Subgoal *1/3'10') is pushed for proof by induction.
+
+])
+Subgoal *1/2
+Subgoal *1/2'
+Subgoal *1/1
+
+So we now return to *1.1, which is
+
+(IMPLIES (AND (TRUE-LISTP CS0) (TRUE-LISTP CS))
+ (EQUAL (LEN (APPEND (CONS-ALL X1 CS0) CS))
+ (+ (LEN CS) (LEN CS0)))).
+Subgoal *1.1/3
+Subgoal *1.1/3'
+Subgoal *1.1/2
+Subgoal *1.1/1
+Subgoal *1.1/1'
+
+*1.1 and *1 are COMPLETED!
+Thus key checkpoints Subgoal *1/3'' and Goal are COMPLETED!
+
+Q.E.D.
+
+Summary
+Form: ( DEFTHM LEN-COMBINATIONS ...)
+Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
+ (:DEFINITION BINARY-APPEND)
+ (:DEFINITION COMB)
+ (:DEFINITION COMBINATIONS)
+ (:DEFINITION CONS-ALL)
+ (:DEFINITION ENDP)
+ (:DEFINITION FIX)
+ (:DEFINITION LEN)
+ (:DEFINITION NOT)
+ (:DEFINITION SYNP)
+ (:DEFINITION TRUE-LISTP)
+ (:ELIM CAR-CDR-ELIM)
+ (:EXECUTABLE-COUNTERPART BINARY-+)
+ (:EXECUTABLE-COUNTERPART CONSP)
+ (:EXECUTABLE-COUNTERPART EQUAL)
+ (:EXECUTABLE-COUNTERPART LEN)
+ (:EXECUTABLE-COUNTERPART ZP)
+ (:FAKE-RUNE-FOR-TYPE-SET NIL)
+ (:INDUCTION COMBINATIONS)
+ (:INDUCTION CONS-ALL)
+ (:INDUCTION LEN)
+ (:INDUCTION TRUE-LISTP)
+ (:REWRITE CAR-CONS)
+ (:REWRITE CDR-CONS)
+ (:REWRITE COMMUTATIVITY-2-OF-+)
+ (:REWRITE COMMUTATIVITY-OF-+)
+ (:REWRITE FOLD-CONSTS-IN-+)
+ (:REWRITE UNICITY-OF-0)
+ (:TYPE-PRESCRIPTION COMBINATIONS)
+ (:TYPE-PRESCRIPTION CONS-ALL)
+ (:TYPE-PRESCRIPTION LEN)
+ (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
+Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
+Prover steps counted: 5105
+ LEN-COMBINATIONS
+
+```
+
+
+
+
+## おわりに
+
+無事に組み合せを求める関数と組み合せの数を求める関数の関係が意図した通りであることを証明できました。
+今回は二つの関数の定義がほとんど同じであったため補助定理を考える必要もなく証明できたのですが、通常はもう少し難しいことが多いです。
+
+`comb` の定義の方法は他にもあるため、他の定義による組み合せの数と一致するかについての証明を試みても良いかもしれません。
+
diff --git a/posts/mail-and-domain.sxml b/posts/mail-and-domain.sxml
index 5799fe9..0d81f5c 100644
--- a/posts/mail-and-domain.sxml
+++ b/posts/mail-and-domain.sxml
@@ -91,7 +91,7 @@
(li "メールアドレスのローカルパートを自由に設定できる")
(ul (li "フリーメールだと空いている名前しか使用できない"))
(li "ドメインを所有している限りメールアドレスは常に使用可能である")
- (ul (li "フリーメールの場合、サービスの終了やアカウントの削除によて使用不能になる場合がる")))
+ (ul (li "フリーメールの場合、サービスの終了やアカウントの削除によて使用不能になる場合がある")))
(p "もちろん、下記のようなデメリットもあるにはあります。")
(ul (li "お金がかかる")
(ul (li "ドメインの取得・維持にかかる費用")
diff --git a/static/css/blog.css b/static/css/blog.css
index 036d0b9..17aa389 100644
--- a/static/css/blog.css
+++ b/static/css/blog.css
@@ -1,5 +1,5 @@
/* TojoQK's website --- TojoQK's personal website
- * Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
+ * Copyright © 2020, 2021, 2021 Masaya Tojo <masaya@tojo.tokyo>
*
* This file is part of TojoQK's website
*
@@ -58,6 +58,15 @@ ul.nav-list > li {
margin-right: auto;
}
+.nav-logo-main {
+ display: flex;
+ flex-wrap: nowrap;
+}
+
+.nav-log-img {
+ padding-right: 8px;
+}
+
.nav-item {
padding: 5px 10px;
font-size: 1.2rem;
@@ -90,6 +99,7 @@ body {
}
h1.post-title {
+ font-size: 1.5em;
margin-bottom: 0;
}
@@ -116,26 +126,18 @@ h1.post-title {
list-style-type: none;
}
-h1 {
+.post h2 {
font-size: 1.4em;
+ border-bottom: 2.5px solid black;
+ padding-bottom: 3px;
}
-h2 {
- font-size: 1.18em;
- display: flex;
- flex-direction: column;
-}
-
-h2:after {
- width: 100%;
- height: 5px;
- content: "";
- background: black;
- margin-top: 0.5rem;
+.post h3 {
+ font-size: 1.25em;
}
-h3 {
- font-size: 1.1em;
+.post h4 {
+ font-size: 1.18em;
}
pre {
diff --git a/static/image/QK-114x114.png b/static/image/QK-114x114.png
index 962f7ed..88b1f0c 100644
--- a/static/image/QK-114x114.png
+++ b/static/image/QK-114x114.png
Binary files differ
diff --git a/static/image/QK-120x120.png b/static/image/QK-120x120.png
index a6057eb..ed692df 100644
--- a/static/image/QK-120x120.png
+++ b/static/image/QK-120x120.png
Binary files differ
diff --git a/static/image/QK-144x144.png b/static/image/QK-144x144.png
index ee818c5..228f951 100644
--- a/static/image/QK-144x144.png
+++ b/static/image/QK-144x144.png
Binary files differ
diff --git a/static/image/QK-152x152.png b/static/image/QK-152x152.png
index 420385e..9c51365 100644
--- a/static/image/QK-152x152.png
+++ b/static/image/QK-152x152.png
Binary files differ
diff --git a/static/image/QK-16x16.png b/static/image/QK-16x16.png
index fc7c197..91d3bd3 100644
--- a/static/image/QK-16x16.png
+++ b/static/image/QK-16x16.png
Binary files differ
diff --git a/static/image/QK-180x180.png b/static/image/QK-180x180.png
index abf33de..f9704d5 100644
--- a/static/image/QK-180x180.png
+++ b/static/image/QK-180x180.png
Binary files differ
diff --git a/static/image/QK-192x192.png b/static/image/QK-192x192.png
index 4e9f5cf..4b199f9 100644
--- a/static/image/QK-192x192.png
+++ b/static/image/QK-192x192.png
Binary files differ
diff --git a/static/image/QK-32x32.png b/static/image/QK-32x32.png
index 71c078d..6975c98 100644
--- a/static/image/QK-32x32.png
+++ b/static/image/QK-32x32.png
Binary files differ
diff --git a/static/image/QK-52x52.png b/static/image/QK-52x52.png
index 0ce8108..2a173a5 100644
--- a/static/image/QK-52x52.png
+++ b/static/image/QK-52x52.png
Binary files differ
diff --git a/static/image/QK-57x57.png b/static/image/QK-57x57.png
index 5b7b212..bcbc35b 100644
--- a/static/image/QK-57x57.png
+++ b/static/image/QK-57x57.png
Binary files differ
diff --git a/static/image/QK-60x60.png b/static/image/QK-60x60.png
index f516d27..6a60ebd 100644
--- a/static/image/QK-60x60.png
+++ b/static/image/QK-60x60.png
Binary files differ
diff --git a/static/image/QK-72x72.png b/static/image/QK-72x72.png
index 348fdb0..a023819 100644
--- a/static/image/QK-72x72.png
+++ b/static/image/QK-72x72.png
Binary files differ
diff --git a/static/image/QK-76x76.png b/static/image/QK-76x76.png
index 463bdc9..07c4a86 100644
--- a/static/image/QK-76x76.png
+++ b/static/image/QK-76x76.png
Binary files differ
diff --git a/static/image/QK-96x96.png b/static/image/QK-96x96.png
index 28e948c..e72003f 100644
--- a/static/image/QK-96x96.png
+++ b/static/image/QK-96x96.png
Binary files differ
diff --git a/static/image/QK.png b/static/image/QK.png
index 868111c..2c623f8 100644
--- a/static/image/QK.png
+++ b/static/image/QK.png
Binary files differ