ケネディと天使の問題を Isabelle で証明 その３ 悪戦苦闘編

■

概要

ケネディと天使の問題、または、うそつき天使問題、気まぐれ天使問題、三人の天使問題…と言われているものを、定理証明システム Isabelle でその答えが正しいかチェック(証明)した。

これは「その３」で、気まぐれ天使問題について悪戦苦闘した私の「失敗」を扱う。

続きを読む "ケネディと天使の問題を Isabelle で証明 その３ 悪戦苦闘編"

ケネディと天使の問題を Isabelle で証明 その２ 気まぐれ天使問題

■

概要

ケネディと天使の問題、または、うそつき天使問題、気まぐれ天使問題、三人の天使問題…と言われているものを、定理証明システム Isabelle でその答えが正しいかチェック(証明)した。

これは「その２」で、気まぐれ天使問題を扱う。

続きを読む "ケネディと天使の問題を Isabelle で証明 その２ 気まぐれ天使問題"

ケネディと天使の問題を Isabelle で証明 その１ うそつき天使問題

■

概要

ケネディと天使の問題、または、うそつき天使問題、気まぐれ天使問題、三人の天使問題…と言われているものを、定理証明システム Isabelle でその答えが正しいかチェック(証明)した。

これは「その１」で、うそつき天使問題を扱う。

続きを読む "ケネディと天使の問題を Isabelle で証明 その１ うそつき天使問題"

Exhaustive Lock Dependency Emulator その３ 修正とチェック

略して ELDE。マルチプロセスの最も簡単な lock/unlock 機構において、そのロックの依存を総当たり的に調べるプログラムを書いた。その１で「虚実行」も数え上げていたのを修正し、「実実行」のみを対象とするようにした。

前回は、意図しない「虚実行」を含めていたため、他の人がやらないような実装になり、その意味では個性があったかもしれないが、今回こそ、特に工夫のない「車輪の再発明」になっていると思う。ただ、前回の怪我の功名で、違う考え方で作った二つの実装が同じ結果を出すのを確かめることで、エミュレータの正しさを多少ともチェックしているのは優位点かもしれない。「証明」がないのは相変わらずではあるが、いくつかの例で、チェックはできた。

前回も書いたとおり、これはマルチプロセス環境を Perl 上でエミュレートするという話ではまったくない。プログラム自体は、シングルプロセスで終了する形をとる。

今回のアイデアのキモは、グローバルな単一ロックのみを扱うため、ロックは重ならず、プロセスをまたいでそれぞれのロックをシーケンシャルに整列して捉えることができるという点にある。その列をロック仕様として総当りで数え上げ、それに基づくよう実行していく。処理の重なりのうち、簡単なものは省いて効率化する。

なお、「プログラム」をコンテクストに関し「関数的(functional)」でなければならない…という条件を課すのは今回も同様である。すなわち、コンテクストが同じように(同じ lock/unlock 順序で)与えられれば、常に同じ「出力」をしなければならない。

続きを読む "Exhaustive Lock Dependency Emulator その３ 修正とチェック"

The Proofs about Alpha-equivalences in Isabelle

■

Abstract

The word of "occurrence" in terms is useful to explain notions intuitively, which frequently leads proofs into ambiguous and inaccurate ones. With theorem provers on the computer like Isabelle, however, we can handle the proofs strictly and maybe complicatedly. In the archive I show, I proved notions of the lambda calculus on the computer especially about alpha-equivalence(s) handling with occurrences.

The second merit was that though I was lacking confidence about mathematics, I could affirm my proofs were correct because of theorem provers. However, I originally proved the proofs in Isabelle before 1998. When I have proved originally, I certainly have comprehended what I did. Now, I almost don't recognize what I do, but I rewrite the legacy proofs into the present style of the Isabelle2015. Though, I often consider proofs partly when rewriting leads to failure. I can't prove in the recommended style of Isar structured proof, but prove in the style of "apply ... done" proofs with tactics and tacticals.

The proofs about alpha-equivalence(s) of the lambda calculus include the proof of correspondence between the definition of alpha-equivalence using occurrences and that using inductive set, and proofs about connection of the usual notation and de Bruijn notation.

続きを読む "The Proofs about Alpha-equivalences in Isabelle"

Exhaustive Lock Dependency Emulator その２ wait_and_lock

※その１の最後に「「虚実行」またはこの仕組みの大きなミスについて」として追記したようにこのフレームワークには大きなミスが見つかっている。以下は参考のために残しておく議論である。※

その１で、このフレームワークにおいて「入力待ち…は…特殊な枝刈りの仕方」ではないかというアイデアを書いた。本稿では、それを実装してみる。

■

理屈

入力待ちは、最も単純にはループして、他のプロセスが $context を変更するのを待てば良い。しかし、それは普通、非効率的で、このエミュレータだと、探索すべき lock 仕様の木の深さを無限に大きくすることになる。

もう少しマシな方法ということであれば、unlock したあと、次に他のプロセスが lock/unlock するのを待ってから lock する「wait_and_lock」と呼ぶべき機構を考えることができる。この方法を先のフレームワークで実現するには、 lock 仕様を見て、間に他の lock がなければ、それを枝刈りするだけで良い。とても簡易で、枝を伸ばすのではなく枝を刈るのだから効率的ですらある。

続きを読む "Exhaustive Lock Dependency Emulator その２ wait_and_lock"

Exhaustive Lock Dependency Emulator その１ 並列処理の総当り

※最後に追記するようにこの記事には大きなミスが見つかった。以下は参考のために残しておく議論である。※

マルチスレッドまたはマルチプロセスの最も簡易な lock/unlock 機構において、その依存を総当たり的に調べるプログラムを(Perlで)書いた。

総当たり的なので、特に工夫があるといえるわけではなく、おそらく他の方が特に言及することなく為していることについて、たまたま私もプログラムする順番が回ってきたぐらいのことになると思う。「車輪の再発明」だが、調べるよりは自分で作ったほうが早い部類の話で、記号論理をやった人間にとって示唆に富む部分があるという印象を受けたので、ブログに書いておくことにした…といったところ。

これはマルチプロセス環境を Perl 上でエミュレートするという話ではまったくない。プログラム自体は、シングルプロセスで終了する形をとる。

アイデアのキモは、シングルプロセス環境ではあるがプロセスを順に何度も起動し、unlock があったときに環境をすべて保存し、lock があったときに以前 unlock された環境に切り換わると考えることにより、lock/unlock のシミュレーションができたと考える点にある。

続きを読む "Exhaustive Lock Dependency Emulator その１ 並列処理の総当り"

Haskell の callCC で goto を作る

本稿では、callCC を使ってループを作り、まるで goto のように見えるような動作を構成してみる。Haskell は、強く型付けされた関数型言語だが、十分実用的であって、無限ループも普通に書ける。goto が作れたからと言ってうれしいことはないかもしれないが、その動作がおよそ非直観的で興味深く、これはぜひ紹介したいと考えたのが、本稿を書いた動機である。

続きを読む "Haskell の callCC で goto を作る"