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 となっていた
アッカーマン関数を 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 で束縛された関数を呼び出せばいい
再帰を使わないで深さ優先探索と幅優先探索は、 データ構造がスタックかキューかだけの違い、と昔習った
しかし、ふと、そうやって深さ優先探索を行うと、 帰りがけ順に処理を行うことができないことに気がついた
例えば、再帰を使わない深さ優先探索は以下のように実装できるだろう
% 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比較の使い方がよくわからなかったのだが、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 *)
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)))) *)
OCaml 4.12.0 が出ていたので、 いつものように opam で install しようとしたが、 opam switch list-available としても、 4.11.2+flambda みたいな flambda を有効にして install する選択肢が出てこない
調べてみるとリリースノートに説明があった
flambda (だけ) を有効にするには以下のようにすればいいようだ
opam switch create 4.12.0+flambda --package=ocaml-variants.4.12.0+options,ocaml-option-flambda
まぁ、組み合わせが自由になっていいことだ、というところかな
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)