ふと無限リストを使ってみた。
Haskell で 0, 1, 2, ... という自然数全体の無限リストを定義するには以下のようにできる。
ns_from i = i : (ns_from (i+1)) ns = ns_from 0
ghci にこれを読み込ませるのは問題なく可能だが、 ns を評価すると延々と表示が止まらない。 先頭の 10個だけということで、以下を実行してみると、期待通りの値が生成されていることが分かる。
> take 10 ns [0,1,2,3,4,5,6,7,8,9]
Coq で同様なことをやると以下のようになる。
Require Import Streams. CoFixpoint ns_from i := Cons i (ns_from (S i)). Definition ns := ns_from 0.
ns を評価すると、 Haskell のように延々と表示されることはなく、以下のように表示される。
Coq < Compute ns.
= (cofix Fcofix (x : nat) : Stream nat := Cons x (Fcofix (S x))) 0
: Stream nat
しかし、これでは期待通りの結果になっているかどうかわからない。
ここで使っている Streams ライブラリを調べると、先頭要素は hd で得られるようなので、 それを使ってみると期待通りに 0 である。
Coq < Compute hd ns.
= 0
: nat
先頭を除いた以降の要素は tl で得られるが、それは以下のようになる。
Coq < Compute tl ns.
= (cofix Fcofix (x : nat) : Stream nat := Cons x (Fcofix (S x))) 1
: Stream nat
これだけだと直感的にちゃんと動いたことを確認できた気がしない。 Haskell の take みたいなのはないのか、と思って探してみるが、見逃しているのでなければないっぽい。
(ssreflect の seq に take があるが、これは list -> list なので Stream には適用できない。 定義の内容はよく似ていて、空リストの処理を削れば同じになるのだが、 有限リストと無限リストは型が違うので別に定義せざるを得ない。)
しょうがないので定義する。
Fixpoint take {T} n (s : Stream T) : list T :=
match n with
| O => nil
| S n' =>
match s with
| Cons v s' => cons v (take n' s')
end
end.
これを使うと、以下のように期待どおりに動作しているようである。
Coq < Compute take 10 ns.
= (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil)%list
: list nat
ここまでが準備である。
さて、Haskell では 0, 1, 2, ... という無限リストを以下のようにも定義できる。
ns' = 0 : map (1+) ns'
評価すれば同様の結果になる。
> take 10 ns' [0,1,2,3,4,5,6,7,8,9]
さて、これを Coq でやろうとすると、うまくいかない。
Coq < CoFixpoint ns' := Cons 0 (map S ns'). Toplevel input, characters 0-37: > CoFixpoint ns' := Cons 0 (map S ns'). > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Recursive definition of ns' is ill-formed. In environment ns' : Stream nat Unguarded recursive call in "cofix map (s : Stream nat) : Stream nat := Cons (S (hd s)) (map (tl s))". Recursive definition is: "Cons 0 (map S ns')".
調べてみるとこれの理由は CPDT に書いてあって、 Coq としては 無限リストが実際に無限に要素を生成できなければならないためで、 それを保証するための制限に巻き込まれて禁止されちゃっているようである。
たとえば、ns' の中の map のところが tl であれば、無限には要素を生成できない。 Coq では禁止されて定義できないが、Haskell では定義できる。
ns'' = 0 : tail ns''
(Haskell の tail は Coq の tl に対応する)
しかし、評価すると以下のように 0 まで表示したところで止まってしまう。
> ns'' [0
もちろん今回の ns' は無限に要素を生成できるので実際には問題なく、 なにかもっとうまい区別の仕方があれば (それは map と tl の違いをうまく区別する必要があるわけだけど)、 ns' を定義可能にすることもできるのかもしれない。
ついでに Ruby でも無限リストっぽいものを作ってみた。 ここではイテレータを使う。
まぁ、0, 1, 2, ... というのは 0.step というだけで作れるのだが、 あえて、ns_from なスタイルで作ると以下のようになる。
def ns_from(i, &b) yield i ns_from(i+1,&b) end def ns enum_for(:ns_from, 0) end p ns.take(10)
ns' みたいに 0 を生成した後、残りを再帰の結果の各要素に 1 を足して生成するならこうか。
def ns2
yield 0
ns2 {|x| yield x + 1 }
end
むりやり map を使うならこうかな。
def ns3(&b)
yield 0
enum_for(:ns3).lazy.map {|x| x + 1 }.each(&b)
endついでに Python でも無限リストっぽいものを作ってみた。 ここではジェネレータを使う。
まぁ、0, 1, 2, ... というのは itertools.count() というだけで作れるのだが、 あえて、ns_from なスタイルで作ると以下のようになる。
import itertools
def ns_from(i):
yield i
for j in ns_from(i+1):
yield j
def ns():
return ns_from(0)
print(list(itertools.islice(ns(), 10)))
ns' みたいに 0 を生成した後、残りを再帰の結果の各要素に 1 を足して生成するならこうか。
def ns2():
yield 0
for x in ns2():
yield x + 1
むりやり map を使うならこうかな。
def ns3():
yield 0
for j in map((lambda x: x+1), ns3()):
yield j[latest]