2009-01-01から1年間の記事一覧

ねむいよー

ちゅらいね・・・。kinabaさんが楽しいものを昨日twitterに流していた(http://twitter.com/kinaba/status/4986574175)ので、ももーい生放送が終わった辺りからねむいねむい言って別の補題(n + (succ m) == succ (n + m))を１つ証明してみました。で、その流…

お腹空いた...

#include <iostream> using namespace std; struct True{}; struct False{}; struct Zero{}; template<typename T> struct Succ{}; template<typename A,typename B> struct Add { }; template<typename B> struct Add<Zero,B> { typedef B val; }; template<typename A,typename B> struct Add<Succ<A>,B> { typedef typen…</succ<a></typename></zero,b></typename></typename></typename></iostream>

色々足りてないから酷い

data Nat : Set0 where zero : Nat succ : Nat -> Nat leibnizEq : Nat -> Nat -> Set1 leibnizEq x1 y1 = (P1 : Nat -> Set0) -> P1 x1 -> P1 y1 g : (P2 : Nat -> Set0) -> Nat -> Nat -> Set0 g P3 x2 z2 = (P3 z2 -> P3 x2) h : (P4 : Nat -> Set0) -> (…

計算機言語を使った定理証明の会

http://atnd.org/events/150710月24日 東京は大久保です。人が7人ぐらい居ないとちょっと広いなーという部屋を借りてしまっているので、俺はやるぞ！！って人はなんとしても来てください。全く宣伝になってないなー。 「当日までにやってくるべきお題」がま…

はこはるるん

今日はカナダ政治の試験らしいけど・・・。なんか明らかに基礎的な所がかけてるので辛いっていうか、まぁなんかこれらはゲームだよなぁみたいな感じです。そう、ゲームだと良いんですけど、そういう要素は無くて全部覚えてこいっていうそれなので心を消して…

■

data Bool : Set0 where true : Bool false : Bool data BoolHold : Bool -> Set0 where boolHold : (b1 : Bool) -> BoolHold b1 not : Bool -> Bool not b2 with b2 ... | true = false ... | false = true g : (b : Bool) -> BoolHold (not b) g b with b …

■

data Nat : Set0 where zero : Nat succ : Nat -> Nat data NatHold : Nat -> Set0 where natHold : (n : Nat) -> NatHold n test : (x : Nat) -> NatHold x test x with x test x | zero with x test x | zero | zero = natHold zero test x | zero | succ …

Agda2で同値関係を表す

昨晩に、ikegamiさんがつくばにいらしてたので、soutaroさんと一緒にご飯を食べに。その時Agdaの過去話を色々聞いて、やっぱり色々だなーとか思っていました。その場でdot-patternがちょっとみたいな事を言ったものの私が今実装してる言語では現時点でdot-pa…

■

人は忙しくなったりする事は無いし、忙しいからという理由で何かやらないのは何か個人的に嫌だからやら無いのであって忙しいからソレみたいな事は無いかなーと思っていたけれども、実は私が今忙しくて、人間は相対的に忙しく成る事は在ると思った。私の忙し…

ミンキーモモ

ファミコンのゲームはたのしい。このゲームでは、フルーツショップのお姉さんがすごい魅力的な気がする。魅力的な人の写真は載せない。

代数データ型 / VariantでExtendしたい

http://www.cs.chalmers.se/~nordland/ohaskell/survey.html data BW = Black | White data Color > BW = Red | Orange | Yellow | Green | Blue | Violet このColor > BWっていうのは、というか、'>'わりと気に食わない記号だけれども兎も角拡張したいなー…

良い3ヶ月でした

というわけで私の3ヶ月(なんだっけ7月から?)が楽しかったのは、敷居の住人という漫画による所が大きいワケです。アイドルは活力なんですが、原動力にならない所とかあって、まぁ私はダメですから。従ってダメです。 今日一日遅れで、5巻と6巻(こっち最終巻)…

The Next 700 Series

LandinのThe Next 700 Programming Language( http://portal.acm.org/citation.cfm?id=365257 )は1966年のCACMに載っていた話なんですけれども、今読んでいるAn Algorithm for Type-Checking Dependent Types ( http://www.cs.chalmers.se/~coquand/type.ps …

Coqはどうなってるんだろう

Inductive Bool : Set := true : Bool | false : Bool. Inductive Ty {A : Set} : A -> Set := ty (a : A) : Ty a. Definition f (arg : Ty true) := match arg with | ty true => true end. これで、fをCheckすると f : Ty true -> match true with | true …

なぜなにあぐだ

髪の毛が乾くまで暇なので書く。 data Unit : Set0 where unit : Unit data Ty : Unit -> Set0 where ty : (u : Unit) -> Ty u f : (Ty unit) -> Unit f (ty unit) = unit g : Ty unit -> Unit g (ty x) = unit この型チェックエラーメッセージ fの型チェッ…

なぜなにあぐだ

data D : Set0 -> Set0 where nat : D Nat bool : D Bool f : {A : Set0} -> A -> D A -> Unit f (zero) (nat) = unit Cannot split on argument of non-datatype @0 when checking the definition of f これは、Agda2のnotesディレクトリの中、"inductive-f…

どつとパタン2

data Nat : Set0 where zero : Nat succ : Nat -> Nat data Ty {A : Set0} : A -> Set0 where ty : (a : A) -> Ty a f : Ty zero -> Nat f (ty .zero) = zero {- f (ty zero) = zeroだとすると a != zero of type Nat when checking that the pattern ty zer…

どつとパタン

昨日のアレはMLで質問してみました http://thread.gmane.org/gmane.comp.lang.agda/1015すると、Wouterさんが、 http://wiki.portal.chalmers.se/agda/agda.php?n=Docs.DatatypeAndFunctionDefinitions ここにdot patternがあるからそれを使えば良いんじゃね…

なぜなにあぐだ

data Unit : Set0 where unit : Unit data Ty : Unit -> Set0 where ty : (u : Unit) -> Ty u f : Ty unit -> Unit f (ty unit) = unit g : Ty unit -> Unit g (ty a) = agがあれだよなー a != unit of type Unit when checking that the pattern ty a has t…

分からんぷいだよなー

module what_happen where data Unit : Set0 where unit : Unit {- data X : Set0 -> Set0 where 要素(canonical element)が無いというコレでも -} data X : Set0 -> Set0 where x : X Unit -- xは定義したものの意味は無い nonsense : X -> Unit -- nonsens…

10月10日の集い

ranha 10月10日ぐらいに、簡単に定理証明系で殴り合うみたいなイベント無いかなぁ。メジャーな○○の使い方も、各々異なる所があるので、やってる人が個別にスタイルを教えてくれたりすると手っ取り早くて良いかなーとか。Proof Generalというかtacticalな証明…

型コンストラクタはパタンマッチで使えない?

Haskellの話じゃなくて、またもAgda2の話です。具体的には data Nat : Set0 where zero : Nat succ : Nat -> Nat data Bool : Set0 where true : Bool false : Boolとかでまぁ、データ型を定義して、その上で次のような関数 nonsense : Set0 -> Nat nonsense…

データ構築子さんの事・・・分からなく成っちゃった・・・

分からなくなるもなにも、最初から何も知らん！！！！！！！ data Bool :: * where true :: Bool false :: Bool みたいな事を書いた時、このtrueとかfalseさんて一体何者なんだろうっていう雰囲気。例えば、 data Bool :: * where true :: Nat false :: Nat …

私の勝手な感想

まず主催者だったんだなぁ的な・・・。主催者っていうか・・・。 はじめに皆さん集合時間にルーズで、でもまぁそれを見越しての11:00だったので、最初に来た人は幻のゾンビFLTVが見られました。 見ても何も良い事は無いですけれども。 真っ黒Scheme Schemeの…

私の発表が、私にも理解出来なかったので文章にしてみる

発表View more documents from ranha.今回の私の発表は、思考の道具としてのプログラミングという観点から見てのプログラミング言語が未来に向かって持つべき何かを探るというような事でした。あの発表からそんな事が考えられていたという事は、分かる筈もな…

FLTVの当日のまとめ

発表者のタイトルや資料 Ustream ヤドカリさん 「真っ黒Scheme」 http://d.hatena.ne.jp/yad-EL/20090830/p1 http://www.ustream.tv/recorded/2072252 natsutanさん 「未来のハードウェア言語」 http://natu.txt-nifty.com/natsutan/2009/08/fltv-0901.html …

みじめな妥協策としては

http://www.iis.sinica.edu.tw/~scm/2007/agda-exercise-length-indexed-mergesort/ via http://twitter.com/ikegami__/status/3573974552いけがみさんの一言でクイックソートはどうでも良いっていうか、この周辺に4日ぐらい居た気がして、その間他の事があ…

もっともっと使われると、変わるんでしょうかね

まぁぼくはどこにもフィードバックしてないので、ユーザとして認識されてないんですけど、こういうのは凄く頭のいい、普通の人100人分ぐらいの人達が使ってるので多分大丈夫のはず module TCheckTest where data Nat : Set0 where zero : Nat succ : Nat -> …

修行失敗

割と良く分からないなーって感じになって、ググるとさかいさんの記事が出て来たので、依存和使っててすごいというか、なんで依存和使ってるか分からん感じだったんですけれども、実際やってみると少し分かりました。http://www.tom.sfc.keio.ac.jp/~sakai/d/…

これはちょっと悲しい子認定されると思う

module Proof1 where data List (A : Set0) : Set0 where [] : List A _::_ : A -> List A -> List A rec1 : {X : Set0} -> List X -> List X rec1 [] = [] rec1 (x :: xs) = rec1 [] -- ここのrec1でrec1の停止性を証明出来ないらしい。うーん・・・。 rec1…