第11回名古屋Scala
9/17 に、第11回名古屋Scala勉強会に参加してきました。
今回は23章と24章の予定だったけど、盛り上がったので24章は次回に。
- 23章 for 式の再説
- モナド (1)
- bind : M[A] => (A => M[B]) => M[B]
- 最初の M[A] がレシーバ (Scala)
- return : A => M[A]
- この 2 つがあるとき、M は モナド (Haskell, do式が使える)
- 不思議な抽象だけど、いろいろ便利
- 例：リスト、Option (Maybe), IO処理、メモリ状態、パーサ、etc.
- Scala だと、bind は flatMap、return は 単一コンストラクタ (ユニットコンストラクタ) に対応
- for 式を使うには、map が必要 (map : M[A] => (A => B) => M[B] (Scala, 最初の M[A] がレシーバ))
- bind : M[A] => (A => M[B]) => M[B]
- F# のコンピューテーション式
- モナド (2)
- パターンマッチ
- 忍者パターンマッチ
- パターンマッチで変数を定義する
- 忍者パターンマッチ
- モナド (1)
scala> val h = ("hoge", 99) h: (java.lang.String, Int) = (hoge,99) scala> val (name, age) = h name: java.lang.String = hoge age: Int = 99
-
-
- ドラゴンパターンマッチ
- パターンマッチで無名関数を定義する
- p.430 inCheck ドラゴンパターンマッチによる実装 ↓
- ドラゴンパターンマッチ
-
scala> def inCheck:((Int,Int),(Int,Int))=>Boolean = { | case ((x1,x2),(y1,y2)) => x1 == y1 || x2 == y2 || (x1 - y1).abs == (x2 - y2).abs | } inCheck: ((Int, Int), (Int, Int)) => Boolean
- こんなの書きました
- bleis とん
- テスティングフレームワーク作ってみた
- パラメタライズドテスト書きたい
- テスト仕様書とかテストケースから自動生成したい
- Excel とか大変
- テスティングフレームワーク作ってみた
- leque さん
- lift で ファイルビューワ的な
- lift でクロージャ → いい感じに js に！
- dump
- List("") とかをいい感じに表示してくれる
- REPL のなかとか、こう...
- 2.8 から catching が使える
- lift で ファイルビューワ的な
- bleis とん
- bleis宅
次の日に Gitの勉強会 があったので、泊めてもらうことに。
wk6 と mrxptn も一緒。
bleis と F# の話してたりして、気付いたら 3時。
そこから (みんな寝てから)、化物語の最終巻と AB を見る。
・・・・・・
天使ちゃんマジ天使。
・・・・・・
お、2人起きた。(6時くらい)
・・・・・・
天使ちゃんマジ天使。
・・・・・・
昼か。(11時くらい)
wk6 は別の勉強会らしく、少し早く出てた。
3人で名古屋駅でラーメン食べて、Git勉強会へ。
続・Coqりさん Q.E.D.
Coqりさん 証明のかけら の続き (再挑戦)。
Require Import Arith. Fixpoint fib1 n:nat := match n with | 0 => 0 | 1 => 1 | S (S m as p) => fib1 p + fib1 m end. Fixpoint fib2 n a b:nat := match n with | 0 => a | S n => fib2 n b (a + b) end. Lemma plus_1_Sn : forall n:nat, n + 1 = S n. Proof. intro n. rewrite plus_n_O. rewrite plus_Snm_nSm. reflexivity. Qed. Lemma plus_2_SSn : forall n:nat, n + 2 = S (S n). Proof. intro n. rewrite plus_n_O. rewrite plus_Snm_nSm. rewrite plus_Snm_nSm. reflexivity. Qed. Theorem fib1_fib : forall n:nat, fib1 n + fib1 (n + 1) = fib1 (n + 2). Proof. intro n. rewrite plus_1_Sn. rewrite plus_2_SSn. simpl fib1. destruct n. reflexivity. ring. Qed. Theorem fib2_fib : forall n a b:nat, fib2 n a b + fib2 (n + 1) a b = fib2 (n + 2) a b. Proof. induction n. intros a b. reflexivity. intros a b. rewrite plus_Sn_m. rewrite plus_Sn_m. simpl. rewrite (IHn b (a + b)). reflexivity. Qed. Lemma fib1_eq_fib2_aux : forall n:nat, fib1 n = fib2 n 0 1 /\ fib1 (S n) = fib2 (S n) 0 1. Proof. induction n. split. reflexivity. reflexivity. destruct IHn. split. exact H0. rewrite <- plus_2_SSn. rewrite <- fib1_fib. rewrite <- fib2_fib. rewrite plus_1_Sn. rewrite <- H. rewrite <- H0. reflexivity. Qed. Theorem fib1_eq_fib2 : forall n:nat, fib1 n = fib2 n 0 1. Proof. intro n. destruct (fib1_eq_fib2_aux n). exact H. Qed.
で、できたー！
これまでは流れが追えるように . で書いてきたけど、そろそろ ; 使っていってもいいかもしれない。
SKK とか
K I = F と、S K K = I を証明してみる。
Definition I {A:Type} x:A := x.
Definition K {A B:Type} (x:A) (y:B) := x.
Definition F {A B:Type} (x:A) (y:B) := y.
Definition S {A B C:Type} (x:A->B->C) (y:A->B) (z:A) := x z (y z).
Theorem ki_f : forall (A B:Type)(x:A)(y:B), K I x y = F x y.
Proof.
intros A B x y.
unfold K.
unfold I.
unfold F.
reflexivity.
Qed.
Theorem skk_i : forall (A B:Type)(x:A), S K (K:A->B->A) x = I x.
Proof.
intros A B x.
unfold S.
unfold K.
unfold I.
reflexivity.
Qed.まぁ、展開するだけなんですけどね。
第1回 Scala座
9/4 に、第1回 Scala座に行ってきました。
- これまでのScala、これからのScala
- これまで編
- Scalaって
- Less typing を目指した言語仕様
- 型推論とか
- メソッド名短め
- 型推論
- ファーストクラス関数とクロージャ
- パターンマッチ
- switch 文を超強力で柔軟にしたもの
- オプション型便利
- List の headOption, reduceLeftOption とか
- List が空だと None を返す
- List の headOption, reduceLeftOption とか
- trait による Mix-in
- 実装を持てるインタフェース的な
- Read-Eval-Print Loop (REPL)
- 対話型評価環境
- テスト書く → REPLで確認 → コードに書く → テストする → (黄金の回転！)
- Scala は公式 LL！
- Scala Way
- 事例
- みんな大好きついったーのバックエンドも一部 Scala で動いてます
- 他にも沢山
- これから編
- これまで編
scala> val fib:Stream[Int] = Stream.cons(0, fib.scanLeft(1)(_+_)) fib: Stream[Int] = Stream(0, ?) scala> fib take 20 foreach (x => printf("%d ", x)) 0 1 1 2 3 5 8 13 21 34 55 89 144 233 377 610 987 1597 2584 4181
- Scalaでプレゼンテーションの試み
- ScalaDaysに行ってみて
- Scala Days 2010
- スイスで開催
- Martin Odersky先生やScalaチームの人に会える！
- 全発表の動画が公式ページから視聴できる！
- 発表
- PEGEX について
- kmizu さん
- パターンマッチライブラリPEGEXについて
- School Days ネタ通じず
- 英語の聞き取り能力大事
- 話す方は身振り手振りでなんとかなる
- A Case Study in DSL Development
- Automated Refactoring for Scala
- Lightweight Language Processing in Kiama and Scala
- 言語処理ライブラリの話
- Lightweight language support for type-based, concurrent event processing
- 型情報を使ってScalaのActorライブラリを最適化
- コードサイズは殆ど同じ
- 劇的に性能改善
- 型情報を使ってScalaのActorライブラリを最適化
- Named and Default Arguments in Scala
- 名前付き引数とデフォルト引数についての話
- 継承やジェネリクスが絡むと複雑
- 型チェックは呼び出し側で行われる
- Automatic refactoring for Scala programs
- An Experiment with Automatic Resource Management
- Type-safe SQL embedded in Scala
- Scala at LinkedIn
- Migration a Struts/Java vE-Mail Application to Lift/Scala
- The Scala IDE for Eclipse
- sbt
- Processing with Spde
- Processing の Scala 版である、Spde の話
- 無名関数などを活用して、Processing よりも簡潔にコードを書ける
- Sneaking Scala Into Your Organization
- The Future of Scala
- グループ毎に Scala の未来について議論する
- 都合により参加できず。
- PEGEX について
- Scala Days 延長戦
- Scala Days 2010
- ScalaでAndroidアプリ開発
- Androidアプリが動くまで
- ソース → .class ファイル → .dex ファイル → .apk ファイル → インストール、実行
- 数十秒かかる
- ソース → .class ファイル → .dex ファイル → .apk ファイル → インストール、実行
- メソッド名を間違えた場合
- 動的型付け言語の場合
- インストールまでして、実行時に初めてエラー
- Scala の場合
- ソースからのコンパイル時にエラー
- 動的型付け言語の場合
- Java と比べて、無名関数とか暗黙の型変換とか便利
- Java っぽく書くことも出来る
- デメリット
- アプリサイズが大きくなる
- 同機能のJava実装と比較して 4 〜 5 倍程度
- protected static メンバにアクセス不可
- 現状は Java 側でラッパーを用意しておくしかない
- Google Maps API (maps.jar) 使うとコンパイルエラー
- 次期バージョン (2.8.1) で修正される予定
- アプリサイズが大きくなる
- 環境
- Androidアプリが動くまで
- Web Flavor
- GAEでLiftやってみた
- → GAE で関数的 Web フレームワーク Lift を使う
- 事例
- Lift について
- 関数的Webフレームワーク
- 他のWebフレームワークと比べて最も特徴的な部分
- Ajax、セッション管理、テンプレート、ORマッピングなど、Webアプリで必要なものは大体ある
- 関数的Webフレームワーク
- プロジェクトの作成
- maven があれば非常に簡単
- コマンドで一発
- maven があれば非常に簡単
- ビルド、テスト、デバッグ
- ビルド、テストはmavenで一発
- ローカルで確認できる
- GAEサーバへのデプロイもコマンドで
- 関数的な部分
- やっててよかった関数型言語
- その他の便利な関数型言語
- まとめ
- Scala, Lift 超便利
- maven があれば簡単ポン
- より詳しい情報は、「GAE/JによるScala/Liftアプリケーション開発」
- caseクラス、高階関数、モナドとか、恐れずに触ってみるといい
- 名古屋Scala勉強会に是非
- 関数型言語Scalaで実装する型推論
- LT
- ScalaでHadoopを動かしてみた
- implicit conversion 便利
- HadoopのMapが簡単に書ける
- implicit conversion 便利
- Lift on GAE/J
- Lift + GAE は制約が多く大変
- Scala2.8でひるまのおしごとしてみたよ
- Scala×Silverlight
- Silverlight
- MS版Flash
- ScalaをSilverlight上で動かす
- scala-msil を使う
- うまくいかない...
- バイナリ弄ればいいじゃん (天使ちゃん(ry)
- 動いた。
- バイナリ弄ればいいじゃん (天使ちゃん(ry)
- うまくいかない...
- Silverlight
- ScalaプログラマのためのF#
- Scala ワンライナ
- Scalaでシューティングゲーム！
- ワラビモチとscalaについて
- 画像を表示するScalaプログラムが動かない
- 2分間で誰か
- 出来た人にわらび餅プレゼント
- 画像を表示するScalaプログラムが動かない
- ScalaでHadoopを動かしてみた
- ToDo 的な
- Scala 2.8 から入ったらしい継続について調べる
- 継続は力 (違
- Scala 2.8 から入ったらしい継続について調べる
|> in Scala
F# の |> を Scala でやってみた。
scala> class Holder[A](a:A) { | def |>[B](f:A => B) = f(a) | } defined class Holder scala> implicit def any2holder[A](a:A) = new Holder(a) any2holder: [A](a: A)Holder[A] scala> val succ = (x:Int) => x + 1 succ: (Int) => Int = <function1> scala> 3 |> succ |> succ res0: Int = 5 scala> 3 |> { (x:Int) => x * 2 } |> succ res1: Int = 7
お、これは・・・
scala> 3 |> { | case x => x * 2 | } res2: Int = 6 scala> 3 match { | case x => x * 2 | } res3: Int = 6
おお！match と同じように使える！
- 追記
scala> class Holder[A](a:A) { | def |>[B](f:A=>B) = f(a) | def <|:[B](f:A=>B) = f(a) | } defined class Holder scala> implicit def any2holder[A](a:A) = new Holder(a) any2holder: [A](a: A)Holder[A] scala> val succ = (x:Int) => x + 1 succ: (Int) => Int = <function1> scala> succ <|: succ <|: 10 res0: Int = 12 scala> val tw = (x:Int) => x * 2 tw: (Int) => Int = <function1> scala> succ <|: succ <|: 10 |> tw |> tw res1: Int = 48 scala> tw <|: tw <|: 10 |> succ |> succ res2: Int = 42
おー！
メモ晒し
自分の Coq メモを晒してみる。
■ ; について T1 ; T2 T1 適用後、T1 によって出来た全てのサブゴールに対して T2 を適用 T1 ; [T2 | T3] T1 適用後、T1 によって出来たサブゴール a, b に対して、a に T2、b に T3 を適用 (不要なら T2, T3 を省略可(何もしない)) ■tacticについて intro / intros 前提の導入 ゴールの forall や -> で括られた部分を前提へ intros で名前を付けるときは左から 前提に持って行かない場合は、名前を _ にする (intros のみ) apply 前提 A -> B、ゴール B があるとき、ゴールを A にする ゴールに適用できる関数があるとき、apply 関数 でゴールに関数を適用する assert assert (前提の名前 := 式) で、式によって証明させる命題を前提に追加する exact 前提 H がゴールと同じ場合、exact H でゴールの証明を終了する 証明と等価な関数があるとき、exact 関数 でゴールの証明を終了する assumption 前提にゴールがある場合、ゴールの証明を終了する elim 前提によって、以下の規則を適用 ・前提が A /\ B の場合 ゴール G を、A -> B -> G にする ・前提が A \/ B の場合 ゴール G を、A -> G と B -> G に分割する ・前提が not A の場合 ゴールを A にする ・前提が exists x : A, P x の場合 ゴール G を、forall x:A, P x -> G にする split and のゴールを分解する apply conj の省略形 left / right or のゴールの片方を選ぶ left は apply or_introl、right は apply or_intror の省略形 exists 前提に H : x:A があるとき、exists H で、ゴールの exists a:A, P a を P x にする clear 指定した前提を除去 auto intro, apply, assumption 等を、ユーザの指示無しで組み合わせてゴールに辿り着ける場合、適用 trivial intro, apply, assumption 等を、1回だけ適用 tauto トートロジーである場合、適用 try tauto tautoが可能であれば、適用 (出来ないならば何もしない) cut cut P で、ゴール G を、P -> G と P に分割する generalize 前提 A、ゴール G のとき、ゴールを A -> G にする rewrite 前提 H : A = B のとき、 ・rewrite (->) H でゴールの A を B にする ・rewrite <- H でゴールの B を A にする replace A with B ゴール G を、G 中の A を B に置き換えたものと、B = A に分割 unfold A ゴールの A を展開する transitivity C ゴールの A = B を A = C と C = B に分割 symmetry ゴールの A = B を B = A にする reflexivity ゴールが A = A のとき、ゴールの証明を終了する (反射律) (* このあたりてきとう *) simpl 簡約 (?) compute / cbv 簡約 (?) congruence ゴールが、同値変形で導ける場合、適用 (?) omega nat, Z 上の、~, /\, \/, -> で組み立てられた等式や不等式を自動で頑張ってくれる? 使うときは、Require Import Omega. ring ゴールが、環の性質を使った変形で導ける場合、適用 (?) field ゴールが、体の性質を使った変形で導ける場合、適用 (?) induction n n に関する帰納法の開始 inversion H H が成立するための前提を前提に追加する injection H コンストラクタ C に対し前提 H : C a = C b のとき、ゴール G を a = b -> G にする ■coqtopのコマンド ＊通常モード Check ... ...の型等を表示 Eval compute in ... ...を計算 Locate "(演算子)" (演算子) の定義を表示 Section ... ...という名前でセクションを切る Goal ...(Prop) ...の証明を開始 Print ...(定理とか) ...の中身を関数形式で表示 ＊証明モード Restart 証明を始めから Abort 証明をやめる Undo 証明を1つ戻す ■その他 -> は右結合
チュートリアル続き読まないと。
(1.4 くらいまでしか行ってない)
- 追記
最新版はここに。
Coq庵
8/29 に、Coq庵 に行ってきました。
資料等はこちら。
行き道で祭りやってた。
一部道が通れなかったりして、少し迷うなど。
- 初めてのCoq
- 仕様記述言語
- Coq の特徴
- Coq の中身
- 関数型プログラム的
- Vernacularコマンド (プログラムの文)
- Gallina式 (プログラムの式)
- 内部はラムダ式
- 論理学的
- tactic
- 証明、証明を含む式
- 小文字で始まって . で終わる
- tactic
- 関数型プログラム的
- Coq のプログラム
- Coq で書かれたプログラム
- Coq 習得の道
- 更に熟練するには
- CPDT (Certified Program with Dependent Types)
- Coq'Art
- その他 Curry-Howard 対応や型理論など
- 勉強会会に参加しよう
- ProofCafe(栄)
- Formal Method 勉強会
- Coq による暗号アルゴリズムの実装の暗号学的安全性検証
- 暗号プログラムの安全性検証の必要
- 暗号学的安全性の検証は行われていない
- 不具合が発見された場合の社会的・経済的影響が大きい
- → 暗号アルゴリズムの安全性検証とプログラム(実装)の検証
- 疑似乱数生成期 BBS (Blum Blum Shub) の実装の安全性検証
- ゲーム列による安全性証明
- システムと攻撃者の挑戦としてモデル化
- 実装の正しさの検証
- ホーア論理、操作的意味論、etc.
- Coqを用いた形式化
- Inductive 内の :> は展開になる
- 暗号プログラムの安全性検証の必要
- にわとりかんさつにっき in お茶大
- 浅井先生の研究室のお話
- Coq 使い多い (8人中 6人)
- Coq ゼミ
- 2008年にあった
- http://pllab.is.ocha.ac.jp/lab.html
- 「型 = 命題、プログラム = 証明」
- Coq 楽しそう
- プログラム書いてテストケース通っても、それがちゃんと正しいかは分からない
- Coq で 証明したら一応安心できるかな
- プログラム書いてテストケース通っても、それがちゃんと正しいかは分からない
- 証明に良さそう
- 手で書く証明よりも間違いがなくて良さそう
- ICFP 2009 B.C.Pierce の招待講演
- http://www.cis.upenn.edu/~bcpierce/sf/
- 基礎から、いろいろまである
- 全部やろうとすると 2 ヶ月くらい Coq 漬けになる
- http://www.cis.upenn.edu/~bcpierce/sf/
- CPS変換
- 「継続渡し形式」ってのに変換する
- 状態を取って処理の続きをやる関数 を引数に渡す
- 「継続渡し形式」ってのに変換する
- 非関数化
- CPSで渡してた関数を、データ構造にする
- CPS変換・非関数化の正当性
- CPS変換 + 非関数化の正当性 (fibonacci)
- 結構複雑になる
- shift/reset
- 継続のオペレータ
- 浅井先生の研究室のお話
- 一般たらいまわし関数の停止性を証明する
- たらい回し関数の定義
- t(x,y,z) := if x <= y then y else t(t(x-1,y,z), t(y-1, z, x), t(z-1, x, y))
- 複雑な再帰
- 停止性が問題
- 深さ制限付きたらい回し関数
- カウントを付ける
- t_n(x,y,z) := if x <= y then y else t_{n-1}(t_{n-1}(x-1,y,z), t_{n-1}(y-1, z, x), t_{n-1}(z-1, x, y))
- t_0(x,y,z) = ⊥ (bottom)
- 停止性
- 整数 x, y, z に対して停止する : ∃n, t_n(x, y, z) ≠ ⊥
- 一般たらいまわし関数
- 引数が増える
- Coq で表現
- ⊥を加えた整数型
- option Z で表現
- Some x が計算完了 (以下 Vx)
- None が 未完了 (以下 B)
- ⊥を加えた整数型
- 深さ制限付き再帰
- 皆さんよく知ってる Y コンビネータ
- Yn O init recur = init
- Yn (S n) init recur = recur (Yn n init recur)
- 普通の Y は、Y f = f (Y f)
- 皆さんよく知ってる Y コンビネータ
- 再帰制限付きたらい回し関数 (ntarai)
- ntarai n v = Yn n ntarai_init ntarai_recur
- ntarai_init x = B
- ntarai_recur f (Vx Vy v) = ...
- ntarai_recur f _ = B
- 最初に証明したいこと
- 深さ n で停止したら、n 以上の m でも n で停止する
- forall n m v x, ntarai n v = V x -> n <= m -> ntarai m v = V x
- bottom が出てきた場合、計算経過が異なることが
- bottom を値に書き換えても結果は変わらないことを証明
- f ⊥ = V a -> ∀x, f x = V a
- 美しくない
- x = y ∨ x = ⊥ -> f x = f y ∨ f x = f ⊥
- 対称になった！
- f ⊥ = V a -> ∀x, f x = V a
- R x y := x = y ∨ x = ⊥ とすると、R は半順序 (x ≪ y)
- 証明したいこと：x ≪ y -> f x ≪ f y
- f は単調増加
- 多変数関数の場合
- [xi] ≪ [yi] <-> forall i, xi ≪ yi
- リストで与える
- 連続な関数の合成は連続
- Coq で順序を定義する
- le を定義
- dZ, list dZ, list (list dZ) の le はそれぞれ違う関数
- 型クラスを使おう！
- dZ, list dZ, list (list dZ) の le はそれぞれ違う関数
- le を定義
- 型クラス
- たらい回し関数の定義
- Coq でガベージコレクションの証明
- コードはgithubに
- マーク & スイープ GC
- GC アルゴリズム3人衆の中で最弱
- マークフェーズ
- ルートから辿れるオブジェクトにマークを付ける
- スイープフェーズ
- マークのついてないオブジェクトを回収し、マークを外す
- GCは完全でなければならない
- トレース漏れ = 不良GC
- 生存中のオブジェクトを削除してしまう (バグ)
- アルゴリズムはホントに正しいか
- アルゴリズムが正しくても、ちゃんと実装できているか
- そこで Coq です！
- トレース漏れ = 不良GC
- Coq でプログラムを書く → 証明する → OCaml 等に変換して実行する
- メモリのモデル化
- Record で表現
- Coq には3種類の集合モジュールがある
- Ensembles, ListSet, FSet
- ルートから辿れるオブジェクトの探索
- 普通に書くと停止性が保証できない
- 未探索のオブジェクトの集合を引数にもらって、停止性を保証する
- 呼び出し毎に必ず減少するので、停止性が保証できる
- 安全なGC
- フリーリストと使用中のメモリに重複がない
- 初期状態はSafety
- SafetyなメモリをGCしてもSafety
- Coq → OCaml
- ペアプルービング
- anarchy proof
- bleis と youku_s と 3 人でトリオプルーピング
- Require Import Definitions. で迷うなど
最初はこんな感じで書いて、
Theorem Modus_ponens: forall (P Q: Prop), (P -> Q) -> P -> Q. Proof. intros P Q. (* forall のところの P Q が Prop だよってのを前提へ *) intro H. (* (P -> Q) -> P -> Q の (P -> Q) を H として前提へ *) intro p. (* P -> Q の P を p をして前提へ *) apply H. (* ゴール Q、前提 H (P -> Q) から、ゴールを P に *) exact p. (* ゴール P 、それは前提 p にある *) Admitted.
2人にまったりと解説のようなものをしてみる。
で、auto ってのがあるよって、
Theorem Modus_ponens: forall (P Q: Prop), (P -> Q) -> P -> Q. Proof. auto. (*｀・ω・´*) Admitted.
Require Import Classical.
Theorem Peirce: forall (P Q: Prop), ((P -> Q) -> P) -> P.
Proof.
intros P Q.
intro H0.
elim (classic P).
intros p.
exact p.
intro p1.
apply H0.
intro p2.
elim p1.
exact p2.
Admitted.classic ってのが、Coq.Logic.Classical_Prop にあって、
Axiom classic : forall P:Prop, P \/ ~ P.
こんな感じになってる。
古典論理の排中律。
Theorem sqrt_2: forall (n m:nat), n*n = 2*m*m -> m = 0.
Proof.
intros n m H0.
destruct m.
reflexivity.
(*´・ω・｀*)
Admitted.こういうのって Coq だと難しめ？
まだ自分には分からなかった (´・ω・｀)
Axiom Falso: False. Fixpoint pow a n := match n with | O => 1 | S m => a * pow a m end. Theorem Fermat's_Last_Theorem: forall (a b c n: nat), n > 2 -> pow a n + pow b n = pow c n -> a = 0 /\ b = 0 /\ c = 0. Proof. elimtype False. exact Falso. Admitted.
elimtype False. でゴールを False にできるらしい。
(他の人の見ると apply False_ind. が普通？)
てか、この場合前提に False があるので、case Falso. でいいらしい。
Theorem Fermat's_Last_Theorem: forall (a b c n: nat), n > 2 -> pow a n + pow b n = pow c n -> a = 0 /\ b = 0 /\ c = 0. Proof. case Falso. Admitted.
(Coq 証明事例集: 前提が……のとき 参考にさせてもらいました)
Axiom Peirce: forall (P Q: Prop), ((P -> Q) -> P) -> P. Theorem Excluded_Middle: forall (P: Prop), P \/ ~P. Proof. intro P. (*Д*) Admitted.
時間切れ。
- ToDo 的な
- あなぷる 4. Converse Peirce の続き
- Software Foundations 読む
- Introduction to generalized type systems 読む (ラムダキューブ、*:□)
- Coq りさん再挑戦
OCaml Meeting 2010 in Nagoya
8/28 に、OCaml Meeting 2010 in Nagoya に行ってきました。
朝早く起きて名古屋大学へ。
暑い・・・
λterm ::=
| x
| λterm λterm
| fun x -> λterm
追加で
| 定数・リスト
| バリアント・ペア
| let, match, if
さらに
| 代入可能な変数・ループ・モジュール
| 多相バリアント・オブジェクト
さらに最新版(3.12)からモジュールが第一級に
OCamlどこいってしまうんや
- F# の流技 / Fluent Feature in F#
- OCaml △！
- → F# △！ → F# |>
- パイプライン演算子 |>
- let (|>) x f = f x
- F# は inline 関数が書ける (コンパイル時に展開)
- |> は inline
- オブジェクト指向的
- x.F().G().H()
- x |> f |> g |> h
- F#「OCamlと違うんです」
- + 演算子とか
- 関数オーバーロード
- 型推論と相性悪い
- 関数オーバーロード
- + 演算子とか
- F# の対話環境は fsi
- 画面出力 System.Console.WriteLine
- オーバーロードされている
- F#「.NETですから」
- OCaml と比べると 型推論 (´・ω・｀)ｼｮﾎﾞｰﾝ
- F# ではよく型を明示する
- |> 使うと型も流してくれるので型明記を少なくできる
- 単位付きの計算ができる
- コンピューテーション式
- F# 版 モナド！？
- OCaml △！
- OCaml 3.12における第一級モジュールと合成可能なシグネチャについて / First-class modules and composable signatures in OCaml 3.12
- モジュールの役割
- プログラム・名前空間の構造化
- インタフェースによる仕様記述・部品化
- 抽象型・プライベート型による隠蔽
- ファンクタによる抽象化
- モジュールがコア言語より優れている点
- 型構成子に対する多相性がある
- 正確な多相型要求
- 存在型(抽象型)の定義
- 3.12の新機能
- 第一級モジュール
- モジュールを通常の値のように受け渡しできる
- モジュールを受け取る関数とか作れる
- パラメータによって、使うモジュールを選択したりできる
- クラスをモジュールに入れて、中のクラスを動的継承によって変更したりできる
- 型の等式を表現できる (GADTs)
- 完全に型付けされている
- 安全！
- 理論的には新しくない (10年前に出てる)
- ファンクターとの干渉で安全でなかった
- モジュールを通常の値のように受け渡しできる
- 第一級モジュールの制限
- ファンクターの中では第一級モジュールを開くことは出来ない
- 型の pack, unpack を全て書かなければならない
- 多相メソッドと同じ機構を使って、多くの型注記が省ける
- シグネチャ言語
- 破壊的代入の制限
- 代入をかけれるのは一番上レベルの型とモジュールのみ
- パス (定義されているもの) しか代入できない
- 型のパラメータ数。順番は変えられない
- 削除によって、構文的にスコープが有効でないシグネチャになったりする
- モジュールの役割
- デザインレシピ、モジュール、抽象データ型 / Design Recipe, module, and abstract data type
- デザインレシピ
- データ定義を行う
- 目的を考え、ヘッダを作る
- 例を作り、それをテストプログラムにする
- テンプレートを作る
- 本体を書く
- テストする
- → 例 (テスト) が先！TDD！
- デザインレシピ
プログラミングの基礎 (Computer Science Library)
- 作者: 浅井健一
- 出版社/メーカー: サイエンス社
- 発売日: 2007/03
- メディア: 単行本
- 購入: 17人 クリック: 404回
- この商品を含むブログ (98件) を見る
- Spot Your White Caml -- How to Make Yourself Happy in OCaml Projects
- コードの成長が早くて、初めからいて少しずつ進化していくなら対応できるが、十分成長したコードをいきなり見ると辛い
- どうやって OCaml のコードを読むか
- まず、mli ファイル (インタフェース) を読む
- ml ファイル (実装) は飛ばす
- よい mli ファイルを書く
- 実装の詳細は隠蔽する
- どう使うか示す
- 良い・短いコメントを付ける
- 型で表す
- ocamlc -i から始めると良い
- 良くない mli ファイルは読まない
- 良い質問
- 何が書かれているか・どこにあるか は無駄
- 何故 を聞くと良い
- 時間の80%は検索に使うので、検索に使う時間を減らす
- → 検索時間が半分になれば、3倍生産的になれる
- 以下のような先輩の助言は無視
- Grepで何とかなるよ
- 手動検索も学習だ
- すぐ慣れるよ
- コンパイラに関連した解析ツールを使う
- 型推論は便利だけど、コード中でこの変数の型なんだっけ？ってなりやすい
- 変数の型を調べてくれるエディタ拡張がある
- 型推論は便利だけど、コード中でこの変数の型なんだっけ？ってなりやすい
- ocamlspotter
- 便利
- 新しい
- 次は Haskell
- OCaml でプログラミングコンテスト / Programming Contest in OCaml
- プログラミングコンテスト
- 時間短い
- バグ入れたら地峡な時間は浪費されてとても不利
- バグ入れにくい言語がいい
- バグ入れたら地峡な時間は浪費されてとても不利
- 仕様変更に強い
- 実行速度
- 時間短い
- Sys.command でコマンド叩ける
- 素の OCaml はライブラリが少ない
- 絵描くの辛い
- ライブラリがあれば OCaml 有利
- 型、無名関数、実行速度
- プログラミングコンテスト
- Lightning Sessions
- FFTW/genfft誰得ハッキングガイド / The Hitchhacker's Guide to the FFTW/genfft
- OCaml版Hoogle、OCamlAPISearchの紹介
- Hoogle
- OCaml API search
- http://search.ocaml.jp/
- OCamlBrowser の関数検索モジュールを利用
- どーOCaml
- http://ocaml.jp/cgi/docaml/docaml.cgi
- fizzbuzz
- when で分岐出来るが、タプルでmatchするといい感じ
- メールアドレスフィルタ
- メールアドレスをファイル名と見て、Filename.check_suffix で判定
- String.is_suffix で判定 (Core ライブラリが必要)
- ファイルコピー
- Maybeモナドを作って、失敗しうる処理を連結
- モジュール内にモジュールを作る
- SQL文生成
- エスケープを Str.global_replace で行う
- プリペアドステートメントは PGOCaml ってのがある
- どーOCamlはOCamlで作られている
- ゴルフ用楽打モジュール
- Golfコンテスト結果発表と表彰
- Sort by Length for OCaml Golf Competition
- 自分にはよく分からない世界が・・・
- 読めん・・・
- この辺は @fusigichang とか好きそう
- もの
- 念願のグリーンバンドを手に入れた
- OCaml Tシャツ 買った！
矛盾
楚人に盾と矛とを鬻（ひさ）ぐ者有り。之（これ）を誉めて（ほめて）曰く「吾が盾の堅きこと、能く（よく）陥す（とほす）もの莫し（なし）」と。また、その矛をほめていはく、「わが矛の利なること、物において陥（とほ）さざることなきなり。」と。あるひといはく、「子の矛を以て、子の盾を陥（とほ）さばいかん。」と。その人応ふること能はざりき。
矛盾 - Wikipedia
Theorem 矛盾 : forall (矛 盾:Type)(突き通す:矛 -> 盾 -> Prop), (exists 最強の矛:矛, forall あらゆる盾:盾, 突き通す 最強の矛 あらゆる盾) -> (exists 最強の盾:盾, forall あらゆる矛:矛, ~ 突き通す あらゆる矛 最強の盾) -> False. Proof. intros 矛 盾 突き通す. intros どんな盾でも貫く矛がある どんな矛でも防ぐ盾がある. elim どんな盾でも貫く矛がある. intros 最強の矛 最強の矛はあらゆる盾を貫く. elim どんな矛でも防ぐ盾がある. intros 最強の盾 最強の盾はあらゆる矛を防ぐ. apply (最強の盾はあらゆる矛を防ぐ 最強の矛). apply (最強の矛はあらゆる盾を貫く 最強の盾). Qed.
買った本
学校の売店に注文してた本が届いたそうなのでもらってきた。
- Emacsの本
Emacsテクニックバイブル ?作業効率をカイゼンする200の技?
- 作者: るびきち
- 出版社/メーカー: 技術評論社
- 発売日: 2010/08/03
- メディア: 単行本（ソフトカバー）
- 購入: 26人 クリック: 1,031回
- この商品を含むブログ (67件) を見る
今年の 8月・9月は Emacs 強化月間。(去年は vim だった)
- 数学の本
- 作者: 竹内外史
- 出版社/メーカー: 日本評論社
- 発売日: 1978/01/20
- メディア: 単行本
- 購入: 3人 クリック: 39回
- この商品を含むブログ (16件) を見る
圏論の基礎 が難しかったので。
