duneでwarningが全部errorになってしまうのをなんとかする

OCamlの(多分次期標準の)ビルドツールであるdune(https://github.com/ocaml/dune)を使ってコンパイルすると、すべてのwarningがerror扱いされてしまいます。例えば、


について

dune exec ./main.exe

を叩くと、

ocamlc .main.eobjs/main.{cmi,cmo,cmt} (exit 2)
(中略)
File "main.ml", line 2, characters 6-7:
Error (warning 26): unused variable x.

となり、未使用変数の警告がエラー扱いされてしまって実行することができません。どうもduneがocamlc(コンパイラ)にwarningすべてをerrorにする「-w @A」をわたしているようです。開発中の未使用変数ぐらい大目に見てほしいので、warningのままでいてほしいです。そこで、duneファイルを

として、ocamlcにさらにwarningすべてをerrorとして扱わない「-warn-error a」を渡すと解決します。

http://ocaml.jp/archive/ocaml-manual-3.06-ja/manual025.html

(ところで、gistで1ファイルだけ埋め込むときはgistの上のほうの埋め込みタグのURIの後ろに「?file=hoge.fuga」をつければいいのね)

横内寛文「プログラム意味論」を流し読みした

本当は読書メータの感想のところに書こうと思ったのだが字数が溢れてしまったのでここに書いておく。
あんまり真面目に読んでないんだ、ごめんね。


気にはなっていたのだか積読で、一念発起して興味あるところだけ読むことにした。そういうわけで全体の話はしてません。

公理的意味論は(他の意味論のスタイルと明確な区別があるわけではないが)プログラムの構文に、その文が意味する数学的対象を直接割り付けるもの。プログラムが停止しないなどのエラーをうまく扱えるその数学的対象としては部分関数が便利で、その順序をうまく扱うためにcpo(complete partial order)という順序集合のクラスを用いる。そうするとこの上で不動点の議論ができ、それが再帰やwhile文といった自明には意味が定義できないものにも意味を割り付けることができる。この議論の後に、λにいくらかの基本型と再帰を許す関数定義μを追加したPCF(Programming language for Computable Function)を定義し、それに対して意味論を与える。

型なしラムダ計算に公理的意味論を与えるのに素朴に集合論で言うところの関数を割り当てようとすると、自由な関数適用のせいで矛盾が起こってしまう。これに対処するには、X→Xの関数がXに埋め込めるようなcpo Xを見つけなければいけない。このような要求を方程式風に書くとX=[X→X]というようになるが、このようなcpoの対象についての方程式を領域方程式という。この方程式の解が見つかれば、そこから型なしラムダ計算の意味論(モデル?)を作ることができるが、実際この解として2点以上の集合Dから埋め込みを繰り返して無限直積を取り作ったcpoであるD∞が解であることを確かめる。なお、この領域方程式を解く方法を研究したり、この状況をcpoだけではなくω-完全な圏でのcolimitを考えて本質を捉えようとするというような議論もこの本ではなされているが、とりあえず具体に興味があったのでそこは読まなかった。

疑問として、そんな風にして意味論を作ってそれで「型なしラムダ計算の理解が深まった」と言えるのか、普通にラムダ式を適当な同値関係で割ったものそのものを眺めるのと比べて何かいいのかという疑問は残ったが、真面目に読んでないからかもしれない。

(8/27追記)公理的意味論がつけば、(λx.xx)(λx.xx)に⊥が対応することがわかるよと教えてもらいました。そういう意味では公理的意味論は数学で言うところの不変量みたいな感じで使えるんですね。

OCamlのwith typeの使い方を失敗から学んだ話(ファンクタシグネチャの返り値でモジュールを制限したくなったときどうすればよいか)

OCamlでのSetの使い方がよくわからない(どれがいいんでしょう) - ashiato45の日記に引き続き、有限オートマトンOCamlで記述することを考えます(前の記事は読んでなくても大丈夫です)。今回は文字列を読んで受理拒否を判定する関数は載せず、純粋に有限オートマトンのデータ構造を提供することを考えます。ただし、アルファベットと状態をあらわす値は好きなものを選べるように、ジェネリック的にしたいとしましょう。
2.3 ファンクタなんかを参考にしながら書くとこんな感じになります。
gist.github.com

これで良さそうな気もするのですがここでさらに、ファンクタAutomに具体的によく使う集合を与えて、具体的なオートマトンのモジュールも作ってこのライブラリで提供することを考えましょう。次のように書いてみます。
gist.github.com
今回はZeroとOneを持っているalph型を定義し、その集合をアルファベット集合AlphSetにします。状態集合は文字列集合StringSetということにします。そしてこれらをAutomファンクタに与え、ZeroOneAutomモジュールを作ります(autom_dame2.mliの19行目)。モジュールはシグネチャで制限してインターフェースを提供してやらないことには外部からアクセスできませんので、4行目で定義したファンクタシグネチャAUTOMを使って

module ZeroOneAutom: AUTOM(AlphSet)(StringSet)

と制約することを考えます…が、これはコンパイルエラーになります。文法が定義してあるOCamlの公式マニュアルの
7.10  Module types (module specifications)を見てみると、そもそもこういう書き方はできず、コロンの右側には基本的にはシグネチャを置かなければならないということがわかります。

そこで、仕方がないのでファンクタで帰ってくるものだけを取り出して書き(以下AUTOM')、AUTOMはAUTOM'を返すようにすることを考えてみます。
gist.github.com
ただし、AUTOM'の定義のときには引数のモジュールの情報は使えませんので、とりあえず必要な型だけをast, sst, aset, ssetとして定義しておいて、それを使って全体を定義しておきます(autom_ok.mliの4-15行目)。そして、AUTOMの定義のなかでwith typeを使って、AUTOM'で仮置きした型と、得られたモジュールの型とが一致するという制約をかけます。これで、ZeroOneAtomはAUTOM'シグネチャとtype withを使って無事制限をかけることができました。ついでに、AlphSetとStringSetも外部からきちんとアクセスできるようにtype withで制約をかけてあります。type withのはたらきですが、merlinの表示する情報を見るのがわかりやすい気がします。

module ZeroOneAutom: AUTOM'
with type ast = AlphSet.t
with type sst = StringSet.t
with type aset = AlphSet.Elt.t
with type sset = StringSet.Elt.t

の情報をmerlinで表示させると、次のようになります

sig
type ast = AlphSet.t
type sst = StringSet.t
type sset = StringSet.Elt.t
type aset = AlphSet.Elt.t
type t = {
alph : ast;
states : sst;
trans : sset -> aset -> sset;
init : sset;
final : sst;
}
end

対して、

module ZeroOneAutom: AUTOM'

の情報は

sig
type ast
type sst
type sset
type aset
type t = {
alph : ast;
states : sst;
trans : sset -> aset -> sset;
init : sset;
final : sst;
}
end

となります。このように、type withを使うと、型の後ろにイコールとその型が何かを追加することができるようです。このことを「シグネチャに型の等価性情報を追加する」というようです*1

ちなみに、先の文法のページ(2.4 ファンクタを使った型の抽象化])を見ていたところ、type withならぬmodule withというのもあるようだったので、これも試してみました。すると、次のようになります。
gist.github.com
「module with M = M2」のようにすることで、AUTOM'シグネチャ内で仮置きしたAlphSetモジュールとStateSetモジュールに(autom_ok2.mliの5、6行目)、モジュールの等価性情報を追加することができています(行18、19や30、31)。実際、

module ZeroOneAutom: AUTOM'
with module AlphSet = AlphSet
with module StateSet = StringSet

の情報をmerlinで見てみると、

sig
module AlphSet :
sig
module Elt :
sig
type t = alph
val t_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t
val sexp_of_t : t -> Ppx_sexp_conv_lib.Sexp.t
(略)
val sexp_of_t : t -> Base__.Ppx_sexp_conv_lib.Sexp.t
end
module StateSet :
sig
module Elt :
sig
type t = string
val t_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t
(略)
val sexp_of_t : t -> Base__.Ppx_sexp_conv_lib.Sexp.t
end
type t = {
alph : AlphSet.t;
states : StateSet.t;
trans : StateSet.Elt.t -> AlphSet.Elt.t -> StateSet.Elt.t;
init : StateSet.Elt.t;
final : StateSet.t;
}
end

となっており、確かになかのAlphSetやStateSetにmodule withで与えたAlphSet(これは外側のalph型のためのモジュールの名前!)やStringSetの情報が反映されていることがわかります。

OCamlでのSetの使い方がよくわからない(どれがいいんでしょう)

前々からOCamlのSetの使い方、というかベストプラクティスがよくわからないと思っていたのですが、うまく言葉にできなかったのですがいい例が作れたのでその例にそって「これをどう書くべきなんだろう」というお話をします。

例として考えるのは普通の決定性有限オートマトン(DFA,
決定性有限オートマトン - Wikipedia)です。
DFAのデータを保持できて、かつある文字列(語)を受理するかどうかの判定ができるものを考えます。素朴にlistを使って実装するとこんな感じになります(getのあたりはレコードで書くべきだったかも…):
gist.github.com

ただ、本来はアルファベットや状態は集合であってリストではないので、これを集合を使って書き直したいと思います。
このときありうる実装をとりあえず2つ作ってみたのですが、それぞれ気持ち悪いところがあってどうすればいいのかよくわからないので誰か教えてください…

オートマトンをあらわすファンクタを作って、それにアルファベットや状態の値のを渡す

gist.github.com
今回はまあいいのですが、状態集合やアルファベット集合はオートマトンとはそもそも別の文脈で作っていて、その集合をオートマトンの状態にしたいなというシナリオのときに、集合を作りはじめる前からMyAutomを作りはじめている(21行目)のが気持ち悪いなという気がしています。

オートマトンをあらわすファンクタを作って、それにアルファベットや状態の値の集合のモジュールを渡す

gist.github.com



先の点を解消するために、集合のモジュールはファンクタの外側で作ってしまって、その集合のモジュールをオートマトンをあらわすファンクタに渡すべきでしょうか。まあやっぱり動くのですが、オートマトンの型は値の型に応じて決まってほしくて、その集合に対する操作の仕方まで規定している集合モジュールを取らせるのは気持ち悪くない…?という気がしています。

あるいはそもそもオートマトンの状態をどう持っているかはシグネチャで隠蔽してしまう?

それで外からappend_statesみたいな命令を使って追加していく形にすべきでしょうか。そのほうが疎結合的な意味では衛生的な気もするのですが、そのために手持ちの状態集合をfoldなりで逐一追加して計算コストをかけるのもな…という気がします…

7/30追記


教えていただきました。ありがとうございます。

QEPCADのインストールと簡単な使い方

QEPCADは量化子除去(QE, Quantifier Elimination)のためのアカデミックツールで、作者のサイト
QEPCAD - Quantifier Elimination by Cylindrical Algebraic Decomposition
で公開されています。インストールのために自前ビルドが必要な上に、サイトの案内
Downloading and Installing QEPCADにそのまま従ってもいまのUbuntuだとインストールに失敗するので覚書をしておきます。

# インストール
1. 必要なライブラリsaclibとQEPCAD本体を(適当なディレクトリで)ダウンロードする

$ wget https://www.usna.edu/CS/qepcadweb/INSTALL/qepcad-B.1.69.tar.gz
$ wget https://www.usna.edu/CS/qepcadweb/INSTALL/saclib2.2.6.tar.gz

2. saclibのビルドに必要になるので先にcshを入れておく

$ sudo apt install csh

3. 普通はccはCコンパイラを指している気がするが、一応ccと叩いて確認しておく。もしも指していないならgccを指すようにしておく。
4. saclibを展開して中に入る。

$ tar xf saclib2.2.6.tar.gz
$ cd saclib2.2.6

5. 変数saclibがそのディレクトリを指すようにする。makeが使うのでexportしておく必要がある。いまはsaclibディレクトリのなかにいるのでpwdでやってしまう。

export saclib=`pwd`

6. 以下を順次叩いてビルドする。何かhoge.hが足りないと言われたら適当にぐぐってそれを含むubuntuパッケージを見つけ(普通はhoge-devみたいな名前になっている)、aptでインストールする。

$ cd $saclib/bin
$ ./sconf
$ ./mkproto
$ ./mkmake
$ ./mklib all

7. エラーが出なければsaclibのインストールはおわり。
8. qepcadのビルドに使うので先にlibreadline-devを入れておく

$ sudo apt install libreadline-dev

9. qepcadを展開し、中に入る。ディレクトリはqesourceという名前になっている。

$ tar xf qepcad-B.1.69.tar.gz
$ cd qesource

10. 変数qeを設定する。これもmakeが使うのでexportしておく必要がある。いまはqesourceのなかにいるのでpwdでやってしまう。

$ export qe=`pwd`

11. サイトだとgmakeを叩くとなっているが普通にmakeを叩く。

$ make

11. 結構時間がかかる。何もエラーがでなければおわり。
f:id:sle:20180425063610p:plain
こんな感じのエラーが出たら、やっぱり足りないものが入っているパッケージをGoogle探してaptで入れる。
12. plot2dをビルドする。先にfreeglutを入れておく。

$ sudo apt install freeglut3-dev

13. makeする

$ cd $qe/plot2d
$ make

14. これでqesource/binにqepcadがビルドされているはず。必要に応じてパスを通す。

# 使い方
例と注意点だけ示す。今回は \exists x. x^2+bx+c=0 \wedge x \ge 0の量化子を消してみる。
1. 起動する。ここでびっくりしたのだが、先の変数qeと変数saclibが有効になっていないとセグフォで落ちるので頻繁に使うのならちゃんと起動時に変数が設定されるようにしておく。
2. このプログラムは対話で進んでいく。まずタイトルを要求されるので、ブラケットで囲んで指定しEnter。今回はhogeにする。

Enter an informal description  between '[' and ']':
[hoge]

3. 式に出てくる変数を、拘束される変数も自由変数もまとめて丸括弧囲み、カンマ区切りで書く。このとき、自由変数を先に、束縛変数(量化子のなかの変数)を後に書かなければならない。今回消したいのはxなので、xをあとに書く。また、拘束される変数は、式を冠頭標準形にしたときの順番で書かなければならない(今回は1個なので関係ないが)。

Enter a variable list:
(b,c,x)

4. 自由変数の個数を指定する。いまはbとcが自由なので2にする。

Enter the number of free variables:
2

5. 式を入力する。まず量化子と拘束する文字の組を並べて丸括弧で囲んで並べる。今回は存在量化子なので「(Ex)」となる。全称量化子のときは「(Ax)]とする。また、今回は量化子が1つだが、複数のときには3で入れた順番で量化子があらわれなければならない。例えば、「(a,b,x,y)」と変数を指定していて、自由変数の個数を2と指定しながら「(Ay)(Ex)」というのは駄目。次にブラケット(丸括弧でない)で囲んで式を書く。かけ算は空白を入れればよい。アンドは「/\」で、オアは「\/」で書く。その辺の記号は公式ページ
https://www.usna.edu/CS/qepcadweb/B/user/EnterForm.htmlにも書いてある。最後にピリオドを打ってEnter。打たないといつまで立っても始まらない(計算が重いんだなと勘違いしがち)。

(Ex)[x^2+b x+c=0 /\ x>=0].

6. よくわかんないけどずっとgoって答えると答えが出る。

=======================================================

Before Normalization >
go

Before Projection (x) >
go

Before Choice >
go

Before Solution >
go

An equivalent quantifier-free formula:

4 c - b^2 <= 0 /\ [ b < 0 \/ c <= 0 ]


=====================  The End  =======================

7. もしもtrueとかしか出なくて不満足なら、ここ
QEPCAD - Entering Formulas
を見ながらBefore solutionでsolution-extension Tなどを試すとよい。

Huaweiの端末はAndroidアプリのログを握り潰す

Adding Voice Capabilities | Android Developersにしたがって、RecognizerIntentを使った音声認識のコードを書いていたのだが、音声認識画面(下画像)でBackボタンを押すとアプリが落ちるという問題が発生した。
f:id:sle:20180226005755p:plain
Android StudioのLogcatを見ても、主要なメッセージは

02-26 00:59:56.197 24384-24384/com.example.ashia.speechwithoutintent I/HwSecImmHelper: mSecurityInputMethodService is null
(中略)
02-26 00:59:56.292 24384-24384/com.example.ashia.speechwithoutintent I/Process: Sending signal. PID: 24384 SIG: 9

しか出てこず、例外が発生したようではない。はじめは、音声認識画面のBackがメインのActivityまで伝わってしまってプログラムが終了するのだと思ってBackの信号を握り潰すなどをやってみがたどうにも解決しない。


しばらく(5時間ぐらい)、ぐぐったり飽きてゲームをしたりしていたのだが、最後にこのような記事を見つけた:
https://stackoverflow.com/questions/38587844/msecurityinputmethodservice-is-null-in-logcat
曰く、

For my Huawei device the following helps:

Dial:

#*#2846579#*#*

and a hidden menu is shown. Go to "Background Setting" -> "Log setting" and enable the log levels.

ということで、デフォルトではHuaweiの端末では、ある程度のログレベル以下のログは握り潰されてしまうらしい。ここにあるように、
電話アプリを起動して「*#*#2846579#*#*」と打つと、以下のような画面がでる。ちなみに、打ち間違えてバックスペースで消して打つと出ないような気がするので、一発で打つ必要があると思う。
f:id:sle:20180226010644p:plain
この上で、「Background Setting」→「Log setting」と入ると、チェックボックスが4つぐらい出てくるのですべてにチェックを入れる。「This might affect the performance!」みたいなことを言われるが、まあ覚悟の上である(必要ならあとで外したほうがいいかも)。

これでデバッグ実行をしてみると、

02-26 00:59:56.265 24384-24384/com.example.ashia.speechwithoutintent E/AndroidRuntime: FATAL EXCEPTION: main
Process: com.example.ashia.speechwithoutintent, PID: 24384
kotlin.NotImplementedError: An operation is not implemented: not implemented
at com.example.ashia.speechwithoutintent.MainActivity$M.onError(MainActivity.kt:44)
at android.speech.SpeechRecognizer$InternalListener$1.handleMessage(SpeechRecognizer.java:450)
at android.os.Handler.dispatchMessage(Handler.java:102)
at android.os.Looper.loop(Looper.java:150)
at android.app.ActivityThread.main(ActivityThread.java:5621)
at java.lang.reflect.Method.invoke(Native Method)
at com.android.internal.os.ZygoteInit$MethodAndArgsCaller.run(ZygoteInit.java:794)

のように新たにエラーメッセージを得ることができて、ちゃんと例外が起こっているということがわかるようになった。

ソフトウェアの基礎を読んでてCoqで詰まったところ(というよりは帰納法の使い方の話)

Hoare論理をCoqでやってみたかったのでソフトウェアの基礎を読んでいた。何かしら書いておかないと自分のなかで記憶がまたゼロに戻ってしまうので何かしら書いておく。当たり前のことをたくさん書く。あと、答えをそのまま書くのはよくないらしいので、Coqの証明を書きたい場面では自然言語での証明を書くに留める。

ソフトウェア的なところ(数学的でないところ)

環境構築

シンタックスハイライティング
  • はじめはubuntu上にapt install coqしたのだが、coqideのシンタックスハイライティングが有効にならなかった。id:qnighyさんに教えてもらって再起動したら直ったのでとりあえず再起動すべし。
コンパイルについて

Lists_Jからは

Require Export Basics_J.

しろというのが出てくるが、その前にBasics_J.vをコンパイルしなければいけない。(自分でBasics_J.vを使ってもよいが、
http://proofcafe.org/sf/sfja.tar.gz
からダウンロードするのが簡単だと思う。)このとき、Basics_J.vを開いた上でメニューの「Compile > Compile buffer」をするのだが、このときBasics_J.vの入っているディレクトリをカレントディレクトリにしておかないとコンパイルが通らなかった。したがって、コンパイルしたいときはcoqideコマンドをそのディレクトリで叩く必要があるっぽい。

コピペについて

ウェブサイトからCoqのコードをコピペしたくなることがあるが、∀はforallに直すなどしないとcoqide上で動いてくれない(本当は何か設定があるのかもしれない)。
そういうわけで、とりあえず次のようなコマンドを作ってxselと一緒に使っていた。

#!/bin/bash

sed -r 's/→/->/g' | sed -r 's/∀/forall/g' | sed -r 's/∧/\/\\/g' | sed -r 's/∨/\\\//g' | sed -r 's/∃/exists/g'

自然数の和の可換性(basic_induction)

Basics_Jの演習のbasic_inductionのplus_commについて。
教訓としては、「とりあえずでintrosするのをやめろ」ということになる。
まず日本語で証明を書いてみるとこうなる*1

  1. nについての帰納法で示す。自然数帰納法の原理は「P(n)を示すには、(a)P(0)を示し、(b)P(n)が成り立っているという仮定のもとでP(S n)を示せばよい。」であるから、P(n)を「任意のmについて『n+m=m+n』となる」として示す。
    1. P(0)を示す。0+m=m+0を示せばよいが、これはm=m+0と同じである。
    2. mについての帰納法でm=m+0を示す。Q(m)を「m=m+0」とする。
      1. Q(0)を示す。これは0=0+0を示すことだが、自明。
      2. Q(m)を仮定し、Q(S m)を示す。Q(m)は「m=m+0」であり、このもとでQ(S m)すなわち、「S m = S m + 0」を示せばよい。
        1. S m = S (m + 0) = S m + 0なので、示された。はじめの等式で帰納法の仮定Q(m)を用い、2つめの等式で自然数の足し算の定義を用いた。
    3. P(n)を仮定し、P(S n)を示す。P(n)、すなわち「任意のmについて、n+m=m+n」を用いてよい。
    4. mについての帰納法でP(S n)、すなわち「S n+m=m+S n」を示す。Q(m)を新たに「S n+m=m+S n」とする。
      1. Q(0)、すなわち「S n+0=0+S n」を示す。S n+0=S (n+0)=S(0+n)=S n=0+ S nなので、示された。ここで、1つ目の等式は足し算の定義、2つ目は帰納法の仮定であるP(n)で、∀mでm=0としたもの。3つめは足し算の定義、4つ目も帰納法の定義。
      2. Q(m)を仮定し、Q(S m)を示す。Q(m)、すなわち「S n+m=m+S n」を用いて、Q(S m)、すなわち「S n+S m = S m + S n」を示す。S n + S m=S (n + S m)=S(Sm + n)=S(S(m+n))である。1つ目の等式は足し算の定義、2つ目はP帰納法の仮定であるP(n)で、∀mでm=S mとしたもの。3つ目は足し算の定義。一方、S m+S n=S(m+S n)=S(Sm+n)=S(S(m+n))である。1つ目の等式は足し算の定義、2つ目はplus_n_Smとしてすでに示されている。3つ目は足し算の定義。

というわけで、まず帰納法を「任意のmについて『n+m=m+n』となる」としてスタートさせなくてはいけないので、

induction n.

と始めなくてはいけない。ここで

intros.
induction n.

とすると、固定したmについて証明が始まってしまってうまく行かない。
普段の手書きの証明だと、∀の外に出たり入ったりを無意識にやってしまうが、その辺をちゃんと意識してやらないとなあと思った。

ちなみに、この命題の証明をぼくはAMSから出ているSaunders MacLane, Garrett Birkhoffの「Algebra」でしか見たことがないんですが他に何かありますか。

リストの2回反転(list_exercisesでのrev_involute)

実は何回かソフトウェアの基礎に挑戦していて、何度もLists_Jのlist_exercisesのrev_involuteで苦戦しているので、手書き証明をここに置いておく。4つ目の等式は帰納法の仮定で、5つ目の等式のために補題を置くのがポイントになる。

f:id:sle:20171203200841p:plain

条件式が常にtrueと等価なWHILE文が停止しないこと

Equiv_JのWHILE_true_nontermの証明が何やってるかよくわからなくなって、段々帰納法ってなんだっけってなったので思い出した話。簡単なところなら帰納法のことが分かっていたつもりになっていたのだが、WHILE言語ぐらい複雑になると落ち着いて振り返らないとよく分からなくなっていた。

示したいのは、

Lemma WHILE_true_nonterm : ∀ b c st st',
     bequiv b BTrue →
     ~( (WHILE b DO c END) / st ⇓ st' ).

である。やりたいことは、「bが式BTrueと等価なら、WHILE b DO c END/st⇓st'がcevalの規則によって導かれるわけはない」ということなので、
cevalの規則から導かれる帰納法の原理ceval_indを上手く使って証明しなくてはいけない。
帰納法の原理ceval_indは、3つ組「c/ st ⇓ st'」についての述語「P(c/st ⇓ st')」を示すには、次のことを示せばいいことを教えてくれる。

  • ベースケース(前提に3つ組が出ない)
    • E_Skip: 任意のstについて、P(SKIP/st⇓st)が成り立つ。
    • E_Ass: 任意のst,a,l,nについて、整数式aがstのもとでnに評価されるなら、P(l::=a/st⇓(stのlをnで置換したもの)が成り立つ。
    • E_WhileEnd: 任意のb,st,cについて、bがstのもとでfalseに評価されるなら、P(WHILE b DO c END/st⇓st)が成り立つ。
  • ステップケース(前提に3つ組が出る)
    • E_Seq: 任意のc1,st,st',st'',c2について、P(c1/st⇓st')とP(c2/st'⇓st'')が成り立つなら、P(c1;c2/st⇓st'')が成り立つ。
    • E_IfTrue: 任意のb,st,st',c,c'について、bがstのもとでtrueに評価され、P(c/st⇓st')が成り立つなら、P(IF b THEN c ELSE c'/st⇓st')が成り立つ。
    • E_IfFalse: 任意のb,st,st',c,c'について、bがstのもとでfalseに評価され、P(c/st⇓st')が成り立つなら、P(IF b THEN c' ELSE c/st⇓st')が成り立つ。
    • E_WhileLoop: 任意のb,st,st',st'',cについて、bがstのもとでtrueに評価され、P(c/st⇓st')が成り立ち、P(WHILE b DO c END/st'⇓st'')が成り立つなら、P(WHILE b DO c END/st⇓st'')が成り立つ。

帰納法の原理はP(c/st ⇓ st')の形をしているので、これを示したいことである「任意のc,st,st'について、~( (WHILE b DO c END) / st ⇓ st' )」に合わせるには、P(c0/st0⇓st0')をcを固定した上で
「c0=(WHILE b DO c END)ならば、false」*2と、命題中でならばを使う。
これで示してみる。

  • Boolean式bはBTrueと等価とする。c,st,st'は固定する。
  • Pを上のように定義し、Pをcevalのの帰納法(この3つ組の導出についての帰納法)で示す。
    • E_Skipについて。P(SKIP/st0⇓st0)を示す。これは、「SKIP=(WHILE b DO c END)ならば、false」だが、「SKIP=(WHILE b DO c END)」というのは構文的におかしい。前提が偽なので、全体は真。
    • E_Assについて。これも同様に前提が「(l::=a)=(WHILE b DO c END)」となってしまって構文的におかしい。
    • E_WhlieEndについて。「bがstのもとでfalseに評価されるならば、P(WHILE b DO c0 END/st⇓st)」を示す。ところが、式bはBTrueと等価なので、前提の「bがstのもとでfalseに評価されるならば」が常に偽になり、全体が真になる。
    • E_Seqについて。「(c1;c2)=(WHILE b DO c END)」となり構文的におかしい。
    • E_IfTrueについて。やっぱり構文的におかしい。
    • E_IfFalseについて。やっぱり構文的におかしい。
    • E_WhileLoopについて。「bがst0のもとでtrueに評価され、P(c0/st0⇓st0')が成り立ち、P(WHILE b DO c0 END/st0'⇓st0'')が成り立つなら、false」を示す。
      • bがst0のもとでtrueに評価され、P(c0/st0⇓st0')が成り立ち、P(WHILE b0 DO c0 END/st0'⇓st0'')が成り立つとする。
      • 「P(c0/st0⇓st0')」は「c0=(WHILE b DO c END)ならば、false」である。
      • 「P(WHILE b DO c0 END/st0'⇓st0'')」は「(WHILE b DO c0 END)=(WHILE b DO c END)ならば、false」である。
      • 示したいのは「P(WHILE b DO c0 END/st0⇓st0'')」だったが、これは「(WHILE b DO c0 END)=(WHILE b DO c END)ならば、false」である。なので、「(WHILE b DO c0 END)=(WHILE b DO c END)」を仮定しよう。ここから、c0=cがわかる。このもとでfalseを導く。
      • 「(WHILE b DO c0 END)=(WHILE b DO c END)ならば、false」と「(WHILE b DO c0 END)=(WHILE b DO c END)」があるので、falseが得られる。示された。

多分、証明を思い付くには、「( (WHILE b DO c END) / st ⇓ st' )」が導出されたとして証明木の一番下がどう導出されたかを見ればよいんだろうなあと思う(?)

*1:Coq上でやろうとして5分行きづまったならとっとと紙と鉛筆をとって証明するべきである。本当に。

*2:この記事の書きはじめは「 任意のc,st,st'について、(c0/st0⇓st0')=(WHILE b DO c END/st⇓st')ならば、~(c0/st0⇓st0')」とやっていてこんがらがって死んでいた。P(c0/st0⇓st0')という書き方から、c0/st0⇓st0'は成立している。