fault on continuation (Gauche-devel-jp) - Gauche - OSDN
Shiro Kawai shiro****@lava***** 2002年 11月 18日 (月) 16:47:21 JST 前の記事 [Gauche-devel-jp] fault on continuation 次の記事 [Gauche-devel-jp] fault on continuation 記事の並び順: [ 日付 ] [ スレッド ] [ 件名 ] [ 著者 ] From: Tetsuya Okada <okaya****@c-cre*****> Subject: [Gauche-devel-jp] fault on continuation Date: Mon, 18 Nov 2002 15:22:44 +0900 > 継続を使ってバックトラックするプログラムを書いていまして、以下のような > ベンチマークを作ったのですが Gauche 0.6.5 が segmentat
Setoids in Agda
Setoid is a record type in Agda, and it appears everywhere from Relation.Binary.EqReasoning to Algebra. But, why do we need such a type ? After reading “setoids in type theory”, I thought that setoids are used for mathematical constructions like subset, quotients in the intensional type theory and the Calculus of Inductive Construction. Since some of functional data structure could be represented
萌えとかプログラミングとか（旧館） : 2x2ルービックキューブで群論（11） 群論の初歩（２）/無人島に行くとしたらどの群を持ってゆくべきか
2010年02月13日13:43 カテゴリパズル群論 2x2ルービックキューブで群論（11） 群論の初歩（２）/無人島に行くとしたらどの群を持ってゆくべきか さて、前回は群の公理を掲げ、その公理から簡単に導かれる帰結、すなわち、単位元 e の一意性と逆元の一意性を示した。読者の便宜を図って再掲しておく： ■定義[1] (群の定義)■ Ｇ : ある集合 ・: Ｇ×Ｇ → Ｇ （二項演算） ★Ｇ が群であるとは、次の(G1)(G2)(G3)が満たされることである： (G1)∀x, y, z ∈ Ｇ (x ・ y) ・ z = x ・ (y ・ z). (G2)∃e ∈ Ｇ ∀x∈Ｇ x ・ e = e ・ x = x. (G3)∀x ∈ Ｇ ∃y∈Ｇ x ・ y = y ・ x = e. さて、数学の理論というのは分析の道具であり、分析の対象がないと学ぶ意味がない。群論にとって、最
Computational Approach to Mathematical Sciences, Video Archives
キーワード: serial=0032, type=講義 ライセンス: ダウンロードした映像の再配布はOK. ただし付属のノートおよび資料, このページとともに再配布すること. また一切の変更は許可されない. (creative commons, 表示-改変禁止 2.1 ) 詳しい説明 講義資料のダウンロード (PDF) ノート (準備中, 参考文献も参照., @s/2007/09 未公開)) 講義映像 Windows上で Streaming で閲覧している場合, 停止するときは, 停止ボタンを必ずおしてください. x で停止しないように. ネットワークの接続速度が極端に遅くなる場合があります.) 右クリックでダウンロード保存可能です. [111-1] Streaming (15M, 約 7 min) ダウンロード(低解像度, 15M) ダウンロード(高解像度, 58M) [111-2] S
F-algebra と catamorphism を Haskell で理解する(2) - らむだ畑でつかまえて (catcher in the λ)
前回の続き。 wikipedia の F-algebra のページ http://en.wikipedia.org/wiki/F-algebra 参照。 上記ページに F(X) = 1 + X という関手の F-algebra の例で (N,[zero,succ]) が出てくる。Haskell で書くと type N = Int a :: Maybe N -> N a Nothing = 0 a (Just x) = x + 1 本当は N は自然数なので負の数も入っている Int とは違うけれどここでは Int でごまかしておく。 a Nothing = 0 の部分が zero に、a (Just x) = x + 1 の部分が succ に対応する。 さて F-algebra (N,a) から別の F-algebra (B,b) b :: Maybe B -> B に対する射 f はど
F-algebra と catamorphism を Haskell で理解する - らむだ畑でつかまえて (catcher in the λ)
wikipedia の F-algebra のページ http://en.wikipedia.org/wiki/F-algebra 参照。 上記ページに集合圏から集合圏への関手F として F(X) = 1 + X という例がでてくるが 1 + X は Haskell では Maybe X である。 Maybe の定義 data Maybe a = Nothing | Just a の「Nothing」が「1」に、「|」が「+」に、「Just a」 が「X」にそれぞれ対応する。 F(f) は fmap f である。 F-algebra の説明にでてくる A を Bool、B を Int とし a :: Maybe Bool -> Bool a Nothing = False a (Just x) = x b :: Maybe Int -> Int b Nothing = 0 b (Just
関数型プログラミング言語 Haskellの理論と応用
「関数型プログラミング言語 Haskellの理論と応用」のホームページです。 概要 本講義では、関数型プログラミング言語Haskellについて、その理論的基礎か ら実際的な応用までを解説する。Haskellは、副作用を持たない、CやJavaなど いわゆる“主流（メインストリーム）の言語”とは一風変わったプ ログラミング言語である。また、強力な型システムを持つことも大きな特徴で ある。本講義では、おもに次のようなトピックについて説明する。 遅延評価 型クラス リスト内包表記とモナド パーサコンビネータ さらに時間が許せば、総合演習として命令型ミニ言語のインタプリタの作成を 行なう。 受講に際しては、ラムダ計算に関する基本的な知識があること、また、Scheme やMLなどの関数型プログラミング言語を使用した経験があることが望ましい。 日程 6/11（月） 13:30 〜 16:40ころ 6/1
Agda2ことはじめ - ラシウラ
参考は http://www.cs.chalmers.se/~ulfn/darcs/AFP08/LectureNotes/AgdaIntro.pdf とAgda2添付のexamples、そしてソースコード。 一応emacsインタフェースで、コード補完(別名、証明補助)できるUIがあるのですが、自分はまったく使ってません。 一応、こういうdependently typedな言語では、式と型の区別はないようなもので、型部分でも値や関数適用ができるため、それらを合わせて項(term)として扱うのですが、そのtermの意味で式や型という語をわざと使っています。 Agda2の基本 簡単なものとして、AgdaIntroにもある、trueとfalseからなるBool型データと、その関連関数を定義しましょう。 まず、Boolデータ型 data Bool : Set where true : Bool fa
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
