Win8でISEをインストールしてFPGAに回路を書きこむまで
CPU実験が始まりました。先学期のハードウェア実験が終わった後にラップトップのOSをWin8にしてHyer-VでUbuntuを動かすように変更したためISEをWin8にインストール。Hyper-VではUSBポートを転送することができないらしい。フベンだ。インストールの際にいくつかハマる点があったので備忘録として書いておく。
環境
Windows 8.1 64bit
問題1: open projectしようとすると落ちる
インストールがやっと終わってプロジェクトを開こうとするとクラッシュするというのはとても辛い事案だ。解決策はいくつかあるようだが自分はこれを使った。無事open projectになった。
問題2: JTAGが認識されない
無事論理合成ができて回路を書き込もうとするもケーブルが認識されない。とても辛い。ここらへんのことを適当にごちゃごちゃやってたらなんか直った。
結論
辛い
microKanrenで始めるlogic programming入門 (2)
単一化しようぜ
==の動作を見てみよう。
(define (== u v) (lambda (s/c) (let ((s (unify u v (car s/c)))) (if s (unit `(,s . ,(cdr s/c))) mzero))))
前にも説明したように(== u v)はuとvが同一であることを宣言している。この時==は引数のstateであるs/cを拡張してuとvが同じ値になるような代入を持つstateを作る関数を生成する。実際にある代入sの下でuとvが同じ値になるような代入を探すのがunifyだ。
(define (unify u v s) (let ((u (walk u s)) (v (walk v s))) (cond ((and (var? u) (var? v) (var=? u v)) s) ((var? u) (ext-s u v s)) ((var? v) (ext-s v u s)) ((and (pair? u) (pair? v)) (let ((s (unify (car u) (car v) s))) (and s (unify (cdr u) (cdr v) s)))) (else (and (eqv? u v) s)))))
unifyの動作例を並べてみる。
(unify #(0) 3 ()) ; => ((#(0) . 3)) (unify 3 #(1) ()) ; => ((#(1) . 3)) (unify 4 4 ()) ; => () (unify 2 4 () ; 単一化に失敗すると#fを返す ; => #f (unify #(0) #(1) '((#(0) . 1))) ; => ((#(1) . 1) (#(0) . 1)) (unify #(0) 2 '((#(0) . 1))) ; 代入と矛盾してるので失敗 ; => #f (unify (list #(0) 2) (list 3 #(1)) mzero) ; リスト同士の単一化もできる ; => ((#(1) . 2) (#(0) . 3))
microKanrenで始めるlogic programming入門 (1)
microKanrenとは
microKanrenの話の前にまずminiKanrenの紹介を。
miniKanrenは埋め込み言語としての利用を想定した論理プログラミング言語で、実際に各種言語上での実装が存在する。The Reasoned SchemerはminiKanrenをscheme上での実例を示しながら紹介するという内容だし、clojureではcore.logicで miniKanrenとほぼ同様のDSLが提供されている。miniKanrenが内部でやっていることはほぼprologのそれと同じで、つまり探索による単一化だ。(もっともminiKanrenもprologのこともよくわかっていないのでこの言い方が正確かは微妙だけれど…)
DSLという性格もあってminiKanrenはコンパクトにまとまった言語で、例えばschemeの実装では784行におさまっている。microKanrenはこのminiKanrenの論理プログラミングのエッセンスを抽出した言語で、そのコア部分のschemeの実装はわずか39行(!)に収まっている。スゴイシンプル。この記事ではmicroKanrenの実装を通じていわゆる論理プログラミング言語が内部で何をやっているかということを紹介していきたい。
一次資料は以下のものがある。ぶっちゃけこっちを読んだ方が早い。
varとgoalとstate
microKanrenはものすごくシンプルでユーザーフレンドリーな部分なんて全くないから基本的な概念を理解しておかないと実例が何やってるかをそもそも理解できない。
varは変数を表す。この変数はschemeのそれではなく、microKanrenのものだ。ユニークなオブジェクトだという理解で問題ない。ちなみに単一化というのはgoalに基いてこのvarと実際の値を対応付ける操作のことを言う。多分。
(var 3) ; => #(3) (let ((v (var 2)) (w (var 3))) (var=? v w)) ; => #f
goalは変数をどのように単一化するかを示すもので、「宣言」と言った方がわかりやすいかもしれない。microKanrenではgoalを生成するオペレータが4つ存在する。==, call/fresh, disj, conjだ。
(== x y) ; 「xとyは同一のものである」という宣言 (call/fresh (lambda (x) ...)) ; xに変数を束縛した上で宣言する (disj g1 g2) ; 「g1かg2のどちらかの宣言が成り立つ」という宣言 (conj g1 g2) ; 「g1とg2のどちらの宣言も成り立つ」という宣言
stateは変数の単一化の状態を表す。car部には現時点での変数と値の対応がalistで入っていてcdr部には現時点で生成された変数の個数が入っている。stateに問い合わせることでどの変数がどういう値を持つかを調べることができる。
; stateとしてありうるのはこんなのとか (((#(0) . 2)) . 1) ; こんなのとか (((#(1) . 2) (#(0) . #(1))) . 2)
goalが具体的にどういうものかというと、stateを受け取ってstateのリストを返す関数だ。つまり、goalは現在の単一化の状態を受け取って、それと宣言の内容からありうる全てのstateを返す。
ちょっと実例
というわけで簡単な例はこんな感じになる。
;; 初期状態では何の対応付けもされてないし変数も生成されていない (define empty-state '(() . 0)) (define (five x) (== x 5)) (define (six x) (== x 6)) ((call/fresh (lambda (x) (five x))) empty-state) ; => ((((#(0) . 5)) . 1)) ((call/fresh (lambda (x) (disj (five x) (six x)))) empty-state) ; => ((((#(0) . 5)) . 1) (((#(0) . 6)) . 1)) ((call/fresh (lambda (x) (conj (five x) (six x)))) empty-state) ; => ()
microKanrenの内部についてはまた今度。最も39行しかないんだし元コード読んだ方が早い。
登山
山に登り始めて早6年目になる。そこそこ多くの山に登ってきたと自分では思ってるが、その経験によると山で良い景色に出会えるのは二三回に一度らしい。景色の良さなんてお天道様の気分次第で脆くも崩れ去ってしまうし、そうなったら山行の楽しみは下山後の温泉くらいのものだ。雨の中何も見えないとわかって踏みに行った頂は結構あって、そいつらはリベンジ山行リストに突っ込まれていつか消費される日を待っている。
しかし今回の山行で見た景色は文句なしに絶景と呼べるものだった。双六岳で二滑りして満足して幕営地へ帰る途中で、夕暮れにはまだ早いかという時分だ。双六小屋から弓折岳へ向かう稜線は雪に覆われてて、その上をひたすら歩いていた。空は昨日の雨が嘘のように晴れ渡っていて、風も穏やかだった。左手には槍ヶ岳から大キレットを通って穂高に至る稜線が空に映えていて、右手には今朝がた滑ってきた双六岳のカールにシュプールが残っている。そんな景色だった。
またあのような景色を見たいと思う。だからまた山に登る、というわけでもないのだが。その翌日はずっと雨に降られていて絶望的にしんどかったのだ。良くも悪くも、という感じの山行だった。
syntax-rulesをexplicit renamingに変換する
桜がそろそろ散り始めてる。桜が散った後で猛烈に後悔するというサイクルをここ数年繰り返している気がする。今年は後悔したくないので週末にどこかへふらっと桜を見に行こうと思う。
さて、しばらく前からsyntax-rulesをexplicit-renamingに変換するマクロを作っていて、一応今日一区切りついた形だ。
https://github.com/wasabiz/picrin/pull/88/files
explicit-renaming以外はR7RSの範囲で実装したつもり。
解決すべき課題はマッチングと健全性の確保。マッチングはルールを再帰的に解析してコードの断片を繋ぎ合わせるということをやっていて、まあよくCLでやりそうな雰囲気がただよってる。健全性についてはerのシステムをそのまま流用させてもらった。
erを使ったのはpicrinがサポートしてたからという程度の理由だったが、もともとこの二つは相性が良い気がする。
