天泣記

2021-06-30 (Wed)

#1 エスケープ解析の論文を読んだ
Goldberg, Benjamin, and Young Gil Park.
"Higher order escape analysis:
optimizing stack allocation in functional program implementations."
European Symposium on Programming. Springer, Berlin, Heidelberg, 1990.

最初、e1 -> e2, e3 という構文がなんなのかわかんなくて悩んだのだが、 if e1 then e2 else e3 という意味だった

Park, Young Gil, and Benjamin Goldberg.
"Escape analysis on lists."
Proceedings of the ACM SIGPLAN 1992 conference on
Programming language design and implementation. 1992.

なお、後続の (リストを扱えるという) こっちの論文では if e1 then e2 else e3 となっていた

2021-05-31 (Mon)

#1 Coq でのアッカーマン関数

アッカーマン関数を Coq で定義する方法はいろいろなところで説明があるが、 自分でも定義してみた

Definition ack :=
  fix ack1 (m : nat) :=
    fix ack2 (n : nat) :=
      match m with
      | 0 => S n
      | S m' =>
        match n with
        | 0 => ack1 m' 1
        | S n' => ack1 m' (ack2 n')
        end
      end.

この書き方がよい、というわけではないのだが、これを書いたことで、 どういう場合に Coq で定義できる (termination checker を通せる) のかはわかった気がする

アッカーマン関数 ack(m,n) の定義の再帰呼び出しを見直すと、 第1引数 m が確実に減る呼び出しでは第2引数 n が増えることも減ることもあるけれど、 第2引数 n が確実に減る呼び出しでは第1引数は変わらない

上の定義だと、ack1 のところは m が確実に減るのだが、n が増えるか減るかはわからない。 ack2 のところは、m は変わらず、n は減る

ちなみに、m は ack2 の外で定義されているので、ack2 は引数としては m は受け取らない。 受け取らないので m は変えられないけど、ack2 は m が変わらないところで呼び出されるので問題ない

なので、引数の並びが辞書順で減少していく場合は定義できるのではないか

引数の数だけ fix を重ねて、内部の再帰呼び出しでは、 その呼び出しで変化 (減少) するいちばん左の引数に対応する fix で束縛された関数を呼び出せばいい

2021-04-29 (Thu)

#1 再帰を使わない深さ優先探索と帰りがけ順の処理

再帰を使わないで深さ優先探索と幅優先探索は、 データ構造がスタックかキューかだけの違い、と昔習った

しかし、ふと、そうやって深さ優先探索を行うと、 帰りがけ順に処理を行うことができないことに気がついた

例えば、再帰を使わない深さ優先探索は以下のように実装できるだろう

% cat preorder.rb
Node = Struct.new(:value, :left, :right)

def n(v, l=nil, r=nil)
  Node.new(v, l, r)
end

tree =
  n(1,
    n(2,
      n(3),
      n(4)),
    n(5,
      n(6),
      n(7)))

stack = [tree]
until stack.empty?
  n = stack.pop
  p n.value
  stack.push n.right if n.right
  stack.push n.left if n.left
end
% ruby preorder.rb
1
2
3
4
5
6
7

ここで、この実装で p n.value というのは行きがけ順に実行される

では、帰りがけ順に処理を行いたいときにはどうしたらいいだろうか

再帰を使う深さ優先探索ならこれは簡単で、子ノードを再帰的に処理した後に 処理を行えばよい (行きがけ順に行う処理は子ノードを再帰的に処理する前に行う)

しかし、再帰を使わない場合は、そういう帰りがけ順の処理になるちょうどいい場所がない

考えてみると、子ノードを再帰的に処理した後に行う、というのは、 最後の子ノードを処理した後の継続 (帰りがけ順の処理をした後に上のノードに return する) が マシンスタックとして表現されているわけで、 データとしてスタックを表現する場合でもその継続と同じ意味のデータが必要なのだろう

というわけで実装してみると、以下のようにすれば、再帰を使わずに、深さ優先探索で帰りがけ順の処理を行える

% cat postorder.rb
Node = Struct.new(:value, :left, :right)

def n(v, l=nil, r=nil)
  Node.new(v, l, r)
end

tree =
  n(1,
    n(2,
      n(3),
      n(4)),
    n(5,
      n(6),
      n(7)))

stack = [[:pre, tree]]
until stack.empty?
  tag, n = stack.pop
  case tag
  when :pre
    stack.push [:post, n]
    stack.push [:pre, n.right] if n.right
    stack.push [:pre, n.left] if n.left
  when :post
    p n.value
  end
end
% ruby postorder.rb
3
4
2
6
7
5
1

2021-03-12 (Fri)

#1 Coq/SSReflect/MathComp の整数の比較

比較の使い方がよくわからなかったのだが、ssreflect/order.v を使えて、 (x < y)%O というような感じに記述できるようだ。

Check (2%:Z < 3%:Z)%O. (* @Order.lt ssrnum.ring_display int_porderType (Posz (S (S O))) (Posz (S (S (S O)))) *)
Compute (2%:Z < 3%:Z)%O. (* true *)

2021-03-11 (Thu)

#1 Coq/SSReflect/MathComp で整数を使う

Coq で整数というと標準の ZArith ライブラリが提供している Z 型があるが、 これは SSReflect の eqType 対応がなくて == が使えないとか、 SSReflect 的ではない。

自分で eqType 対応するのは可能ではあるだろうけど、 SSReflect 的な整数が提供されていないわけがないだろうということで探すと、 mathcomp/algebra/ssrint.v にあった。

中を見ると以下の型が定義されていて、Z 型とは違う型のようだ。

Variant int : Set := Posz of nat | Negz of nat.

ちょっと試してみると、以下のように使える模様。

From mathcomp Require Import all_ssreflect ssralg ssrint.

Open Scope int_scope.
Open Scope distn_scope.
Open Scope ring_scope.

Compute 2%:Z. (* 2, Posz (S (S O)) *)
Compute -2%:Z. (* Negz 1, Negz (S O) *)
Compute 1%:Z + 2%:Z. (* 3 *)
Compute 1%:Z - 3%:Z. (* Negz 1 *)
Compute 2%:Z * 3%:Z. (* 6 *)
Compute 3%:Z ^ 2%:Z. (* 9 *)
Compute `| 1%:Z - 2%:Z |. (* 1 : nat *)

Check 1%:Z = 2%:Z :> int. (* @eq int (Posz (S O)) (Posz (S (S O))) *)
Check 1%:Z == 2%:Z :> int. (* @eq_op int_eqType (Posz (S O) : int) (Posz (S (S O)) : int) *)
Check 1%:Z != 2%:Z :> int. (* negb (@eq_op int_eqType (Posz (S O) : int) (Posz (S (S O)) : int)) *)
Check 1%:Z <> 2%:Z :> int. (* not (@eq int (Posz (S O)) (Posz (S (S O)))) *)

2021-02-28 (Sun)

#1 OCaml 4.12.0 と opam

OCaml 4.12.0 が出ていたので、 いつものように opam で install しようとしたが、 opam switch list-available としても、 4.11.2+flambda みたいな flambda を有効にして install する選択肢が出てこない

調べてみるとリリースノートに説明があった

OCaml 4.12.0

flambda (だけ) を有効にするには以下のようにすればいいようだ

opam switch create 4.12.0+flambda --package=ocaml-variants.4.12.0+options,ocaml-option-flambda

まぁ、組み合わせが自由になっていいことだ、というところかな

2021-01-18 (Mon)

#1 PEPM 2021 で発表した

Akira Tanaka. Coq to C Translation with Partial Evaluation. Proceedings of the 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM '21), 2021-01-18, Virtual. (paper) (slides) (DOI)



田中哲