読者です 読者をやめる 読者になる 読者になる

combine: マクロのいらないRustのパーサーコンビネーター

はじめに Rustには有名なnomというパーサーコンビネーターライブラリがあるが、せっかく高級な型システムと最適化があるのにマクロで何とかしようとするのは勿体無いと思うので、マクロに深く依存しないcombineを使ってみた。 combineの主な特徴 parsec リス…

OCamlのformat (型安全なprintf/scanf) の仕組み

OCamlのPervasives (デフォルトでopenされるモジュール) には、Printf/Format/Scanfで使うための format という型がある。OCamlの特殊機能として、型推論時に文字列リテラルにstringではなくformatという型がつくことがある。 $ ocaml OCaml version 4.04.0+…

C言語で部分適用したい!(実は、できるアーキテクチャがあるんです)

通常、C言語の関数ポインタは、クロージャではない。したがって、関数を部分適用したり、カリー化したり、ローカル変数をキャプチャーした関数ポインタを返したりすることはできない。しかし、実際にC言語が動作する環境のなかには、そのようなことが実現で…

巻き舌できるようになった(たぶん)

これまで巻き舌ができなかったが、今日ふと試したらできるようになった。巻き舌といっても、舌を変な形にするほうではなく、Rの音を出すほう。あんまり参考にならないかもしれないけど、一応どんな風にやったか書いておく 舌を意図的に動かす ロシア語やイタ…

ランサムウェアを作ってみた(シェルスクリプトで)

ランサムウェアの暗号化部分についての実証コードを書いてみた。暗号の計算にはOpenSSLのコマンドが使えるので、シェルスクリプトを使って書いた。github.com 注意 このコードを試して起こった損害について作者は責任を追わない。基本的にdocuments/以下にあ…

とある偽シャッフルアルゴリズムとその分布

次のようなシャッフルアルゴリズムを考える(簡単のためrand()%Nと表記したが、この部分で0以上N-1未満の一様な整数乱数が生成されると仮定して議論する)。出力されるものは 0, ..., 255 を並び換えたもの(置換)である。 std::vector<int> a(N); for(int i = 0; i </int>…

C/C++の静的解析ツール・事例まとめ

C/C++の静的解析は、どう考えても大変なんだけどどう考えても需要が高いので、やはり色々なソフトウェアや事例があるようだ。まとまった情報が欲しいけど見つからなかったので自分の調べた範囲でまとめることにした。他にも耳寄りな情報があったら教えてほし…

latexmk設定メモ

LaTeX文書のコンパイルをよしなにやってくれるlatexmkについて。全体設定である ~/.latexmkrcには以下のように記入してある。 #!/usr/bin/env perl $pdf_mode = 3; $latex = 'uplatex -kanji=utf8 -synctex=1 -file-line-error -halt-on-error -interaction=…

volatileとatomicの違い

volatileとatomicの違いを調べるために、以下のC++プログラムをコンパイルしてみる。 #include <atomic> void func1(int *p) { ++*p; ++*p; } void func2(volatile int *p) { ++*p; ++*p; } void func3(std::atomic_int *p) { ++*p; ++*p; } $ g++ -std=c++11 -pthre</atomic>…

文脈自由文法(CFG)と解析表現文法(PEG)をHaskellのモナドで説明する話

文脈自由文法(Context Free Grammar) と 解析表現文法(Parsing Expression Grammar) は記法が似ているものの、その性質は大きく異なっている。しかし、以下のようにHaskellのモナドを用いて、左再帰的でない文脈自由文法をそのままパーサーコンビネーターと…

GCC拡張の無効化 (と、それにまつわる細かい話)

端的に言えば-pedantic-errorsを使えばよい。(できれば-std=...も併用したほうがいいだろう)以下解説GCCのC/C++コンパイラは、独自の拡張機能を導入している。これを無効化するオプションには2種類あり、意味が異なる。 C標準と矛盾する拡張機能を無効化する…

64bit windows上でのalloy* (hola)

Alloy (hola) のバックエンドはSATソルバであり、いくつかのバックエンドから選べる。しかし、64bit windows上の64bit JREでは、SAT4J以外は動作しない。以下の手順で自分でjarを作成すれば、minisat等が動くバイナリが作れる。 kodkodのネイティブライブラ…

C++11 random 覚え書き

C++11以降では<random>ヘッダで良質な擬似乱数を得ることができる。 #include <random> 外部からの乱数 外部から乱数を得るにはrandom_deviceを使う。 #include <random> #include <iostream> int main() { std::random_device rand_dev; std::cout << rand_dev() << std::endl; std::cout << r</iostream></random></random></random>…

いわゆる「中卒」は数学/情報オリンピックには参加できるのか否か

「高校生に相当する年齢だが、高校等の教育機関に在学していない」場合、数学オリンピックや情報オリンピックには参加できるのか、という問題がある。該当する組織に直接訊ねるのが最も正確だと思われるが、2015/06/26時点の資料を読む限り、おそらく以下の…

C言語(標準)にM_PIは無い

C言語で円周率πを使うには M_PI を使う、と経験で知っている人は多いが、あれは実はC言語の規格には含まれていない。むしろ、処理系がM_PIを定義してはいけない事情(c - Using M_PI with C89 standard - Stack Overflow)がある。 ここでは、C言語の最新規格…

GW-450DやWN-AC433UKをRaspberry Piで使う

planexのありがたい記事を参考に作業。環境としてはRaspbian wheezyを仮定。おおまかな流れ : まず、下準備としてカーネルモジュールのビルドに必要な道具を揃える(既に揃えてある人はスルーしてよい)。続いて、ドライバのソースコードを取得し、必要な変更…

Coqの新機能、Primitive Projectionについて

Coqリポジトリのtrunkを見ると、次の2つの機能が入っていることがわかります。 Universe Polymorphism Primitive Projection Universe Polymorphismは、グローバル定義をUniverseのレベルについて量化した形で定義することができる機能で、型に飾り付けをし…

よく使う Coq.Logic の公理

Coq.Logic にはCoqの集合論モデルにおいて正しい公理や、それらの間の関係が記述されている。ここではその一部を取り上げて、意味を説明する。 前提知識 公理を仮定しない状態では、 Coqの論理は直観主義論理である。 ある2つが「等しい」という命題が証明で…

WindowsでCoqIDEの見た目をWindows風にする方法

%COQ%\share\themes\MS-Windows\gtk-2.0\gtkrc を %COQ%\etc\gtk-2.0 の下にコピーする。ただし、%COQ%はCoqのインストールディレクトリのことを指すとする。たとえば %COQ% = C:\Program Files (x86)\Coq

C++で多倍長整数ライブラリGMPを使う

目的 GCJなど一部のプログラミングコンテストでは既存のライブラリを使用することが認められている。特にC++であれば多倍長整数ライブラリとしてGMPを使うのが妥当であると考えられる。GMPを直接叩くのもよいが、GMPのC++バインディングを使うのが簡単である…

PowerPC64アセンブリ開発環境の整備

目的 PowerPC64アセンブリの演習のための環境を手元で構築する. 最新情報へのリンク 2015/01/11 以下のように事情が変化している。 PowerPC64 アセンブリ開発環境の設定メモに、以下の手順を現在行った場合に起きる問題への対処法がある。 crosstool-ngのバ…

ipc_botの紹介

この記事はTheorem Prover Advent Calendarの22日めの担当記事です.今年の僕の持ちネタの一つですが,ipc_bot というTwitter botを作りました.https://twitter.com/ipc_botこのbotは直観主義命題論理の命題を投げると解いてくれるbotです. 仕組み 証明を…

情報オリンピック予選 2014

情報オリンピックの予選に参加しました.(予選は誰でも参加できます)次のような制約で解くことにしていました. 1番は Wolf RPGエディター 2番は TeX 3番は Scratch 4番は Excel 5番は APL 6番は Bash 結局1と4を解きました. 1番 Wolf RPGエディターで解き…

夏季セミナー参加記&反省会

来年やる人が同じ失敗をしないために色々書いておきます途中で「です・ます」調でなくなっているのは息切れです。めんどくさいので直していません 参加記 端的にまとめます 場所:今年は埼玉の準山奥でやりました。2009年に僕が生徒として参加したときと同じ…

情報オリンピック夏季セミナーの参加記一覧とか

2013/08/26 - 08/30の間、夏季セミナーというのにチューターとして参加していました。以下はその記録として参照できる各種媒体へのリンクです。参考:去年のリンク集 募集案内 実施の概要 参加者のtwitterリスト 発表会の様子(Togetter) その1(AI) その2(グ…

ICFPC参加記

チーム名 qnighy メンバー qnighy (計1名) 記録 08/06 ICFPCの登録期限が目前に迫っていたのでEasyChairに登録する。 08/07 EasyChairに登録するだけではだめで、ICFPCという名前のカンファレンスに論文を登録したことにしないといけないことを知り、論文の…

今週のContest Management System (2)

CMS (Contest Management System) の最近の動向について書いてみようかなと思います企画2週目 DBモデルの修整とインポーターのダイエット lerks(Luca) がDBモデルの細かい問題点をチェックし、修整しています。例えば、アクセス元の許可リストとしてIPアドレ…

今週のContest Management System

CMS (Contest Management System) の最近の動向について書いてみようかなと思います クロアチアと日本での採用 CMSが次の大会で採用されました。 クロアチアの3段階ある国内大会 日本の国内大会のうち、代表選抜合宿 クロアチアでの採用を報告したメールによ…

CoqのtacticをOCamlで書く話

CoqのtacticをOCamlで書いてみたので、同じようなことをしたい人のためにメモ。なお私はOCamlについてはそれほど詳しくないので、そこの正確性については注意が必要。 同じ事をしているtacticがないか探す 同じようなことを考えている人は必ずいるはず。とい…

Advent Calendar Advent Calendar (2012) 12日目

飛び入りで書きます。Advent Calendar Advent Calendar僕が今日紹介するのはLispギャグアドベントカレンダーです。 Lispギャグアドベントカレンダー 2011 Lispギャグアドベントカレンダー 2012 Lispに関するギャグが、かわいい絵とともに書かれています。で…

Re:永続データ構造が分からない人のためのスライド

この記事はCompetitive Programming Advent Calendar 2012の12/01担当分の記事です。永続データ構造が分からない人のために、「Re:永続データ構造が分からない人のためのスライド」というスライドを頑張って作りました。 slideshareで見る SpeakerDeckで見る…

情報オリンピック夏季セミナーの参加記一覧とか

2012/08/25 - 08/29の間、夏季セミナーというのにチューターとして参加していました。以下はその記録として参照できる各種媒体へのリンクです。 募集案内 実施の概要 参加者のtwitterリスト 発表会の様子(Togetter) その1 その2 その3 その4 その5 slideshar…

お久しぶりです

qnighyです。ブログ移行しました。ここまでにあった出来事 東京大学(理科一類)合格 (余裕の点数でした) 情報オリンピック春合宿(チューターとして参加) ICPC国内予選(学内予選落ち) 私立プログラミングキャンプ参加 情報オリンピック夏季セミナー(チューター…

センター試験参加記

前提 qnighyは東大理一志望で、他の大学や科類には興味ない。東大の前期と後期のみ受験予定。 qnighyの強みは数学、弱みは国語。 2012年東大のセンター概要 センター試験は国語・外国語・数学・社会・理科が各200点ずつで最大1000点分の試験を受験できるが、…

Krakatoa and Jessieを用いた、Javaプログラムの正当性&安全性証明(アルゴリズムもあるよ!)

概要 Javaプログラムに専用の記法で満たすべき条件を形式的に記述し、それをCoqの問題に変換して手動で証明する。この記事はCompetitive Programming Advent Calendar 2011およびTheorem Proving Advent Calendar 2011の12日目の担当記事である。 用意するも…

Why 2.30とWhy3のビルド&インストール (Ubuntu)

目的 これに続く記事において、Krakatoa+Why3で証明を行うため。 想定環境 Ubuntu 11.10 (oneiric ocelot) なお、筆者の環境はamd64。 関連パッケージの準備 余計なのも書いてるかも。 $ sudo apt-get install build-essential devscripts dh-ocaml ocaml-no…

IOI2011メモ

07/20 荷物整理 パソコン…一台あれば十分だが、二台持っていった。 衣服…下着は毎日替える。他は適度に使い回し。 書籍…「計算困難問題に対するアルゴリズム理論」を暇つぶし用に。また、競技中は紙の辞書を使用できるので、念のため持参した。(ただし、普通…

高校生がアルゴリズムで世界に挑んできます

2011年7月22日から29日にかけて、IOI2011 (詳細は後述) がタイで開催されます。 以下の4名が日本代表として参加します。 村井 翔悟 (開成) 原 将己 (筑駒) ←自分です 今西 健介 (八千代松陰) 城下 慎也 (灘) 以下では、IOIに関してひと通り説明したあと、今…

第23回国際情報オリンピック(タイ大会)の日本代表になりました。

IOI概要 国際情報オリンピックは、問題を効率よく解くアルゴリズムに対する洞察力を競うためのプログラミングコンテストであり、数学・生物・化学・物理と並ぶ国際科学オリンピックの一つであると同時に、数あるプログラミングコンテストのうちの1つでもあり…

情報オリンピック合宿中止

まえがき 僕のいる地域は東京の隣にある多摩ニュータウンという地域で、地震の被害については交通機関のマヒ以外は無事でした。震災にあっている人のために出来ることは限られているので、はてな経由で200ポイントだけ寄付したのち、元の生活に戻ろうという…

こんなWikipedia○○言語版ってあり?

Wikipediaにはすごい数の○○言語版があります。 Wikipedia:全言語版の統計 - Wikipediaによると現在279言語ですって!その中でも目を引くものがいくつかあったので紹介します。 エスペラント http://eo.wikipedia.org/ http://eo.wikipedia.org/:image:small …

SELinuxを独学したよ。

こんにちは。今回は誰得感の否めないSELinuxエントリです。しかも独学なのでかなり眉唾物です。SELinuxのポリシーをスクラッチで書くのが目的です。既存のポリシーを運用する話ではないです。環境はDebian squeezeです。 SELinuxとは SELinuxは、Linuxにおい…

優先順位つきキューが壊れたのでセグメントツリーを使ってDijkstraを実装してみました。

ネタを思いついたので実装してみました。As priority_queue broken, we tried implementing Dijkstra using RMQ. — Gistオーダーは変わりません。既にRMQの実装が手元にあるのであれば、こっちの実装方法のほうが楽ということもあるかもしれないとだけ言って…

情報オリンピック参加者の皆さんへ

情報オリンピックに参加した皆さんこんにちは。僕はqnighyです。一応すごい人です。予選で終わってしまった人も、本選で終わってしまった人も、これから合宿に行けるという人もいると思いますが、これ以降も競技プログラミングに精進したい!という人のため…

JOIは銀賞でした

20+20+20+6+20japljの呪詛によって4番がエンバグしました。詳細はあとで調べます。

第10回日本情報オリンピック(JOI)本選

出来事 学校でゼミをやってから代々木に直接行った。 いつもの面子との再会と、きゅうりperyaudo組との遭遇。 Practiceはほとんどやらずにずっと駄弁っていた ちなみに今回はVimではなくEmacsを使うことにした 名刺はPractice中に配りまくった。しかし、40枚…

バレンタインチョコ欲しい!キャンペーン

バレンタインチョコ欲しい! 欲しいプレゼントは… BPS バトルプログラマーシラセ ( DVD2枚組 )出版社/メーカー: スターチャイルド発売日: 2004/03/24メディア: DVD購入: 3人 クリック: 157回この商品を含むブログ (25件) を見る 他の人からのプレゼントもお…

TopCoderのコンパイラバージョンって判別むずかしい…

Java バージョンを調べるAPI。 public void printVersion() { System.out.println(System.getProperty("java.version")); } 上記を実行して調べた結果、1.5.0_08でした。 Java‚̃o[ƒWƒ‡ƒ“‚ðƒvƒƒOƒ‰ƒ€‚ÅŠm”F‚·‚é(Javaƒ}ƒXƒ^[) C++ プリプロセッサマクロで…

C++のiostreamは遅いという話

大量の入出力データを扱う課題を解く際に,入出力の処理に cin, cout ストリームを使用した C++ プログ ラムは scanf, printf 関数を使用した同等のプログラムに比べてとても遅くなることに注意してほしい.よっ て,cin / cout ストリームを使用しているの…