2016年8月27日 (土)

モンティ・ホール問題または三囚人問題の拡張とその確率操作シミュレーション

はじめに


近年、J. ローゼンハウスの『モンティ・ホール問題テレビ番組から生まれた史上最も議論を呼んだ確率問題の紹介と解説』という本が出た。この本は、モンティ・ホール問題について詳しく、この本が出る前に私が考えていた問題の拡張についても書かれてしまっていた。この本を読んで、一端は、私がこれ以上、この問題について何か書く必要はないかと思った。が、それからしばらくして、私がやったことも少しは意味があるかと思い直し、私の思考の跡を備忘的に記録するため、ちょっとした確率モデルのシミュレーションに関する論考を足して、レポートにしておくことにした。

続きを読む "モンティ・ホール問題または三囚人問題の拡張とその確率操作シミュレーション"

2016-08-27 21:17:40 (JST) in Perl, シミュレーション | | コメント (1) | トラックバック (0)

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)

2015年10月16日 (金)

quail-naggy.el: 単漢字変換 Input Method for Emacs.

About the "quail-naggy.el"


Windows 用単漢字変換日本語 IME 『風』の実用性とアイデアを受け、将来的に非 Windows 環境や IME 非対応の Windows 用 Emacs でも『風』のようなインプット・メソッドが使えるようにしておこうとして開発されたのが本ソフトである。

quail-naggy.el 本体は、仮想鍵盤の表示がメインで、変換時の辞書引きなどには、同梱の naggy-backend.pl という Perl プログラムをバックエンドとして使っている。

quail-naggy.el 自体は、Emacs に付属している quail/japanese.el と kkc.el を大いに参考にして作った。また、随分前に私自身が作ってほぼ身内でのみ配布した vkegg.el も参考にしている。

バックエンドを使うこともあり、インストールが複雑なのが本ソフトの弱点である。また、Emacs のバージョンの違いによる表示の差も設定を難しくする要因となる。

本ドキュメントでは、その難しいインストール作業をまず説明し、次いで操作方法を説明する。

続きを読む "quail-naggy.el: 単漢字変換 Input Method for Emacs."

2015-10-16 20:05:48 (JST) in Emacs/Meadow, JRF 作成ソフトウェア, Perl | | コメント (5) | トラックバック (0)

2014年3月20日 (木)

Cocolog_Pro_Analyzer:ココログプロ用アクセス解析補助 Greasemonkey

ココログの新しいアクセス解析が 2013年12月に導入され、2014年2月に完全に切り換わった。基本的には便利になって、要望の多いらしい生ログなども将来的に対応していくそうだから、私は大きな不満はない。

ただ、ココログプロを使っていて複数のブログを扱っていると、ブログを横断したデータの閲覧性が低下した点は気になる。そういうのは、前は Perl などで robot を書けば、なんとかなったんだが、今回のアクセス解析は JavaScript がメインの動的なページのため、それが難しい。そのあたりを補うための Greasemonkey スクリプトを書いてみた。

配布物

Cocolog_Pro_Analyzer.user.js。メイン配布物。

count_access.pl。上記をページビューに関して使って生成した JSON の後処理として計数する Perl スクリプトの例。というか私のアクセス解析報告で使う(予定の)スクリプト。

count_access_2.pl。JSON の取得がうまくいかないことがある。そういうときは、手作業でコピペしたテキストを用意するしかない。タイトルのところで改行が入るので、二行ずつで一データのテキストを得てそれを処理する。

続きを読む "Cocolog_Pro_Analyzer:ココログプロ用アクセス解析補助 Greasemonkey"

2014-03-20 03:46:54 (JST) in JavaScript, ウェブログ・ココログ関連 | | コメント (5) | トラックバック (0)

2014年3月17日 (月)

Perl でオブジェクト指向 C++風 その4 HashFreezer

このシリーズの最初の記事からもう3年は経過した。先日、 jrf_semaphore.pl (紹介記事へのリンク)を公開し、そこで、デバッグに便利なテクニックを構築したので、今回はその紹介をする。

このシリーズの方法では、メンバ変数へのアクセスは直接、オブジェクト本体であるハッシュ(のリファレンス)をいじって行う。そのため、メンバ名のミススペルがあると、参照時は undefined なので警告があることもあるが、代入時には何の警告も起きない。しかも、こういうときのミススペルに限ってとても見つけにくい。代入したはずのものが、undefined で参照されて警告があっても、そこから、どの代入にミスがあったか、その推理が簡単にできるとは限らない。

これを避けるには、メンバ変数へのアクセスに、setter や getter の関数をいちいち定義していくという方法もありえるのだが、setter が関数になるのはカッコ悪く、かといって lvalue を取るようにするのは、Perl 5.18.1 の perlsub ですら未だに「実験的」という記述が抜けてなくて怖い。caller でメンバ変数名を判断する実装だと、関数渡しにミスが出る可能性も出てくる。

そこで、思い付いたのが Perl の tie の仕組みを使う今回の方法。ハッシュの代入や参照をいちいちチェックするから速度面で不利になる(はずではある)のだが、$DEBUG 変数で、new のときに使わないよう設定できるようにすることで軽くした(つもり)。

続きを読む "Perl でオブジェクト指向 C++風 その4 HashFreezer"

2014-03-17 18:20:35 (JST) in Perl | | コメント (0) | トラックバック (0)

2014年3月11日 (火)

JRF Flag Semaphore for NES Emulator を作った

私は『Monty Python』(日本版)の VHS ビデオを持っている。そのコントの中に大小さまざまな手旗で、会話というかストーリー(『嵐ヶ丘』)を紡ぐというものがあった。

大学時代、ブラウザは xmosaic か最新の netscape かというころ、ウェブのウィジェットを作るネタを考えていて、ふとそのコントを思い出した。そのころの知り合いが、入力された文字列を元に 3D で文字を表示できるようにしたりしたと聞いていた。私は、そういう技術面でのすごさを出せなくても、ネタ的にクスッと笑えるようなものとして、「手旗フォント」みたいなものを作りたいと思った。

続きを読む "JRF Flag Semaphore for NES Emulator を作った"

2014-03-11 08:00:00 (JST) in JavaScript, JRF 作成ソフトウェア, Perl, ハード | | コメント (8) | トラックバック (0)

2014年3月 5日 (水)

Perl で unpack_bits

Perl の unpack では、ビット表現つまり 2 進数にするための B や b が使える。が、…使えてねぇ!

例えば、

my ($mapper, $four_screen, $trainer, $sram, $vertical_mirror)
  =  unpack("B4BBBB", $ines_flags);


で、$ines_flags には 0x43 でも入ってるとしよう。すると、欲しい値は (4, 0, 0, 1, 1) だ。が、返ってくる値は ("0011", "0", undef, undef, undef) になる。

続きを読む "Perl で unpack_bits"

2014-03-05 06:24:44 (JST) in Perl | | コメント (0) | トラックバック (0)

2014年2月 8日 (土)

hide_img.js:画像のクラス指定に順って閲覧を要クリック化する

暴力表現や性的表現を含むような画像で、「18禁」まではいかないが、「見たくないものを見ない権利」に多少配慮して、何か[おお]いはかけておきたいといったことがある。本サイトではそういうとき、img タグの class に sexual や violence を指定してやると、あとから JavaScript が要クリックの覆いをかけるようになっている。パスワードによる「閲覧制限」まではしない。

例としては《壁紙化:「moecco vol.31」 その1》だと、おとなしめなので覆いを(モデル活動を知らない家族以外の)誰が外してもそれほどの不快がないはず。私の、覆いをかける基準とか哲学みたいなのは、今のところ《デスクトップ壁紙公開についてのこのサイトのポリシー》のコメント欄が参照先になる。

使い方は、次をページ(ブログテンプレートとか)で CSS や JavaScript をロードしてる部分に足すだけ。ただし、私は下のように書かず、CSS はブログ全体のスタイルシートから @import するようにしている。

<style type="text/css">
  @import url('http://jrf.cocolog-nifty.com/archive/lib/hide_img.css');
</style>
<script type="text/javascript" src="http://jrf.cocolog-nifty.com/archive/lib/hide_img.js"></script>


もちろん、hide_img.jshide_img.css はダウンロードして自分のサイトに置いて使ったほうがいい。難しいことはやってないので、ソースを読めるなら、sexual や violence を指定したときの表示等も簡単に変えられるはず。

そして、ブログ記事等を書くときは、img タグに class="sexual" とするか、すでに class="nantoka kantoka" ってのがあれば class="nantoka kantoka sexual"みたいにスペースを開けて sexual を足すだけで機能するはず。このあたりは、自作の「電子小切手」的な広告非表示ツール No_Ad_URL と相性がいい。

ただ、このスクリプト、置き換えた要素の CSS 周りが難しくて、 vertical-align とか float 等のからみで相性良くないページとかはありそうで要注意。このスクリプトのひとことでの紹介は [cocolog:78822199] なんだけど、そこでは float がらみでハマった経験を書いている。

スクリプトのブラウザ対応状況に関しても注意が必要で、スクリプト自体は IE 6 でも動くんだけど、古い IE は CSS の opacity に対応してない。このスクリプトでは、画像を隠すのに CSS で opacity をまず 0.0 して、表示するときに、それを 1.0 にするというトリックを使う。JavaScript を OFF にしてると、opacity が 0.0 で画像が見れなくなり、IE 6 みたいに opacity が効かないと、覆うまでの時間差でチラっと見えちゃう。だから、私のサイトではその辺りの注意書きとして次のようなことをしている。

<style type="text/css">
#nonjs-warning { font-size: x-small; }
#opa-warning { font-size: x-small; opacity: 0.0; }
</style>

(…中略…)

<!-- 下をサブタイトル部分などに挿入 -->
<noscript><span id="nonjs-warning">JavaScript が OFF のため、機能が制限されています。画像が見えなかったり、要クリックの画像がいきなり見えたりする可能性があります。</span></noscript>
<script type="text/javascript">
<!--
document.write('<span id="opa-warning">本サイトには閲覧者が成人であることを前提にした画像があります。御不快、御寛恕願います。</span>');
-->
</script>

(…略…)


「素人」が自分のサイトで使うために作っただけなので、コード品質は「良い」とは言えないと思う。ただ、その程度なのでパブリックドメインが著者たる私の意志。商用だろうが改造しようが、お好きに使っていただいても私は文句言いません。

とはいえ、上で書いたように使う上で注意すべきことが多くて正直、他のサイトでは使いにくいと思う。普及させようとして設定する人と使う人が違うと、導入よりも class 指定のほうが敷居が高いかもしれず、もっと広く、大手がちゃんとした機能として導入するなら、「素人」の私のソースは使わないだろうし。機能の実現性を聞かれたときとかにプレゼンで使うにはいいかも…といったぐらいか。
更新: 2014-02-08,2014-02-12
初公開: 2014年02月08日 17:22:44
最新版: 2014年07月25日 11:16:35

2014-02-08 17:22:42 (JST) in JavaScript, JRF 作成ソフトウェア | | コメント (3) | トラックバック (0)

gengou.js:日付を後付けで元号表示にする

ブログ記事の上の日付とかを西暦から元号に変えるための JavaScript。最初の紹介はいちおう [cocolog:78797141] になるが、ほぼ説明してない。このサイトで使ってるので、どういう感じになるかは PC でこのサイトを見てればわかるはず。使い方は、次をページ(ブログテンプレートとか)で JavaScript をロードしてる部分に足すだけ。

<script type="text/javascript" src="http://jrf.cocolog-nifty.com/archive/lib/gengou.js"></script>
<script type="text/javascript">
<!--
add_event_listener_rewrite_gengou("//div[@class='content']/h2");
add_event_listener_rewrite_gengou("//div[@class='sticky-entry']/h2");
-->
</script>


どの日付を換えるかは、上の add_event_listener_rewrite_gengou の引数の XPath で指定してるので、そこを変えればほぼどんなサイトでも使えるはず。

もちろん、gengou.js はダウンロードして自分のサイトに置いて使ったほうがいい。そのときは、内部で古いブラウザ用にここから取ってきた XPath のライブラリを使ってるので、それもいっしょに置いて、ソースの GENGOU_XPATH_JS で指定すること。(どうせならと、XPath 2.0とかを選ぶ人もいるかもしれないけど。)

ただ、このスクリプト、元号は直近の記事分は変わらないようになってて、「その日以降元号にする」という部分は、ソース直書きになる。そこはソース中の↓の "2014-02-12" を最新の日付に更新しさえすればいい。私は(生きてれば)だいたい3ヶ月ごとに更新していくはず。三つ組の最後の部分は終了日で、ネット時代になってからずっと平成なので null のまま、ソースには「ももくり三年」にちなんだ例が載ってて、"平成%(数)G年%(和)m%(数)d日" と指定して「平成二十六年如月十一日」と漢数字化するような例も載ってる。

var Gengou = [
  [null, "2014-02-12", null], 
  ["平成%G年(%Y年) %_m月%_d日", "1989-01-08", null]
];


一番上でリンクしたひとことでも書いたんだけど、私が死んだあと誰かがここを引き継ぐと、デフォルトでは元号の表示が切れるわけで、そこは少し失礼にあたる。ずっと同じ元号のほうが失礼が薄いという考え方もあるのは知ってるが、私の後継者が万一現れたとき、よくわからないまま、この先のすごい高齢化社会において「新しく若い元号」を認めないような形になるのをむしろ避けたかった。

そういうことだから、このスクリプトを自分のとこにおけないと、私の更新が止まれば元号表示が止まっちゃう。こういうスクリプトの提供は政府がやってくれたら便利なんだけどね…。政府だと責任とか小回りの点で難しかったら、神社の団体とか、特定のデカい神社とかがやってくれたらありがたいのに。(いちおう、最新の JavaScript には Intl.DateTimeFormat とかいう機能があるらしいけど…。)

「素人」が自分のサイトで使うために作っただけなので、コード品質は「良い」とは言えないと思う。ただ、その程度なのでパブリックドメインが著者たる私の意志。商用だろうが改造しようが、お好きに使っていただいても私は文句言いません。
更新: 2014-02-08,2014-02-11
初公開: 2014年02月08日 00:37:43
最新版: 2014年02月11日 23:38:13

2014-02-08 00:37:41 (JST) in JavaScript, JRF 作成ソフトウェア | | コメント (2) | トラックバック (0)

2013年2月23日 (土)

HLPVIEW: プチコンmkII用の簡易アドヴェンチャーゲーム用ルーチン

ハイパーテキストという概念があり、現在の Web が(一部)実現したハイパーリンクのもとになった考え方という見方もある。NCSA Mosaic という最初のネットブラウザーがでてくる以前にも、Mac には HyperCard があったし、90年代のエロゲーの中には、システムを一般化して内部でリンクを辿っていくような処理をしているものもあった。

なんでエロゲーの話が出てくるかというと、私が最初にこの概念に触れたのがそのエロゲーの解析をしていたときだからであるというのは、内緒だ!と宣言しておく。(^^)

ゲーム作りに関心のあるようなゲーマーにとってみれば、そういうストーリーを選択して追うだけの「アドヴェンチャーゲーム」ならば、「プログラム」をしなくても良いという点に売りがある。この点、Web が広まるにつれて、そこかしこでそういうゲームにもっと出くわすようにも私は考えたんだが、そうならなかった。

そういったハイパーテキスト風のリンクを辿って文書を読むしくみを、簡単なものだが、プチコンmkII 用にも実装した。それが STACKLIB に含まれる hlpview.prg である。実際の文書例としては『易双六 PTC』の YSCHELP プログラムがそれになる。

続きを読む "HLPVIEW: プチコンmkII用の簡易アドヴェンチャーゲーム用ルーチン"

2013-02-23 09:53:30 (JST) in JRF 作成ソフトウェア, プチコン | | コメント (2) | トラックバック (0)