filter : {X : Set0} -> (X -> Bool) -> List X -> List X filter p [] = [] filter p (x :: xs) with p x ... | true = filter p xs -- x :: (filter p xs) ... | false = filter p xsfilterをこう書き直して、つまり、[]しか返さないんですけれども、これ…

でません・・・。 natEq : Nat -> Nat -> Bool natEq zero zero = true natEq zero (succ b) = false natEq (succ a) zero = false natEq (succ a) (succ b) = natEq a b boolEq : Bool -> Bool -> Bool boolEq true true = true boolEq false false = true …

natRight : {a : Nat} {b : Nat} -> a NatPair b -> Nat natRight (a natPair b) = b getNatRight : {a : Nat} {b : Nat} -> a NatPair b -> Val b getNatRight (a natPair b) = val b valNat : (a : Nat) -> Val a valNat a = val a body : (length (filter…

けれども、分かりません・・・。 module QSort where open import Data.List open import Data.Bool open import Data.Product data Nat : Set0 where zero : Nat succ : Nat -> Nat Length : {A : Set0} -> List A -> Nat Length [] = zero Length (x &#875…

です

Agdaにはさん付けが良いのか、くんづけが良いのか、その他(って言っても)が良いのか分かりません。あとAgdaは定理証明系の属という呼び方が普通で、それはPrologが人工知能向けだとかっていう(まぁLispが人工知能界隈向きというよりはマシな気がするんですけ…

「もぉ↘にゃどぉぅ↺」じゃないのかむしろ！！？？！

「もぉ↘にゃどぅぉ↺」って感じなんじゃないかなー

亜美真美が言う「もにゃどー」を想像したら、頑張ろう！！って気持ちになった。ドガー。

環境はMacBook 10.5.8でAgda-2.2.4を以下の内容を元にインストールhttp://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.MacOSX最初からHaskell周りのあれこれは入れてたので、2.install from the darcs repository, for the latest sourceの方に基づいて…

暇なのと、FLTVのネタ蒐集を兼ねてJSSST読んでました。http://www.jstage.jst.go.jp/browse/jssst/25/3/_contents/-char/ja/ここの 「モデル生成型定理証明と要素技術」と「論理・制約プログラミングと並行計算」。あと気になったのは(つまり読んでない)のは…

を行ったので、本棚をログとして上げてみました。かわいー本が欲しいです。かわいー本というわけでは無い感じですが、一番下にちっこく映ってる「敷居の住人」は面白いです。

圏合宿が終わった時間が22:00だとかで、やっぱりこれはつくば帰れないよなーって事で、秋葉原のネットカフェへ。実は参宮橋駅前のサークルKサンクスでアイマスねんぷちが買えるというハッピーな出来事がありました。 kawaii!!(圏合宿の時に話に上がった本を…

http://d.hatena.ne.jp/hiroki_f/20090813/1250129085に参加してきました。テキストは層・圏・トポス(竹内外史著)で、米田の補題手前まで。相変わらず数学の本ていうのは「書いている事をそのまま理解する」事が大事だよなーというのを感じたり。 あとは、圧…

FLTVはこれ( http://atnd.org/events/1102 )です。こんかいは画像無しです。でも天海春香さんが登場しています。Finger Tree Translate for RanhaView more documents from ranha.(reverse "amamiharukasan"を順にEmptyに足して行く、ですね。間違ってます。…

今日 8/5 はIDOLM@STER MASTER SPECIALシリーズの最後となるMASTER SPECIAL 06が発売されるので、まずそれを買います。そして次に、ぼくのはじめてのりすぷ！！ どこから処理系を取るんや http://yices.csl.sri.com/http://yices.csl.sri.com/download.shtml…

お昼 soutaroさんとsakaiさんと軽いロシア料理を出してくれるお店に入ってお昼ご飯を決めた。一応その時の内容メモ: MLの進化の系譜についてどうだこうだする会あってほしい。(私的な意味で。ただしどう考えてもお二方が企画とかすれば良くて私は本当に聞き…

午後からは色々忙しかったので・・・。一応私が聞けた発表はRubyに対する静的コード解析統合開発環境のモノだけです。殆ど・・・。 http://rubykaigi.org/2009/ja/talks/18S03話の内容としては、既存のRubyの静的コード解析器にまとめて投げてその結果を一括…

RubyKaigiに行くので今から(am 6:00)寝るわけにも行かず取りあえず水島さんところで見つけた次の問題をやってみた。 http://d.hatena.ne.jp/kmizushima/20090629/1246212207 sig Person { pet : one Pet , tabacco : one Tabacco } sig Pet { } sig Tabacco …

のATNDページを作ってみました。こういうのがあるんだけれども、どうでしょう。ただし、一応未来志向(ってなんだろう...)になっているイベントです。http://atnd.org/events/11028/30は丁度空いてるんですよね。な方は是非！！それと会場がどうしよう問題が…

それは私の頭が残念だからなんですが。。。今日の昼間についつたでPolymorphismの話がちろと出たので、というか私が出してたので、そこからふと次のケースら (1) forall a.a (2) forall a.(Num a) => a (3) forall a.a -> a (4) [ forall a.a ] (5) forall a…

Future Language TVが8/30とかでも良いと思います！！http://twitter.com/masahiro_sakai/status/2653751580 http://twitter.com/ranha/status/2654390360そういえば、昨日びっくりドンキーに行った時にさりげなく水島さんにLLTVの翌日なんか出来ないッスか…

アイマスは実はちゃんと買ったものの、全然ちゃんとやったこと無くて・・・っていうか初プレイ時は凄い悲惨な事に成ったので思い出ボックスにしまっていたものの、夏休み始まってから毎日アイマス動画をニコニコで見て/聞いてるのでまぁやっぱりやろう。とい…

さかいさんの指摘通りで、 one sig Root extends Dir { } { no parent } //fact { FSObject in Root.*contents } コメントアウトしてます結局こうなってるとこういうモデルが出て来ちゃいますからそうだ。

最近爆発的に盛り上がっているAlloyをやってみる。どこでとかは知らないけれども爆発的に盛り上がっている事は間違いない。今現在 6:17 リアルタイムに色々書いて行く。 そもそもあろいって何? 全く分からない。全くっていうのは、情報が何も無いという事で…

LLTBことLLTVのチケットを買って来ました。なんか軽量言語っぽい感じでLLTVを略せないもんですかね。 ロリロリなトランザクショナルにcall-by-Value意味がダメです・・・。http://slashdot.jp/developers/09/07/08/0718253.shtmlスラッシュドットにちょーど…

を買うぞ。買ってください・・・。http://atelier-ps3.jp/rorona/夏休みにゲームかよみたいな。うーん。夏休みはなんかたまりにたまった証明をやりなおしつつ主になんかうーんつまりあんまりやる事も無くて。いやあるんだけれどもその外部的なイベントってい…

今日は既に7月4日なんですが、7/3にICPC 2009の国内予選が在りました。今年は26チーム(カナ?)がアジア地区予選に進めるようで、 そんでまぁうちのチームは自力29位の選抜ルールで25位ぐらいでなんとかアジア地区予選まで行くんですが・・・。去年と代わらず…

「諸君らの愛した表示的意味論(R5RS)は死んだ。なぜだ?」 と述べられた時、シャアさんはR6RSに鑑みて、ひいてはプログラミング言語意味論を思ってどう答えるのでしょうか?教えてください。m(_ _)m ここに至った流れ 藍ちゃんの「表示的意味論て要らない子な…

なんかそういう地味な作業の結果は公開してねって、みよしちゃんが言ってたので、それもそうなのかもしれない・・・。 でもこういう所に張った直後全てのpaperがインターネットから失われる様なそういう悲しい予感があるので、嫌なんですけど私は既に確保済…