サクサク読めて、アプリ限定の機能も多数！
トップへ戻る
iPhone 16
www.tom.sfc.keio.ac.jp/~sakai
λ. ICFP Programming Contest 2012 “Lambda Lifter” 連休中は ICFP Programming Contest 2012 を割と頑張ってた。 いつものメンバーのTeamSampouで参加(使用言語はHaskell)。 今回は仕様も簡単でとっつきやすくて良かった。が、結局今年も大したことはできなかったけれど。 レポジトリ: <URL:https://github.com/msakai/icfpc2012> 今回は昨年の田中さんたちを真似て、githubのプライベートレポジトリを使ってみた。(コンテスト終わったので、公開済み) 概要 問題文 採掘ロボのプログラムを書く問題で、2次元のマップが与えられていて、穴を掘ったりして地中にあるラムダをすべて回収して、ゴールに移動するのが目的。ただし、障害物として岩があって、下が安定しない岩はある規則にしたがっ
λ. Closed Freyd- and kappa-categories, John Power and Hayo Thielecke を読んだ。この論文はArrowについて書かれたわけではないのだけど、これでArrowについては大体分かった。Monad が Kleisli category で「計算」を扱うのに対して、Arrowはsymmetric pre-monoidal category で「計算」を扱う。Haskell のデータ型と関数のなすカテゴリからこのカテゴリへの関手を加えた構造を Freyd-category と呼ぶ。で、Freyd-categoryはκ-calculusのモデルの一般化であるκ-categoryと等しくて…… いやー、面白いなぁ。
LLDN / キミならどう書く Haskell 編 規定競技 ソースコード: Calc1.hs 資料: Calc1.ppt, Calc1.pdf 自由競技 〜 λ電卓 ソースコード: Calc2.hs ソースコード(修正版): Calc2a.hs 資料: Calc2.ppt, Calc2.pdf
www.tom.sfc.keio.ac.jp
λ. 『抽象によるソフトウェア設計』がついに出版されます 先日、レビュワーを募集していた "Software Abstractions"の翻訳本ですが、ついに来週『抽象によるソフトウェア設計』として出版されることになりました。 2009年のFLTVで告知してから二年も経ってしまいましたが、ついに出版されることになったかと思うと非常に感慨深いです。これは訳者の贔屓目ですが、それだけの時間に見合う素晴らしい仕上がりの本になっていると思います。 抽象によるソフトウェア設計−Alloyではじめる形式手法−(Ｄａｎｉｅｌ Jackson/中島 震/今井 健男/酒井 政裕/遠藤 侑介/片岡 欣夫) この本はAlloyという言語・ツールを用いた形式手法の教科書です。 Alloyというのは、モデル発見器と呼ばれているツールの一つで、条件を与えるとその条件を満たす具体例を探してくれます。モデルというのは、条
λ. Cleanの定関数と定グラフ <URL:http://d.hatena.ne.jp/lethevert/20060601/p1> より。 Haskellはグラフ書き換えによる意味論を言語仕様に採用していないので、言語仕様上はCleanの定関数や定グラフのような概念は存在しない。というか、そもそもHaskellの言語仕様は実行メカニズムをほとんど規定していない。では実際の処理系ではどうかというと、例えばGHCでは(ある種の最適化後に)ラムダ抽象以外の形をしている定義は、すべてCleanでいうところの定グラフとしてコンパイルされる。 full laziness transformation また、full laziness transformation (full laziness optimisation, let-floating) によって、局所的な定義が大域的な定義に引き上げられ
修士論文 2006年度 (平成 18年度) 非正格関数に対して適用可能な融合変換 Fusion Transformations Applicable to Non-Strict Functions 慶應義塾大学大学院 政策・メディア研究科 酒井 政裕 修士論文要旨 2006 年度 (平成 18 年度) 非正格関数に対して適用可能な融合変換 概要 関数型言語が広範な関心を集めており、関数型言語最適化の手法としてプログラム変換、特に融 合変換の重要性が高まっている。 Haskell のような純粋関数型言語は参照透明であり、未定義な値や停止しない計算を含む参照透 明な言語の数学的モデルは、非正格な関数 (未定義な引数値に対しても値が定義される関数) を含 む圏となる。 しかし、CPO と正格な連続関数の圏では再帰的データ型を始代数として解釈可能であるが、 CPO と (正格なものに制限されない
λ. iteratee I/O勉強会 に参加。詳しくはmaoeさんのブログなどを参照。 Tweetvite :: iteratee I/O勉強会 Lazy I/O must go! - Iteratee: 列挙ベースのI/O - 純粋関数型雑記帳 maoeのブログ HIMA' #1: iteratee I/O勉強会 - maoeのブログ iteratee I/O勉強会 - maoeのブログ iteratee law とかないのなと思う。 IterVがMonadであることを含意するのが最低限の条件。 それと、以下の iteratee-0.4 での定義をCPSスタイルと言っていたけど、感じとしてはIterVMのモナディックなチャーチエンコーディング(?)を考えているような雰囲気だと思った。もう少しちゃんと考えたいところだけど。 iteratee-0.2 での定義: data IterVM e
Gimp 使用者のための Ruby 入門: 酒井政裕 著、Copyright 2001 GDPCL に基づいて配布 38.0 まずはじめに 初めに断っておきますが、これはGUMの「Gimp 使用者のための Scheme 入門」のパクリです。「入門」と書いてありますが、正直この文章で入門するのは避けた方が良いかと。それと、画像はまだ差し替えていないので、微妙に違いますが、気にしないで下さい。 38.1 はじめに Gimp のすばらしい機能の一つとして、全ての機能がスクリプト(というかPDB)を通して利用できるということが挙げられる。Gimp で使用される主なスクリプト言語として Scheme があるが、この文章で扱うのは Ruby である。この文章は Script-Fu と比較しながら、Ruby-Fu の簡単な紹介をする。 38.1.2 お約束 Ruby-Fuでスクリプトを書く際には、通常、
λ. Whyでバブルソートの正当性を示す 計算機言語で定理証明 (Proof Party.JP)のときには、Jahobというツールを使って色々やってみたが、最近Whyという似たツールを知ったので、こっちでも同じようなことをやってみる。 まずは、Jahobでも試したバブルソートの例*1。 BubbleSort.java これを gwhy BubbleSort.java としてgwhyを起動すると、Proof Obligation が抽出されて一覧されるので、あとはメニューから「Proof」「Prove all obligations」とかを選べば定理証明器などが走って証明をしてくれる。 定理照明器としては、Alt-Ergoしかインストールしていなかったけれど、この例ではあっさり全 Proof Obligation が証明された。 以下が結果の画面。 gwhyのこのインターフェースはテストツー
λ. STモナドとSTRefをHaskell上で実装する [FAQ]Haskellには副作用があるのか、ないのか の話。 kazu-yamamotoさんはSTモナドを、「処理系の力を借りないといけないモナド」で、副作用や参照透明性の観点からはStateモナドと本質的に違うものだと主張している。 だけど、STモナドが処理系に組み込まれている理由は効率のためであって、意味的にはStateモナドと大差ないし、効率とあと細かい点を気にしなければHaskellレベルでも実装できるはず。 というわけで書いてみたのが以下のコード。 {-# LANGUAGE Rank2Types, ExistentialQuantification #-} import Control.Monad.State import qualified Data.IntMap as IntMap import Unsafe.Coe
λ. 超集合論 - circularityの論理の現在 - こないだの「ラッセルのパラドックス100年」の時の資料。 Quoation 一方，帰納法の双対である余帰納的(co-inductive)構成は，トップダウン的な確認の論理であり，対象が地に足がついているかどうかには関心がない．すなわち循環構造をも受け入れる論理である．しかしながら，その循環性の論理による統制は，帰納的構成の場合とおなじくらいに堅固である．このことは帰納法と余帰納法の間に「双対性」が成り立つことがその根拠である．ブール代数である定理が成り立てば，その双対の定理も成り立つという良く知られた双対性定理というメタ定理の類似である．余帰納法は，「悪循環」ではない，「正しい循環」のために論理といえよう．
λ. 関数型プログラマにとっての副作用 「Haskell に副作用なんて、あるわけないじゃん。大げさだなぁ」(死亡フラグ)と思っていたけれど、HAMA#3の話をみて自分の考え方を整理できた気がするので、ちょっと書いてみる。 入出力は副作用? 命令型プログラマに説明するときの便法としては、kazuさんの説明は確かに効率が良いとは思うものの、自分がこの説明をするのには結構抵抗がある。 どこに抵抗があるのかというと、その背後にある「入出力するなら副作用がある、Haskellは入出力する、だからHaskellには副作用がある。」というような考え方。 この考え方では、言語がどのようなものであろうと、最終的に実行時に計算機上の現象として入出力が発生すれば、副作用が存在するということになってしまう。 しかし、関数型プログラマにとって、副作用とはあくまでも言語や式の性質であって、実行時に計算機上で発生する
λ. iPhoneのSMSのバックアップ iTunesがバックアップしているファイルが、Windowsならば c:/Users/ユーザ名/AppData/Roaming/Apple Computer/MobileSync/Backup/iPhoneのID?/3d0d7e5fb2ce288813306e4d4636395e047a3d28.mddata とかにあるので、このファイルをバックアップしておけばよい。 このファイルはSQLiteのファイルなので、sqlite3 -csv -separator ',' 3d0d7e5fb2ce288813306e4d4636395e047a3d28.mddata "select * from message;" > output.csv でCSVに変換できる。
λ. 有限領域での推移閉包の公理化 昨日も書いたように、推移閉包は一般には一階述語論理では表現できないので、領域を有限に限定した場合でも領域のサイズの上限 n に依存した形、たとえば以下のような形でしか表現できないと思い込んでいた。 ∀x,y. Tk(x,y) ⇔ R(x,y) ∨ σ1 ∨ … ∨ σn-2 where σn := ∃z1,…,zn. R(x,z1) ∧ R(z1,z2) ∧ … ∧ R(zn-1,zn) ∧ R(zn,y) Automating First-Order Relational Logic なんかでも、「The transitive closure is obtained by applying an operator that computes closure using iterative doubling, as explained in [15].」
λ. “Referential transparency, definiteness and unfoldability” by Harald Søndergaard and Peter Sestoft Chatonのhaskell-jpルームで2009-07-03と2009-07-04にあった、参照透明性と副作用の定義に関わる話で出てきた論文。積読論文の中にあったので読んでみた。 参照透明性(referential transparency)はQuineによって考えられた概念で、LandinとStracheyによってプログラミング言語の性質として使われるようになった。が、その定義・使われ方は変化しており、それらは同値ではないという話。 それらを、この論文での呼び方で呼ぶと以下のような感じ。 確定性 (definiteness) 変数がそのスコープの中で単一の値を持つこと。xを変数とすると
次のページ
このページを最初にブックマークしてみませんか？
『www.tom.sfc.keio.ac.jp』の新着エントリーを見る
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
