サクサク読めて、アプリ限定の機能も多数!
トップへ戻る
大谷翔平
keisukenakano.hatenablog.com
TRICK というのは Transcendental Ruby Imbroglio Contest for rubyKaigi の略で, Ruby を使って狂ったプログラムを書くというコンテストで,今回が 2 回めだそうです. 今年の 9 月の FTD 2015 (日本ソフトウェア科学会大会の併設イベント) で TRICK 2015 のことを知り, 遠藤さんから「なにかネタがあったら投稿しませんか」というお話をいただいたので,参加させていただきました. 思いついたネタとしては 3 つほどあって, 実は 3 つとも投稿できる状態にはなっていたのですが, 1 つは完成度的にいまいちだったので投稿を断念し,残りの 2 つを投稿しました. どちらか一方でも審査員の目に留まれば…と思っていたのですが, なんと 2 位と 5 位という非常にありがたい評価をいただきました. ただ,企業の大合併とは違うの
この記事は Theorem Prover Advent Calendar 2013 最終日 (25日目)*1の記事です. 元々このネタは, 後学期の3年生向けの実験でCoqを教える際に提示した 「挿入ソートの正当性を示す」という最終課題の模範解答を作成する際に気づいたことです. このため,ここで紹介するプログラムや証明は, タクティクの種類やライブラリの利用が必要最低限に絞られているので, もしかしたら Coq 初心者の方にも参考になるかもしれません (各タクティクの作用を明確に理解してもらうため,敢えて auto も使いませんでした). Coq 上級者には冗長な証明が気になるかもしれませんが,その点は予めご了承ください. はじめに 比較関数を利用して整列するアルゴリズムは比較ソートと呼ばれ, クイックソートやマージソートをはじめとする多くの整列アルゴリズムがこれに属します (逆に比較ソー
(更新を滞るとずっと侵略されているように見えてしまうので,むりヤリ記事をひねり出すことにしました) さて,今年も 12 月 25 日が近づいてまいりました.皆さんご存知の「ク」で始まるあの日です. そう,クワイン (W. V. Quine) の命日ですね. ということで,今回はクワインの話です.プログラミングを嗜む人であれば,クワインというと, を二度書け! を二度書け! のような「実行すると自分自身を出力するプログラム」を思い浮かべますが, 今回はそういう話ではありません. 彼が残した短い記事を紹介します. といってもだいぶアレンジしているので,興味のある人は元の文献 *1 を読んでください. もうすぐお正月.初詣ではおみくじでその年の運勢を占ったりしますが, みくじ棒の入った筒を振って出た数字から大吉やら凶やらが書かれた紙と交換することがあります. みくじ棒を再利用できるように中から出
OCaml Meeting 2010 の 3 日前である本日 14:30 から,OCaml Golf Competition が開催されます. テクニックの紹介を連載すると言いながら,全然できていなくてすみません.昨年のスライドを修正した内容を掲載します. ユーザ定義関数・変数は1文字で これはゴルフでは当たり前ですね. 空白・括弧の省略 バイト数を短くするには,空白の除去は必須です.除去してよいか迷ったときは「とりあえず省略して動かしてみる」というのが原則です. if i>1then i*2else 6 のように,キーワードの直前の空白は大抵省略可能です.意外な空白も省略できるので,取りあえず消してみましょう.また,括弧についても「取りあえず消してみる」というのが有効です. ;; (ダブルセミコロン) の省略 OCaml では,文と文の間に「;;」というセパレータを入れることがありますが
OCaml では,違う型で再帰する多相関数を書くことが難しい. 以下のデータ型 ('a,'b) twist を考える. type ('a,'b) twist = Nil | Cons of 'a * 'b * ('b,'a) twist 例えば,次の値はデータ型 (int,bool) twist を持っている.let twist_data = Cons(1,true,Cons(false,2,Nil)) このデータ型に対し,長さ(Consの個数)を求める関数を定義してみよう.let rec length = function Nil -> 0 | Cons(a,b,rest) -> 1 + length rest 関数 length の定義は自然のように思えるが,実際には ('a,'a) twist -> int という型が推論されてしまい,上記の twist_data には適用できない.
PPL2009 に参加してくださった皆さん,本当にありがとうございました. バタバタしていて,あまり多くの方とはお話しできずにすみませんでした. OCaml Users Meeting を日本で開催する際にはぜひ参加したいですね. 参加希望ついでに,ずいぶん前に書いた OCaml のコードを晒しておきます. 今回は (今回も?) あまり役に立たないお話で,なんとかモルフィズムの一覧です. 以前ここで紹介した代数的データ型の続きみたいなもので, catamorphism や anamorphism や hylomorphism 以外のものも実装しています. ここで実装しているのは以下の14個のほげほげモルフィズム (説明はテキトー) です. 全部知っているという人はかなりのマニアです. catamorphism list でいう foldr anamorphism cata の双対 hylo
10/4まで北京泊・10/5 京都泊・10/6 東京泊・10/7 機内泊・10/8からシドニー泊…という激しいスケジュールを経て NICTA を訪問中です. 最近,再び OCaml のコードをたくさん書く機会ができたので, 久しぶりに OCaml プログラミングに関するメモを公開します. Ruby には p という便利な関数 (メソッド) があってどんな値でも可視化できますが, OCaml だと自分で書かなきゃいけなくて面倒です. extlib に Std.print という関数がありますが,これは実行時の値を出力する関数なので, 実行時に単なる組になってしまうレコードやバリアントではフィールドやコンストラクタの名前が失われてしまい,十分な可視化ができているとは言えません.このため,結局自分で書く必要があります. 今回紹介する print.ml はそれを補助するプログラムで,先日公開した
草言語Grassが流行っているようなので,Grassプログラミング支援ツールGlidを公開します. Objective Camlで実装されているという点ではYTさんに先を越されてしまいましたが, より多くの機能を提供しています. といっても,実装の効率はあまりよくないので,速いGrass処理系が欲しいだけの方にはあまり役に立ちません. Glidは,簡単にいうと言語Grassと言語Letの間の双方向の翻訳ツールです. 言語Letは,次の文法で与えられる単純な関数型言語でGrassよりは楽にプログラムが書けます. Prog := Def* Def := let Var Var* = Exp Exp := Var | Exp Exp | let Var = Exp in Exp | Exp;Exp Var := In | Out | Succ | W | [_a-zA-Z0-9]+ 主な使用目的
この日記のタイトルになっているラムダ式「λx. x K S K」は, 「*1の一点基底」と呼ばれるコンビネータで, 全ての閉ラムダ式はこのコンビネータ X = λx. x K S K から構築することができる. このことは,S と K がそれぞれ X (X X) と X X X で表現できることから確認できる. このような一点基底は多数知られている. ベーム*2による一点基底 X = λf. f (f S (K K K I)) K *3 を用いると, S と K をそれぞれ X (X X) と X X で表すことができる. また,バーレンドレヒト*4は,X = λf. f (f S (K K)) K という一点基底を提案しており, この X により,S と K はそれぞれ X (X X X) と X X X で表現できる. 現在のところ,フォッカー*5による X コンビネータ X = λf
前の記事のコメント欄で shinh さんから私の投稿した Brainfuck の Quine が実は世界記録ではないかという指摘があったので一応メモ. 負数のメモリ番地は反則らしいので,投稿した 392B (改行除く,以下同様)ではなく shinh さんの書き直した 404B が最短となる. 以下に簡単な解説を示すが,以前までの記録であった(と思われる)410B のものも全く同じ構造をしている. Brainfuck での Quine は,大まかに 3 つのパート A, B, C に分けられる. 具体的には,(A)「B+C」を表現するデータ列を生成, (B) A のデータ列から「A」自身を表現するデータ列への変換(同時に元のデータ列も複製), (C) 作られたデータ列の出力処理(つまり「A+B+C」が出力される),という構成になっている. 最初に投稿した 587B のものでは,B の部分で,
Haskell の場合,任意の関数 f に対し, `f` のように `(バッククオート)で囲むことにより中置演算子(infix operator)として用いることができる. 一方,OCaml でユーザが定義できる中置演算子は一部の記号に限定されている. 以下では,OCaml で任意の関数を中置演算子にしてしまう狡い(?)方法を紹介する. まず,次のような中置演算子を定義する. let (<|) x y = y x and (|>) x y = x y この <| と|> を使うことにより, Haskell のように簡単に中置演算子化することができる. たとえば,二引数の最小値をとる関数 min に対して, 3 <|min|> 4 と記述することができる. 後ろの |> は実際何もしてないのだが, 演算子の優先順位の都合上 (3 <| min) 4 などと書く必要があるため, あまり中置演算
先日,フランスの XML 関係の研究者と共著する機会があり, 「こっちの方が早いだろ」「いやココを変えればこっちの方が」 「いやいやまだまだ改善できる」だの OCaml のコードで文通をしたりしていたが, そんな中,相手のこの一行に愕然としてしまった. external set_field : 'a -> int -> 'b -> unit = "%obj_set_field" 確かに,効率的な実装を実現するうえで Obj モジュールを使うことはたまにあるが, ここまでやってしまうとは. というわけで,今日は Obj モジュールについて少しだけ触れる. ただし,この記事は Obj モジュールの利用を推奨するものではない.むしろ禁止したい. また,その性質からバージョンによって動作しない可能性も高い. ちなみに,以下のプログラムは 3.09.2 での動作を確認している. 「Not for t
OCaml では,let rec を使わずに再帰関数を模倣することができる. 但し「for ループを使えばできる」とかそういう話ではない. 例えば,階乗を計算する関数 fact は,通常 let rec を用いて, let rec fact n = if n > 0 then n * fact (n-1) else 1 と再帰的に定義されるが,次のように let rec を使わなくても定義できる.let turing (`M x) y = y (fun z -> x (`M x) y z) let fact = turing (`M turing) (fun f n -> if n > 0 then n * f (n-1) else 1) ちょっと読み難いが,実際に fact 10 と実行してみれば, 3628800 と正しい出力が得られることが確認できるだろう. このカラクリを支えている
このページを最初にブックマークしてみませんか?
『λx. x K S K @はてな』の新着エントリーを見る
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く