Alloyでコンビネータ論理・続編

今回は項書換え的な書き方にしてみた。まずKコンビネータから。

open util/ordering[Term]

some abstract sig Term {}

one sig K extends Term {}

sig Apply extends Term {
  f, g: Term
}

fact {
  all x, y: Term | (x -> y) in (f + g) => y not in (x.prevs + x)
}

pred equal (x, y: Term) {
  x in Apply and x.f in Apply and x.f.f = K and y = x.f.g
}

fun apply(x, y: Term): Term{  
  {a: Apply | a.f = x and a.g = y }
}

run {
  some x, y: Term | equal[x, y]
} for 5 Term

「all x, y: Term | (x -> y) in (f + g) => y not in (x.prevs + x)」は、ある項AがBを使っていて項BはAを使っていて、という循環が起きると見づらいし説明しにくいので禁止するために入れてみた。(追記: y in x.nextsの方がいいね) このequalの定義では、自分自身とのequalがfalseなのでネーミングが適切ではない気がする。まあこれでrunの述語「some x, y: Term | equal[x, y]」つまり「項xとyがあって、その二つはequal」ってのを探させると期待通りに解が見つかる。

yはKで、Apply3がKにKを適用したものだからKK、xはKKにKKを適用したものだから(KK)(KK)となっている。で、Kxy=xのルールによって(KK)(KK) = K K (KK) = Kになるのでめでたしめでたし、という。

さて、次はこれにSコンビネータを導入したいところだけど、このequalの実装のままSコンビネータを実装するのはめんどくさいなぁ。Kをまず綺麗にしよう。きれいにした時にバグを仕込んでないかどうか確認するためのfactを作る。

pred equal_k (x, y: Term) {
	x in Apply and x.f in Apply and x.f.f = K and y = x.f.g
}
pred equal_k2 (x, y: Term) {
	one a, b: Term | x = apply[apply[K, a], b] and y = a
}
check {
	some x, y: Term | equal_k[x, y] iff equal_k2[x, y]
}

あれ、反例が見つかる。ってことはequal_kとequal_k2は等価ではないのか。

このケースでequal_k2[$x, $y]がfalseらしい。あ、{a, b: Term | $x = apply[apply[K, a], b]}が空のようだ。期待と違う。{a, b: Term | a = apply[K, b]}は{Apply$3->K$0}だそうな。あれ？関係を返している？あ、これは内包表記が2つのタプルになっているからそう表示されているだけか。

Apply$2 = apply[Apply$3, Apply$3]がfalseだな。どういうことだろう。

あ、わかった。apply[Apply$3, Apply$3]が{Apply$2, Apply$0}だ。そうか、全く同じ引数に対して適用されたApplyのインスタンスが複数存在しうるのか。

じゃあこういう制約をつけよう。

fact {
  all x, y: Term | lone apply[x, y]
}

任意の項x, yについて、apply[x, y]は最大1個である。

これで反例が見つからなくなった。

項の数が…

Sの実装をしたのだが、スカラーの集合に対する量化子が展開されるってことを考えるとa, b, cのところがO(N^3)なんじゃないか疑惑。

pred equal_s (x, y: Term) {
	one a, b, c: Term {
		x = apply[apply[apply[S, a], b], c]
		and
		y = apply[apply[a, c], apply[b, c]]
	}
}

8 Termで解が見つからないが、もっと増やせば見つかるのか、そもそも間違っているのか。

あ、少なくともひとつ間違いがある。現状のequalの定義だと1回の項書換えで到達できる範囲しかequalじゃないな。書き換えてみる。

pred equal (x, y: Term) {
	equal_k[x, y] or equal_s[x, y] or 
	one z: Term | equal[x, z] and equal[z, y]
}

述語は再帰呼び出ししてはいけない、というエラーになった。うーん、どうしようかなぁ。