天泣記

2017-10-09 (Mon)

#2 Python の無限リスト

ついでに 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
#1 Ruby の無限リスト

ついでに 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

2017-10-08 (Sun)

#1 Haskell と Coq の無限リスト

ふと無限リストを使ってみた。

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' を定義可能にすることもできるのかもしれない。

2017-09-20 (Wed)

#1 RubyKaigi の発表

RubyKaigi 2017 で、 Ruby Extension Library Verified using Coq Proof-assistant という発表をした

2017-08-31 (Thu)

#1 右代入

今日は Ruby 開発者会議があって、すこし右代入について matz と話した。 ふつうの代入が変数を左に書く「var = expr」という形なのに対して、 右代入は変数を右に書く「expr 右代入記号 var」 というようなものである。

これの意図は、method chain とかで処理が左から右に流れていく時に、 最後の結果を変数に代入しようとしたときに代入は最後の処理なので右端に書きたい ということである。 (yield_self が使われる状況のいくらかは、右代入のほうが適切なのではないかと思っている。)

機能自体には matz も positive なのだが、問題はどんな記号を選ぶかである。 今日は、内部の式には許さないという制約をつけることにより => を使えるのではないかという話になったのだが、 後からよく考えると以下のように引数の最後に {} にくくらないハッシュを与える場合は 曖昧になってしまうことに気がついた。

ruby -e 'def f(h) p h end; v = 1; f :a => v'
{:a=>1}

いまは右代入がないので f({:a => v}) と解釈されるが、=> による 右代入を採用すると、f(:a) => v つまり v = f(:a) という解釈も可能で、 曖昧になってしまう。

しかし、将来的に {} でくくらないハッシュ引数は禁止する方向という話もある。 だから、禁止した後なら右代入に使えるかもしれない。

2017-07-23 (Sun)

#1 Proof Summit 2017

Proof Summit 2017 で 「Coq からの C プログラム生成」発表した

2017-06-04 (Sun)

#1 Coq の Program で定義した div2 はとても遅い

Coq の Program で定義した div2 を実行して時間を測ってみた。

Time Eval vm_compute in div2 1. (* 0.012 secs (0.u,0.s) *)
Time Eval vm_compute in div2 2. (* 0.338 secs (0.243u,0.008s) *)
Time Eval vm_compute in div2 3. (* 9.522 secs (5.68u,0.3s) *)

3 / 2 で 9秒というのはなんというか、信じ難いほど遅い。まぁ、かなり大きな証明項を作るからしょうがないのかもしれない。

2017-05-30 (Tue)

#1 Coq の Program を試した

Coq には Program という機能があるらしいので、ちょっとためしてみた。

リファレンスマニュアル に書いてあった例に、書いてなかった証明を補完して、最後まで通るようにしてみた。

Require Import Program.
Require Import Arith.

Program Definition id (n : nat) : { x : nat | x = n } :=
        if dec (leb n 0) then 0
        else S (pred n).

Obligation 1.
Proof.
  apply Nat.leb_le in H.
  inversion H.
  auto.
Qed.

Obligation 2.
Proof.
  apply leb_complete_conv in H.
  inversion H; auto.
Qed.

Extraction id.
(*
let id n =
  match sumbool_of_bool (Nat.leb n O) with
  | Left -> O
  | Right -> S (pred n)
*)

Program Fixpoint div2 (n : nat) {measure n} :
        { x : nat | n = 2 * x \/ n = 2 * x + 1 } :=
        match n with
        | S (S p) => S (div2 p)
        | _ => O
        end.

Obligation 2.
Proof.
  simpl.
  destruct (div2 p (le_S (S p) (S p) (le_n (S p)))).
  simpl.
  rewrite<- plus_n_O in o.
  rewrite<- plus_n_Sm.
  rewrite<- plus_n_O.
  destruct o.
    left.
    auto.
  right.
  rewrite H.
  auto.
Qed.

Obligation 3.
Proof.
  clear div2.
  destruct n.
    left; auto.
  destruct n.
    right; auto.
  exfalso.
  apply (H n).
  reflexivity.
Qed.

Extraction div2.
(*
let rec div2 x =
  let div3 = fun n -> div2 n in
  (match x with
   | O -> O
   | S n ->
     (match n with
      | O -> O
      | S p -> S (div3 p)))
*)

試した結果 (あとマニュアルも読んだ結果)、これは sig 型を使いやすくしようという話だと理解した。

sig 型というのは { x : T | P x } みたいな、P が成り立つ T 型の値の集合、つまり T の部分集合を表現するやつである。プログラムの中ではいつでも T 型の式を { x : T | P x } 型の式として扱えて、でもそうやって扱ったところで P が成り立つことは後で証明しないといけない、という仕掛けのようだ。(なお、こういう、述語で値を制限する型は refinement type とも言うらしい。)

なお、Extraction すると、div2 のなかの div3 のように、変なもの (ソースにはない、証明のための変形の残骸) が出ることがあるようだ。

もうちょっと単純な例を作ってみた。(あと、こっちでは SSreflect を使ってみた)

From mathcomp Require Import ssreflect eqtype ssrbool ssrnat.
Require Import Program.

Program Definition f (n : { x : nat | x <= 3 }) : { x : nat | x <= 10 } := n.

Next Obligation.
Proof.
  by apply (@leq_trans 3).
Qed.

Print f.
(*
f =
fun n : {x : nat | x <= 3} =>
exist (fun x : nat => x <= 10) (` n)
  ((fun n0 : {x : nat | x <= 3} => f_obligation_1 n0) n)
     : {x : nat | x <= 3} -> {x : nat | x <= 10}
*)

これだと、3以下な引数 n を受け取って、10以下の値を返す、という振る舞いを型として記述できている。



田中哲