一ヶ月以上努力した甲斐があり、証明が完成しました。
883行もあるのは明らかに異常なので、いかにして短く記述するかを考えます。
Permalink | コメント(0) | トラックバック(0) | 03:46
明けましておめでとうございます。
((1+2)+((3+4)*(5+(6*((7*8)-9))))) ((1+2)-((3+4)*(((5-(6*7))*8)+9))) ((1+2)+((3+4)*((((5*6)+7)*8)-9))) ((1-2)+(3*(((4*5)*((6*7)-8))-9))) ((1-2)+((3-(4*((5/6)-(7*8))))*9)) (((1+2)-3)+(4*((5-6)+((7*8)*9)))) (((1-2)-3)-((((4*(5-6))*7)*8)*9)) (((1-2)-3)-((((4/(5-6))*7)*8)*9)) (((1+(2*3))*4)*(((5-6)/7)+(8*9))) ((((1+2)-3)+4)*((5-6)+((7*8)*9))) ((((1+2)/3)*4)*((5-6)+((7*8)*9))) ((1-((2-(3*4))*(((5*6)*7)-8)))-9) ((1+(((2*3)+4)*(((5*6)*7)-8)))-9)
Permalink | コメント(0) | トラックバック(0) | 04:01
去年出したものよりも、ずっと正確かつ分かりやすい本になっていると思います。
Permalink | コメント(0) | トラックバック(0) | 01:11
この記事はHaskell Advent Calendar 2011の22日目の記事です。
Haskell の遅延評価は便利な一方で、大きな罠になり得ると私は考えています。今日はそのことについて書きます。
途中に出てくる話はあまりに当然過ぎるかもしれないので、分かっていれば読み飛ばしても良いでしょう。
# あまりに Haskell を書いていないせいでこのような面白くない話になってしまいましたが、どうしても面白いものを見たければ agda2-mode を改造し、高速化する - Hatena::Diary::pi8027などを見てください。ReadS を monadic parser combinator にしています。
とあるデータ型の定義の中で、そのデータ型自身が使われているとします。このようなデータ型を再帰的なデータ型と呼びます。
例えば、
data List a = Cons a (List a) | Nil
という定義を持つリスト型は再帰的であると言えます。
この定義を使って、
Cons 1 (Cons 2 (Cons 3 Nil))
と書くことで、1, 2, 3のリストを作れます。
(List 型は説明のために定義したものなので、これ以降では Prelude のリスト型を使います。)
Haskell は遅延評価という仕組みを持ち、再帰的なデータ型の値が無限長になることを許しています。
例えば、
repeat :: a -> [a] repeat a = a : repeat a
のようにして引数として取った値のみを要素とする無限長のリストが作れます。
repeat 関数によって作られるリストを末尾まで辿ることはできませんが、有限の範囲内で要素を取り出すことができます。
再帰的な値や関数の定義では、その計算を実行して結果を取り出せるかということ、即ち計算の停止性に注意しなければなりません。
このようなことを簡単に保証できるような再帰の形をいくつか考えることができます。
停止しない計算を作るのは非常に簡単です。例えば、
bottom = bottom
と書いて bottom を評価してやれば、その計算は停止せず、値を取り出せません。
map :: (a -> b) -> [a] -> [b] map f [] = [] map f (x : xs) = f x : map f xs
という定義を持つ map 関数について考えてみましょう。
これは与えられるリストが正しい有限長のリストであれば結果も(同じ長さの)有限長のリストであり、
正しい無限長のリストであれば結果も無限長のリストであると言えます。
length :: [a] -> Int length [] = 0 length (_ : xs) = succ $ length xs
という定義を持つ length 関数について考えてみましょう。
これは与えられるリストが有限長のリストであれば正しく結果が取り出せますが、無限長であれば計算は停止しません。
無限長のデータと有限長のデータを区別しづらいことや停止性について慎重でないことが原因で、意図せず停止しない計算を日常的に書いている方が多いと思います。
実は、計算を停止させる方法は非常に簡単です。ここではその二通りのやりかたを説明します。
まず一つは、有限長の引数を呼び出しごとにコンストラクタを解いてサイズを小さくしていく方法です。lengthの定義はこれにあてはまります。
もう一つは、定義内で呼び出された再帰関数の結果の外側で、コンストラクタを使ってサイズを大きくしていく方法です。これは結果が無限長になるかもしれませんが、コンストラクタを解けなくなってしまうことはありません。repeatの定義はこれにあてはまります。
また、mapの定義はどちらにもあてはまるので問題が起きづらいと言えますが、そもそも無限長かもしれないリストと必ず有限長であるリストを正確に区別しない考え方が停止しない計算を生んでいるのだと私は考えています。
割とこの話をすることが多かったのでまとめてみました。
そもそもこの話は多くの定理証明系で利用できる帰納法と余帰納法とほとんど同じことなので、Coq や Agda2 を日常的に使うようにするというのも一つの手かもしれません。これらの処理系では有限長のデータの型と無限長になり得るデータの型を区別し、また停止しない計算は記述できないようになっています。
Permalink | コメント(0) | トラックバック(0) | 23:47
この記事はTheorem Proving Advent Calendar 2011の17日目の記事です。
筑波大学の計算モデル論という授業でλ計算の合流性の証明を習ったので、せっかくだから Agda2 で証明してみよう。ということで証明を書いています。
今までに書けた証明はhttp://github.com/pi8027/sandpit/tree/master/agda_stdlib/Lambdaにあります。
変数の捕獲などを考えると非常に面倒なので、考える必要性の無い De Bruijn index を用いることに。
import Level
open import Function
open import Data.Nat
open import Relation.Nullary
open import Relation.Binary
data Term : Set where
tvar : ℕ → Term
tapp : Term → Term → Term
tabs : Term → Term
shift : ℕ → ℕ → Term → Term
shift d c (tvar n) with c ≤? n
...| yes p = tvar (n + d)
...| no p = tvar n
shift d c (tapp t1 t2) = tapp (shift d c t1) (shift d c t2)
shift d c (tabs t) = tabs $ shift d (suc c) t
unshift : ℕ → ℕ → Term → Term
unshift d c (tvar n) with c ≤? n
...| yes p = tvar (n ∸ d)
...| no p = tvar n
unshift d c (tapp t1 t2) = tapp (unshift d c t1) (unshift d c t2)
unshift d c (tabs t) = tabs $ unshift d (suc c) t
_[_≔_] : Term → ℕ → Term → Term
tvar n' [ n ≔ t ] with n ≟ n'
...| yes p = t
...| no p = tvar n'
tapp t1 t2 [ n ≔ t ] = tapp (t1 [ n ≔ t ]) (t2 [ n ≔ t ])
tabs t1 [ n ≔ t ] = tabs $ t1 [ suc n ≔ shift 1 0 t ]
data _→β_ : Rel Term Level.zero where
→βbeta : ∀ {t1 t2} → tapp (tabs t1) t2 →β unshift 1 0 (t1 [ 0 ≔ shift 1 0 t2 ])
→βappl : ∀ {t1 t1' t2} → t1 →β t1' → tapp t1 t2 →β tapp t1' t2
→βappr : ∀ {t1 t2 t2'} → t2 →β t2' → tapp t1 t2 →β tapp t1 t2'
→βabs : ∀ {t t'} → t →β t' → tabs t →β tabs t'
data rtclosure {ℓ} {A : Set ℓ} (rel : Rel A ℓ) : Rel A ℓ where
rtc0 : ∀ {a} → rtclosure rel a a
rtcs : ∀ {a b c} → rel a b → rtclosure rel b c → rtclosure rel a c
_→β*_ : Rel Term Level.zero
_→β*_ = rtclosure _→β_
できるだけ楽をしたいので、Parallel reduction を使います。
data _→βP_ : Rel Term Level.zero where
→βPvar : ∀ {n} → tvar n →βP tvar n
→βPapp : ∀ {t1 t1' t2 t2'} → t1 →βP t1' → t2 →βP t2' → tapp t1 t2 →βP tapp t1' t2'
→βPabs : ∀ {t t'} → t →βP t' → tabs t →βP tabs t'
→βPbeta : ∀ {t1 t1' t2 t2'} → t1 →βP t1' → t2 →βP t2' →
tapp (tabs t1) t2 →βP unshift 1 0 (t1' [ 0 ≔ shift 1 0 t2' ])
_* : Term → Term
tvar n * = tvar n
tapp (tabs t1) t2 * = unshift 1 0 (t1 * [ 0 ≔ shift 1 0 (t2 *) ])
tapp t1 t2 * = tapp (t1 *) (t2 *)
tabs t * = tabs (t *)
上に示した定義と方針では、大変な量の証明を書かなくてはいけないことに後から気が付きました。shift と代入の入れ替えや shift の合成や代入の入れ替えなどの大量の補題を証明しなければなりません。
結局、1ヶ月近く経った今でも証明が終わっていないので別の方針も試す必要がありそうです。
Permalink | コメント(0) | トラックバック(0) | 23:54
