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

きくらげ観察日記

好きなことを、適当に。

正規表現エンジン制作入門(2): いろいろなDFA

オートマトンの単位を落としてしまいましたが、正規表現エンジンは作っていきたいと思います。前回定義したDFAを思い出してみましょう。inkar-us-i.hatenablog.comDFAは状態を持ち、入力された文字によってその状態を変えていく機械でした。この図はsが初期…

Haskellでtest/**/*Spec.hsを全部拾ってテストしてくれるやつ

よく忘れるのでメモ {-# OPTIONS_GHC -F -pgmF hspec-discover #-} test/Spec.hsにこの1行を書くだけで、test/内の全部のテストを拾い集めて実行してくれるmainを生成してくれます。 明日は正規表現エンジンのこと書きます。

rsyncでポート番号を指定する

本当は正規表現エンジンについての話を書きたかったのですが、最近まとまった時間が取れないので関係ないことを書きます。タイトルの通り。 $ rsync -e "ssh -p 12345" hoge@fuga.com:/foo/bar/baz/ /piyo/rofi/ これでok

正規表現エンジン制作入門(1): 正規表現とDFA

オートマトンの単位は落としそうですが、今日から数回に分けてHaskellで正規表現エンジンを自作していきたいと思います。 完成図 実は既に手元に完成品があるのですが、今回はHaskellで正規表現風DSLを構築したいと思います。動作例は以下の通り。 >>> str "…

Coqで型クラスで群論

Coq

群論に関する定義をするのであれば、型クラスを使うのが一番うまくいくと思います。 Class Group G := { gunit : G; gadd : G -> G -> G; ginv : G -> G; gadd_unit_l : forall g : G, gadd gunit g = g; gadd_unit_r : forall g : G, gadd g gunit = g; gad…

Coqで型クラスでモナド

Coq

Haskell大好きなので、モナドを実装できそうな言語があればとりあえず実装してしまう癖があります。 Coqでモナド使うほどのことを書くのか、と言われればアレですが。 Class Monad (M : Type -> Type) := { point {A : Type} : A -> M A; bind {A B : Type} …

Coqで型クラス

Coq

Coqにも型クラスがあるらしいです。 Class Ord a := { le : a -> a -> bool }.これでleというメソッドを持つ型クラスOrdを定義できます。インスタンス定義は以下のように行います。 Fixpoint le_nat (n m : nat) : bool := match n, m with | O, O => true |…

Elmの型関連が弱すぎてつらい

Elm

inkar-us-i.hatenablog.comここでやたらElm推してるみたいな書き方をしてしまいましたが、僕自身はそんなにElm好きではありません。 型クラスがない Elmには型クラスが無いため、まともに多相的な関数を書くことはできません。 例えば、Elmには至る所でモナ…

Elm始めてみました。

Elm

Elmという言語を一ヶ月ほど触ってみたので、この言語の特徴などを紹介したいと思います。 Elmとは http://elm-lang.org/この言語はざっくりと言うと、「JavaScriptにコンパイルされる、純粋関数型でHaskellっぽい文法の言語」です。 純粋関数型 ElmはHaskell…

ムシャクシャしたのでテトリスを作った

試験の出来が悪かったので、ムシャクシャして2時間くらいキーボードを叩いていたらテトリスができていました。完成品は以下のURLに上げています。http://monamonamonad.github.io/tetris/Elmはこれくらいの小規模なアプリケーションを書くのに便利ですね。 …

型クラスのインスタンスが複数ある場合の話(Haskell編)

inkar-us-i.hatenablog.comこちらで出した例はScalaでしたが、Haskellでも同様の問題は起こりえます。 -- TreeSet.hs module TreeSet ( Cmp(..) , TreeSet() , empty , insert , fromList , elem ) where import Prelude hiding (elem) class Cmp a where eq…

implicit parameterによる型クラスの罠

Scalaの型クラスは暗黙引数の受け渡しにより行われるため、スコープごとに同一な型クラスの別なインスタンス実装を使うことができます。 例えば、以下のような比較を行う型クラス、Cmpを考えてみましょう。 trait Cmp[A] { def eq(x : A, y : A) : Boolean d…

Smith-Waterman法で配列の局所アラインメントを求める

今度は局所アラインメントを求めます。 前回の大域アラインメントと違って、今度は最も一致度の高い部分文字列を求めるアルゴリズムになります。 type alignment = char option list let maximums_by (key : 'a -> 'b) (lst : 'a list) : 'a list = let rec …

Needleman-Wunsch法により配列の大域アラインメントを求める

アラインメントとは、2つの配列s, tに欠損記号「-」を挿入して、出来る限り2つの一致度が高くなるように並べたものです。 例えば、2つの文字列"ABCD"と"ACDE"があったとき、これは1つめの文字列から'B'を削除して末尾に'E'を挿入たものだと考えるのが自然で…

OCamlの値の比較について

OCamlには2種類の値の比較方法があります。 ==, != これらの演算子は、右辺と左辺が全く同一のオブジェクトであるかを判定します。==という名前は大抵の言語で使われているので、つい癖で値の比較に使用してしまいそうですが、この演算子はむしろSchemeのeq?…

OCamlのmatch文とbegin..end

OCamlにはオフサイドルールは無いので、例えばmatch文をネストした時に、 let rec zip xs ys = match xs with | x :: xs' -> match ys with | y :: ys' -> (x, y) :: zip xs ys | [] -> [] | [] -> [] これは次のように解釈されます。 let rec zip xs ys = m…

教養としてCOBOLに触れてみる

教養として一度くらいCOBOLに触れてみなければダメなんじゃないかと思ったので、COBOL入門としてFizz Buzzを書いてみました。コードはこちら。 000010 IDENTIFICATION DIVISION. this 000020 PROGRAM-ID. FIZZBUZZ. is 000030 AUTHOR. HOGE. a 000040 DATE-W…

Prologでしょぼい型推論器みたいなものを作る

Prologの練習です。 以下で定義される簡単な式の型を推論し、その値を評価します。 * 数値はint型 * t, nilはbool型 * XがT型、YがU型のとき、ペアX & YはT & U型 * FがT -> U型、XがT型のとき、関数適用F $ XはU型組み込み関数はadd, eq, and, neg, car, cd…

Prologならではのソートアルゴリズム

簡単な問題なら問題をPrologの言葉で書いてやるだけで勝手に解けてしまうのが、Prologのすごい所です。 例えばソートに関しても、(計算量とかの話に目を瞑ってしまえば)こんなに簡単に書くことができるようになります。 % sort.pl % remove(X, L, M) : リス…

Coqで代数的データ型の各要素についての等式を得る

Coq

前提 C x y z = C x' y' z から x = x', y = y', z = z' を導くためのタクティックが用意されています。 injection 等式 H : C x y z = C x' y' z' についてinjection Hをすると、ゴールをx = x' -> y = y' -> z = z' -> (元のゴール)という形に書き換えてく…

Coqで等式の左右を入れ替える

Coq

タイトルの通りです。eq_reflをdestructしていい感じにやるような方法でも解けることは解けます。 Goal forall (T : Type) (x y : T), x = y -> y = x. Proof. intros T x y H. (* H : x = y *) destruct H. (* Goal: x = x *) reflexivity. Qed.しかし、等…

Coqのintrosでパターンマッチング

Coq

destructは以下のような代数的データ型 Inductive T : Type := | C1 : x11 -> x12 -> ... -> T | C2 : x21 -> x22 -> ... -> T ... | Cn : xn1 -> xn2 -> ... -> T.の値xに対して、 destruct x as [x11 x22 ... | x21 x22 ... | ... | xn1 xn2 ... ]でパター…

Ubuntuで最新のnode.jsを使う

Ubuntuの標準のリポジトリに入っているnode.jsがバージョン4.1くらいなので、新しめの文法を使おうとすると割とつらいものがあります。github.comNodeSourceという便利なものをどこかの誰かが用意してくれているので、これを使いましょう。これを使うと各デ…

Amazon Dash Buttonが届いたのでとりあえずツイートボタンにしてみた

ついに我が家にもAmazon Dash Buttonが届きました。そのまま使うのも面白くないので、npmのdash-buttonというライブラリを使ってツイートボタンにしてみたいと思います。github.com 注意: dash-buttonはES2015の新文法をバリバリ使っているので、比較的新し…

Quineの書き方

inkar-us-i.hatenablog.com前回の記事で書き初めと称してQuineを書きましたが、実は僕自身Quineを書くのは初めてでした。 書き始める前はQuineは何をやってるかわからない黒魔術にしか見えませんでしたが、実際に書いてみると意外と楽にできることがわかった…

書き初めQuineを書きました

皆様、明けましておめでとうございます。 新年早々インフルエンザに罹り、意図せず寝正月を送っていたのですが、そろそろ体調がよくなってきたので書き初めでもしてみようかと思います。 eval(x="c=($)=>String.fromCharCode($);q=c(34);b=c(92);s=c(59);n=c…

さよならインクルードガード

C

タイトルは嘘です。ある程度経験のあるCプログラマーなら、 #ifndef HOGEHOGE_H #define HOGEHOGE_H .... #endif /* HOGEHOGE_H */ といった定型文をおそらく数百回は書いたことがあるでしょう。 これらを省略するため[要出典]に、#pragma onceというディレ…

JavaでMapの初期化を行う方法いろいろ

Javaの面倒臭さの一つに、Mapリテラルが存在しないというものがあります。普通にMapを使おうとすると、 import java.util.*; class MapLiteralExample { public static void main(String[] args) { Map<String, Integer> hogeMap = new HashMap<>(); hogeMap.put("hoge", 3); </string,>…

プログラミング初心者が最初に選ぶべき言語73選

これからプログラミングを始めようとする人にとって、最初の壁となるのが「プログラミング言語の種類が多すぎて、どの言語を勉強すればいいかわからない」ということだと思います。 今日はそんなプログラミング初心者のために、選ぶべき言語をたった73種類に…

アドホックな多相性の実現方法いろいろ

inkar-us-i.hatenablog.com 先日OCamlのFunctorという新たな多相性の実現方法を学んだので、せっかくなので各言語のアドホック多相性についてまとめてみたいと思います。クラスとその継承ではなく、アドホックな方法で多相を実現する手段はいくつかあります…

OCamlのFunctorという概念を知らずに自分で再発明していた話

最近わけあってOCamlの勉強をしているのですが、OCamlは多相的な関数を定義する方法として、Functorというものを持っています。 (* 要素の型と、その比較方法を定義するモジュール *) module type Cmp = sig type elt val le : elt -> elt -> bool (* <= *) …

機械学習でAV女優かどうかを判定するプログラムを作った

AV女優判定機タイトルの通りです。 Gaucheの練習 & 機械学習の勉強として作ってみました。 ナイーブベイズを用いて、ユーザーの直近の発言内容からそのユーザーが「AV女優、一般男性、一般女性、bot」のうちどれに最も近いかを判定します。このように、AV女…

SWI-Prologを始めてみる

長いこと積んであった『Prolog Programming for Artificial Intelligence』を少しずつ読み始めることにしたので、現在使っているUbuntuにSWI-Prologをインストールすることにしてみました。 $ sudo apt install swi-prolog実行はprologコマンドでできます。 …

OCaml初心者が戸惑いそうな謎記号一覧

^(キャレット) ^は文字列連結の演算子です。 # "hoge" ^ "fuga";; - : string = "hogefuga" +., -., *., /. 浮動小数点数同士の演算には、元の演算の記号の後にドットが付きます。Schemeと同じですね。 # 3.0 +. 4.0;; - : float = 7. <> <>はノットイコール…

Gaucheのwriteのバグ(?)を発見した

全角スペースはwriteでは||で囲われずに普通に表示されるのに、readでは半角スペースと同一の扱いでスキップされます。 gosh> (with-output-to-string (^() (write '| |))) ; 全角スペース " " gosh> (call-with-input-string "| |" read) ; ||で囲わないとr…

nginxで特定のパスを別なポートにリダイレクトする

一般的にはリバースプロキシというらしいです。 Railsで作ったものを12345番ポート、Yesodで作ったものを12346番ポート、Playで作ったものを12347番ポートで公開して、 example.com/railsでexample.com:12345, example.com/yesodでexample.com:12346, exampl…

apacheのポート番号を変更する

apacheのポート番号を12345に変えたいとします。まずは/etc/apache2/sites-available/000-default.confの <VirtualHost *:80> ... </VirtualHost>を <VirtualHost *:12345> ... </VirtualHost>に変更します。次に、/etc/apache2/ports.confの Listen 80を Listen 12345に変更。あとはapacheを再起動すればポート番号が変更されて…

CGIの仕様

とある理由からGaucheでCGIとかいう謎なことをしなければならなくなったので、ここにメモしておきます。 メソッドは環境変数REQUEST_METHODに保存される。 GETパラメータは環境変数QUERY_STRING、POSTのボディは標準入力。ただし、GET/POSTパラメータはGauch…

ApacheでCGIを動かす

今更CGI、と思うかもしれませんが、諸般の事情によりCGIを実行せざるを得ない状況に陥ってしまったので、ここにその方法をメモしておきます。 CGIのモジュールが読み込まれているか確認 少なくともUbuntuのapache2では、cgi_moduleはデフォルトでは読み込ま…

Coqのsplit, left, rightについてもう少し詳しく

Coq

inkar-us-i.hatenablog.com上の記事でandを証明するためにsplit, orを証明するためにleft, rightを使えばいいと書きましたが、実はこれらのタクティックはもう少し一般的に作られています。 split splitはandのみではなく、コンストラクタがC : X1 -> X2 -> …

Coqで「任意のxについて…」「あるxが存在して…」を扱う

Coq

Coqで「任意のxについて…」を表すforall xは、xを受け取って残りの命題の証明を返す関数となっています。 Definition prop_1 : forall (x : nat), x = x := fun x => eq_refl x.また、「あるxが存在して…」を表すexists xは、以下のようなデータ型として定義…

Coqで「…かつ…」、「…または…」を扱う

Coq

連言「かつ」、選言「または」を表すandとorは、Coqでは次のようなデータ構造として定義されています。 Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\ B where "A /\ B" := (and A B) : type_scope. Inductive or (A B:Prop) : Prop := | or_in…

Coqで定理の証明中に補題を示す

Coq

assertタクティックを使うと、証明の途中で他の補題を証明できます。 Goal forall P Q R : Prop, P -> (P \/ Q -> R) -> R. Proof. intros P Q R H1 H2. (* H1 : P *) (* H2 : P \/ Q -> R *) (* 先にP -> Rを示す *) assert (P -> R). { (* P -> R の証明 *…

Coqで前提や定理を適用して証明する

Coq

ゴールが前提や既にある定理そのものである場合が、証明の一番簡単なパターンです。 前提がゴールそのものである場合 assumptionを使うと、前提にあるゴールと全く同じ命題をそのまま適用してくれます。 Goal forall P : Prop, P -> P. Proof. intros. (* P …

Coqで数学的帰納法を行う

Coq

数学的帰納法を行いたい場合は、基本的にelimかinductionのどちらかのタクティックを利用します。 elim こちらが最も基本的な帰納法です。elim x.とすることで、xについての帰納法を行うことができます。 例えば、以下のコードでは直接to_zero n = 0を示すの…

Coqでデータ型に対して条件分岐を行う

Coq

証明中にデータ型に対して条件分岐を行うためには、case, case_eq, destruct等を使います。 とりあえず普通に条件分岐をする caseは普通の条件分岐です。例えばb : boolに対してcase b.とすると、b = trueである場合とb = falseである場合の2つに分かれ、そ…

Coqで定理の特定の項だけを書き換える

Coq

rewriteやsimplを使って定理を書き換えようとすると、どうしても思ったとおりに書き換えがいかないことがあります。 (* 結合法則と交換法則を使って、3つの項を入れ替える *) Goal forall (T : Type) (op : T -> T -> T), (forall x y z : T, op (op x y) z …

Coqで既存の定理、定義に従って計算する。

Coq

定義に従って計算する 定義に従って計算するには、simpl, compute, unfoldが使えます。 simpl.はゴールの式をいい感じに簡単にしてくれるのに対し、compute.はとりあえず式展開します。また、unfoldは定義の左辺から右辺に書き換えます。 Fixpoint fact (n :…

Coqで前提の矛盾から定理を証明する

Coq

矛盾を導く方法は何通りかあります。 すでに前提にFalseがある場合。 まずは一番基本的な方法から。既に前提にFalseがある場合です。 Falseの定義は、以下のようになっています。 Inductive False := (* コンストラクタが1つもない *).従って、前提にP : Fal…

Gaucheで文字列のシーケンシャルアクセス

Gaucheでそこそこサイズの大きい文字列へのシーケンシャルアクセスをしたい場合の注意点です。例として、以下のURLにある『吾輩は猫である』の文書中に、何回「猫」という文字が出てくるかを調べてみましょう。http://www.aozora.gr.jp/cards/000148/card789…