« quail-naggy.el: 単漢字変換 Input Method for Emacs. | トップページ | モンティ・ホール問題または三囚人問題の拡張とその確率操作シミュレーション »

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.
Contents


In the archive, we have *.thy files, which are the proofs. I dedicate the works to the Isabelle2015. If you want to load all of the works into the Isabelle2015, you open AllLambda.thy from jEdit or console system. (With jEdit, at first you must select Logics_ZF of logics of Theories panel, and restart Isabelle2015, and open AllLambda.thy.)

Though the Isabelle2015 have many mechanisms of documentation, I don't leave comments at all, because I write above that now I don't recognize my work correctly.

In the "legacy" directory of the archive, I put the legacy proofs on Isabelle before 1998 for reference. It may be convenient if you must prove the same lemmas in the future. They are more readable than those for the Isabelle2015. The legacy proofs were the contents of my master's thesis in Hokkaido University.

The tutorial advice bound variable should be rewritten by rewrite_tac, but I can't obey the advice, because the number of bound variables is many in complicated proof and the temporal names isn't changed from the legacy proof for the most part.


Homepage


I put the archive in a page of my blog which is written in Japanese. The page is below:

Author

License


The author is a Japanese.

I intended this program to be public-domain, but you can treat this program under the (new) BSD-License or under the Artistic License, if it is convenient for you.

Within three months after the release of this program, I especially admit responsibility of efforts for rational requests of correction to this program.

I often have bouts of schizophrenia, but I believe that my intention is legitimately fulfilled.


Distribution

isabelle_TheLambda.tar.gz. The same contents above.




要約


項の中の「出現」という語は、概念を説明するのに便利だが、しばしば、証明をあいまいで不正確なものにしがちである。しかし、それを Isabelle のような定理証明システム上で行うなら話が違う。その証明は、たとえ複雑なものになったとしても、とても厳密なものにできる。このアーカイブでは、ラムダ計算の特にα同値性に関して出現を用いて証明を行った。

この証明の第二の「売り」は、私が数学に関して素人で信用がないにもかかわらず、定理証明システムを使っているがゆえに正しいと肯定できるとう点にあった。しかしながら、元々、この証明は Isabelle 上で 1998 年以前になされたもので、そのころ証明したときには、何をやってるかを自分で理解できていたが、今や、何をやっているかを理解しているとはいい難い。今回やったのは、昔の証明を今の Isabelle2015 のスタイルに書き換えることだけである。もちろん、書き換えがうまくいかないことがあって、しばしば考え込むことがあったが、証明の大枠の理解は抜け落ちている。書き換えるだけなので、推奨されている Isar structured proof のスタイルで証明することはできず、apply ... done タイプの tactics と tacticals を使う証明のスタイルの終始した。

ラムダ計算のα同値に関する証明では、出現を用いた定義と帰納的定義の一致を証明したり、ラムダ計算の通常の表記法と de Bruijn 表記法の間の関係に関する証明を行っている。


アーカイブの内容


このアーカイブには、*.thy ファイルが含まれていて、それらが、証明になる。 Isabelle2015 用に専念して書かれているため、他のバージョン、例えば次のバージョンでは動かないかもしれないほど依存性が高い。私の証明のすべてを Isabelle2015 に読み込ませるには、jEdit かコンソールシステム上から AllLambda.thy を読み込めばいい。(jEdit では、まず、Theories パネルの論理を選ぶところで Logics_ZF を選び、Isabelle2015 を再起動した上で、 AllLambda.thy を読み込ませる必要がある。)

Isabelle2015 はドキュメント化のための様々な便宜を提供しているが、それらはまったく利用せず、コメントすら残していない。上にも書いたように現在の私は証明を理解しているとは言い難いというのがその理由の一つである。

アーカイブの中の "legacy" ディレクトリには、1998年以前にやった証明を一応含めておいた。もし、読者が私と同じ証明をすることになったら、 Isabelle2015 上の証明より、legacy な証明のほうが参照しやすいと思ったからだ。なお、legacy な証明は、私の北海道大学での修士論文(相当)の内容だった。

チュートリアルでは、束縛変数名を証明内で参照するときには、rewrite_tac を使って名前を与えよとアドバイスしているが、それにはしたがえなかった。最初はしたがおうとしたが、束縛変数の数がとても多くなり、それでも、 legacy な証明とほとんどの場合、名前の使い方が変わっていないことから、結局、ひよった。


このアーカイブのホームページ


アーカイブは、私の(日本語の)ブログ内の一ページに置かれている。その URL は以下の通り:

著者

ライセンス


(上の英語版のライセンスを読んで下さい。)


参考

caeruiro》 の Isabelle Tutorial の日本語訳には特に Exercise を解くときにお世話になった。

Isabelle/Isar(その1) - ATPとCASのこと(謄)》。ここでは Isar structured proof が学べる。結局、使わなかったが、将来的に役立てたらいいなと思う。


配布物

isabelle_TheLambda.tar.gz。内容は上と同じ。
更新: 2016-01-07
初公開: 2016年01月07日 15:10:06
最新版: 2016年01月25日 22:48:42

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

JRF 作成ソフトウェア」カテゴリ内の最近の記事

関数型言語・定理証明器」カテゴリ内の最近の記事

批評や挨拶のためのネットコミュニティ

  • はてなブックマーク(って何?) このエントリーをはてなブックマークに追加 このエントリーを含むはてなブックマーク このエントリーを含むはてなブックマーク
  • Twitter (って何?)

トラックバック

この記事のトラックバックURL:
http://app.cocolog-nifty.com/t/trackback/93568/63020574

トラックバックのポリシー

他サイトなどからこの記事に自薦された関連記事(トラックバック)はまだありません。
» JRF のソフトウェア Tips:The Proofs about Alpha-equivalences in Isabelle (この記事)

コメント

diamond 初公開:isabelle_TheLambda-20160107.zip。バージョン番号は付けない方針だが、あえて付けるならバージョン 0.01。

初公開後、上のドキュメントで Logics_ZF を選んだ上で Isabell2015 の再起動をしたあと、AllLambda.thy を読み込む旨を書き足した。それをドキュメントに反映したバージョンは一週間後くらいに公開する予定。

投稿: JRF | 2016-01-08 13:29:19 (JST)

spade 更新:isabelle_TheLambda-20160113.zip。バージョン 0.02。

主にドキュメントの書き換えのみ。あとは、証明で back を使っていた三ヶ所を使わないように書き換えた。新しい定理などはない。

投稿: JRF | 2016-01-13 00:18:56 (JST)

コメントを書く



(メールアドレス形式)


※匿名投稿を許可しています。ゆるめのコメント管理のポリシーを持っています。この記事にまったく関係のないコメントはこのリンク先で受け付けています。
※暗号化パスワードを設定すれば、後に「削除」、すなわち JavaScript で非表示に設定できます。暗号解読者を気にしないならメールアドレスでもかまいません。この設定は平文のメールで管理者に届きます。
※コメントを書くために<b>ボールド</b>、<pre>詩文やソースコード</pre>、<a href="">リンク</a>、その他のHTMLタグが使えます。また、漢字[かんじ]でルビが、[google: キーワード] で検索指定が使えます。


ランダムことわざ: 猿も木から落ちる。