「JRF 作成ソフトウェア」カテゴリ内の記事 このカテゴリをはてなブックマークに追加 このカテゴリを含むはてなブックマーク (初公開日順)

★ ドキュメントのURLの後ろに ?mode=long を付けるとトップページのような表示になります。
[更新日] [タイトル]
[概要]
[初公開日] in [カテゴリ] | [諸データ]
■ 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...

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

■ About the "quail-naggy.el" Windows 用単漢字変換日本語 IME 『風』の実用性とアイデアを受け、将来的に非 Windows 環境や IME 非対応の Windows 用 Emacs でも『風』のようなインプット・メソッドが使えるようにしておこうとして開発されたのが本ソフトである。 quail-naggy.el 本体は、仮想鍵盤の表示がメイン...

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

私は『Monty Python』(日本版)の VHS ビデオを持っている。そのコントの中に大小さまざまな手旗で、会話というかストーリー(『嵐ヶ丘』)を紡ぐというものがあった。 大学時代、ブラウザは xmosaic か最新の netscape かというころ、ウェブのウィジェットを作るネタを考えていて、ふとそのコントを思い出した。そのころの知り合いが、入力された文字列を元に 3D で文字を表示できるよ...

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

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

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

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

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

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

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

プチコン(mkII)の SMILE BASIC には、いわゆる関数定義の方法はないが、 GOSUB & RETURN はある。GOSUB は、変数に入ったラベル名でも OK な優れものだが、引数を取れないので、引数や戻り値をどうやって返すかは、(自分で) 決めておく必要がある。 普通には、A1="A":A2="B":GOSUB @F1:PRINT R といっ...

2013-02-21 04:44:53 (JST) in JRF 作成ソフトウェア, Perl, プチコン | | コメント (7) | トラックバック (3)

2013年正月明けに 3DS と共にプチコンをダウンロード購入。最初から作るものは決めていた。可能ならば、自作の(Web版の)『易双六』を移殖したい…。 しかし、その前には数々の困難が待ち受けるのであった。

2013-02-21 04:29:42 (JST) in JRF 作成ソフトウェア, プチコン | | コメント (9) | トラックバック (1)

ハードのメディアプレイヤーで画像をランダムに閲覧したい。私が持っているメディアプレイヤーに限らず専用ハードのものはたいていそうだが、PC などのソフトではあった、zip にまとめられたものを見るようなことはできず、また、ディレクトリの構造を奥へ奥へと "recursive" に辿って見るような機能もない。フォルダ内のランダム再生はある。 そこでディレクトリ構造を平坦化(flat...

2012-02-09 22:26:15 (JST) in Cygwin, JRF 作成ソフトウェア, Perl | | コメント (2) | トラックバック (0)

私の《ひとこと》サイトで「クロスリファレンス」を張ろうと思い立った。少し試した段階でスパム制限等のため時間がかかることがわかったので、その前に《ひとこと》を「ダンプ」つまりフルバックアップすることにした。 ココログの機能として、他所に移転するのを支援するために、バックアップの機能がもとからあるが、これは、元の URL やトラックバック URL、記事 ID などを記録しないため、今回の目的には適さな...

2012-01-07 14:28:08 (JST) in JRF 作成ソフトウェア, Perl, ウェブログ・ココログ関連 | | コメント (0) | トラックバック (0)

■ このアプリケーションは何? ユーザーとして MovableTyle の機能を XMLRPC から使い、Twitter.com やはてな社が実装する OAuth をユーザー認証に用いることで、CGI のサーバーにリソース・セキュリティが乏しい場合でも、ユーザー追加型の「ひとこと」サイトを一般ユーザーが比較的安心して運用できる Web アプリケーションです。 MovableType のテンプレート...

2011-06-03 05:28:30 (JST) in JavaScript, JRF 作成ソフトウェア, Perl, ウェブログ・ココログ関連 | | コメント (4) | トラックバック (2)

2011年6月30日終了したアバウトミー(aboutme.jp)から、「ひとこと」のデータをココログプロに移転するために作ったツールです。このドキュメントは、移行の手順を示すものです。 あくまで私個人用に作ったもので、あまり多くの人が使うことを想定していません。よってツール類も個人的嗜好と私の労力削減に重きを置いたものになっています。移行まで時間もなく人数が少ないことが想定されるのでそうしています...

2011-04-23 08:56:02 (JST) in HTML/XML/CSS, JavaScript, JRF 作成ソフトウェア, Perl, ウェブログ・ココログ関連 | | コメント (35) | トラックバック (4)

本作は、ずっと以前からアイデアがあり、2005 年ぐらいに sendmail 等のメーラー用プログラムとして一端書き上げたが、組織で運用するようなチャンスもなく、そのままオクラ入りになっていた。死蔵していても無意味だし、せっかく sendmail 等がなくても Perl の標準ライブラリがあれば動くようにしているので、Net::SMTP を直に利用するサンプルとして、私の個人サイトにコソッと置いて...

2010-05-22 21:46:54 (JST) in JRF 作成ソフトウェア, Perl | | コメント (0) | トラックバック (1)

Firefox の .xpi をいじろうとすると、locale の部分で .properties の拡張子を持ったファイルを JAVA で使える形式にしないとダメなんだそうだ。そのためのコマンドとして native2ascii というものが JDK に入っているらしい。 ただ、それだけのために JDK を入れるのもバカらしいので、Perl のスクリプトを書いてみた。native2ascii.pl ...

2006-02-26 05:31:33 (JST) in JRF 作成ソフトウェア, Perl, Windows アプリ | | コメント (1) | トラックバック (1)

Meadow で電子辞書を使うには普通、Lookup を使うところなのですが、使えない辞書も多いようですし、更新も止まっているようなので、 DDwin32 に乗り換えました。 DDwin は起動時のオプションにより、簡単に既存のウィンドウで検索するよう指定できます。そこで突貫工事で Meadow から call-process 関数を使って DDwin に検索語を渡す Elisp を書きました。 ...

2006-02-22 14:41:23 (JST) in Emacs/Meadow, JRF 作成ソフトウェア | | コメント (0) | トラックバック (2)