「関数型言語・定理証明器」カテゴリ内の記事 このカテゴリをはてなブックマークに追加 このカテゴリを含むはてなブックマーク (初公開日順)

下記のほか、雑記にある論理学情報工学・コンピュータ科学のカテゴリにも関連記事があります。

2016年1月 7日 (木)

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"

2016-01-07 14:20:18 (JST) in JRF 作成ソフトウェア, 関数型言語・定理証明器 | | コメント (2) | トラックバック (0)

2011年7月 1日 (金)

Exhaustive Lock Dependency Emulator その2 wait_and_lock

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

理屈


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

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

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

2011-07-01 22:37:18 (JST) in Perl, シミュレーション, 関数型言語・定理証明器 | | コメント (1) | トラックバック (0)

2011年6月20日 (月)

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

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

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

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

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

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

2011-06-20 02:54:31 (JST) in Perl, シミュレーション, 関数型言語・定理証明器 | | コメント (2) | トラックバック (3)

2011年1月20日 (木)

Haskell の callCC で goto を作る

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

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

2011-01-20 19:37:45 (JST) in 関数型言語・定理証明器 | | コメント (2) | トラックバック (1)