電子情報通信学会の論文誌
ComEX IEICE
に私の論文（正確にはレター）が掲載されました。
タイトルは
A short proof for the multi-deletion error correction property of Helberg codes
私の単著で、
公開日２０１６年２月３日。
内容のキーワードは Helberg codes, deletion error, Levenshtein codes です。
DOIは http://doi.org/10.1587/comex.2015XBL0182。
論文は こちら からDLできます。
是非、ご覧ください。
科学者をやっていると、
いや、
やればやるほど
わからないことに遭遇する。
研究という仕事に限らず、
無論、
ソクラテスの言葉「無知の知」のような高尚な話ではなく、
日常の何気ないことでも
自分の知性や理解の浅はかさに嘆くときがある。
最近だと、酔わないウメッシュのCMがわからない。
どこに向かっているのかわからない。
https://youtu.be/klHx0EZSozo
これはバンド編。
編で終わるからには他のものもある。
https://youtu.be/HGF4pVsvTEs
こちらはデュオ編。
さらにミュージックビデオ
「ワタシは酔わない」なんてのもある。
歌詞の冒頭は
「You Wanna 酔わないウメッシュ」
こういうのをガデムモーター超フル回転と言うのだろうか。
混乱した為かわからないが、最近寝ぼけて、
妻のお尻のにおいをかいだ。
この話はまた今度。
Coq 8.5が公式にリリースされました。
そして、Windows版の SSReflect, MathComp もリリースされました。
早速インストール＆動作確認しました。
基本的にはインストーラをクリックするだけなのですが、
ノウハウとして
入手方法やインストールの方法を
メモしておきます。
気を付けることは、
これまでに Coq と SSReflect, MathComp をインストールしていた場合、
・アンインストールをする
もしくは
・これまでのCoqとは異なるフォルダに
新しい Coq 8.5 をインストールする
ということです。
◆Coq 8.5の入手方法とインストール
Windows版は 32ビット版と64ビット版の二つのインストーラが提供されました。
２０１６年１月２２日現在では、どちらも
https://coq.inria.fr/download
から入手可能です。
ここからインストーラをダウンロードして、起動します。
あとはインストーラの指示に従うだけでOKです。
途中でインストール先を選択する画面が現れます。
上に述べましたが、
もしも他のバージョンの Coq が既にインストールされていたら、
・それらをアンインストールする
もしくは
・Coq 8.5 を他のCoqとは異なるフォルダにインストールする
のどちらかにすると良いでしょう。
◆SSReflect/MathCompの入手方法とインストール
Windows版 Coq 8.5 をインストーラからインストールした場合、
SSReflectやMathCompのバージョンは 1.6 を使うことになります。
こちらにもWindows版インストーラが用意されています。
下のURIからダウンロードできます。
http://ssr.msr-inria.inria.fr/FTP/
インストーラは３２ビット版と６４ビット版の両方が提供されています。
それぞれ
ssreflect-mathcomp-installer-1.6-win32.exe
ssreflect-mathcomp-installer-1.6-win64.exe
という名前がつけられています。
先のURIの先にあるHPの下の方にあります。
インストールはインストーラをクリックするだけでできます。
途中でインストール先を選択する画面が現れます。
その際には、Coq 8.5で指定したディレクトリ名をそのまま指定してください。
以上でインストールは終わりです。
◆動作確認
Coqを起動するには
スタートメニューなどから
CoqIDE
を選んでください。
SSReflect/MathCompを読み込むには
CoqIDEのスクリプトエリアに
From mathcomp
Require Import ssreflect.
と入力し、CoqIDEの一行読み込みボタンをクリックしてください。
上部にあるアイコンのうち、左から３番目の ↓ のことです。
入力した上の２行「From … ssreflect.」が緑色に変われば
正しく動作しています。
